Algorithmic theory of natural numbers: Różnice pomiędzy wersjami
| 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:=x; \textbf{while }t\neq y\textbf{ do }t:=s(t); w:=s(w) \textbf{ od}\}w & \\ | ||
\end{align*} </math><br /> | \end{align*} </math><br /> | ||
| − | Among | + | |
| + | Among theorems 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> | <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> | ||
and | and | ||
Wersja z 11:46, 2 paź 2018
The theory 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 \{m:=0; \mathbf{while}\ n\neq m\ \mathbf{do}\ m:=s(m)\ \mathbf{od} \}(n=m)
\end{align*} [/math]
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.
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 four axioms that define operation of addition, subtraction predecessor and predicate <.
[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:=x; \textbf{while }t\neq y\textbf{ do }t:=s(t); w:=s(w) \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 \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]
and
