Algorithmic theory of natural numbers: Różnice pomiędzy wersjami

Z Lem
Skocz do: nawigacji, wyszukiwania
 
(Nie pokazano 25 pośrednich wersji utworzonych przez tego samego użytkownika)
Linia 1: Linia 1:
−
The theory of one constant 0, one one-argument functor <math>s</math> and predicate of equality =.<br />
+
The theory <math>\mathcal{ATN} </math>  of one constant 0, one one-argument functor <math>s</math> and predicate of equality =.<br />
 
'''Axioms''' <br />
 
'''Axioms''' <br />
−
<math>\begin{align*}
+
<math>   \begin{align*}
−
&\tag{I}  \forall_n s(n) \neq 0 \\
+
\tag{I}  \forall_n s(n) &\neq 0 &\\
−
&\tag{M}  \forall_n \forall_m s(n)=s(m) \implies n=m \\
+
\tag{M}  \forall_n \forall_m s(n)=s(m) &\implies n=m &\\
−
&\tag{S}  \forall_n \{m:=0; \mathbf{while}\ n\neq m\ \mathbf{do}\ m:=s(m)\ \mathbf{od}  \}(n=m)
+
\tag{S}  \forall_n \left\{ \begin{array}{l}m:=0; \\ \mathbf{while}\ n\neq m\ \mathbf{do}\\ \quad  m:=s(m)\\ \mathbf{od}  \end{array}\right\}&(n=m) &
−
\end{align*} </math><br />
+
\end{align*}   </math><br />
−
This set of formulas gives a complete specification of the set of natural numbers with the successor operation. It means that any implementation whether hardware or software (e.g. by means of a class) that satisfies three  axioms listed above is correct.  
+
This set of formulas gives a complete specification of the structure <math>\mathfrak{N} </math>  of natural numbers with the successor operation. It means that any implementation whether hardware or software (e.g. by means of a class) that satisfies three  axioms listed above is correct.  
 
It means also that if an algorithmic formula is valid in the standard model of these axioms then it has a proof with the use of program calculus.<br />
 
It means also that if an algorithmic formula is valid in the standard model of these axioms then it has a proof with the use of program calculus.<br />
−
One may extend this set adding four axioms that define operation of addition, subtraction predecessor and predicate <.
+
One may extend this set adding five axioms that define operation of addition, subtraction predecessor and predicate < and operation of multiplication.
 
<math>\begin{align*}
 
<math>\begin{align*}
 
\tag{A}\label{add} & x+y  \stackrel{df}{=} \{t:=0; w:=x; \textbf{while }t\neq y\textbf{ do }t:=s(t); w:=s(w) \textbf{ od}\}w  &  \\
 
\tag{A}\label{add} & x+y  \stackrel{df}{=} \{t:=0; w:=x; \textbf{while }t\neq y\textbf{ do }t:=s(t); w:=s(w) \textbf{ od}\}w  &  \\
Linia 16: Linia 16:
 
\ \textbf{while } s(w)\neq x\textbf{ do }  w:=s(w) \textbf{ od} \
 
\ \textbf{while } s(w)\neq x\textbf{ do }  w:=s(w) \textbf{ od} \
 
\textbf{fi}\end{array} \}w  & \\
 
\textbf{fi}\end{array} \}w  & \\
−
\tag{O}\label{odejm} & x\stackrel{.}{\_\_}y \stackrel{df}{=} \{w:=x; t:=0; \mathbf{while }\ t\neq y\ \mathbf{ do }\ t:=s(t); w:=P(w)\ \mathbf{ od} \}w &
+
\tag{O}\label{odejm} & x\stackrel{.}{\_\_}y \stackrel{df}{=} \{w:=x; t:=0; \mathbf{while }\ t\neq y\ \mathbf{ do }\ t:=s(t); w:=P(w)\ \mathbf{ od} \}w & \\
 +
\tag{M}\label{mult} & x\cdot y  \stackrel{df}{=} \{t:=0; w:=0; \textbf{while }t\neq y\textbf{ do }t:=s(t); w:=w+x \textbf{ od}\}w  &  \\
 
\end{align*} </math><br />
 
\end{align*} </math><br />
−
Among theorem of this theory one can find theorem on correctness of Euclid's algoritm <br />
+
 
−
<math> \tag{Eucl} \underbrace{\forall_{n\neq 0}\,\forall_{m\neq 0}\left\{\begin{array}{l}\textbf{while }n \neq m \textbf{ do }\\ \quad \textbf{if }n\geq m  \textbf{ then } n:=n-m  \textbf{ else }   m:=m-n   \textbf{ fi}\\ \textbf{ od} \end{array}\right\}(n=m)}_{halting\ formula\ of\ Euclid's\ algorithm}  </math>
+
Among theorems of this theory one can find theorem on correctness of Euclid's algoritm <br />
−
and
+
<math> \tag{Eucl} \underbrace{\forall_{n\neq 0}\,\forall_{m\neq 0}\left\{\begin{array}{l}\textbf{while }n \neq m \textbf{ do }\\ \quad \textbf{if }n\geq m  \\
 +
\quad \textbf{ then } \\
 +
\qquad  n:=n-m  \\
 +
\quad \textbf{ else }\\
 +
\qquad    m:=m-n \\  \quad\textbf{ fi}\\ \textbf{ od} \end{array}\right\}(n=m)}_{halting\ formula\ of\ Euclid's\ algorithm}  </math>
 +
and the theorem stating that the structure of natural numbers  enjoys the Archimedean property
 +
<math>\mathfrak{N} \models
 +
\tag{Archi} \underbrace{\forall_{n\neq 0}\,\forall_{m\neq 0}\left\{\begin{array}{l}
 +
a:=n; \\
 +
\textbf{while }\ a \leq  m\ \textbf{ do }\\
 +
\quad a :=a+x  \\
 +
\textbf{ od} \end{array}\right\}(a > x)}_{ \ axiom\ of\ Archimedes\ }  </math>

Aktualna wersja na dzień 15:34, 11 lis 2024

The theory [math]\mathcal{ATN} [/math] of one constant 0, one one-argument functor [math]s[/math] and predicate of equality =.
Axioms
[math] \begin{align*} \tag{I} \forall_n s(n) &\neq 0 &\\ \tag{M} \forall_n \forall_m s(n)=s(m) &\implies n=m &\\ \tag{S} \forall_n \left\{ \begin{array}{l}m:=0; \\ \mathbf{while}\ n\neq m\ \mathbf{do}\\ \quad m:=s(m)\\ \mathbf{od} \end{array}\right\}&(n=m) & \end{align*} [/math]
This set of formulas gives a complete specification of the structure [math]\mathfrak{N} [/math] of natural numbers with the successor operation. It means that any implementation whether hardware or software (e.g. by means of a class) that satisfies three axioms listed above is correct. It means also that if an algorithmic formula is valid in the standard model of these axioms then it has a proof with the use of program calculus.
One may extend this set adding five axioms that define operation of addition, subtraction predecessor and predicate < and operation of multiplication. [math]\begin{align*} \tag{A}\label{add} & x+y \stackrel{df}{=} \{t:=0; w:=x; \textbf{while }t\neq y\textbf{ do }t:=s(t); w:=s(w) \textbf{ od}\}w & \\ \tag{L}\label{less} & x \lt y \stackrel{df}{\equiv} \{ w:=0; \textbf{while }w\neq y\land w\neq x \textbf{ do } w:=s(w) \textbf{ od}\}(w=x \land w\neq y) & \\ \tag{P}\label{predec} & P(x)\stackrel{df}{=} \{\begin{array}{l}w:=0;\ \textbf{if }x \neq 0 \textbf{ then } \ \textbf{while } s(w)\neq x\textbf{ do } w:=s(w) \textbf{ od} \ \textbf{fi}\end{array} \}w & \\ \tag{O}\label{odejm} & x\stackrel{.}{\_\_}y \stackrel{df}{=} \{w:=x; t:=0; \mathbf{while }\ t\neq y\ \mathbf{ do }\ t:=s(t); w:=P(w)\ \mathbf{ od} \}w & \\ \tag{M}\label{mult} & x\cdot y \stackrel{df}{=} \{t:=0; w:=0; \textbf{while }t\neq y\textbf{ do }t:=s(t); w:=w+x \textbf{ od}\}w & \\ \end{align*} [/math]

Among theorems of this theory one can find theorem on correctness of Euclid's algoritm
[math] \tag{Eucl} \underbrace{\forall_{n\neq 0}\,\forall_{m\neq 0}\left\{\begin{array}{l}\textbf{while }n \neq m \textbf{ do }\\ \quad \textbf{if }n\geq m \\ \quad \textbf{ then } \\ \qquad n:=n-m \\ \quad \textbf{ else }\\ \qquad m:=m-n \\ \quad\textbf{ fi}\\ \textbf{ od} \end{array}\right\}(n=m)}_{halting\ formula\ of\ Euclid's\ algorithm} [/math] and the theorem stating that the structure of natural numbers enjoys the Archimedean property [math]\mathfrak{N} \models \tag{Archi} \underbrace{\forall_{n\neq 0}\,\forall_{m\neq 0}\left\{\begin{array}{l} a:=n; \\ \textbf{while }\ a \leq m\ \textbf{ do }\\ \quad a :=a+x \\ \textbf{ od} \end{array}\right\}(a \gt x)}_{ \ axiom\ of\ Archimedes\ } [/math]

Źródło „http://lem12.uksw.edu.pl/index.php?title=Algorithmic_theory_of_natural_numbers&oldid=3054”