Finally! 

Możemy ogłosić, że [http://arxiv.org/abs/2310.13035 dowód] hipotezy Collatza został ukończony. 
Oto wersja złożona do druku [https://lem12.uksw.edu.pl/images/6/69/CollatzConjecturebecomesTheorem2026-03-15.pdf]
<big><big>Absract</big></big> 
We are showing that the following conjecture
''For every <math>n</math>, if <math>n</math> is a natural number then Collatz computation is finite.''
is a semantically valid statement. 

This is asserted by the Main lemma. 

A corollary of the lemma says: every instance of the cnjecture where the variable <math>n</math> is replaced by any natural number <math>r \neq 0</math>, is a theorem of arithmetic, in which the addition is the only operation. 
Note, the set <math>St_0</math>of is a recursive set of theorems of Presburger arithmetic, hence the theorems of algorithmic theory of natural numbers. 

Paradoxically, the Collatz conjecture itself is not a theorem of number theory (Peano's arithmetic), nor any mathematical theory that uses the first-order language and the classical predicate logic. 

It is so because, '''1''') there is no first-order theory such that all its models are isomorphic to the standard model of natural numbers
and hence '''2''') the infinite computations can be n observed in a ''non-standard computable'' model of the elementary theory of natural numbers with addition. 

To avoid the paradox, we will use the calculus of programs <math>\mathcal{AL}</math> instead of the predicate calculus. The halting condition <math>H</math> of the Collatz computations is written as an algorithmic formula.

<math> \qquad \underbrace{\boxed{\left\lbrace \begin{array}{l}
m:=n \div 2^{\kappa(n)}; \\
\mathbf{while}\ m \neq 1 \\
\mathbf{do} \\
\quad m:=3 \cdot m +1; \\
\quad m:= m \div 2^{\kappa(m)} \\
\mathbf{od}
\end{array}\right\rbrace(m=1)} }_{ {the\ computation\ for\ n\ is\ finite} } \qquad (H)
</math>

There is no finite, traditional proof the following theorem .
<math> \begin{array}{p{14cm}}
% We are answering to the question (\textit{i}) formulating the thesis of the \textsc{Theorem}\eqref{thM}.
% \label{main}
\mathcal{ATN}\vdash
\forall_{n \neq 0} \underbrace{\boxed{\left\lbrace \begin{array}{l}
q:=1; \\
\mathbf{while}\ n \neq q \\
\mathbf{do} \\
\quad q:=q+1 \\
\mathbf{od}
\end{array}\right\rbrace(n=q) } }_{\color{black}{IF\ n>0 \ is\ a\ natural\ number\ }}
\implies
\underbrace{\boxed{\left\lbrace \begin{array}{l}
m:=n \div 2^{\kappa(n)}; \\
% (*\ \ m= 2^{\kappa(n)} (2 \rho(m)+1) \ \ *) \\
\mathbf{while}\ m \neq 1 \\
\mathbf{do} \\
\quad m:=3 \cdot m +1; \\
\quad m:= m \div 2^{\kappa(m)} \\
\mathbf{od}
\end{array}\right\rbrace(m=1)} }_{ {THEN\ the\ computation\ for\ n\ is\ finite\ FI} }
\end{array} </math>

Function <math>\kappa</math> for a given natural number <math> n </math> returns the multiplicity of 2 in the factorization of the number <math>n</math>.

Instead, we are presenting an rgument showing that the proof can be carried out in the calculus of programs <math>\mathcal{AL}</math>. To achieve his goal one has to construct an infinite tree <math>\mathcal{D}</math>. The root of the tree is the halting formula . The formula is the consequence of the infinitary inference rule <math>R_3</math> of the algorithmic logic <math>\mathcal{AL}</math>. For each premise one can construct a a finite subtree, i.e. a finite proof which is using one formula of the set <math>St_0</math>. \\
Note, that that the set <math>St_0</math> is a recursive set of formulas without variables and that all its elements are theorems of Presburger's arithmetic. 
end of Abstract 01/10/2025

==Introduction==
Let's consider the statement 
for every natural number <math>n</math>, the following program <math>Cl</math> has a finite computation. 
<math>\color{blue}\qquad Cl:\,\left\{\begin{array}{l} \mathbf{while}\ n \neq 0 \ \mathbf{do} \\
\quad \mathbf{if}\ odd(n) \ \mathbf{then}\ n:=3n+1 \ \mathbf{else}\ n:=n/2\ \mathbf{fi} \\
\mathbf{od} \end{array}\right\} </math> 
We begin by noting that the truth of the above statement entails the truth of Collatz's thesis as it was formulated before World War II. 
But in 1937, neither computers nor programming languages existed. 
On the other hand, the theory of algorithms did exist and was already well developed. The theory of recursive functions was developed in Göttingen (David Hilbert and his students), Budapest (Rozsza Pterer, Laszlo Kalmar), ... 
In London, Alan Turing created the abstract Turing machine. 
In Moscow, Kolmogorov and in Kazan, Maltsev explored the concept of a computable function. 
 
In Warsaw, Alfred Tarski, together with his students Mojżesz Presburger and Stanisław Jaskowski, obtained important results concerning the theory of addition of natural numbers.

==Our observations from 2004==
* The Collatz algorithm <math>Cl</math> does not require multiplication or division operations. Multiplying by 3 (because 3x=x+x+x) and dividing by 2 (a simple algorithm adding every other 1 is sufficient), is sufficient.
* In the algebraic structure <math>\mathfrak{M}</math>, which is a non-standard model of the elementary theory of addition of natural numbers (there is one, see below), the algorithm <math>Cl</math> has an infinite computation for many arguments.
* Therefore, the Collatz theorem cannot be proven based on the axioms of the elementary theory of addition of natural numbers.
* Moreover, in the language of elementary theory of addition, there is no stopping formula for the Collatz algorithm! It is a corollary from the Goedel incompleteness theorem. 
So what do we have to prove?

==Have a look==
<math> \begin{figure}
\resizebox{\textwidth}{!}{
{\footnotesize \begin{tikzcd}[ampersand replacement=\&,scale =0.15, column sep=normal,row sep=0.7cm,arrows=<-]
% [arrows=<-]
% \node[circle,fill=red!15,align=center,text=black] { $ \frac{W_{41}}{>51} $}; \& \color{red}27 \&\cdots \\ \& \dots \\
% \node[circle,fill=red!15,align=center,text=black] {$ \frac{W_{40}}{26} $}; & &\cdots \\ \dots & \\
% \node[circle,fill=red!15,align=center,text=black] {$ \frac{W_9}{26} $}; \& 121 \& 89 \&\cdots \\
% \node[circle,fill=red!15,align=center,text=black] {$ \frac{W_8}{26} $}; \& 33 \& 91 \& 67 \&\cdots \\
% \node[circle,fill=red!15,align=center,text=black] {$ \frac{W_7}{26} $}; \& 25 \& 49 \&\color{red}51 \& 101 \&197 \&205\&\cdots \\
% \dots \\
\node[circle,fill=brown!15,align=center,text=black] {$ \frac{W_6}{24} $}; \& \color{red}9\& 19 \&37 \& 77 \&325 \& \cdots \\
\node[circle,fill=red!15,align=center,text=black] {$ \frac{W_5}{8} $}; \& 7\arrow[u]\arrow[urr] \&\color{red}15 \&29\arrow[ul]\arrow[ur] \& 61\arrow[ur] \& \cdots \\
\node[circle,fill=blue!30,align=center,text=black] {$ \frac{W_4}{6} $}; \& 11\arrow[u]\arrow[urr] \& 23\arrow[u]\arrow[urr] \&\color{red}45 \&\color{red}93 \& 181 \& 373 \& \cdots \\
\node[circle,fill=yellow!30,align=center,text=black] {$ \frac{W_3}{6} $}; \&17\arrow[urr] \arrow[u]\arrow[urrrr] \& 35\arrow[u] \arrow[urr] \arrow[urrrr] \& \color{red}69 \& \color{red}75 \& \color{red}141\&
151 \&277 \& 301 \&\cdots \\
\node[circle,fill=gray!30,align=center,text=black] {$ \frac{W_2}{6} $ }; \&\color{red}3 \& 13\arrow[ul]\arrow[ur]\arrow[urrrrr]\& 53\arrow[ul] \arrow[urr]\& 113\arrow[u] \arrow[urrrr]\& \color{red}213 \& 227\arrow[u] \& \color{red}453 \& 853 \&\color{red}909 \& \cdots \\
\node [circle,fill=red!30,align=center,text=black] {$ \frac{W_1}{2} $ }; \& 5\arrow[u]\arrow[ur]\arrow[urr]\arrow[urrrr]\&\color{red}21 \& 85\arrow[ur]\arrow[urrrr,near end] \& 341\arrow[urr] \arrow[urrrrr] \& \color{red}1365 \& 5461 \&\cdots \\
\node [circle,fill=green,align=center,text=black] {$ \frac{W_0}{2} $ }; \& \& \& 1\arrow[ull] \arrow[ul]\arrow[u]\arrow[ur] \arrow[urr] \arrow[urrr] \\
% %\end{scriptsize}
\end{tikzcd} }
}
\caption{F \textsc{Ilustracja} fragment grafu $\mathcal{F} $} \label{grafF}
\end{figure}
</math>

==Correct formulation of the Collatz theorem==
In the standard structure of natural numbers with the addition operation,
our program <math>Cl</math> has a finite computation for each argument ''n''.

==Stop formula==
i.e.
=== A necessary and sufficient condition for the computation to be finite===
Therefore, we need to create a formula <math>\theta</math> (a logical expression) such that it evaluates to true if and only if the computation of the program <math>Cl</math> is finite. There are many such formulas in the language of program calculation, i.e. algorithmic logic. 
,<math>\qquad \theta:\,\left\{\begin{array}{l} \mathbf{while}\ n \neq 0 \ \mathbf{do} \\
\quad \mathbf{if}\ odd(n) \ \mathbf{then}\ n:=3n+1 \ \mathbf{else}\ n:=n/2\ \mathbf{fi} \\
\mathbf{od} \end{array}\right\} (n=1) </math>
 
The value of the <math>\theta</math> formula depends only on the initial value of the "n" variable. This formula is satisfied by the value of the variable "n" if and only if the evaluation of the while ... program is finished and the final value of the variable "n" is equal to 1. 
Other formulas can also be considered, e.g., 
,<math>\qquad \xi:\,\bigcup \left\{\overbrace{\begin{array}{l} \mathbf{if}\ n \neq 0 \ \mathbf{then} \\
\quad \mathbf{if}\ odd(n) \ \mathbf{then}\ n:=3n+1 \ \mathbf{else}\ n:=n/2\ \mathbf{fi} \\
\mathbf{fi} \end{array} }^{K}\right\} (n=1) </math> 
{co reads: "there exists an iteration <math>K^i</math> of the program <math>K</math> such that after executing <math>K^i</math> the equality <math>n=1</math> is satisfied."} 
In other words, we are dealing with an upper bound on the values of the formulas <math>K^i(n=1)</math>, where <math>i= 0,1,2 \dots</math>. 

The second part of the problem is much more difficult: we must prove the stopping formula using the axioms of program calculus and the axioms of the algorithmic theory of natural numbers. 

 
==Elementary Theory of Addition of Natural Numbers==
The previous observation that Collatz's theorem cannot be proved in this theory remains valid. However, the properties of the non-standard model of this theory and a few of its theorems will be helpful in further considerations. 
 
This theory is defined by specifying three components:
* the language,
* the logic, i.e., the consequence operation, and
* the axioms specific to this theory. 
'''Language.''' The expressions of the language are composed of the following symbols: variable symbols, e.g., x, y, n, the + symbol for a binary operation, the = symbol for a binary relation, constant symbols, logical functor symbols, and auxiliary symbols, e.g., parentheses. 
. Examples of expressions are... 

'''Logic.''' The consequence (inference) operation is determined by specifying the axioms of first-order logic and the rules of inference. 
'''Axioms.'''
<math>
\begin{align}
\tag{a} \forall_x\ x+1 &\neq 0 \\
\tag{b} \forall_x\, \forall_y\ x+1=y+1 &\implies x=y \\
\tag{c} \forall_{x}\ x+0&=x \\
\tag{d} \forall_{x,y}\ (y+1)+x&=(y+x)+1 \\
\tag{I} \Phi(0)\land \forall_x\,[\Phi(x) \implies \Phi(x+1)]&\implies \forall_x\Phi(x)
\end{align}
</math>
The expression <math>\Phi(x)</math> may be replaced by any formula. The result is an axiom of theory
This is the induction scheme. 
We augment the set of axioms adding four axioms that define a coiple of useful notions. 
<math>
\begin{align}
\tag{e} even(x) &\stackrel{df}{\equiv} \exists_y\, x=y+y \\
% \tag{o} odd(x) &\stackrel{df}{\equiv} \exists_y\, x=y+y+1 \\
% \tag{D2} x\, div\, 2 = y &\equiv (x=y+y\, \lor\, x=y+y+1) \\
% \tag{3x} 3x&\stackrel{df}{=} x+x+x
\end{align}
</math>

'''Models of Presburger Arithmetic''' 
As expected, the sequence of standard values 0, 1, 2, 3, ... is a model of this theory.

Stanisław Jaśkowski discovered another, nonstandard model of Presburger arithmetic in 1929.

[[File:MonStandardModel.png|center|thumb|600px|Nonstandard model of Presburger arithmetic]]
The universe of the model is a subset of the set of complex numbers <math>a+\math b</math>
where <math>a \in \mathbb{Z} </math> i.e. a is an integer number and <math>b \in \mathbb{Q}^+ </math> is a positive rational number. Additionally, whenever <math>b=0 </math> we have <math>a>0</math>.
Addition is defined as usual addition of complex numbers.

Both models are computable. There are also unpredictable models with arbitrarily high power.

==Algorithmic Theory of Natural Numbers==
* Language. The alphabet of a language contains a set of variables, e.g., x,y. a functor + a two-argument addition operation, two constants 0 and 1, a relation sign = equality. 
Terms (i.e., nomenclature expressions): this is the smallest set of expressions containing variables, constants, and closed under the combination of two terms in this way (t1 + t2). 
Formulae.
* Logic. Program calculus. Program calculus includes first-order logic. In addition to first-order formulas, the language of program calculus also contains algorithmic formulas. The simplest such formula is a string consisting of a program and a formula (usually a first-order formula) following it.
To the axioms of first-order logic, axioms describing the properties of program-generating connectives should be added; see [[Algorithmic Logic]].
To the inference rules of first-order logic, rules specific to program calculus should be added. 

* Axioms of the theory. 
Only three formulas. 
<math>
\begin{eqnarray}
\tag{ATN1} \forall_x\, x+1 \neq 0 &&\\
\tag{ATN2} \forall_{x,y}\,x+1=y+1 \implies x=y &&\\
\tag{ATN3}\forall_x\, \{y :=0; \mathbf{while}\ y\neq x\ \mathbf{do}\ y:=y+1\ \mathbf{od} \}\,(y=x) &&
\end{eqnarray} </math> 

These are essentially the axioms of the successor theory. 
The ATN1 formula states that 0 is not the successor of any natural number. 
The ATN2 formula states that the successor is a one-to-one function. 
The formula ATN3 states that every natural number is ''reachable'' from zero by adding a finite number of ones. 
In this theory, one can write definitions for addition, multiplication, and any computable function.

==Analiza formuły stopu==
xxx

==Trójki ==
Spostrzeżenie (wynikłe z przygladania się formule stopu). 

<math>\forall_{n \neq 0} \exists_{x,y,z}\ n \cdot 3^x+y=2^z </math>

==Drzewo Collatza==
[[Plik:StratDrzewoCollatza.png|thumb|center |750px| Rys. 1 Fragmenty warstw <math>W_0, \dots W_4 </math> drzewa Collatza ]]

==Własności obliczeń na trójkach==
Tutaj napiszemy więcej 
==Kalejdoskop==

Oglądaj rysunki, wykonuj obliczenia, rozwiązuj zadania, formułuj swoje zdanie, próbuj je uzasadnić, ... 

Tu znajdziesz .... 
===Obliczenia utemperowane===
[[Plik:ObliczN19.pdf.png|thumb|center|750px|Utemperowane obliczenie dla n=76]]
Trzy zadania. Odpowiedz czy są one jakos powiązane? 
* Masz do dyspozycji bardzo wiele trójkątnych płytek, w dwu kolorach.
Czy potrafisz ułożyć chodnik łączący posesje o numerze n z numerem 1?
*[[Ułamek piętrowy]]
* Czy obliczenie 3x+1 jest skończone dla każdej liczby naturalnej?

===Struktury algebraiczne===
Struktura liczb naturalnych. 
Algebra Jaśkowskiego. 
===Teorie===
elementarna teoria liczb naturalnych z dodawaniem. 
algorytmiczna teoria liczb naturalnych 
===Zadania===

<math>\alpha</math> 

== Archiwum kolejnych wersji pracy ==
[CollatzConjecturebecomesTheorem11Aug23 http://lem12.uksw.edu.pl/images/3/3b/CollatzConjecturebecomesTheorem11Aug23.pdf]

[https://dx.doi.org/10.2139/ssrn.4158238 \On Collatz theorem II.pdf wersja z 5 czerwca 2022 ]

][http://lem12.uksw.edu.pl/images/a/ab/On-Collatz-thm17-09-21.pdf wersja z 20 wrzesnia 2021]

[http://lem12.uksw.edu.pl/images/7/7d/Algorytmy-bliskie-Collatzowi.pdf algorytmy wokół Collatzowe]

[http://lem12.uksw.edu.pl/images/c/c0/On-Collatz-thm-27-09-21.pdf wersja z 27 wrzesnia 2021]

[http://lem12.uksw.edu.pl/images/8/8f/On-Collatz-thm-7-10-21.pdf wersja z 7 pażdziernika 2021]

2026-02-27T12:01:59Z

AndrzejSalwicki: AndrzejSalwicki przesłano nową wersję pliku „Plik:CollatzConjecturebecomesTheorem2026Jan29.pdf“

Logika Algorytmiczna

2026-02-25T12:40:11Z

AndrzejSalwicki:

''Felix qui potuit rerum cognoscere causas'' 
=Próba zmian
= Wprowadzenie =
Zmiana kontrolna Środa 21 maja 2025 g. 19:25
Logika algorytmiczna AL jest ''rachunkiem logicznym''. Nie jest to byle jaki system logiczny. Stworzony został przez nas jako narzedzie pomocne i niezbędne w pracy nad oprogramowaniem. 
Rachunek programów tj. logika algorytmiczna:
* uzupełnia język o programy,
* program jest wyrażeniem zbudowanym z programów atomowych - instrukcji przypisania przy pomocy kilku operatorów programotwócztch: while, if, złożenie,
* program może poprzedzać formułę i takie wyrażenie jest także formułą,

Rachunek programów AL umożliwia:
# Wyrażenie własności programu przez odpowiednio napisaną formułę języka systemu AL [[Wyrażalność semantycznych własności programów]]
# Przeprowadzanie dowodów formuł wyrażających ważne semantyczne własności programów, [[Przykłady dowodów]].
# Podanie aksjomatów dla wielu struktur danych. Aksjomaty takie wykluczają struktury niechciane, czy wręcz struktury patologiczne.[[Aksjomaty struktur]]
# Specyfikację oprogramowania, [[SpecVer]]
# Weryfikację oprogramowania względem ustalonej specyfikacji.
# Aksjomatyczny opis semantyki danego języka programowania.[[Aksjomatyczna definicja języka programowania]]
# i wiele innych rzeczy.
[[Plik:4logiki.jpg|thumb|center |750px| Rys. 1 Cztery systemy logiczne ]]
Powyższy rysunek 1 ilustruje relacje zachodzące pomiędzy tymi czterema rachunkami logicznymi. Strzałki wskazują na zachodzenie następującej relacji <math>\mathcal{L}\rightarrow\mathcal{L}'</math> pomiędzy dwoma rachunkami logicznymi <math>\mathcal{L}</math> i <math>\mathcal{L}'</math>: ''Każda tautologia'' <math>\alpha</math> ''rachunku'' <math>\mathcal{L}</math> ''staje się tautologią rachunku ''<math>\mathcal{L}</math>' ''po zastąpieniu atomów formuły'' <math>\alpha</math> ''przez formuły rachunku'' <math>\mathcal{L}</math>. Nieco więcej informacji uzyskamy porównując zbiory wyrażeń poprawnie zbudowanych <math>\mathcal{WFF} </math>. 
Języki tych rachunków logicznych różnią się. Każdy język jest parą <alfabet, zbiór wyrażen poprawnie zbudowanych>. Zwróćmy uwagę na to, że za każdym razem struktura zbioru wyrażeń poprawnie zbudowanych <math>\mathcal{WFF} </math> (''ang''. well formed formulas) jest inna. 
Oznaczenia przyjete na rysunku: <math>\mathcal{L}</math> - język, <math>\mathcal{A}</math> - alfabet, <math>\mathcal{T}</math> - zbiór termów (wyrażeń arytmetycznych, obiektowych,...), <math>\mathcal{F}</math> - zbiór formuł, <math>\mathcal{P}</math> - zbiór programów.
[[Plik:AxiomPL.jpg|thumb|750px| Rys. 2 Aksjomaty rachunku zdań ]]
[[Plik:axiomsFOL-AL.jpg|thumb |750px| Rys. 3 Aksjomaty rachunku predykatów(Ax12 i Ax13) i rachunku programów ]]
[[Plik:inferenceRules.jpg| thumb |750px| Rys. 4 Reguły wnioskowania ]]
Zbiór formuł logiki algorytmicznej zawiera w sobie wszystkie formuły pierwszego rzędu i ponadto, jest zamknięty ze względu na poprzedzanie formuły programem. Jeśli <math>\alpha</math> jest formułą i <math>K</math> jest programem to wyrazenie postaci <math>K\alpha</math> jest formułą logiki algorytmicznej, krócej, formułą algorytmiczna. 
Jak takiej formule <math>K\alpha</math> przypisać wartość logiczną prawda lub fałsz?
[[Plik:Kalfa.jpg |thumb|left|300px|Rys. 5 Wyznaczanie wartośći formuły <math>K\alpha</math> ]]
Rysunek 5 powinien wszystko wyjaśnić.Pozostaje jednak przypadek gdy obliczenie programu K nie daje wyniku, z powodu zapętlenia się programu lub innego błędu. Oczywiście nie możemy wtedy twierdzić, że ''dla danych v, obliczenie programu K kończy się pomyślnie i wyniki spełniają warunek <math>\alpha</math>''. A więc w tym przypadku wartościa formuły <math>K\alpha</math> jest fałsz. 

O logice algorytmicznej możemy też powiedzieć, że jest [[rachunek programów|''rachunkiem programów'']]. Język logiki algorytmicznej zawiera programy i formuły algorytmiczne. '''Ważne''' jest to, że ''każda semantyczna własność programów np. poprawność, równowazność, kończenie obliczeń lub przeciwnie zapętlanie, ... może być wyrażona przez odpowiednią formułę''. Pozwala to zamienić zadanie wykazania, że pewien program <math>P</math> posiada pewną własnośc semantyczną <math>S</math> na zadanie udowodnić formułę <math>\beta</math> należąca do języka logiki algorytmicznej. '''Przykład''' 
Własność: ''Dla każdych danych <math>v</math>, jeśli program <math>K</math> rozpoczyna obliczenia z danymi spełniającymi warunek <math>\alpha</math> to jego obliczenie zakończy się (nie będzie zapętlenia, ani przerwania obliczeń) i jego wyniki spełniają warunek <math>\beta</math>'', jest wyrażana formułą <math>\alpha \rightarrow K\beta</math>. Nie musimy więc podejmować trudu testowania czy dla kazdych danych obliczenie programu K będzie skończone i ... 

Formuły tworzą algebrę z działaniami: konkatenacji, alternatywy, negacji i implikacji oraz z działaniami nieskończonymi tj. kwantyfikatorami, ponadto programy są modalnościami. Programy też tworzą algebrę: działaniami tej algebry są iteracja, rozgałęzienie i złożenie programów. Mamy więc do czynienia ze splotem dwu algebr. Możemy go nazwać rachunkiem programów. Zadaniem logiki algorytmicznej jest poszukiwanie ''praw rachunku programów''.

Celem jest zebranie praw i reguł wnioskowania, które umożliwią analizę algorytmów i wydawanie opinii o ich własnościach semantycznych, bez wykonywania obliczeń, na podstawie samego tekstu algorytmu i aksjomatów struktury danych w jakiej dany program ma byc interpretowany.

'''Przykład'''
Rozpatrzmy prosty program
{| class="wikitable"
|-
| (* Dane: x>0 i y>0 liczby naturalne *)
'''Deklaracje:''' typ(x, y, n, m, r, q, max)='''N''' & typ(n_mniejsze)=Boolean

n:=x; m:=y;
'''while''' n ≠ m '''do'''
'''''Oznaczenie''''' niech l=max(n,m)
r:=0;
'''while''' r ≠n '''and''' r ≠m '''do''' r:=r+1 '''od''';
'''if''' r=n '''then''' n_miejsze:=true; max:=m '''else''' n_mniejsze:=false; max:=n '''fi''';
'''''Stwierdzenie''''' (n<m & m=max(n,m) lub m<n & n=max(n,m))
q:=0;
'''while''' r≠max '''do''' r:= r+1; q:=q+1 '''od''';
'''''Stwierdzenie''''' q = |m-n| & (1 ≤ q < max(n,m))& r=max(n,m)
'''if''' n_mniejsze '''then''' m:=q '''else''' n := q '''fi'''
'''''Stwierdzenie''''' max(n,m) < l
'''od''' ( wynik = n)
(* Wynik: nwd(x,y) *)
|}

Co robi ten program? Czy to jest pytanie dobrze postawione?
Czy obliczenie tego programu jest skończone dla każdych danych <math>n</math> i <math>m</math>?
Czym są te dane? Jakie znaczenie mają operacje - i + oraz stała 1? Jakie znaczenie ma predykat <?

Wiele osób powie,że przecież to proste. Powyższy program oblicza największy wspólny dzielnik liczb naturalnych <math>xP</math> i <math>y</math>. No tak, ale skąd wiesz, że środowisko w którym wykonujesz ten program nie jest podejrzane? Na kolejnej stronie możesz zobaczyć klasę która implementuje operacje dodawania liczb naturalnych i relację równości w niestandardowy sposób. Powyższy program w otoczeniu tej klasy zachowuje się niestandardowo. Po pierwsze, obliczenia tego programu sa nieskończone dla pewnych danych. Powiesz mi, ta klasa nie spełnia aksjomatów liczb naturalnych? Otóż '''spełnia'''. Jakie więc aksjomaty należy wziąć pod uwagę i o co mamy pytać?

Zanim zaczniesz analizować działanie programu powinieneś zdać sobie sprawę z kilku rzeczy:
# Program zachowuje się różnie w różnych otoczeniach. Czym jest otoczenie? To zależy, może to być pierwotny typ danych np. integer w wielu językach programowania lub struktura danych opisana za pomocą pewnej klasy.
# Podczas analizy powinniśmy rozpatrywać program <math>P</math> w parze z jego otoczeniem <math>E</math>. Podczas analizy nie wystarczy nam nazwa otoczenia, ani sygnatura nazywana przez programistów interfejsem (ang, ''interface'').
# W procesie analizy musimy korzystać z własności otoczenia np. z przemienności i łączności dodawania.
# Musimy też sobie zadawać sprawę, że wielu podstawowych własności nie da się wyrazić formułami pierwszego rzędu.
# '''Własności algorytmiczne naszych programów wynikają z własności algorytmicznych otoczenia.''' 

Zechciej przejść na stronę [[Euklides]] by poznać nasze argumenty.

== Program logiki algorytmicznej ==
Zadaniem logiki algorytmicznej jest dostarczenie narzędzi do analizowania semantycznych własności programów takich jak: własność stopu, poprawność programu, etc.
W języku logiki algorytmicznej znajdujemy trzy zbiory: zbiór formuł, zbiór wyrażeń (zbiór termów) i zbiór programów (zbiór algorytmów).
'''Uwaga''' W języku logiki zdaniowej (rachunku zdań) rozważany jest jeden tylko zbiór wyrażeń poprawnie zbudowanych, jest to zbiór formuł (zdaniowych). Formuły stanowią najmniejszy zbiór napisów zawierający zbiór zmiennych zdaniowych i zamknięty ze względu na operatory logiczne.
W jeżyku logiki pierwszego rzędu zb→ór wyrażen poprawnie zbudowanych jest suma dwu rozłącznych zbiorów: zbioru termów(inaczej zbiór wyrażen nazwowych) i zbioru formuł. W rachunku programów (czyli logice algorytmicznej) w naturalny sposób pojaia się zbiór algorytmów. '''koniec uwagi'''
Znaczeniem programu <math>P</math> jest funkcja ze zbioru <math>W</math> wartościowań zmiennych w ten sam zbiór. Zazwyczaj funkcję tę określa się przy pomocy pojęcia [[obliczenia programu]]. 

== Zastosowania ==
Stosując logikę algorytmiczną czyli rachunek programów potrafimy odpowiedziec twierdząco na nastepujące pytania:
# Czy można podać aksjomaty i reguły wnioskowania, które opiszą semantykę operacyjną języka programowania?
# Czy (i jakie) własności struktur danych (systemów algebraicznych) są wyrażalne w języku logiki algorytmicznej?
# Czy (i jakie) własności programów są wyrażalne formułami algorytmicznymi? 

Ad 2. W matematyce rozważa się wiele własności ważnych struktur algebraicznych, których nie można wyrazić w języku pierwszego rzędu. Większość z nich może być wyrażona przy pomocy formuł algorytmicznych 

* bycie liczbą naturalną,
* aksjomat Archimedesa
* aksjomat ciał charakterystyki zero
* aksjomat grup torsyjnych
* aksjomat grup cyklicznych
i in. 
Dla informatyków niezwykle ważny jest fakt, że niemal wszystkie napotykane w programach struktury danych mogą być scharakteryzowane przy pomocy formuł algorytmicznych
* s jest stosem (skończonym)
* q jest kolejką FIFO skończoną
* s jest drzewem binarnym
* d jest drzewem binarnych poszukiwań
* q jest kolejką priorytetową
* d jest strukturą słownika (ang. dictionary)
* k jest kopcem
itd.
== Inne logiki programów ==
Możesz się zapytać jak się ma rachunek programów (tj. logika algorytmiczna) do innych logik programów : np. rachunek Floyda, logika Hoare'a, rachunek najsłabszego warunku wstępnego Dijkstry, logiki dynamicznaj, etc.?

[[calculus of Floyd|rachunek Floyda]] 

[[logic of Hoare|logika Hoare'a]] 

calculus of weakest precondition of Dijkstra 

[[dynamic logic]] 

== Uwagi historyczne ==
Algorytmy pojawiły sie kilka tysięcy lat temu. W Babilonie, Egipcie i Grecji. 

W czasach nowożytnych studia nad algorytmami podjęli Goedel, Turing, Church, Markov, Kołmogorov i wielu innych. Szkoda, że Tarski nie rozszerzył swych badań nad semantyką na funkcje obliczalne. Szkoda, że studia funkcji obliczalnych skupiły się na samych funkcjach, zaniedbując aspekt językowy. Prawie nie zajmowano się językiem służcym do definiowania funkcji rekurencyjnych. Alonzo Curch był chyba wyjatkiem? D. Kleene był blisko - jego definicja operatora minimum ograniczonego to przeciez petla FOR, a operacja minimum efektywnego to pętla WHILE. Warto pamietac twierdzenie S. Kleene z r. 1942 o tym, że zbiór funkcji obliczalnych jesli jest zamknięty ze względu na superpozycję i minimum efektywne ( i zawiera kilka funkcji poczatkowych) to definiowanie funkcji obliczalnych przez rekursję prostą może być zastąpione przez operację minimum efektywnego. 

Po drugiej wojnie światowej gdy pojawiły się komputery (zwane wtedy maszynami matematycznymi), ich programy zapisywano w kodzie maszynowym lub (później) w assemblerze. Trudno było dostrzec struktury i prawidłowości. W maszynie von Neumanna wszystko jest ciągiem bitów - liczbą. Ale pamiętam odczyt Antoniego Mazurkiewicza (ok 1960 r.) i jego dowód poprawności algorytmu z jedną pętla. Algorytm miał obliczyć sumę liczb zapisanych w tablicy. Kod maszyny XYZ-1 był bardzo ubogi. Program wymagał pobrania instrukcji "''weź kolejną komórkę pamięci do Akumulatora''" do rejestru Akumulator, zwiększenia adresu i zapisaniu tak zmienionej instrukcji w pamięci rozkazów na swoim pierwotnym miejscu. Program był więc ciągiem słów binarnych - każde słowo można jednak interpretować dwoiście, jako liczbę lub jako instrukcję. Nie ma w tym żadnej widocznej struktury. 

Prekursorzy logiki algorytmicznej 
Janov - jego praca poprzedza zdaniową logikę dynamiczną. Przedmiotem analizy są schematy programów (zapisywane w bardzo specjalny sposób) i relacja równoważności schematów. Dzisiaj powiedzielibyśmy, że schemat programu jest grafem skończonym. Wierzchołkom grafu przyporządkowano albo zmienną programowa albo formułę zdaniowa. Praca Janova jest nie tylko trudno dostępna, ale przede wszystkim mało czytelna. W książce A.P. Ershova można znaleźć przystępną ekspozycję teorii Janova. 
Engeler(1967) - zauważył, że własność stopu programu można wyrazić jako formułę logiki <math>L_{\omega1\,\omega} </math>, a dokładniej jako nieskończoną alternatywę formuł otwartych. 
Warto też wspomnieć o pracach Glushkova dotyczących systemów algebr algorytmicznych i książkę Helmuta Thielego. 
''Rasiowa'' - w książce ''Mathematics of metamathematics''(1963) str. 218 sformułowała podstawową własność instrukcji przypisania. Niech <math> s </math> oznacza jakieś odwzorowanie <math> s\colon V \to T </math> gdzie <math> V </math> jest zbiorem zmiennych indywiduowych, a <math> T </math> jest zbiorem termów. Odwzorowanie <math> s </math> nazywa się podstawieniem. Jeśli <math> \tau </math> oznacza jakiś term to <math> s\,\tau </math> oznacza wyrażenie powstające z termu <math> \tau </math> przez równoczesne zastąpienie wszystkich wystąpień zmiennych indywiduowych <math> \tau </math> przez odpowiednie wartości odwzorowania <math> s </math>. Oznaczmy term <math> \tau </math> przez <math> \tau(x_1,\dots,x_n)</math> podkreślając, że zmienne <math> x_1,\dots,x_n </math> to są wszystkie zmienne występujące w termie <math> \tau </math>. Wynik równoczesnego podstawienia za zmienne <math> x_1,\dots,x_n </math> występujące w termie <math> \tau </math>, termów <math> s(x_1),\dots,s(x_n) </math> oznaczmy <math> s\tau </math>. Mamy więc równość <math> s\tau(x_1,\dots,x_n)= \tau(s(x_1),\dots,s(x_n)) </math>. Można bez trudu udowodnić, że wynik jest tez termem.
Przypomnijmy teraz ten element definicji pojęcia spełniania (Tarski): dla ustalonej interpretacji symboli funkcyjnych <math> R </math> i ustalonego wartościowania zmiennych <math> v </math>, term <math> \tau </math> wyznacza funkcję ze zbioru wartościowań w zbiór wartoścowań.
Teraz możemy sformułować 
Niech <math> R </math> będzie dowolnie ustaloną interpretacją symboli funkcyjnych, niech <math> v </math> będzie dowolnym wartościowaniem zmiennych. Dla każdego podstawienia <math> s </math> i każdego termu <math> \tau </math> zachodzi równość
<math> s\tau_R(v)=\tau_R(s_R(v)) </math> 
Zauważmy, że w czasie pisania ksiązki ''Mathematics of metamathematics''(przed r. 1963) ani Rasiowa ani Sikorski nie mieli pojęcia o programowaniu. A jednak, gdy zapisać podstawienie <math> s </math> w trochę innej formie <math> \{x_1:=\tau_1 \& \dots \& x_n:=\tau_n \} </math> i zrozumieć, że wartościowanie zmiennych to to samo co stan pamięci, a interpretacja <math> R </math> to po prostu jednostka arytmetyczna komputera, to wszystko trafia na swoje miejsce.

== Bibliografia ==
Książki

# [AlgoLog] [[Media:Algorithmic_Logic.pdf | {{cytuj książkę |odn=tak| nazwisko = Mirkowska| imię = Grażyna | nazwisko2 = Salwicki | imię2 = Andrzej | tytuł = Algorithmic Logic | wydawca = PWN | miejsce = Warszawa | data = 1987 | strony = 345}}]]
# [LogProg1] [[Media:LogikaAlgorytmiczna_1z2.pdf | {{cytuj książkę | odn=tak |imię2=Andrzej | nazwisko2=Salwicki | imię=Grażyna | nazwisko=Mirkowska| tytuł=Logika Algorytmiczna dla Programistów|wydawca=WNT | miejsce=Warszawa| data=1992|strony=294 }}]] cz.1 
[[book Algorithmic Logic ]]
# [LogProg2] [[Media:LogikaAlgorytmiczna_2z2.pdf | {{cytuj książkę | odn=tak |imię2=Andrzej | nazwisko2=Salwicki | imię=Grażyna | nazwisko=Mirkowska| tytuł=Logika Algorytmiczna dla Programistów|wydawca=WNT | miejsce=Warszawa| data=1992|strony=294 }}]] cz.2
#[AL4software] [[Media:AlgoLogic.pdf| {{cytuj książkę | odn=tak |imię2=Andrzej | nazwisko2=Salwicki | imię=Grażyna | nazwisko=Mirkowska| tytuł=Algorithmic Logic for Software Construction and Verification|wydawca=Dąbrowa Research | miejsce=Dąbrowa Leśna| data=2014|strony=154 }}]]
# [CentrumBanachAL] [[ Media:bcp211.pdf |{{Cytuj książkę |odn=tak| nazwisko = Banachowski | imię = Lech | tytuł = An introduction to Algorithmic Logic - Metamathematical Investigations of Theory of Programs | wydawca = PWN | miejsce = Warszawa | data = 1977 | seria = Banach Center Publications | strony = 7-99 | isbn = 123 | nazwisko2 = Kreczmar | imię2 = Antoni | nazwisko3 = Mirkowska | imię3 = Grażyna | nazwisko4 = Rasiowa | imię4 = Helena | nazwisko5 = Salwicki | imię5 = Andrzej | tom = 2 | tytuł tomu = Banach Center Publications }}]]
# [HRAL] {{Cytuj książkę | odn=tak | nazwisko= Rasiowa | imię=Helena | tytuł= Algorithmic Logic - Notes from Seminar in Simon Fraser University | data=1975 | seria= Reports of Institute of Computer Science PAS | tom=281 | miejsce=Warsaw }}
# [AB] {{Cytuj książkę | odn=tak | nazwisko= Biela | imię=Andrzej | tytuł= Algorithmic structural completeness and a retrieval system for proving theorems in algorithmic theories | data=2000 | wydawca=Wydawnictwo Uniwersytetu Śląskiego | tom=1901 | miejsce=Katowice | strony=122 | url=http://lem12.uksw.edu.pl/images/4/40/A-Biela.pdf }}
Artykuły (wybór)
# [GMP] [[Media:GMP1970.pdf | {{cytuj pismo | odn=tak | nazwisko = Góraj | imię = Anna | nazwisko2= Mirkowska | imię2 = Grazyna | nazwisko3 = Paluszkiewicz | imię3 = Anna| tytuł = On the notion of description of program | czasopismo = Bull. Acad. Polon. Sci. Ser. Math. Astr. Phys.| rok= 1970 |strony = 499 - 505 }}]]
# [GM1971] {{cytuj pismo | odn=tak |nazwisko= Mirkowska | imię= Grażyna | tytuł = On Formalized Systems of Algorithmic Logic | czasopismo= Bull. Polish Academy Sciences, Ser. Math. Phys. |rok =1971 |tom = 19 | strony=421-428 |url=http://lem12.uksw.edu.pl/images/6/6f/On_Formalized-Mirk.pdf}}
# [GM1] [[Media:MirkowskaI-1-17.pdf| {{cytuj pismo | odn=tak | nazwisko= Mirkowska | imię = Grazyna | tytuł = Algorithmic logic and its applications in the theory of programs I | czasopismo = Fundamenta Informaticae| rok= 1977 |strony = 1-17 }} ]]
# [GM2] [[Media:Mirkowska-II-147-165.pdf| {{cytuj pismo | odn=tak | nazwisko= Mirkowska | imię = Grazyna | tytuł = Algorithmic logic and its applications in the theory of programs II | czasopismo = Fundamenta Informaticae| rok= 1977 |strony = 147-165 }} ]]
# [AS1] [[Media:FormalizedAlgorithmicLanguages.pdf | {{cytuj pismo | odn=tak | nazwisko= Salwicki | imię = Andrzej | tytuł = Formalized Algorithmic Languages | czasopismo = Bull. Acad. Polon. Sci. Ser. Math. Astr. Phys.| rok= 1970 |tom=18 |strony = 227-232 }} ]]
# [AS3] [[Media:CalculuswIterationQuantifiers.pdf | {{cytuj pismo | odn=tak | nazwisko= Salwicki | imię = Andrzej | tytuł = On the predicate calculi with iteration quantifiers | czasopismo = Bull. Acad. Polon. Sci. Ser. Math. Astr. Phys.| rok= 1970 |tom=18 |strony = 279-285 }} ]]
# [LB1] [[Media:BanI-93-119.pdf| {{cytuj pismo | odn=tak | nazwisko= Banachowski | imię = Lech | tytuł = Investigations of Properties of Programs by means of Extended Algorithmic Logic I | czasopismo = Fundamenta Informaticae| rok= 1977 |strony = 93-119 }} ]]
# [LB2] [[Media:Banachowski-II-167-193.pdf| {{cytuj pismo | odn=tak | nazwisko= Banachowski | imię = Lech | tytuł = Investigations of Properties of Programs by means of Extended Algorithmic Logic II | czasopismo = Fundamenta Informaticae| rok= 1977 |strony = 167-193 }} ]]
# [LB3] [[Media:BanachowskiDataStruct.pdf| {{cytuj pismo | odn=tak | nazwisko= Banachowski | imię = Lech | tytuł = An Axiomatic Approach to the Theory of Data Structures | czasopismo = Bull. Acad. Polon. Sci. Ser. Math. Astr. Phys. | rok= 1975 |strony = 315-323 }} ]]
# [AK1] [[Media:Kreczmar-Program-Fields.pdf| {{Cytuj pismo |odn=a | imię=Antoni | nazwisko=Kreczmar |tytuł=Programmability in Fields |czasopismo=Fundamenta Informaticae |strony=195-230 |rok=1977}}]]
# [AK2] [[Media:Kreczmar-Efficiency-problems.pdf| {{Cytuj pismo |odn=b | imię=Antoni | nazwisko=Kreczmar |tytuł=Effectivity problems of Algorithmic Logic |czasopismo=Fundamenta Informaticae |strony=19-32 |rok=1977}}]]
# [MSS2009] [[Media:Verifying-a-class.pdf |{{cytuj pismo| odn=tak| nazwisko=Mirkowska| imię=Grażyna| nazwisko2=Salwicki| imię2=Andrzej| nazwisko3=Świda| imię3=Oskar| tytuł=Verifying a Class: combining Testing and Proving|czasopismo=Fundamenta Informaticae| strony= 305-324 |rok= 2009 }}]]
# [AS2017] [[Media:On-Euclids-algorithm-2018.pdf | {{Cytuj pismo| odn=nie| nazwisko=Salwicki| imię=Andrzej| tytuł=A new proof of Euclid's algorithm | czasopismo= }}]]
# [WD1] [[ Media:WDnonprog.pdf | {{Cytuj pismo | odn=nie| nazwisko= Dańko | imię=Wiktor | tytuł=Nonprogrammable function defined by a procedure }} ]]

==Protokół rozbieżności==
Następujący tekst został złożony do druku
[[Media:On-Euclids-algorithm-2018.pdf | {{Cytuj pismo| odn=nie| nazwisko=Salwicki| imię=Andrzej| tytuł=A new proof of Euclid's algorithm | czasopismo= }}]] 

Pierwsza recenzja była rzeczowa, pomocna i jej sugestie zostały, z podziękowaniem, wykorzystane http://lem12.uksw.edu.pl/images/8/8c/1pierwszaRec.pdf. 

Drugi recenzent przedstawił następującą opinię http://lem12.uksw.edu.pl/images/0/0b/Second-report-08.pdf. 

Na to autor odpowiedział prosząc o referencje do zapowiadanych twierdzeń lub o przedstawienie dowodu. 

Oto protokół rozbieżności:
http://lem12.uksw.edu.pl/images/9/9a/DiscrepancyReport.pdf

==Pytania otwarte==
* Rozpatrzmy teorię algorytmiczną <math>Th_{2.5} = \langle L,C,A \rangle </math> gdzie
<math>L</math> - język, jest językiem struktury liczb naturalnych, algorytmicznym, 

<math>C</math> - operacja konskwencji jest wyznaczona przez zbiór aksjomatów i reguł wnioskowania logiki algorytmicznej (rachunku programów), 

<math>A</math> - zbiór aksjomatów, jest zbiorem wszystkich formuł pierwszego rzędu prawdziwych w standardowym modelu liczb naturalnych. 

Czy formuła <math>\color{blue}\forall x\, \{y:=0;\, \mathbf{while}\ x\neq y\ \mathbf{do}\ y:=y+1\ \mathbf{done}\}(x=y) </math> jest twierdzeniem tej teorii?
--[[Użytkownik:AndrzejSalwicki|AndrzejSalwicki]] ([[Dyskusja użytkownika:AndrzejSalwicki|dyskusja]]) 15:34, 30 maj 2018 (CEST)
* Czy teoria <math>Th_{2.5}</math> jest zupełna?
--[[Użytkownik:AndrzejSalwicki|AndrzejSalwicki]] ([[Dyskusja użytkownika:AndrzejSalwicki|dyskusja]]) 19:09, 31 maj 2018 (CEST)
* Według Harela, zob. Dynamic Logic, każda formuła algorytmiczna prawdziwa w standardowym modelu arytmetyki powinna być twierdzeniem teorii <math>Th_{2.5}</math>

* Czy teoria kontenerów (tj. słowników, dictionaries) bez aksjomatu algorytmicznego jest zupełna?

[[Category:Logika Algorytmiczna}}]]

Logika Algorytmiczna

2026-02-25T12:39:18Z

AndrzejSalwicki:

''Felix qui potuit rerum cognoscere causas'' 
=Próba zmian
= Wprowadzenie =
Zmiana kontrolna Środa 21 maja 2025 g. 19:25
Logika algorytmiczna AL jest ''rachunkiem logicznym''. Nie jest to byle jaki system logiczny. Stworzony został przez nas jako narzedzie pomocne i niezbędne w pracy nad oprogramowaniem. 
Rachunek programów tj. logika algorytmiczna:
* uzupełnia język o programy,
* program jest wyrażeniem zbudowanym z programów atomowych - instrukcji przypisania przy pomocy kilku operatorów programotwócztch: while, if, złożenie,
* program może poprzedzać formułę i takie wyrażenie jest także formułą,

Rachunek programów AL umożliwia:
# Wyrażenie własności programu przez odpowiednio napisaną formułę języka systemu AL [[Wyrażalność semantycznych własności programów]]
# Przeprowadzanie dowodów formuł wyrażających ważne semantyczne własności programów, [[Przykłady dowodów]].
# Podanie aksjomatów dla wielu struktur danych. Aksjomaty takie wykluczają struktury niechciane, czy wręcz struktury patologiczne.[[Aksjomaty struktur]]
# Specyfikację oprogramowania, [[SpecVer]]
# Weryfikację oprogramowania względem ustalonej specyfikacji.
# Aksjomatyczny opis semantyki danego języka programowania.[[Aksjomatyczna definicja języka programowania]]
# i wiele innych rzeczy.
[[Plik:4logiki.jpg|thumb|center |750px| Rys. 1 Cztery systemy logiczne ]]
Powyższy rysunek 1 ilustruje relacje zachodzące pomiędzy tymi czterema rachunkami logicznymi. Strzałki wskazują na zachodzenie następującej relacji <math>\mathcal{L}\rightarrow\mathcal{L}'</math> pomiędzy dwoma rachunkami logicznymi <math>\mathcal{L}</math> i <math>\mathcal{L}'</math>: ''Każda tautologia'' <math>\alpha</math> ''rachunku'' <math>\mathcal{L}</math> ''staje się tautologią rachunku ''<math>\mathcal{L}</math>' ''po zastąpieniu atomów formuły'' <math>\alpha</math> ''przez formuły rachunku'' <math>\mathcal{L}</math>. Nieco więcej informacji uzyskamy porównując zbiory wyrażeń poprawnie zbudowanych <math>\mathcal{WFF} </math>. 
Języki tych rachunków logicznych różnią się. Każdy język jest parą <alfabet, zbiór wyrażen poprawnie zbudowanych>. Zwróćmy uwagę na to, że za każdym razem struktura zbioru wyrażeń poprawnie zbudowanych <math>\mathcal{WFF} </math> (''ang''. well formed formulas) jest inna. 
Oznaczenia przyjete na rysunku: <math>\mathcal{L}</math> - język, <math>\mathcal{A}</math> - alfabet, <math>\mathcal{T}</math> - zbiór termów (wyrażeń arytmetycznych, obiektowych,...), <math>\mathcal{F}</math> - zbiór formuł, <math>\mathcal{P}</math> - zbiór programów.
[[Plik:AxiomPL.jpg|thumb|750px| Rys. 2 Aksjomaty rachunku zdań ]]
[[Plik:axiomsFOL-AL.jpg|thumb |750px| Rys. 3 Aksjomaty rachunku predykatów(Ax12 i Ax13) i rachunku programów ]]
[[Plik:inferenceRules.jpg| thumb |750px| Rys. 4 Reguły wnioskowania ]]
Zbiór formuł logiki algorytmicznej zawiera w sobie wszystkie formuły pierwszego rzędu i ponadto, jest zamknięty ze względu na poprzedzanie formuły programem. Jeśli <math>\alpha</math> jest formułą i <math>K</math> jest programem to wyrazenie postaci <math>K\alpha</math> jest formułą logiki algorytmicznej, krócej, formułą algorytmiczna. 
Jak takiej formule <math>K\alpha</math> przypisać wartość logiczną prawda lub fałsz?
[[Plik:Kalfa.jpg |thumb|left|300px|Rys. 5 Wyznaczanie wartośći formuły <math>K\alpha</math> ]]
Rysunek 5 powinien wszystko wyjaśnić.Pozostaje jednak przypadek gdy obliczenie programu K nie daje wyniku, z powodu zapętlenia się programu lub innego błędu. Oczywiście nie możemy wtedy twierdzić, że ''dla danych v, obliczenie programu K kończy się pomyślnie i wyniki spełniają warunek <math>\alpha</math>''. A więc w tym przypadku wartościa formuły <math>K\alpha</math> jest fałsz. 

O logice algorytmicznej możemy też powiedzieć, że jest [[rachunek programów|''rachunkiem programów'']]. Język logiki algorytmicznej zawiera programy i formuły algorytmiczne. '''Ważne''' jest to, że ''każda semantyczna własność programów np. poprawność, równowazność, kończenie obliczeń lub przeciwnie zapętlanie, ... może być wyrażona przez odpowiednią formułę''. Pozwala to zamienić zadanie wykazania, że pewien program <math>P</math> posiada pewną własnośc semantyczną <math>S</math> na zadanie udowodnić formułę <math>\beta</math> należąca do języka logiki algorytmicznej. '''Przykład''' 
Własność: ''Dla każdych danych <math>v</math>, jeśli program <math>K</math> rozpoczyna obliczenia z danymi spełniającymi warunek <math>\alpha</math> to jego obliczenie zakończy się (nie będzie zapętlenia, ani przerwania obliczeń) i jego wyniki spełniają warunek <math>\beta</math>'', jest wyrażana formułą <math>\alpha \rightarrow K\beta</math>. Nie musimy więc podejmować trudu testowania czy dla kazdych danych obliczenie programu K będzie skończone i ... 

Formuły tworzą algebrę z działaniami: konkatenacji, alternatywy, negacji i implikacji oraz z działaniami nieskończonymi tj. kwantyfikatorami, ponadto programy są modalnościami. Programy też tworzą algebrę: działaniami tej algebry są iteracja, rozgałęzienie i złożenie programów. Mamy więc do czynienia ze splotem dwu algebr. Możemy go nazwać rachunkiem programów. Zadaniem logiki algorytmicznej jest poszukiwanie ''praw rachunku programów''.

Celem jest zebranie praw i reguł wnioskowania, które umożliwią analizę algorytmów i wydawanie opinii o ich własnościach semantycznych, bez wykonywania obliczeń, na podstawie samego tekstu algorytmu i aksjomatów struktury danych w jakiej dany program ma byc interpretowany.

'''Przykład'''
Rozpatrzmy prosty program
{| class="wikitable"
|-
| (* Dane: x>0 i y>0 liczby naturalne *)
'''Deklaracje:''' typ(x, y, n, m, r, q, max)='''N''' & typ(n_mniejsze)=Boolean

n:=x; m:=y;
'''while''' n ≠ m '''do'''
'''''Oznaczenie''''' niech l=max(n,m)
r:=0;
'''while''' r ≠n '''and''' r ≠m '''do''' r:=r+1 '''od''';
'''if''' r=n '''then''' n_miejsze:=true; max:=m '''else''' n_mniejsze:=false; max:=n '''fi''';
'''''Stwierdzenie''''' (n<m & m=max(n,m) lub m<n & n=max(n,m))
q:=0;
'''while''' r≠max '''do''' r:= r+1; q:=q+1 '''od''';
'''''Stwierdzenie''''' q = |m-n| & (1 ≤ q < max(n,m))& r=max(n,m)
'''if''' n_mniejsze '''then''' m:=q '''else''' n := q '''fi'''
'''''Stwierdzenie''''' max(n,m) < l
'''od''' ( wynik = n)
(* Wynik: nwd(x,y) *)
|}

Co robi ten program? Czy to jest pytanie dobrze postawione?
Czy obliczenie tego programu jest skończone dla każdych danych <math>n</math> i <math>m</math>?
Czym są te dane? Jakie znaczenie mają operacje - i + oraz stała 1? Jakie znaczenie ma predykat <?

Wiele osób powie,że przecież to proste. Powyższy program oblicza największy wspólny dzielnik liczb naturalnych <math>xP</math> i <math>y</math>. No tak, ale skąd wiesz, że środowisko w którym wykonujesz ten program nie jest podejrzane? Na kolejnej stronie możesz zobaczyć klasę która implementuje operacje dodawania liczb naturalnych i relację równości w niestandardowy sposób. Powyższy program w otoczeniu tej klasy zachowuje się niestandardowo. Po pierwsze, obliczenia tego programu sa nieskończone dla pewnych danych. Powiesz mi, ta klasa nie spełnia aksjomatów liczb naturalnych? Otóż '''spełnia'''. Jakie więc aksjomaty należy wziąć pod uwagę i o co mamy pytać?

Zanim zaczniesz analizować działanie programu powinieneś zdać sobie sprawę z kilku rzeczy:
# Program zachowuje się różnie w różnych otoczeniach. Czym jest otoczenie? To zależy, może to być pierwotny typ danych np. integer w wielu językach programowania lub struktura danych opisana za pomocą pewnej klasy.
# Podczas analizy powinniśmy rozpatrywać program <math>P</math> w parze z jego otoczeniem <math>E</math>. Podczas analizy nie wystarczy nam nazwa otoczenia, ani sygnatura nazywana przez programistów interfejsem (ang, ''interface'').
# W procesie analizy musimy korzystać z własności otoczenia np. z przemienności i łączności dodawania.
# Musimy też sobie zadawać sprawę, że wielu podstawowych własności nie da się wyrazić formułami pierwszego rzędu.
# '''Własności algorytmiczne naszych programów wynikają z własności algorytmicznych otoczenia.''' 

Zechciej przejść na stronę [[Euklides]] by poznać nasze argumenty.

== Program logiki algorytmicznej ==
Zadaniem logiki algorytmicznej jest dostarczenie narzędzi do analizowania semantycznych własności programów takich jak: własność stopu, poprawność programu, etc.
W języku logiki algorytmicznej znajdujemy trzy zbiory: zbiór formuł, zbiór wyrażeń (zbiór termów) i zbiór programów (zbiór algorytmów).
'''Uwaga''' W języku logiki zdaniowej (rachunku zdań) rozważany jest jeden tylko zbiór wyrażeń poprawnie zbudowanych, jest to zbiór formuł (zdaniowych). Formuły stanowią najmniejszy zbiór napisów zawierający zbiór zmiennych zdaniowych i zamknięty ze względu na operatory logiczne.
W jeżyku logiki pierwszego rzędu zb→ór wyrażen poprawnie zbudowanych jest suma dwu rozłącznych zbiorów: zbioru termów(inaczej zbiór wyrażen nazwowych) i zbioru formuł. W rachunku programów (czyli logice algorytmicznej) w naturalny sposób pojaia się zbiór algorytmów. '''koniec uwagi'''
Znaczeniem programu <math>P</math> jest funkcja ze zbioru <math>W</math> wartościowań zmiennych w ten sam zbiór. Zazwyczaj funkcję tę określa się przy pomocy pojęcia [[obliczenia programu]]. 
<math>
\usepackage{tikzcd}
\begin{tikzcd}
A\arrow[r] & B
\end{tikzcd}
</math>

<math>
\begin{figure}[h]\begin{center}
\usepackage{tikz}
\tikzstyle{stan}=[rectangle , text=blue]
\tikzstyle{is}=[->,>=latex,rounded corners=4pt]
\begin{tikzpicture}[scale=0.38]
%\draw [gray, very thin] (-2,-2) grid [step=1cm] (28,50);
\draw (-2,5) -- (4,18) -- (27,18) -- (23,5) -- cycle[fill=green!25];
\node[stan] (T) at (4.44,14) {$v:\frac{x\, y\, z}{k\,l\,p}$};
\node[stan] (U) at (24,14) {$\frac{true}{false}$};
\node[stan] (V) at (14,6.2) {$v^{\prime}:\frac{x\, y\, z}{n\,l\,p}$};
\draw[is] (T) to[bend left]node[midway,below]{ $\bigl(\alpha(x/\tau)\bigr)_{\color{red}{\mathfrak{A}}\color{black}{}}$ } (U) ;
\draw[is] (T) to[bend right]node[midway,above ]{$\bigl(\{x:=\tau\}\alpha\bigr)_{\color{red}{\mathfrak{A}}\color{black}}$} (U) ;
\draw[is] (V) -- (U)node[midway,right]{$ \alpha(x)_{\color{red}{\mathfrak{A}}\color{black}{\ }}$ };
\draw[is] (T) -- (V)node[midway,left]{$\{x:=\tau \}_{\color{red}{\mathfrak{A}}\color{black}}$ };
\draw (0,20) -- (4,24) -- (27,24) -- (23,20) -- cycle[fill=yellow!35];

\node[stan] (T1) at (9,22) {$\{x:=\tau\}\alpha $ };
\node[stan] (U1) at (19,22) {$\alpha(x/\tau) $ };
\node[stan] (V1) at (14,22) {$\Leftrightarrow$ };

\draw [color=red, thick, ->] (9,22) -> (13,12.4)node[midway,left,near start]{$\mathfrak{A}$} ;
\draw [color=red, thick, ->] (19,22) -> (16,16.5)node[midway,left]{$\mathfrak{A}$} ;
\end{tikzpicture}
\caption{Aksjomat instrukcji przypisania \\
"\textit{warunek $\alpha(x)$ zachodzi po wykonaniu instrukcji $x\,:=\tau$ wttw, gdy przed wykonaniem tej instrukcji zachodzi warunek $\alpha(x/ \tau)$}"
jest tautologią\\
\begin{scriptsize}
na górnej płaszczyznie wydrukowaliśmy text aksjomatu, \\
na dolnej płaszczyznie objaśniamy co się dzieje podczas obliczeń i wskazujemy znaczenie (tj. semantykę) aksjomatu,
Litera $\mathfrak{A}$ oznacza dowolny typ (na razie przyjmij, że może to być typ integer lub typ real). Czerwone strzałki łączą formułę $\alpha(x/\tau) $ (odpowiednio \{x:=$\tau$\}$\alpha $) z funkcją $\alpha(x/\tau)_{\mathfrak{A}}$ (odpowiednio $\{x:=\tau \}(\alpha)_{\mathfrak{A}}$ ).
Stan pamięci $v'$ i dodatkowe strzałki ilustrują sposób obliczania wartości formuły, $\{x:=\tau \}(\alpha)$, zauważ, wartość $v'(x)=n= \tau_{\mathfrak{A}}( v(x))$.
\end{scriptsize}}\label{rAx18}
\end{center}
\end{figure}
</math>

== Zastosowania ==
Stosując logikę algorytmiczną czyli rachunek programów potrafimy odpowiedziec twierdząco na nastepujące pytania:
# Czy można podać aksjomaty i reguły wnioskowania, które opiszą semantykę operacyjną języka programowania?
# Czy (i jakie) własności struktur danych (systemów algebraicznych) są wyrażalne w języku logiki algorytmicznej?
# Czy (i jakie) własności programów są wyrażalne formułami algorytmicznymi? 

Ad 2. W matematyce rozważa się wiele własności ważnych struktur algebraicznych, których nie można wyrazić w języku pierwszego rzędu. Większość z nich może być wyrażona przy pomocy formuł algorytmicznych 

* bycie liczbą naturalną,
* aksjomat Archimedesa
* aksjomat ciał charakterystyki zero
* aksjomat grup torsyjnych
* aksjomat grup cyklicznych
i in. 
Dla informatyków niezwykle ważny jest fakt, że niemal wszystkie napotykane w programach struktury danych mogą być scharakteryzowane przy pomocy formuł algorytmicznych
* s jest stosem (skończonym)
* q jest kolejką FIFO skończoną
* s jest drzewem binarnym
* d jest drzewem binarnych poszukiwań
* q jest kolejką priorytetową
* d jest strukturą słownika (ang. dictionary)
* k jest kopcem
itd.
== Inne logiki programów ==
Możesz się zapytać jak się ma rachunek programów (tj. logika algorytmiczna) do innych logik programów : np. rachunek Floyda, logika Hoare'a, rachunek najsłabszego warunku wstępnego Dijkstry, logiki dynamicznaj, etc.?

[[calculus of Floyd|rachunek Floyda]] 

[[logic of Hoare|logika Hoare'a]] 

calculus of weakest precondition of Dijkstra 

[[dynamic logic]] 

== Uwagi historyczne ==
Algorytmy pojawiły sie kilka tysięcy lat temu. W Babilonie, Egipcie i Grecji. 

W czasach nowożytnych studia nad algorytmami podjęli Goedel, Turing, Church, Markov, Kołmogorov i wielu innych. Szkoda, że Tarski nie rozszerzył swych badań nad semantyką na funkcje obliczalne. Szkoda, że studia funkcji obliczalnych skupiły się na samych funkcjach, zaniedbując aspekt językowy. Prawie nie zajmowano się językiem służcym do definiowania funkcji rekurencyjnych. Alonzo Curch był chyba wyjatkiem? D. Kleene był blisko - jego definicja operatora minimum ograniczonego to przeciez petla FOR, a operacja minimum efektywnego to pętla WHILE. Warto pamietac twierdzenie S. Kleene z r. 1942 o tym, że zbiór funkcji obliczalnych jesli jest zamknięty ze względu na superpozycję i minimum efektywne ( i zawiera kilka funkcji poczatkowych) to definiowanie funkcji obliczalnych przez rekursję prostą może być zastąpione przez operację minimum efektywnego. 

Po drugiej wojnie światowej gdy pojawiły się komputery (zwane wtedy maszynami matematycznymi), ich programy zapisywano w kodzie maszynowym lub (później) w assemblerze. Trudno było dostrzec struktury i prawidłowości. W maszynie von Neumanna wszystko jest ciągiem bitów - liczbą. Ale pamiętam odczyt Antoniego Mazurkiewicza (ok 1960 r.) i jego dowód poprawności algorytmu z jedną pętla. Algorytm miał obliczyć sumę liczb zapisanych w tablicy. Kod maszyny XYZ-1 był bardzo ubogi. Program wymagał pobrania instrukcji "''weź kolejną komórkę pamięci do Akumulatora''" do rejestru Akumulator, zwiększenia adresu i zapisaniu tak zmienionej instrukcji w pamięci rozkazów na swoim pierwotnym miejscu. Program był więc ciągiem słów binarnych - każde słowo można jednak interpretować dwoiście, jako liczbę lub jako instrukcję. Nie ma w tym żadnej widocznej struktury. 

Prekursorzy logiki algorytmicznej 
Janov - jego praca poprzedza zdaniową logikę dynamiczną. Przedmiotem analizy są schematy programów (zapisywane w bardzo specjalny sposób) i relacja równoważności schematów. Dzisiaj powiedzielibyśmy, że schemat programu jest grafem skończonym. Wierzchołkom grafu przyporządkowano albo zmienną programowa albo formułę zdaniowa. Praca Janova jest nie tylko trudno dostępna, ale przede wszystkim mało czytelna. W książce A.P. Ershova można znaleźć przystępną ekspozycję teorii Janova. 
Engeler(1967) - zauważył, że własność stopu programu można wyrazić jako formułę logiki <math>L_{\omega1\,\omega} </math>, a dokładniej jako nieskończoną alternatywę formuł otwartych. 
Warto też wspomnieć o pracach Glushkova dotyczących systemów algebr algorytmicznych i książkę Helmuta Thielego. 
''Rasiowa'' - w książce ''Mathematics of metamathematics''(1963) str. 218 sformułowała podstawową własność instrukcji przypisania. Niech <math> s </math> oznacza jakieś odwzorowanie <math> s\colon V \to T </math> gdzie <math> V </math> jest zbiorem zmiennych indywiduowych, a <math> T </math> jest zbiorem termów. Odwzorowanie <math> s </math> nazywa się podstawieniem. Jeśli <math> \tau </math> oznacza jakiś term to <math> s\,\tau </math> oznacza wyrażenie powstające z termu <math> \tau </math> przez równoczesne zastąpienie wszystkich wystąpień zmiennych indywiduowych <math> \tau </math> przez odpowiednie wartości odwzorowania <math> s </math>. Oznaczmy term <math> \tau </math> przez <math> \tau(x_1,\dots,x_n)</math> podkreślając, że zmienne <math> x_1,\dots,x_n </math> to są wszystkie zmienne występujące w termie <math> \tau </math>. Wynik równoczesnego podstawienia za zmienne <math> x_1,\dots,x_n </math> występujące w termie <math> \tau </math>, termów <math> s(x_1),\dots,s(x_n) </math> oznaczmy <math> s\tau </math>. Mamy więc równość <math> s\tau(x_1,\dots,x_n)= \tau(s(x_1),\dots,s(x_n)) </math>. Można bez trudu udowodnić, że wynik jest tez termem.
Przypomnijmy teraz ten element definicji pojęcia spełniania (Tarski): dla ustalonej interpretacji symboli funkcyjnych <math> R </math> i ustalonego wartościowania zmiennych <math> v </math>, term <math> \tau </math> wyznacza funkcję ze zbioru wartościowań w zbiór wartoścowań.
Teraz możemy sformułować 
Niech <math> R </math> będzie dowolnie ustaloną interpretacją symboli funkcyjnych, niech <math> v </math> będzie dowolnym wartościowaniem zmiennych. Dla każdego podstawienia <math> s </math> i każdego termu <math> \tau </math> zachodzi równość
<math> s\tau_R(v)=\tau_R(s_R(v)) </math> 
Zauważmy, że w czasie pisania ksiązki ''Mathematics of metamathematics''(przed r. 1963) ani Rasiowa ani Sikorski nie mieli pojęcia o programowaniu. A jednak, gdy zapisać podstawienie <math> s </math> w trochę innej formie <math> \{x_1:=\tau_1 \& \dots \& x_n:=\tau_n \} </math> i zrozumieć, że wartościowanie zmiennych to to samo co stan pamięci, a interpretacja <math> R </math> to po prostu jednostka arytmetyczna komputera, to wszystko trafia na swoje miejsce.

== Bibliografia ==
Książki

# [AlgoLog] [[Media:Algorithmic_Logic.pdf | {{cytuj książkę |odn=tak| nazwisko = Mirkowska| imię = Grażyna | nazwisko2 = Salwicki | imię2 = Andrzej | tytuł = Algorithmic Logic | wydawca = PWN | miejsce = Warszawa | data = 1987 | strony = 345}}]]
# [LogProg1] [[Media:LogikaAlgorytmiczna_1z2.pdf | {{cytuj książkę | odn=tak |imię2=Andrzej | nazwisko2=Salwicki | imię=Grażyna | nazwisko=Mirkowska| tytuł=Logika Algorytmiczna dla Programistów|wydawca=WNT | miejsce=Warszawa| data=1992|strony=294 }}]] cz.1 
[[book Algorithmic Logic ]]
# [LogProg2] [[Media:LogikaAlgorytmiczna_2z2.pdf | {{cytuj książkę | odn=tak |imię2=Andrzej | nazwisko2=Salwicki | imię=Grażyna | nazwisko=Mirkowska| tytuł=Logika Algorytmiczna dla Programistów|wydawca=WNT | miejsce=Warszawa| data=1992|strony=294 }}]] cz.2
#[AL4software] [[Media:AlgoLogic.pdf| {{cytuj książkę | odn=tak |imię2=Andrzej | nazwisko2=Salwicki | imię=Grażyna | nazwisko=Mirkowska| tytuł=Algorithmic Logic for Software Construction and Verification|wydawca=Dąbrowa Research | miejsce=Dąbrowa Leśna| data=2014|strony=154 }}]]
# [CentrumBanachAL] [[ Media:bcp211.pdf |{{Cytuj książkę |odn=tak| nazwisko = Banachowski | imię = Lech | tytuł = An introduction to Algorithmic Logic - Metamathematical Investigations of Theory of Programs | wydawca = PWN | miejsce = Warszawa | data = 1977 | seria = Banach Center Publications | strony = 7-99 | isbn = 123 | nazwisko2 = Kreczmar | imię2 = Antoni | nazwisko3 = Mirkowska | imię3 = Grażyna | nazwisko4 = Rasiowa | imię4 = Helena | nazwisko5 = Salwicki | imię5 = Andrzej | tom = 2 | tytuł tomu = Banach Center Publications }}]]
# [HRAL] {{Cytuj książkę | odn=tak | nazwisko= Rasiowa | imię=Helena | tytuł= Algorithmic Logic - Notes from Seminar in Simon Fraser University | data=1975 | seria= Reports of Institute of Computer Science PAS | tom=281 | miejsce=Warsaw }}
# [AB] {{Cytuj książkę | odn=tak | nazwisko= Biela | imię=Andrzej | tytuł= Algorithmic structural completeness and a retrieval system for proving theorems in algorithmic theories | data=2000 | wydawca=Wydawnictwo Uniwersytetu Śląskiego | tom=1901 | miejsce=Katowice | strony=122 | url=http://lem12.uksw.edu.pl/images/4/40/A-Biela.pdf }}
Artykuły (wybór)
# [GMP] [[Media:GMP1970.pdf | {{cytuj pismo | odn=tak | nazwisko = Góraj | imię = Anna | nazwisko2= Mirkowska | imię2 = Grazyna | nazwisko3 = Paluszkiewicz | imię3 = Anna| tytuł = On the notion of description of program | czasopismo = Bull. Acad. Polon. Sci. Ser. Math. Astr. Phys.| rok= 1970 |strony = 499 - 505 }}]]
# [GM1971] {{cytuj pismo | odn=tak |nazwisko= Mirkowska | imię= Grażyna | tytuł = On Formalized Systems of Algorithmic Logic | czasopismo= Bull. Polish Academy Sciences, Ser. Math. Phys. |rok =1971 |tom = 19 | strony=421-428 |url=http://lem12.uksw.edu.pl/images/6/6f/On_Formalized-Mirk.pdf}}
# [GM1] [[Media:MirkowskaI-1-17.pdf| {{cytuj pismo | odn=tak | nazwisko= Mirkowska | imię = Grazyna | tytuł = Algorithmic logic and its applications in the theory of programs I | czasopismo = Fundamenta Informaticae| rok= 1977 |strony = 1-17 }} ]]
# [GM2] [[Media:Mirkowska-II-147-165.pdf| {{cytuj pismo | odn=tak | nazwisko= Mirkowska | imię = Grazyna | tytuł = Algorithmic logic and its applications in the theory of programs II | czasopismo = Fundamenta Informaticae| rok= 1977 |strony = 147-165 }} ]]
# [AS1] [[Media:FormalizedAlgorithmicLanguages.pdf | {{cytuj pismo | odn=tak | nazwisko= Salwicki | imię = Andrzej | tytuł = Formalized Algorithmic Languages | czasopismo = Bull. Acad. Polon. Sci. Ser. Math. Astr. Phys.| rok= 1970 |tom=18 |strony = 227-232 }} ]]
# [AS3] [[Media:CalculuswIterationQuantifiers.pdf | {{cytuj pismo | odn=tak | nazwisko= Salwicki | imię = Andrzej | tytuł = On the predicate calculi with iteration quantifiers | czasopismo = Bull. Acad. Polon. Sci. Ser. Math. Astr. Phys.| rok= 1970 |tom=18 |strony = 279-285 }} ]]
# [LB1] [[Media:BanI-93-119.pdf| {{cytuj pismo | odn=tak | nazwisko= Banachowski | imię = Lech | tytuł = Investigations of Properties of Programs by means of Extended Algorithmic Logic I | czasopismo = Fundamenta Informaticae| rok= 1977 |strony = 93-119 }} ]]
# [LB2] [[Media:Banachowski-II-167-193.pdf| {{cytuj pismo | odn=tak | nazwisko= Banachowski | imię = Lech | tytuł = Investigations of Properties of Programs by means of Extended Algorithmic Logic II | czasopismo = Fundamenta Informaticae| rok= 1977 |strony = 167-193 }} ]]
# [LB3] [[Media:BanachowskiDataStruct.pdf| {{cytuj pismo | odn=tak | nazwisko= Banachowski | imię = Lech | tytuł = An Axiomatic Approach to the Theory of Data Structures | czasopismo = Bull. Acad. Polon. Sci. Ser. Math. Astr. Phys. | rok= 1975 |strony = 315-323 }} ]]
# [AK1] [[Media:Kreczmar-Program-Fields.pdf| {{Cytuj pismo |odn=a | imię=Antoni | nazwisko=Kreczmar |tytuł=Programmability in Fields |czasopismo=Fundamenta Informaticae |strony=195-230 |rok=1977}}]]
# [AK2] [[Media:Kreczmar-Efficiency-problems.pdf| {{Cytuj pismo |odn=b | imię=Antoni | nazwisko=Kreczmar |tytuł=Effectivity problems of Algorithmic Logic |czasopismo=Fundamenta Informaticae |strony=19-32 |rok=1977}}]]
# [MSS2009] [[Media:Verifying-a-class.pdf |{{cytuj pismo| odn=tak| nazwisko=Mirkowska| imię=Grażyna| nazwisko2=Salwicki| imię2=Andrzej| nazwisko3=Świda| imię3=Oskar| tytuł=Verifying a Class: combining Testing and Proving|czasopismo=Fundamenta Informaticae| strony= 305-324 |rok= 2009 }}]]
# [AS2017] [[Media:On-Euclids-algorithm-2018.pdf | {{Cytuj pismo| odn=nie| nazwisko=Salwicki| imię=Andrzej| tytuł=A new proof of Euclid's algorithm | czasopismo= }}]]
# [WD1] [[ Media:WDnonprog.pdf | {{Cytuj pismo | odn=nie| nazwisko= Dańko | imię=Wiktor | tytuł=Nonprogrammable function defined by a procedure }} ]]

==Protokół rozbieżności==
Następujący tekst został złożony do druku
[[Media:On-Euclids-algorithm-2018.pdf | {{Cytuj pismo| odn=nie| nazwisko=Salwicki| imię=Andrzej| tytuł=A new proof of Euclid's algorithm | czasopismo= }}]] 

Pierwsza recenzja była rzeczowa, pomocna i jej sugestie zostały, z podziękowaniem, wykorzystane http://lem12.uksw.edu.pl/images/8/8c/1pierwszaRec.pdf. 

Drugi recenzent przedstawił następującą opinię http://lem12.uksw.edu.pl/images/0/0b/Second-report-08.pdf. 

Na to autor odpowiedział prosząc o referencje do zapowiadanych twierdzeń lub o przedstawienie dowodu. 

Oto protokół rozbieżności:
http://lem12.uksw.edu.pl/images/9/9a/DiscrepancyReport.pdf

==Pytania otwarte==
* Rozpatrzmy teorię algorytmiczną <math>Th_{2.5} = \langle L,C,A \rangle </math> gdzie
<math>L</math> - język, jest językiem struktury liczb naturalnych, algorytmicznym, 

<math>C</math> - operacja konskwencji jest wyznaczona przez zbiór aksjomatów i reguł wnioskowania logiki algorytmicznej (rachunku programów), 

<math>A</math> - zbiór aksjomatów, jest zbiorem wszystkich formuł pierwszego rzędu prawdziwych w standardowym modelu liczb naturalnych. 

Czy formuła <math>\color{blue}\forall x\, \{y:=0;\, \mathbf{while}\ x\neq y\ \mathbf{do}\ y:=y+1\ \mathbf{done}\}(x=y) </math> jest twierdzeniem tej teorii?
--[[Użytkownik:AndrzejSalwicki|AndrzejSalwicki]] ([[Dyskusja użytkownika:AndrzejSalwicki|dyskusja]]) 15:34, 30 maj 2018 (CEST)
* Czy teoria <math>Th_{2.5}</math> jest zupełna?
--[[Użytkownik:AndrzejSalwicki|AndrzejSalwicki]] ([[Dyskusja użytkownika:AndrzejSalwicki|dyskusja]]) 19:09, 31 maj 2018 (CEST)
* Według Harela, zob. Dynamic Logic, każda formuła algorytmiczna prawdziwa w standardowym modelu arytmetyki powinna być twierdzeniem teorii <math>Th_{2.5}</math>

* Czy teoria kontenerów (tj. słowników, dictionaries) bez aksjomatu algorytmicznego jest zupełna?

[[Category:Logika Algorytmiczna}}]]

Logika Algorytmiczna

2026-02-25T12:35:51Z

AndrzejSalwicki:

''Felix qui potuit rerum cognoscere causas'' 
=Próba zmian
= Wprowadzenie =
Zmiana kontrolna Środa 21 maja 2025 g. 19:25
Logika algorytmiczna AL jest ''rachunkiem logicznym''. Nie jest to byle jaki system logiczny. Stworzony został przez nas jako narzedzie pomocne i niezbędne w pracy nad oprogramowaniem. 
Rachunek programów tj. logika algorytmiczna:
* uzupełnia język o programy,
* program jest wyrażeniem zbudowanym z programów atomowych - instrukcji przypisania przy pomocy kilku operatorów programotwócztch: while, if, złożenie,
* program może poprzedzać formułę i takie wyrażenie jest także formułą,

Rachunek programów AL umożliwia:
# Wyrażenie własności programu przez odpowiednio napisaną formułę języka systemu AL [[Wyrażalność semantycznych własności programów]]
# Przeprowadzanie dowodów formuł wyrażających ważne semantyczne własności programów, [[Przykłady dowodów]].
# Podanie aksjomatów dla wielu struktur danych. Aksjomaty takie wykluczają struktury niechciane, czy wręcz struktury patologiczne.[[Aksjomaty struktur]]
# Specyfikację oprogramowania, [[SpecVer]]
# Weryfikację oprogramowania względem ustalonej specyfikacji.
# Aksjomatyczny opis semantyki danego języka programowania.[[Aksjomatyczna definicja języka programowania]]
# i wiele innych rzeczy.
[[Plik:4logiki.jpg|thumb|center |750px| Rys. 1 Cztery systemy logiczne ]]
Powyższy rysunek 1 ilustruje relacje zachodzące pomiędzy tymi czterema rachunkami logicznymi. Strzałki wskazują na zachodzenie następującej relacji <math>\mathcal{L}\rightarrow\mathcal{L}'</math> pomiędzy dwoma rachunkami logicznymi <math>\mathcal{L}</math> i <math>\mathcal{L}'</math>: ''Każda tautologia'' <math>\alpha</math> ''rachunku'' <math>\mathcal{L}</math> ''staje się tautologią rachunku ''<math>\mathcal{L}</math>' ''po zastąpieniu atomów formuły'' <math>\alpha</math> ''przez formuły rachunku'' <math>\mathcal{L}</math>. Nieco więcej informacji uzyskamy porównując zbiory wyrażeń poprawnie zbudowanych <math>\mathcal{WFF} </math>. 
Języki tych rachunków logicznych różnią się. Każdy język jest parą <alfabet, zbiór wyrażen poprawnie zbudowanych>. Zwróćmy uwagę na to, że za każdym razem struktura zbioru wyrażeń poprawnie zbudowanych <math>\mathcal{WFF} </math> (''ang''. well formed formulas) jest inna. 
Oznaczenia przyjete na rysunku: <math>\mathcal{L}</math> - język, <math>\mathcal{A}</math> - alfabet, <math>\mathcal{T}</math> - zbiór termów (wyrażeń arytmetycznych, obiektowych,...), <math>\mathcal{F}</math> - zbiór formuł, <math>\mathcal{P}</math> - zbiór programów.
[[Plik:AxiomPL.jpg|thumb|750px| Rys. 2 Aksjomaty rachunku zdań ]]
[[Plik:axiomsFOL-AL.jpg|thumb |750px| Rys. 3 Aksjomaty rachunku predykatów(Ax12 i Ax13) i rachunku programów ]]
[[Plik:inferenceRules.jpg| thumb |750px| Rys. 4 Reguły wnioskowania ]]
Zbiór formuł logiki algorytmicznej zawiera w sobie wszystkie formuły pierwszego rzędu i ponadto, jest zamknięty ze względu na poprzedzanie formuły programem. Jeśli <math>\alpha</math> jest formułą i <math>K</math> jest programem to wyrazenie postaci <math>K\alpha</math> jest formułą logiki algorytmicznej, krócej, formułą algorytmiczna. 
Jak takiej formule <math>K\alpha</math> przypisać wartość logiczną prawda lub fałsz?
[[Plik:Kalfa.jpg |thumb|left|300px|Rys. 5 Wyznaczanie wartośći formuły <math>K\alpha</math> ]]
Rysunek 5 powinien wszystko wyjaśnić.Pozostaje jednak przypadek gdy obliczenie programu K nie daje wyniku, z powodu zapętlenia się programu lub innego błędu. Oczywiście nie możemy wtedy twierdzić, że ''dla danych v, obliczenie programu K kończy się pomyślnie i wyniki spełniają warunek <math>\alpha</math>''. A więc w tym przypadku wartościa formuły <math>K\alpha</math> jest fałsz. 

O logice algorytmicznej możemy też powiedzieć, że jest [[rachunek programów|''rachunkiem programów'']]. Język logiki algorytmicznej zawiera programy i formuły algorytmiczne. '''Ważne''' jest to, że ''każda semantyczna własność programów np. poprawność, równowazność, kończenie obliczeń lub przeciwnie zapętlanie, ... może być wyrażona przez odpowiednią formułę''. Pozwala to zamienić zadanie wykazania, że pewien program <math>P</math> posiada pewną własnośc semantyczną <math>S</math> na zadanie udowodnić formułę <math>\beta</math> należąca do języka logiki algorytmicznej. '''Przykład''' 
Własność: ''Dla każdych danych <math>v</math>, jeśli program <math>K</math> rozpoczyna obliczenia z danymi spełniającymi warunek <math>\alpha</math> to jego obliczenie zakończy się (nie będzie zapętlenia, ani przerwania obliczeń) i jego wyniki spełniają warunek <math>\beta</math>'', jest wyrażana formułą <math>\alpha \rightarrow K\beta</math>. Nie musimy więc podejmować trudu testowania czy dla kazdych danych obliczenie programu K będzie skończone i ... 

Formuły tworzą algebrę z działaniami: konkatenacji, alternatywy, negacji i implikacji oraz z działaniami nieskończonymi tj. kwantyfikatorami, ponadto programy są modalnościami. Programy też tworzą algebrę: działaniami tej algebry są iteracja, rozgałęzienie i złożenie programów. Mamy więc do czynienia ze splotem dwu algebr. Możemy go nazwać rachunkiem programów. Zadaniem logiki algorytmicznej jest poszukiwanie ''praw rachunku programów''.

Celem jest zebranie praw i reguł wnioskowania, które umożliwią analizę algorytmów i wydawanie opinii o ich własnościach semantycznych, bez wykonywania obliczeń, na podstawie samego tekstu algorytmu i aksjomatów struktury danych w jakiej dany program ma byc interpretowany.

'''Przykład'''
Rozpatrzmy prosty program
{| class="wikitable"
|-
| (* Dane: x>0 i y>0 liczby naturalne *)
'''Deklaracje:''' typ(x, y, n, m, r, q, max)='''N''' & typ(n_mniejsze)=Boolean

n:=x; m:=y;
'''while''' n ≠ m '''do'''
'''''Oznaczenie''''' niech l=max(n,m)
r:=0;
'''while''' r ≠n '''and''' r ≠m '''do''' r:=r+1 '''od''';
'''if''' r=n '''then''' n_miejsze:=true; max:=m '''else''' n_mniejsze:=false; max:=n '''fi''';
'''''Stwierdzenie''''' (n<m & m=max(n,m) lub m<n & n=max(n,m))
q:=0;
'''while''' r≠max '''do''' r:= r+1; q:=q+1 '''od''';
'''''Stwierdzenie''''' q = |m-n| & (1 ≤ q < max(n,m))& r=max(n,m)
'''if''' n_mniejsze '''then''' m:=q '''else''' n := q '''fi'''
'''''Stwierdzenie''''' max(n,m) < l
'''od''' ( wynik = n)
(* Wynik: nwd(x,y) *)
|}

Co robi ten program? Czy to jest pytanie dobrze postawione?
Czy obliczenie tego programu jest skończone dla każdych danych <math>n</math> i <math>m</math>?
Czym są te dane? Jakie znaczenie mają operacje - i + oraz stała 1? Jakie znaczenie ma predykat <?

Wiele osób powie,że przecież to proste. Powyższy program oblicza największy wspólny dzielnik liczb naturalnych <math>xP</math> i <math>y</math>. No tak, ale skąd wiesz, że środowisko w którym wykonujesz ten program nie jest podejrzane? Na kolejnej stronie możesz zobaczyć klasę która implementuje operacje dodawania liczb naturalnych i relację równości w niestandardowy sposób. Powyższy program w otoczeniu tej klasy zachowuje się niestandardowo. Po pierwsze, obliczenia tego programu sa nieskończone dla pewnych danych. Powiesz mi, ta klasa nie spełnia aksjomatów liczb naturalnych? Otóż '''spełnia'''. Jakie więc aksjomaty należy wziąć pod uwagę i o co mamy pytać?

Zanim zaczniesz analizować działanie programu powinieneś zdać sobie sprawę z kilku rzeczy:
# Program zachowuje się różnie w różnych otoczeniach. Czym jest otoczenie? To zależy, może to być pierwotny typ danych np. integer w wielu językach programowania lub struktura danych opisana za pomocą pewnej klasy.
# Podczas analizy powinniśmy rozpatrywać program <math>P</math> w parze z jego otoczeniem <math>E</math>. Podczas analizy nie wystarczy nam nazwa otoczenia, ani sygnatura nazywana przez programistów interfejsem (ang, ''interface'').
# W procesie analizy musimy korzystać z własności otoczenia np. z przemienności i łączności dodawania.
# Musimy też sobie zadawać sprawę, że wielu podstawowych własności nie da się wyrazić formułami pierwszego rzędu.
# '''Własności algorytmiczne naszych programów wynikają z własności algorytmicznych otoczenia.''' 

Zechciej przejść na stronę [[Euklides]] by poznać nasze argumenty.

== Program logiki algorytmicznej ==
Zadaniem logiki algorytmicznej jest dostarczenie narzędzi do analizowania semantycznych własności programów takich jak: własność stopu, poprawność programu, etc.
W języku logiki algorytmicznej znajdujemy trzy zbiory: zbiór formuł, zbiór wyrażeń (zbiór termów) i zbiór programów (zbiór algorytmów).
'''Uwaga''' W języku logiki zdaniowej (rachunku zdań) rozważany jest jeden tylko zbiór wyrażeń poprawnie zbudowanych, jest to zbiór formuł (zdaniowych). Formuły stanowią najmniejszy zbiór napisów zawierający zbiór zmiennych zdaniowych i zamknięty ze względu na operatory logiczne.
W jeżyku logiki pierwszego rzędu zb→ór wyrażen poprawnie zbudowanych jest suma dwu rozłącznych zbiorów: zbioru termów(inaczej zbiór wyrażen nazwowych) i zbioru formuł. W rachunku programów (czyli logice algorytmicznej) w naturalny sposób pojaia się zbiór algorytmów. '''koniec uwagi'''
Znaczeniem programu <math>P</math> jest funkcja ze zbioru <math>W</math> wartościowań zmiennych w ten sam zbiór. Zazwyczaj funkcję tę określa się przy pomocy pojęcia [[obliczenia programu]]. 
<math>
\begin{figure}[h]\begin{center}
\usepackage{tikz}
\tikzstyle{stan}=[rectangle , text=blue]
\tikzstyle{is}=[->,>=latex,rounded corners=4pt]
\begin{tikzpicture}[scale=0.38]
%\draw [gray, very thin] (-2,-2) grid [step=1cm] (28,50);
\draw (-2,5) -- (4,18) -- (27,18) -- (23,5) -- cycle[fill=green!25];
\node[stan] (T) at (4.44,14) {$v:\frac{x\, y\, z}{k\,l\,p}$};
\node[stan] (U) at (24,14) {$\frac{true}{false}$};
\node[stan] (V) at (14,6.2) {$v^{\prime}:\frac{x\, y\, z}{n\,l\,p}$};
\draw[is] (T) to[bend left]node[midway,below]{ $\bigl(\alpha(x/\tau)\bigr)_{\color{red}{\mathfrak{A}}\color{black}{}}$ } (U) ;
\draw[is] (T) to[bend right]node[midway,above ]{$\bigl(\{x:=\tau\}\alpha\bigr)_{\color{red}{\mathfrak{A}}\color{black}}$} (U) ;
\draw[is] (V) -- (U)node[midway,right]{$ \alpha(x)_{\color{red}{\mathfrak{A}}\color{black}{\ }}$ };
\draw[is] (T) -- (V)node[midway,left]{$\{x:=\tau \}_{\color{red}{\mathfrak{A}}\color{black}}$ };
\draw (0,20) -- (4,24) -- (27,24) -- (23,20) -- cycle[fill=yellow!35];

\node[stan] (T1) at (9,22) {$\{x:=\tau\}\alpha $ };
\node[stan] (U1) at (19,22) {$\alpha(x/\tau) $ };
\node[stan] (V1) at (14,22) {$\Leftrightarrow$ };

\draw [color=red, thick, ->] (9,22) -> (13,12.4)node[midway,left,near start]{$\mathfrak{A}$} ;
\draw [color=red, thick, ->] (19,22) -> (16,16.5)node[midway,left]{$\mathfrak{A}$} ;
\end{tikzpicture}
\caption{Aksjomat instrukcji przypisania \\
"\textit{warunek $\alpha(x)$ zachodzi po wykonaniu instrukcji $x\,:=\tau$ wttw, gdy przed wykonaniem tej instrukcji zachodzi warunek $\alpha(x/ \tau)$}"
jest tautologią\\
\begin{scriptsize}
na górnej płaszczyznie wydrukowaliśmy text aksjomatu, \\
na dolnej płaszczyznie objaśniamy co się dzieje podczas obliczeń i wskazujemy znaczenie (tj. semantykę) aksjomatu,
Litera $\mathfrak{A}$ oznacza dowolny typ (na razie przyjmij, że może to być typ integer lub typ real). Czerwone strzałki łączą formułę $\alpha(x/\tau) $ (odpowiednio \{x:=$\tau$\}$\alpha $) z funkcją $\alpha(x/\tau)_{\mathfrak{A}}$ (odpowiednio $\{x:=\tau \}(\alpha)_{\mathfrak{A}}$ ).
Stan pamięci $v'$ i dodatkowe strzałki ilustrują sposób obliczania wartości formuły, $\{x:=\tau \}(\alpha)$, zauważ, wartość $v'(x)=n= \tau_{\mathfrak{A}}( v(x))$.
\end{scriptsize}}\label{rAx18}
\end{center}
\end{figure}
</math>

== Zastosowania ==
Stosując logikę algorytmiczną czyli rachunek programów potrafimy odpowiedziec twierdząco na nastepujące pytania:
# Czy można podać aksjomaty i reguły wnioskowania, które opiszą semantykę operacyjną języka programowania?
# Czy (i jakie) własności struktur danych (systemów algebraicznych) są wyrażalne w języku logiki algorytmicznej?
# Czy (i jakie) własności programów są wyrażalne formułami algorytmicznymi? 

Ad 2. W matematyce rozważa się wiele własności ważnych struktur algebraicznych, których nie można wyrazić w języku pierwszego rzędu. Większość z nich może być wyrażona przy pomocy formuł algorytmicznych 

* bycie liczbą naturalną,
* aksjomat Archimedesa
* aksjomat ciał charakterystyki zero
* aksjomat grup torsyjnych
* aksjomat grup cyklicznych
i in. 
Dla informatyków niezwykle ważny jest fakt, że niemal wszystkie napotykane w programach struktury danych mogą być scharakteryzowane przy pomocy formuł algorytmicznych
* s jest stosem (skończonym)
* q jest kolejką FIFO skończoną
* s jest drzewem binarnym
* d jest drzewem binarnych poszukiwań
* q jest kolejką priorytetową
* d jest strukturą słownika (ang. dictionary)
* k jest kopcem
itd.
== Inne logiki programów ==
Możesz się zapytać jak się ma rachunek programów (tj. logika algorytmiczna) do innych logik programów : np. rachunek Floyda, logika Hoare'a, rachunek najsłabszego warunku wstępnego Dijkstry, logiki dynamicznaj, etc.?

[[calculus of Floyd|rachunek Floyda]] 

[[logic of Hoare|logika Hoare'a]] 

calculus of weakest precondition of Dijkstra 

[[dynamic logic]] 

== Uwagi historyczne ==
Algorytmy pojawiły sie kilka tysięcy lat temu. W Babilonie, Egipcie i Grecji. 

W czasach nowożytnych studia nad algorytmami podjęli Goedel, Turing, Church, Markov, Kołmogorov i wielu innych. Szkoda, że Tarski nie rozszerzył swych badań nad semantyką na funkcje obliczalne. Szkoda, że studia funkcji obliczalnych skupiły się na samych funkcjach, zaniedbując aspekt językowy. Prawie nie zajmowano się językiem służcym do definiowania funkcji rekurencyjnych. Alonzo Curch był chyba wyjatkiem? D. Kleene był blisko - jego definicja operatora minimum ograniczonego to przeciez petla FOR, a operacja minimum efektywnego to pętla WHILE. Warto pamietac twierdzenie S. Kleene z r. 1942 o tym, że zbiór funkcji obliczalnych jesli jest zamknięty ze względu na superpozycję i minimum efektywne ( i zawiera kilka funkcji poczatkowych) to definiowanie funkcji obliczalnych przez rekursję prostą może być zastąpione przez operację minimum efektywnego. 

Po drugiej wojnie światowej gdy pojawiły się komputery (zwane wtedy maszynami matematycznymi), ich programy zapisywano w kodzie maszynowym lub (później) w assemblerze. Trudno było dostrzec struktury i prawidłowości. W maszynie von Neumanna wszystko jest ciągiem bitów - liczbą. Ale pamiętam odczyt Antoniego Mazurkiewicza (ok 1960 r.) i jego dowód poprawności algorytmu z jedną pętla. Algorytm miał obliczyć sumę liczb zapisanych w tablicy. Kod maszyny XYZ-1 był bardzo ubogi. Program wymagał pobrania instrukcji "''weź kolejną komórkę pamięci do Akumulatora''" do rejestru Akumulator, zwiększenia adresu i zapisaniu tak zmienionej instrukcji w pamięci rozkazów na swoim pierwotnym miejscu. Program był więc ciągiem słów binarnych - każde słowo można jednak interpretować dwoiście, jako liczbę lub jako instrukcję. Nie ma w tym żadnej widocznej struktury. 

Prekursorzy logiki algorytmicznej 
Janov - jego praca poprzedza zdaniową logikę dynamiczną. Przedmiotem analizy są schematy programów (zapisywane w bardzo specjalny sposób) i relacja równoważności schematów. Dzisiaj powiedzielibyśmy, że schemat programu jest grafem skończonym. Wierzchołkom grafu przyporządkowano albo zmienną programowa albo formułę zdaniowa. Praca Janova jest nie tylko trudno dostępna, ale przede wszystkim mało czytelna. W książce A.P. Ershova można znaleźć przystępną ekspozycję teorii Janova. 
Engeler(1967) - zauważył, że własność stopu programu można wyrazić jako formułę logiki <math>L_{\omega1\,\omega} </math>, a dokładniej jako nieskończoną alternatywę formuł otwartych. 
Warto też wspomnieć o pracach Glushkova dotyczących systemów algebr algorytmicznych i książkę Helmuta Thielego. 
''Rasiowa'' - w książce ''Mathematics of metamathematics''(1963) str. 218 sformułowała podstawową własność instrukcji przypisania. Niech <math> s </math> oznacza jakieś odwzorowanie <math> s\colon V \to T </math> gdzie <math> V </math> jest zbiorem zmiennych indywiduowych, a <math> T </math> jest zbiorem termów. Odwzorowanie <math> s </math> nazywa się podstawieniem. Jeśli <math> \tau </math> oznacza jakiś term to <math> s\,\tau </math> oznacza wyrażenie powstające z termu <math> \tau </math> przez równoczesne zastąpienie wszystkich wystąpień zmiennych indywiduowych <math> \tau </math> przez odpowiednie wartości odwzorowania <math> s </math>. Oznaczmy term <math> \tau </math> przez <math> \tau(x_1,\dots,x_n)</math> podkreślając, że zmienne <math> x_1,\dots,x_n </math> to są wszystkie zmienne występujące w termie <math> \tau </math>. Wynik równoczesnego podstawienia za zmienne <math> x_1,\dots,x_n </math> występujące w termie <math> \tau </math>, termów <math> s(x_1),\dots,s(x_n) </math> oznaczmy <math> s\tau </math>. Mamy więc równość <math> s\tau(x_1,\dots,x_n)= \tau(s(x_1),\dots,s(x_n)) </math>. Można bez trudu udowodnić, że wynik jest tez termem.
Przypomnijmy teraz ten element definicji pojęcia spełniania (Tarski): dla ustalonej interpretacji symboli funkcyjnych <math> R </math> i ustalonego wartościowania zmiennych <math> v </math>, term <math> \tau </math> wyznacza funkcję ze zbioru wartościowań w zbiór wartoścowań.
Teraz możemy sformułować 
Niech <math> R </math> będzie dowolnie ustaloną interpretacją symboli funkcyjnych, niech <math> v </math> będzie dowolnym wartościowaniem zmiennych. Dla każdego podstawienia <math> s </math> i każdego termu <math> \tau </math> zachodzi równość
<math> s\tau_R(v)=\tau_R(s_R(v)) </math> 
Zauważmy, że w czasie pisania ksiązki ''Mathematics of metamathematics''(przed r. 1963) ani Rasiowa ani Sikorski nie mieli pojęcia o programowaniu. A jednak, gdy zapisać podstawienie <math> s </math> w trochę innej formie <math> \{x_1:=\tau_1 \& \dots \& x_n:=\tau_n \} </math> i zrozumieć, że wartościowanie zmiennych to to samo co stan pamięci, a interpretacja <math> R </math> to po prostu jednostka arytmetyczna komputera, to wszystko trafia na swoje miejsce.

== Bibliografia ==
Książki

# [AlgoLog] [[Media:Algorithmic_Logic.pdf | {{cytuj książkę |odn=tak| nazwisko = Mirkowska| imię = Grażyna | nazwisko2 = Salwicki | imię2 = Andrzej | tytuł = Algorithmic Logic | wydawca = PWN | miejsce = Warszawa | data = 1987 | strony = 345}}]]
# [LogProg1] [[Media:LogikaAlgorytmiczna_1z2.pdf | {{cytuj książkę | odn=tak |imię2=Andrzej | nazwisko2=Salwicki | imię=Grażyna | nazwisko=Mirkowska| tytuł=Logika Algorytmiczna dla Programistów|wydawca=WNT | miejsce=Warszawa| data=1992|strony=294 }}]] cz.1 
[[book Algorithmic Logic ]]
# [LogProg2] [[Media:LogikaAlgorytmiczna_2z2.pdf | {{cytuj książkę | odn=tak |imię2=Andrzej | nazwisko2=Salwicki | imię=Grażyna | nazwisko=Mirkowska| tytuł=Logika Algorytmiczna dla Programistów|wydawca=WNT | miejsce=Warszawa| data=1992|strony=294 }}]] cz.2
#[AL4software] [[Media:AlgoLogic.pdf| {{cytuj książkę | odn=tak |imię2=Andrzej | nazwisko2=Salwicki | imię=Grażyna | nazwisko=Mirkowska| tytuł=Algorithmic Logic for Software Construction and Verification|wydawca=Dąbrowa Research | miejsce=Dąbrowa Leśna| data=2014|strony=154 }}]]
# [CentrumBanachAL] [[ Media:bcp211.pdf |{{Cytuj książkę |odn=tak| nazwisko = Banachowski | imię = Lech | tytuł = An introduction to Algorithmic Logic - Metamathematical Investigations of Theory of Programs | wydawca = PWN | miejsce = Warszawa | data = 1977 | seria = Banach Center Publications | strony = 7-99 | isbn = 123 | nazwisko2 = Kreczmar | imię2 = Antoni | nazwisko3 = Mirkowska | imię3 = Grażyna | nazwisko4 = Rasiowa | imię4 = Helena | nazwisko5 = Salwicki | imię5 = Andrzej | tom = 2 | tytuł tomu = Banach Center Publications }}]]
# [HRAL] {{Cytuj książkę | odn=tak | nazwisko= Rasiowa | imię=Helena | tytuł= Algorithmic Logic - Notes from Seminar in Simon Fraser University | data=1975 | seria= Reports of Institute of Computer Science PAS | tom=281 | miejsce=Warsaw }}
# [AB] {{Cytuj książkę | odn=tak | nazwisko= Biela | imię=Andrzej | tytuł= Algorithmic structural completeness and a retrieval system for proving theorems in algorithmic theories | data=2000 | wydawca=Wydawnictwo Uniwersytetu Śląskiego | tom=1901 | miejsce=Katowice | strony=122 | url=http://lem12.uksw.edu.pl/images/4/40/A-Biela.pdf }}
Artykuły (wybór)
# [GMP] [[Media:GMP1970.pdf | {{cytuj pismo | odn=tak | nazwisko = Góraj | imię = Anna | nazwisko2= Mirkowska | imię2 = Grazyna | nazwisko3 = Paluszkiewicz | imię3 = Anna| tytuł = On the notion of description of program | czasopismo = Bull. Acad. Polon. Sci. Ser. Math. Astr. Phys.| rok= 1970 |strony = 499 - 505 }}]]
# [GM1971] {{cytuj pismo | odn=tak |nazwisko= Mirkowska | imię= Grażyna | tytuł = On Formalized Systems of Algorithmic Logic | czasopismo= Bull. Polish Academy Sciences, Ser. Math. Phys. |rok =1971 |tom = 19 | strony=421-428 |url=http://lem12.uksw.edu.pl/images/6/6f/On_Formalized-Mirk.pdf}}
# [GM1] [[Media:MirkowskaI-1-17.pdf| {{cytuj pismo | odn=tak | nazwisko= Mirkowska | imię = Grazyna | tytuł = Algorithmic logic and its applications in the theory of programs I | czasopismo = Fundamenta Informaticae| rok= 1977 |strony = 1-17 }} ]]
# [GM2] [[Media:Mirkowska-II-147-165.pdf| {{cytuj pismo | odn=tak | nazwisko= Mirkowska | imię = Grazyna | tytuł = Algorithmic logic and its applications in the theory of programs II | czasopismo = Fundamenta Informaticae| rok= 1977 |strony = 147-165 }} ]]
# [AS1] [[Media:FormalizedAlgorithmicLanguages.pdf | {{cytuj pismo | odn=tak | nazwisko= Salwicki | imię = Andrzej | tytuł = Formalized Algorithmic Languages | czasopismo = Bull. Acad. Polon. Sci. Ser. Math. Astr. Phys.| rok= 1970 |tom=18 |strony = 227-232 }} ]]
# [AS3] [[Media:CalculuswIterationQuantifiers.pdf | {{cytuj pismo | odn=tak | nazwisko= Salwicki | imię = Andrzej | tytuł = On the predicate calculi with iteration quantifiers | czasopismo = Bull. Acad. Polon. Sci. Ser. Math. Astr. Phys.| rok= 1970 |tom=18 |strony = 279-285 }} ]]
# [LB1] [[Media:BanI-93-119.pdf| {{cytuj pismo | odn=tak | nazwisko= Banachowski | imię = Lech | tytuł = Investigations of Properties of Programs by means of Extended Algorithmic Logic I | czasopismo = Fundamenta Informaticae| rok= 1977 |strony = 93-119 }} ]]
# [LB2] [[Media:Banachowski-II-167-193.pdf| {{cytuj pismo | odn=tak | nazwisko= Banachowski | imię = Lech | tytuł = Investigations of Properties of Programs by means of Extended Algorithmic Logic II | czasopismo = Fundamenta Informaticae| rok= 1977 |strony = 167-193 }} ]]
# [LB3] [[Media:BanachowskiDataStruct.pdf| {{cytuj pismo | odn=tak | nazwisko= Banachowski | imię = Lech | tytuł = An Axiomatic Approach to the Theory of Data Structures | czasopismo = Bull. Acad. Polon. Sci. Ser. Math. Astr. Phys. | rok= 1975 |strony = 315-323 }} ]]
# [AK1] [[Media:Kreczmar-Program-Fields.pdf| {{Cytuj pismo |odn=a | imię=Antoni | nazwisko=Kreczmar |tytuł=Programmability in Fields |czasopismo=Fundamenta Informaticae |strony=195-230 |rok=1977}}]]
# [AK2] [[Media:Kreczmar-Efficiency-problems.pdf| {{Cytuj pismo |odn=b | imię=Antoni | nazwisko=Kreczmar |tytuł=Effectivity problems of Algorithmic Logic |czasopismo=Fundamenta Informaticae |strony=19-32 |rok=1977}}]]
# [MSS2009] [[Media:Verifying-a-class.pdf |{{cytuj pismo| odn=tak| nazwisko=Mirkowska| imię=Grażyna| nazwisko2=Salwicki| imię2=Andrzej| nazwisko3=Świda| imię3=Oskar| tytuł=Verifying a Class: combining Testing and Proving|czasopismo=Fundamenta Informaticae| strony= 305-324 |rok= 2009 }}]]
# [AS2017] [[Media:On-Euclids-algorithm-2018.pdf | {{Cytuj pismo| odn=nie| nazwisko=Salwicki| imię=Andrzej| tytuł=A new proof of Euclid's algorithm | czasopismo= }}]]
# [WD1] [[ Media:WDnonprog.pdf | {{Cytuj pismo | odn=nie| nazwisko= Dańko | imię=Wiktor | tytuł=Nonprogrammable function defined by a procedure }} ]]

==Protokół rozbieżności==
Następujący tekst został złożony do druku
[[Media:On-Euclids-algorithm-2018.pdf | {{Cytuj pismo| odn=nie| nazwisko=Salwicki| imię=Andrzej| tytuł=A new proof of Euclid's algorithm | czasopismo= }}]] 

Pierwsza recenzja była rzeczowa, pomocna i jej sugestie zostały, z podziękowaniem, wykorzystane http://lem12.uksw.edu.pl/images/8/8c/1pierwszaRec.pdf. 

Drugi recenzent przedstawił następującą opinię http://lem12.uksw.edu.pl/images/0/0b/Second-report-08.pdf. 

Na to autor odpowiedział prosząc o referencje do zapowiadanych twierdzeń lub o przedstawienie dowodu. 

Oto protokół rozbieżności:
http://lem12.uksw.edu.pl/images/9/9a/DiscrepancyReport.pdf

==Pytania otwarte==
* Rozpatrzmy teorię algorytmiczną <math>Th_{2.5} = \langle L,C,A \rangle </math> gdzie
<math>L</math> - język, jest językiem struktury liczb naturalnych, algorytmicznym, 

<math>C</math> - operacja konskwencji jest wyznaczona przez zbiór aksjomatów i reguł wnioskowania logiki algorytmicznej (rachunku programów), 

<math>A</math> - zbiór aksjomatów, jest zbiorem wszystkich formuł pierwszego rzędu prawdziwych w standardowym modelu liczb naturalnych. 

Czy formuła <math>\color{blue}\forall x\, \{y:=0;\, \mathbf{while}\ x\neq y\ \mathbf{do}\ y:=y+1\ \mathbf{done}\}(x=y) </math> jest twierdzeniem tej teorii?
--[[Użytkownik:AndrzejSalwicki|AndrzejSalwicki]] ([[Dyskusja użytkownika:AndrzejSalwicki|dyskusja]]) 15:34, 30 maj 2018 (CEST)
* Czy teoria <math>Th_{2.5}</math> jest zupełna?
--[[Użytkownik:AndrzejSalwicki|AndrzejSalwicki]] ([[Dyskusja użytkownika:AndrzejSalwicki|dyskusja]]) 19:09, 31 maj 2018 (CEST)
* Według Harela, zob. Dynamic Logic, każda formuła algorytmiczna prawdziwa w standardowym modelu arytmetyki powinna być twierdzeniem teorii <math>Th_{2.5}</math>

* Czy teoria kontenerów (tj. słowników, dictionaries) bez aksjomatu algorytmicznego jest zupełna?

[[Category:Logika Algorytmiczna}}]]

Logika Algorytmiczna

2026-02-25T12:34:11Z

AndrzejSalwicki: /* Program logiki algorytmicznej */

''Felix qui potuit rerum cognoscere causas'' 
=Próba zmian
= Wprowadzenie =
Zmiana kontrolna Środa 21 maja 2025 g. 19:25
Logika algorytmiczna AL jest ''rachunkiem logicznym''. Nie jest to byle jaki system logiczny. Stworzony został przez nas jako narzedzie pomocne i niezbędne w pracy nad oprogramowaniem. 
Rachunek programów tj. logika algorytmiczna:
* uzupełnia język o programy,
* program jest wyrażeniem zbudowanym z programów atomowych - instrukcji przypisania przy pomocy kilku operatorów programotwócztch: while, if, złożenie,
* program może poprzedzać formułę i takie wyrażenie jest także formułą,

Rachunek programów AL umożliwia:
# Wyrażenie własności programu przez odpowiednio napisaną formułę języka systemu AL [[Wyrażalność semantycznych własności programów]]
# Przeprowadzanie dowodów formuł wyrażających ważne semantyczne własności programów, [[Przykłady dowodów]].
# Podanie aksjomatów dla wielu struktur danych. Aksjomaty takie wykluczają struktury niechciane, czy wręcz struktury patologiczne.[[Aksjomaty struktur]]
# Specyfikację oprogramowania, [[SpecVer]]
# Weryfikację oprogramowania względem ustalonej specyfikacji.
# Aksjomatyczny opis semantyki danego języka programowania.[[Aksjomatyczna definicja języka programowania]]
# i wiele innych rzeczy.
[[Plik:4logiki.jpg|thumb|center |750px| Rys. 1 Cztery systemy logiczne ]]
Powyższy rysunek 1 ilustruje relacje zachodzące pomiędzy tymi czterema rachunkami logicznymi. Strzałki wskazują na zachodzenie następującej relacji <math>\mathcal{L}\rightarrow\mathcal{L}'</math> pomiędzy dwoma rachunkami logicznymi <math>\mathcal{L}</math> i <math>\mathcal{L}'</math>: ''Każda tautologia'' <math>\alpha</math> ''rachunku'' <math>\mathcal{L}</math> ''staje się tautologią rachunku ''<math>\mathcal{L}</math>' ''po zastąpieniu atomów formuły'' <math>\alpha</math> ''przez formuły rachunku'' <math>\mathcal{L}</math>. Nieco więcej informacji uzyskamy porównując zbiory wyrażeń poprawnie zbudowanych <math>\mathcal{WFF} </math>. 
Języki tych rachunków logicznych różnią się. Każdy język jest parą <alfabet, zbiór wyrażen poprawnie zbudowanych>. Zwróćmy uwagę na to, że za każdym razem struktura zbioru wyrażeń poprawnie zbudowanych <math>\mathcal{WFF} </math> (''ang''. well formed formulas) jest inna. 
Oznaczenia przyjete na rysunku: <math>\mathcal{L}</math> - język, <math>\mathcal{A}</math> - alfabet, <math>\mathcal{T}</math> - zbiór termów (wyrażeń arytmetycznych, obiektowych,...), <math>\mathcal{F}</math> - zbiór formuł, <math>\mathcal{P}</math> - zbiór programów.
[[Plik:AxiomPL.jpg|thumb|750px| Rys. 2 Aksjomaty rachunku zdań ]]
[[Plik:axiomsFOL-AL.jpg|thumb |750px| Rys. 3 Aksjomaty rachunku predykatów(Ax12 i Ax13) i rachunku programów ]]
[[Plik:inferenceRules.jpg| thumb |750px| Rys. 4 Reguły wnioskowania ]]
Zbiór formuł logiki algorytmicznej zawiera w sobie wszystkie formuły pierwszego rzędu i ponadto, jest zamknięty ze względu na poprzedzanie formuły programem. Jeśli <math>\alpha</math> jest formułą i <math>K</math> jest programem to wyrazenie postaci <math>K\alpha</math> jest formułą logiki algorytmicznej, krócej, formułą algorytmiczna. 
Jak takiej formule <math>K\alpha</math> przypisać wartość logiczną prawda lub fałsz?
[[Plik:Kalfa.jpg |thumb|left|300px|Rys. 5 Wyznaczanie wartośći formuły <math>K\alpha</math> ]]
Rysunek 5 powinien wszystko wyjaśnić.Pozostaje jednak przypadek gdy obliczenie programu K nie daje wyniku, z powodu zapętlenia się programu lub innego błędu. Oczywiście nie możemy wtedy twierdzić, że ''dla danych v, obliczenie programu K kończy się pomyślnie i wyniki spełniają warunek <math>\alpha</math>''. A więc w tym przypadku wartościa formuły <math>K\alpha</math> jest fałsz. 

O logice algorytmicznej możemy też powiedzieć, że jest [[rachunek programów|''rachunkiem programów'']]. Język logiki algorytmicznej zawiera programy i formuły algorytmiczne. '''Ważne''' jest to, że ''każda semantyczna własność programów np. poprawność, równowazność, kończenie obliczeń lub przeciwnie zapętlanie, ... może być wyrażona przez odpowiednią formułę''. Pozwala to zamienić zadanie wykazania, że pewien program <math>P</math> posiada pewną własnośc semantyczną <math>S</math> na zadanie udowodnić formułę <math>\beta</math> należąca do języka logiki algorytmicznej. '''Przykład''' 
Własność: ''Dla każdych danych <math>v</math>, jeśli program <math>K</math> rozpoczyna obliczenia z danymi spełniającymi warunek <math>\alpha</math> to jego obliczenie zakończy się (nie będzie zapętlenia, ani przerwania obliczeń) i jego wyniki spełniają warunek <math>\beta</math>'', jest wyrażana formułą <math>\alpha \rightarrow K\beta</math>. Nie musimy więc podejmować trudu testowania czy dla kazdych danych obliczenie programu K będzie skończone i ... 

Formuły tworzą algebrę z działaniami: konkatenacji, alternatywy, negacji i implikacji oraz z działaniami nieskończonymi tj. kwantyfikatorami, ponadto programy są modalnościami. Programy też tworzą algebrę: działaniami tej algebry są iteracja, rozgałęzienie i złożenie programów. Mamy więc do czynienia ze splotem dwu algebr. Możemy go nazwać rachunkiem programów. Zadaniem logiki algorytmicznej jest poszukiwanie ''praw rachunku programów''.

Celem jest zebranie praw i reguł wnioskowania, które umożliwią analizę algorytmów i wydawanie opinii o ich własnościach semantycznych, bez wykonywania obliczeń, na podstawie samego tekstu algorytmu i aksjomatów struktury danych w jakiej dany program ma byc interpretowany.

'''Przykład'''
Rozpatrzmy prosty program
{| class="wikitable"
|-
| (* Dane: x>0 i y>0 liczby naturalne *)
'''Deklaracje:''' typ(x, y, n, m, r, q, max)='''N''' & typ(n_mniejsze)=Boolean

n:=x; m:=y;
'''while''' n ≠ m '''do'''
'''''Oznaczenie''''' niech l=max(n,m)
r:=0;
'''while''' r ≠n '''and''' r ≠m '''do''' r:=r+1 '''od''';
'''if''' r=n '''then''' n_miejsze:=true; max:=m '''else''' n_mniejsze:=false; max:=n '''fi''';
'''''Stwierdzenie''''' (n<m & m=max(n,m) lub m<n & n=max(n,m))
q:=0;
'''while''' r≠max '''do''' r:= r+1; q:=q+1 '''od''';
'''''Stwierdzenie''''' q = |m-n| & (1 ≤ q < max(n,m))& r=max(n,m)
'''if''' n_mniejsze '''then''' m:=q '''else''' n := q '''fi'''
'''''Stwierdzenie''''' max(n,m) < l
'''od''' ( wynik = n)
(* Wynik: nwd(x,y) *)
|}

Co robi ten program? Czy to jest pytanie dobrze postawione?
Czy obliczenie tego programu jest skończone dla każdych danych <math>n</math> i <math>m</math>?
Czym są te dane? Jakie znaczenie mają operacje - i + oraz stała 1? Jakie znaczenie ma predykat <?

Wiele osób powie,że przecież to proste. Powyższy program oblicza największy wspólny dzielnik liczb naturalnych <math>xP</math> i <math>y</math>. No tak, ale skąd wiesz, że środowisko w którym wykonujesz ten program nie jest podejrzane? Na kolejnej stronie możesz zobaczyć klasę która implementuje operacje dodawania liczb naturalnych i relację równości w niestandardowy sposób. Powyższy program w otoczeniu tej klasy zachowuje się niestandardowo. Po pierwsze, obliczenia tego programu sa nieskończone dla pewnych danych. Powiesz mi, ta klasa nie spełnia aksjomatów liczb naturalnych? Otóż '''spełnia'''. Jakie więc aksjomaty należy wziąć pod uwagę i o co mamy pytać?

Zanim zaczniesz analizować działanie programu powinieneś zdać sobie sprawę z kilku rzeczy:
# Program zachowuje się różnie w różnych otoczeniach. Czym jest otoczenie? To zależy, może to być pierwotny typ danych np. integer w wielu językach programowania lub struktura danych opisana za pomocą pewnej klasy.
# Podczas analizy powinniśmy rozpatrywać program <math>P</math> w parze z jego otoczeniem <math>E</math>. Podczas analizy nie wystarczy nam nazwa otoczenia, ani sygnatura nazywana przez programistów interfejsem (ang, ''interface'').
# W procesie analizy musimy korzystać z własności otoczenia np. z przemienności i łączności dodawania.
# Musimy też sobie zadawać sprawę, że wielu podstawowych własności nie da się wyrazić formułami pierwszego rzędu.
# '''Własności algorytmiczne naszych programów wynikają z własności algorytmicznych otoczenia.''' 

Zechciej przejść na stronę [[Euklides]] by poznać nasze argumenty.

== Program logiki algorytmicznej ==
Zadaniem logiki algorytmicznej jest dostarczenie narzędzi do analizowania semantycznych własności programów takich jak: własność stopu, poprawność programu, etc.
W języku logiki algorytmicznej znajdujemy trzy zbiory: zbiór formuł, zbiór wyrażeń (zbiór termów) i zbiór programów (zbiór algorytmów).
'''Uwaga''' W języku logiki zdaniowej (rachunku zdań) rozważany jest jeden tylko zbiór wyrażeń poprawnie zbudowanych, jest to zbiór formuł (zdaniowych). Formuły stanowią najmniejszy zbiór napisów zawierający zbiór zmiennych zdaniowych i zamknięty ze względu na operatory logiczne.
W jeżyku logiki pierwszego rzędu zb→ór wyrażen poprawnie zbudowanych jest suma dwu rozłącznych zbiorów: zbioru termów(inaczej zbiór wyrażen nazwowych) i zbioru formuł. W rachunku programów (czyli logice algorytmicznej) w naturalny sposób pojaia się zbiór algorytmów. '''koniec uwagi'''
Znaczeniem programu <math>P</math> jest funkcja ze zbioru <math>W</math> wartościowań zmiennych w ten sam zbiór. Zazwyczaj funkcję tę określa się przy pomocy pojęcia [[obliczenia programu]]. 
<math>
\begin{figure}[h]\begin{center}
\tikzstyle{stan}=[rectangle , text=blue]
\tikzstyle{is}=[->,>=latex,rounded corners=4pt]
\begin{tikzpicture}[scale=0.38]
%\draw [gray, very thin] (-2,-2) grid [step=1cm] (28,50);
\draw (-2,5) -- (4,18) -- (27,18) -- (23,5) -- cycle[fill=green!25];
\node[stan] (T) at (4.44,14) {$v:\frac{x\, y\, z}{k\,l\,p}$};
\node[stan] (U) at (24,14) {$\frac{true}{false}$};
\node[stan] (V) at (14,6.2) {$v^{\prime}:\frac{x\, y\, z}{n\,l\,p}$};
\draw[is] (T) to[bend left]node[midway,below]{ $\bigl(\alpha(x/\tau)\bigr)_{\color{red}{\mathfrak{A}}\color{black}{}}$ } (U) ;
\draw[is] (T) to[bend right]node[midway,above ]{$\bigl(\{x:=\tau\}\alpha\bigr)_{\color{red}{\mathfrak{A}}\color{black}}$} (U) ;
\draw[is] (V) -- (U)node[midway,right]{$ \alpha(x)_{\color{red}{\mathfrak{A}}\color{black}{\ }}$ };
\draw[is] (T) -- (V)node[midway,left]{$\{x:=\tau \}_{\color{red}{\mathfrak{A}}\color{black}}$ };
\draw (0,20) -- (4,24) -- (27,24) -- (23,20) -- cycle[fill=yellow!35];

\node[stan] (T1) at (9,22) {$\{x:=\tau\}\alpha $ };
\node[stan] (U1) at (19,22) {$\alpha(x/\tau) $ };
\node[stan] (V1) at (14,22) {$\Leftrightarrow$ };

\draw [color=red, thick, ->] (9,22) -> (13,12.4)node[midway,left,near start]{$\mathfrak{A}$} ;
\draw [color=red, thick, ->] (19,22) -> (16,16.5)node[midway,left]{$\mathfrak{A}$} ;
\end{tikzpicture}
\caption{Aksjomat instrukcji przypisania \\
"\textit{warunek $\alpha(x)$ zachodzi po wykonaniu instrukcji $x\,:=\tau$ wttw, gdy przed wykonaniem tej instrukcji zachodzi warunek $\alpha(x/ \tau)$}"
jest tautologią\\
\begin{scriptsize}
na górnej płaszczyznie wydrukowaliśmy text aksjomatu, \\
na dolnej płaszczyznie objaśniamy co się dzieje podczas obliczeń i wskazujemy znaczenie (tj. semantykę) aksjomatu,
Litera $\mathfrak{A}$ oznacza dowolny typ (na razie przyjmij, że może to być typ integer lub typ real). Czerwone strzałki łączą formułę $\alpha(x/\tau) $ (odpowiednio \{x:=$\tau$\}$\alpha $) z funkcją $\alpha(x/\tau)_{\mathfrak{A}}$ (odpowiednio $\{x:=\tau \}(\alpha)_{\mathfrak{A}}$ ).
Stan pamięci $v'$ i dodatkowe strzałki ilustrują sposób obliczania wartości formuły, $\{x:=\tau \}(\alpha)$, zauważ, wartość $v'(x)=n= \tau_{\mathfrak{A}}( v(x))$.
\end{scriptsize}}\label{rAx18}
\end{center}
\end{figure}
</math>

== Zastosowania ==
Stosując logikę algorytmiczną czyli rachunek programów potrafimy odpowiedziec twierdząco na nastepujące pytania:
# Czy można podać aksjomaty i reguły wnioskowania, które opiszą semantykę operacyjną języka programowania?
# Czy (i jakie) własności struktur danych (systemów algebraicznych) są wyrażalne w języku logiki algorytmicznej?
# Czy (i jakie) własności programów są wyrażalne formułami algorytmicznymi? 

Ad 2. W matematyce rozważa się wiele własności ważnych struktur algebraicznych, których nie można wyrazić w języku pierwszego rzędu. Większość z nich może być wyrażona przy pomocy formuł algorytmicznych 

* bycie liczbą naturalną,
* aksjomat Archimedesa
* aksjomat ciał charakterystyki zero
* aksjomat grup torsyjnych
* aksjomat grup cyklicznych
i in. 
Dla informatyków niezwykle ważny jest fakt, że niemal wszystkie napotykane w programach struktury danych mogą być scharakteryzowane przy pomocy formuł algorytmicznych
* s jest stosem (skończonym)
* q jest kolejką FIFO skończoną
* s jest drzewem binarnym
* d jest drzewem binarnych poszukiwań
* q jest kolejką priorytetową
* d jest strukturą słownika (ang. dictionary)
* k jest kopcem
itd.
== Inne logiki programów ==
Możesz się zapytać jak się ma rachunek programów (tj. logika algorytmiczna) do innych logik programów : np. rachunek Floyda, logika Hoare'a, rachunek najsłabszego warunku wstępnego Dijkstry, logiki dynamicznaj, etc.?

[[calculus of Floyd|rachunek Floyda]] 

[[logic of Hoare|logika Hoare'a]] 

calculus of weakest precondition of Dijkstra 

[[dynamic logic]] 

== Uwagi historyczne ==
Algorytmy pojawiły sie kilka tysięcy lat temu. W Babilonie, Egipcie i Grecji. 

W czasach nowożytnych studia nad algorytmami podjęli Goedel, Turing, Church, Markov, Kołmogorov i wielu innych. Szkoda, że Tarski nie rozszerzył swych badań nad semantyką na funkcje obliczalne. Szkoda, że studia funkcji obliczalnych skupiły się na samych funkcjach, zaniedbując aspekt językowy. Prawie nie zajmowano się językiem służcym do definiowania funkcji rekurencyjnych. Alonzo Curch był chyba wyjatkiem? D. Kleene był blisko - jego definicja operatora minimum ograniczonego to przeciez petla FOR, a operacja minimum efektywnego to pętla WHILE. Warto pamietac twierdzenie S. Kleene z r. 1942 o tym, że zbiór funkcji obliczalnych jesli jest zamknięty ze względu na superpozycję i minimum efektywne ( i zawiera kilka funkcji poczatkowych) to definiowanie funkcji obliczalnych przez rekursję prostą może być zastąpione przez operację minimum efektywnego. 

Po drugiej wojnie światowej gdy pojawiły się komputery (zwane wtedy maszynami matematycznymi), ich programy zapisywano w kodzie maszynowym lub (później) w assemblerze. Trudno było dostrzec struktury i prawidłowości. W maszynie von Neumanna wszystko jest ciągiem bitów - liczbą. Ale pamiętam odczyt Antoniego Mazurkiewicza (ok 1960 r.) i jego dowód poprawności algorytmu z jedną pętla. Algorytm miał obliczyć sumę liczb zapisanych w tablicy. Kod maszyny XYZ-1 był bardzo ubogi. Program wymagał pobrania instrukcji "''weź kolejną komórkę pamięci do Akumulatora''" do rejestru Akumulator, zwiększenia adresu i zapisaniu tak zmienionej instrukcji w pamięci rozkazów na swoim pierwotnym miejscu. Program był więc ciągiem słów binarnych - każde słowo można jednak interpretować dwoiście, jako liczbę lub jako instrukcję. Nie ma w tym żadnej widocznej struktury. 

Prekursorzy logiki algorytmicznej 
Janov - jego praca poprzedza zdaniową logikę dynamiczną. Przedmiotem analizy są schematy programów (zapisywane w bardzo specjalny sposób) i relacja równoważności schematów. Dzisiaj powiedzielibyśmy, że schemat programu jest grafem skończonym. Wierzchołkom grafu przyporządkowano albo zmienną programowa albo formułę zdaniowa. Praca Janova jest nie tylko trudno dostępna, ale przede wszystkim mało czytelna. W książce A.P. Ershova można znaleźć przystępną ekspozycję teorii Janova. 
Engeler(1967) - zauważył, że własność stopu programu można wyrazić jako formułę logiki <math>L_{\omega1\,\omega} </math>, a dokładniej jako nieskończoną alternatywę formuł otwartych. 
Warto też wspomnieć o pracach Glushkova dotyczących systemów algebr algorytmicznych i książkę Helmuta Thielego. 
''Rasiowa'' - w książce ''Mathematics of metamathematics''(1963) str. 218 sformułowała podstawową własność instrukcji przypisania. Niech <math> s </math> oznacza jakieś odwzorowanie <math> s\colon V \to T </math> gdzie <math> V </math> jest zbiorem zmiennych indywiduowych, a <math> T </math> jest zbiorem termów. Odwzorowanie <math> s </math> nazywa się podstawieniem. Jeśli <math> \tau </math> oznacza jakiś term to <math> s\,\tau </math> oznacza wyrażenie powstające z termu <math> \tau </math> przez równoczesne zastąpienie wszystkich wystąpień zmiennych indywiduowych <math> \tau </math> przez odpowiednie wartości odwzorowania <math> s </math>. Oznaczmy term <math> \tau </math> przez <math> \tau(x_1,\dots,x_n)</math> podkreślając, że zmienne <math> x_1,\dots,x_n </math> to są wszystkie zmienne występujące w termie <math> \tau </math>. Wynik równoczesnego podstawienia za zmienne <math> x_1,\dots,x_n </math> występujące w termie <math> \tau </math>, termów <math> s(x_1),\dots,s(x_n) </math> oznaczmy <math> s\tau </math>. Mamy więc równość <math> s\tau(x_1,\dots,x_n)= \tau(s(x_1),\dots,s(x_n)) </math>. Można bez trudu udowodnić, że wynik jest tez termem.
Przypomnijmy teraz ten element definicji pojęcia spełniania (Tarski): dla ustalonej interpretacji symboli funkcyjnych <math> R </math> i ustalonego wartościowania zmiennych <math> v </math>, term <math> \tau </math> wyznacza funkcję ze zbioru wartościowań w zbiór wartoścowań.
Teraz możemy sformułować 
Niech <math> R </math> będzie dowolnie ustaloną interpretacją symboli funkcyjnych, niech <math> v </math> będzie dowolnym wartościowaniem zmiennych. Dla każdego podstawienia <math> s </math> i każdego termu <math> \tau </math> zachodzi równość
<math> s\tau_R(v)=\tau_R(s_R(v)) </math> 
Zauważmy, że w czasie pisania ksiązki ''Mathematics of metamathematics''(przed r. 1963) ani Rasiowa ani Sikorski nie mieli pojęcia o programowaniu. A jednak, gdy zapisać podstawienie <math> s </math> w trochę innej formie <math> \{x_1:=\tau_1 \& \dots \& x_n:=\tau_n \} </math> i zrozumieć, że wartościowanie zmiennych to to samo co stan pamięci, a interpretacja <math> R </math> to po prostu jednostka arytmetyczna komputera, to wszystko trafia na swoje miejsce.

== Bibliografia ==
Książki

# [AlgoLog] [[Media:Algorithmic_Logic.pdf | {{cytuj książkę |odn=tak| nazwisko = Mirkowska| imię = Grażyna | nazwisko2 = Salwicki | imię2 = Andrzej | tytuł = Algorithmic Logic | wydawca = PWN | miejsce = Warszawa | data = 1987 | strony = 345}}]]
# [LogProg1] [[Media:LogikaAlgorytmiczna_1z2.pdf | {{cytuj książkę | odn=tak |imię2=Andrzej | nazwisko2=Salwicki | imię=Grażyna | nazwisko=Mirkowska| tytuł=Logika Algorytmiczna dla Programistów|wydawca=WNT | miejsce=Warszawa| data=1992|strony=294 }}]] cz.1 
[[book Algorithmic Logic ]]
# [LogProg2] [[Media:LogikaAlgorytmiczna_2z2.pdf | {{cytuj książkę | odn=tak |imię2=Andrzej | nazwisko2=Salwicki | imię=Grażyna | nazwisko=Mirkowska| tytuł=Logika Algorytmiczna dla Programistów|wydawca=WNT | miejsce=Warszawa| data=1992|strony=294 }}]] cz.2
#[AL4software] [[Media:AlgoLogic.pdf| {{cytuj książkę | odn=tak |imię2=Andrzej | nazwisko2=Salwicki | imię=Grażyna | nazwisko=Mirkowska| tytuł=Algorithmic Logic for Software Construction and Verification|wydawca=Dąbrowa Research | miejsce=Dąbrowa Leśna| data=2014|strony=154 }}]]
# [CentrumBanachAL] [[ Media:bcp211.pdf |{{Cytuj książkę |odn=tak| nazwisko = Banachowski | imię = Lech | tytuł = An introduction to Algorithmic Logic - Metamathematical Investigations of Theory of Programs | wydawca = PWN | miejsce = Warszawa | data = 1977 | seria = Banach Center Publications | strony = 7-99 | isbn = 123 | nazwisko2 = Kreczmar | imię2 = Antoni | nazwisko3 = Mirkowska | imię3 = Grażyna | nazwisko4 = Rasiowa | imię4 = Helena | nazwisko5 = Salwicki | imię5 = Andrzej | tom = 2 | tytuł tomu = Banach Center Publications }}]]
# [HRAL] {{Cytuj książkę | odn=tak | nazwisko= Rasiowa | imię=Helena | tytuł= Algorithmic Logic - Notes from Seminar in Simon Fraser University | data=1975 | seria= Reports of Institute of Computer Science PAS | tom=281 | miejsce=Warsaw }}
# [AB] {{Cytuj książkę | odn=tak | nazwisko= Biela | imię=Andrzej | tytuł= Algorithmic structural completeness and a retrieval system for proving theorems in algorithmic theories | data=2000 | wydawca=Wydawnictwo Uniwersytetu Śląskiego | tom=1901 | miejsce=Katowice | strony=122 | url=http://lem12.uksw.edu.pl/images/4/40/A-Biela.pdf }}
Artykuły (wybór)
# [GMP] [[Media:GMP1970.pdf | {{cytuj pismo | odn=tak | nazwisko = Góraj | imię = Anna | nazwisko2= Mirkowska | imię2 = Grazyna | nazwisko3 = Paluszkiewicz | imię3 = Anna| tytuł = On the notion of description of program | czasopismo = Bull. Acad. Polon. Sci. Ser. Math. Astr. Phys.| rok= 1970 |strony = 499 - 505 }}]]
# [GM1971] {{cytuj pismo | odn=tak |nazwisko= Mirkowska | imię= Grażyna | tytuł = On Formalized Systems of Algorithmic Logic | czasopismo= Bull. Polish Academy Sciences, Ser. Math. Phys. |rok =1971 |tom = 19 | strony=421-428 |url=http://lem12.uksw.edu.pl/images/6/6f/On_Formalized-Mirk.pdf}}
# [GM1] [[Media:MirkowskaI-1-17.pdf| {{cytuj pismo | odn=tak | nazwisko= Mirkowska | imię = Grazyna | tytuł = Algorithmic logic and its applications in the theory of programs I | czasopismo = Fundamenta Informaticae| rok= 1977 |strony = 1-17 }} ]]
# [GM2] [[Media:Mirkowska-II-147-165.pdf| {{cytuj pismo | odn=tak | nazwisko= Mirkowska | imię = Grazyna | tytuł = Algorithmic logic and its applications in the theory of programs II | czasopismo = Fundamenta Informaticae| rok= 1977 |strony = 147-165 }} ]]
# [AS1] [[Media:FormalizedAlgorithmicLanguages.pdf | {{cytuj pismo | odn=tak | nazwisko= Salwicki | imię = Andrzej | tytuł = Formalized Algorithmic Languages | czasopismo = Bull. Acad. Polon. Sci. Ser. Math. Astr. Phys.| rok= 1970 |tom=18 |strony = 227-232 }} ]]
# [AS3] [[Media:CalculuswIterationQuantifiers.pdf | {{cytuj pismo | odn=tak | nazwisko= Salwicki | imię = Andrzej | tytuł = On the predicate calculi with iteration quantifiers | czasopismo = Bull. Acad. Polon. Sci. Ser. Math. Astr. Phys.| rok= 1970 |tom=18 |strony = 279-285 }} ]]
# [LB1] [[Media:BanI-93-119.pdf| {{cytuj pismo | odn=tak | nazwisko= Banachowski | imię = Lech | tytuł = Investigations of Properties of Programs by means of Extended Algorithmic Logic I | czasopismo = Fundamenta Informaticae| rok= 1977 |strony = 93-119 }} ]]
# [LB2] [[Media:Banachowski-II-167-193.pdf| {{cytuj pismo | odn=tak | nazwisko= Banachowski | imię = Lech | tytuł = Investigations of Properties of Programs by means of Extended Algorithmic Logic II | czasopismo = Fundamenta Informaticae| rok= 1977 |strony = 167-193 }} ]]
# [LB3] [[Media:BanachowskiDataStruct.pdf| {{cytuj pismo | odn=tak | nazwisko= Banachowski | imię = Lech | tytuł = An Axiomatic Approach to the Theory of Data Structures | czasopismo = Bull. Acad. Polon. Sci. Ser. Math. Astr. Phys. | rok= 1975 |strony = 315-323 }} ]]
# [AK1] [[Media:Kreczmar-Program-Fields.pdf| {{Cytuj pismo |odn=a | imię=Antoni | nazwisko=Kreczmar |tytuł=Programmability in Fields |czasopismo=Fundamenta Informaticae |strony=195-230 |rok=1977}}]]
# [AK2] [[Media:Kreczmar-Efficiency-problems.pdf| {{Cytuj pismo |odn=b | imię=Antoni | nazwisko=Kreczmar |tytuł=Effectivity problems of Algorithmic Logic |czasopismo=Fundamenta Informaticae |strony=19-32 |rok=1977}}]]
# [MSS2009] [[Media:Verifying-a-class.pdf |{{cytuj pismo| odn=tak| nazwisko=Mirkowska| imię=Grażyna| nazwisko2=Salwicki| imię2=Andrzej| nazwisko3=Świda| imię3=Oskar| tytuł=Verifying a Class: combining Testing and Proving|czasopismo=Fundamenta Informaticae| strony= 305-324 |rok= 2009 }}]]
# [AS2017] [[Media:On-Euclids-algorithm-2018.pdf | {{Cytuj pismo| odn=nie| nazwisko=Salwicki| imię=Andrzej| tytuł=A new proof of Euclid's algorithm | czasopismo= }}]]
# [WD1] [[ Media:WDnonprog.pdf | {{Cytuj pismo | odn=nie| nazwisko= Dańko | imię=Wiktor | tytuł=Nonprogrammable function defined by a procedure }} ]]

==Protokół rozbieżności==
Następujący tekst został złożony do druku
[[Media:On-Euclids-algorithm-2018.pdf | {{Cytuj pismo| odn=nie| nazwisko=Salwicki| imię=Andrzej| tytuł=A new proof of Euclid's algorithm | czasopismo= }}]] 

Pierwsza recenzja była rzeczowa, pomocna i jej sugestie zostały, z podziękowaniem, wykorzystane http://lem12.uksw.edu.pl/images/8/8c/1pierwszaRec.pdf. 

Drugi recenzent przedstawił następującą opinię http://lem12.uksw.edu.pl/images/0/0b/Second-report-08.pdf. 

Na to autor odpowiedział prosząc o referencje do zapowiadanych twierdzeń lub o przedstawienie dowodu. 

Oto protokół rozbieżności:
http://lem12.uksw.edu.pl/images/9/9a/DiscrepancyReport.pdf

==Pytania otwarte==
* Rozpatrzmy teorię algorytmiczną <math>Th_{2.5} = \langle L,C,A \rangle </math> gdzie
<math>L</math> - język, jest językiem struktury liczb naturalnych, algorytmicznym, 

<math>C</math> - operacja konskwencji jest wyznaczona przez zbiór aksjomatów i reguł wnioskowania logiki algorytmicznej (rachunku programów), 

<math>A</math> - zbiór aksjomatów, jest zbiorem wszystkich formuł pierwszego rzędu prawdziwych w standardowym modelu liczb naturalnych. 

Czy formuła <math>\color{blue}\forall x\, \{y:=0;\, \mathbf{while}\ x\neq y\ \mathbf{do}\ y:=y+1\ \mathbf{done}\}(x=y) </math> jest twierdzeniem tej teorii?
--[[Użytkownik:AndrzejSalwicki|AndrzejSalwicki]] ([[Dyskusja użytkownika:AndrzejSalwicki|dyskusja]]) 15:34, 30 maj 2018 (CEST)
* Czy teoria <math>Th_{2.5}</math> jest zupełna?
--[[Użytkownik:AndrzejSalwicki|AndrzejSalwicki]] ([[Dyskusja użytkownika:AndrzejSalwicki|dyskusja]]) 19:09, 31 maj 2018 (CEST)
* Według Harela, zob. Dynamic Logic, każda formuła algorytmiczna prawdziwa w standardowym modelu arytmetyki powinna być twierdzeniem teorii <math>Th_{2.5}</math>

* Czy teoria kontenerów (tj. słowników, dictionaries) bez aksjomatu algorytmicznego jest zupełna?

[[Category:Logika Algorytmiczna}}]]

Plik:Notatka15maja.pdf

2026-02-23T08:42:05Z

AndrzejSalwicki:

Plik:Argumenty 11Gru2025.pdf

2026-02-19T09:29:26Z

AndrzejSalwicki:

2025-10-01T13:07:25Z

AndrzejSalwicki:

Finally! 

Możemy ogłosić, że dowód hipotezy Collatza został ukończony. 
<big><big>Absract</big></big> 
We are showing that the following conjecture ''For every <math>n</math>, if <math>n</math> is a natural number then Collatz computation is finite.'' is a semantically valid statement. 

This is asserted by the Main lemma. 

A corollary of the lemma says: every instance of the cnjecture where the variable <math>n</math> is replaced by any natural number <math>r \neq 0</math>, is a theorem of arithmetic, in which the addition is the only operation. 
Note, the set <math>St_0</math>of is a recursive set of theorems of Presburger arithmetic, hence the theorems of algorithmic theory of natural numbers. 

Paradoxically, the Collatz conjecture itself is not a theorem of number theory (Peano's arithmetic), nor any mathematical theory that uses the first-order language and the classical predicate logic. 

It is so because, '''1''') there is no first-order theory such that all its models are isomorphic to the standard model of natural numbers
and hence '''2''') the infinite computations can be n observed in a ''non-standard computable'' model of the elementary theory of natural numbers with addition. 

To avoid the paradox, we will use the calculus of programs <math>\mathcal{AL}</math> instead of the predicate calculus. The halting condition <math>H</math> of the Collatz computations is written as an algorithmic formula.

<math> \qquad \underbrace{\boxed{\left\lbrace \begin{array}{l}
m:=n \div 2^{\kappa(n)}; \\
\mathbf{while}\ m \neq 1 \\
\mathbf{do} \\
\quad m:=3 \cdot m +1; \\
\quad m:= m \div 2^{\kappa(m)} \\
\mathbf{od}
\end{array}\right\rbrace(m=1)} }_{ {the\ computation\ for\ n\ is\ finite} } \qquad (H)
</math>

There is no finite, traditional proof the following theorem .
<math> \begin{tabular}{p{14cm}}
% We are answering to the question (\textit{i}) formulating the thesis of the \textsc{Theorem}\eqref{thM}.
\[ \label{main}
\mathcal{ATN}\vdash
\forall_{n \neq 0} \underbrace{\boxed{\left\lbrace \begin{array}{l}
q:=1; \\
\mathbf{while}\ n \neq q \\
\mathbf{do} \\
\quad q:=q+1 \\
\mathbf{od}
\end{array}\right\rbrace(n=q) } }_{\color{black}{\textsc{IF}\ n>0 \ is\ a\ natural\ number\ }}
\implies
\underbrace{\boxed{\left\lbrace \begin{array}{l}
m:=n \div 2^{\kappa(n)}; \\
% (*\ \ m= 2^{\kappa(n)} (2 \rho(m)+1) \ \ *) \\
\mathbf{while}\ m \neq 1 \\
\mathbf{do} \\
\quad m:=3 \cdot m +1; \\
\quad m:= m \div 2^{\kappa(m)} \\
\mathbf{od}
\end{array}\right\rbrace(m=1)} }_{ {\textsc{THEN}\ the\ computation\ for\ n\ is\ finite\ \textsc{FI}} }
\ \ \ \ \ \ \ (6.1) \]
\end{tabular} </math>
Instead, we are presenting an rgument showing that the proof can be carried out in the calculus of programs <math>\mathcal{AL}</math>. To achieve his goal one has to construct an infinite tree <math>\mathcal{D}</math>. The root of the tree is the halting formula . The formula is the consequence of the infinitary inference rule R3, see p. . For each premise one can construct a a finite subtree, i.e. a finite proof which is using one formula of the set $St_{0} $. \\
Note, that that the set $St_{0}$ is a recursive set of formulas without variables and that all its elements are theorems of Peano's arithmetic.

Work on the problem took 83 years. 
We succeeded. We are changing the status of the "Collatz conjecture" to [http://lem12.uksw.edu.pl/images/3/37/CollatzConjecturebecomesTheorem20Nov23.pdf] 

==Introduction==
Let's consider the statement 
for every natural number <math>n</math>, the following program <math>Cl</math> has a finite computation. 
<math>\color{blue}\qquad Cl:\,\left\{\begin{array}{l} \mathbf{while}\ n \neq 0 \ \mathbf{do} \\
\quad \mathbf{if}\ odd(n) \ \mathbf{then}\ n:=3n+1 \ \mathbf{else}\ n:=n/2\ \mathbf{fi} \\
\mathbf{od} \end{array}\right\} </math> 
We begin by noting that the truth of the above statement entails the truth of Collatz's thesis as it was formulated before World War II. 
But in 1937, neither computers nor programming languages existed. 
On the other hand, the theory of algorithms did exist and was already well developed. The theory of recursive functions was developed in Göttingen (David Hilbert and his students), Budapest (Rozsza Pterer, Laszlo Kalmar), ... 
In London, Alan Turing created the abstract Turing machine. 
In Moscow, Kolmogorov and in Kazan, Maltsev explored the concept of a computable function. 
 
In Warsaw, Alfred Tarski, together with his students Mojżesz Presburger and Stanisław Jaskowski, obtained important results concerning the theory of addition of natural numbers.

==Our observations from 2004==
* The Collatz algorithm <math>Cl</math> does not require multiplication or division operations. Multiplying by 3 (because 3x=x+x+x) and dividing by 2 (a simple algorithm adding every other 1 is sufficient), is sufficient.
* In the algebraic structure <math>\mathfrak{M}</math>, which is a non-standard model of the elementary theory of addition of natural numbers (there is one, see below), the algorithm <math>Cl</math> has an infinite computation for many arguments.
* Therefore, the Collatz theorem cannot be proven based on the axioms of the elementary theory of addition of natural numbers.
* Moreover, in the language of elementary theory of addition, there is no stopping formula for the Collatz algorithm! It is a corollary from the Goedel incompleteness theorem. 
So what do we have to prove?

==Correct formulation of the Collatz theorem==
In the standard structure of natural numbers with the addition operation,
our program <math>Cl</math> has a finite computation for each argument ''n''.

==Stop formula==
i.e.
=== A necessary and sufficient condition for the computation to be finite===
Therefore, we need to create a formula <math>\theta</math> (a logical expression) such that it evaluates to true if and only if the computation of the program <math>Cl</math> is finite. There are many such formulas in the language of program calculation, i.e. algorithmic logic. 
,<math>\qquad \theta:\,\left\{\begin{array}{l} \mathbf{while}\ n \neq 0 \ \mathbf{do} \\
\quad \mathbf{if}\ odd(n) \ \mathbf{then}\ n:=3n+1 \ \mathbf{else}\ n:=n/2\ \mathbf{fi} \\
\mathbf{od} \end{array}\right\} (n=1) </math>
 
The value of the <math>\theta</math> formula depends only on the initial value of the "n" variable. This formula is satisfied by the value of the variable "n" if and only if the evaluation of the while ... program is finished and the final value of the variable "n" is equal to 1. 
Other formulas can also be considered, e.g., 
,<math>\qquad \xi:\,\bigcup \left\{\overbrace{\begin{array}{l} \mathbf{if}\ n \neq 0 \ \mathbf{then} \\
\quad \mathbf{if}\ odd(n) \ \mathbf{then}\ n:=3n+1 \ \mathbf{else}\ n:=n/2\ \mathbf{fi} \\
\mathbf{fi} \end{array} }^{K}\right\} (n=1) </math> 
{co reads: "there exists an iteration <math>K^i</math> of the program <math>K</math> such that after executing <math>K^i</math> the equality <math>n=1</math> is satisfied."} 
In other words, we are dealing with an upper bound on the values of the formulas <math>K^i(n=1)</math>, where <math>i= 0,1,2 \dots</math>. 

The second part of the problem is much more difficult: we must prove the stopping formula using the axioms of program calculus and the axioms of the algorithmic theory of natural numbers. 

 
==Elementary Theory of Addition of Natural Numbers==
The previous observation that Collatz's theorem cannot be proved in this theory remains valid. However, the properties of the non-standard model of this theory and a few of its theorems will be helpful in further considerations. 
 
This theory is defined by specifying three components:
* the language,
* the logic, i.e., the consequence operation, and
* the axioms specific to this theory. 
'''Language.''' The expressions of the language are composed of the following symbols: variable symbols, e.g., x, y, n, the + symbol for a binary operation, the = symbol for a binary relation, constant symbols, logical functor symbols, and auxiliary symbols, e.g., parentheses. 
. Examples of expressions are... 

'''Logic.''' The consequence (inference) operation is determined by specifying the axioms of first-order logic and the rules of inference. 
'''Axioms.'''
<math>
\begin{align}
\tag{a} \forall_x\ x+1 &\neq 0 \\
\tag{b} \forall_x\, \forall_y\ x+1=y+1 &\implies x=y \\
\tag{c} \forall_{x}\ x+0&=x \\
\tag{d} \forall_{x,y}\ (y+1)+x&=(y+x)+1 \\
\tag{I} \Phi(0)\land \forall_x\,[\Phi(x) \implies \Phi(x+1)]&\implies \forall_x\Phi(x)
\end{align}
</math>
The expression <math>\Phi(x)</math> may be replaced by any formula. The result is an axiom of theory
This is the induction scheme. 
We augment the set of axioms adding four axioms that define a coiple of useful notions. 
<math>
\begin{align}
\tag{e} even(x) &\stackrel{df}{\equiv} \exists_y\, x=y+y \\
% \tag{o} odd(x) &\stackrel{df}{\equiv} \exists_y\, x=y+y+1 \\
% \tag{D2} x\, div\, 2 = y &\equiv (x=y+y\, \lor\, x=y+y+1) \\
% \tag{3x} 3x&\stackrel{df}{=} x+x+x
\end{align}
</math>

'''Models of Presburger Arithmetic''' 
As expected, the sequence of standard values 0, 1, 2, 3, ... is a model of this theory.

Stanisław Jaśkowski discovered another, nonstandard model of Presburger arithmetic in 1929.

[[File:MonStandardModel.png|center|thumb|600px|Nonstandard model of Presburger arithmetic]]
The universe of the model is a subset of the set of complex numbers <math>a+\math b</math>
where <math>a \in \mathbb{Z} </math> i.e. a is an integer number and <math>b \in \mathbb{Q}^+ </math> is a positive rational number. Additionally, whenever <math>b=0 </math> we have <math>a>0</math>.
Addition is defined as usual addition of complex numbers.

Both models are computable. There are also unpredictable models with arbitrarily high power.

==Algorithmic Theory of Natural Numbers==
* Language. The alphabet of a language contains a set of variables, e.g., x,y. a functor + a two-argument addition operation, two constants 0 and 1, a relation sign = equality. 
Terms (i.e., nomenclature expressions): this is the smallest set of expressions containing variables, constants, and closed under the combination of two terms in this way (t1 + t2). 
Formulae.
* Logic. Program calculus. Program calculus includes first-order logic. In addition to first-order formulas, the language of program calculus also contains algorithmic formulas. The simplest such formula is a string consisting of a program and a formula (usually a first-order formula) following it.
To the axioms of first-order logic, axioms describing the properties of program-generating connectives should be added; see [[Algorithmic Logic]].
To the inference rules of first-order logic, rules specific to program calculus should be added. 

* Axioms of the theory. 
Only three formulas. 
<math>
\begin{eqnarray}
\tag{ATN1} \forall_x\, x+1 \neq 0 &&\\
\tag{ATN2} \forall_{x,y}\,x+1=y+1 \implies x=y &&\\
\tag{ATN3}\forall_x\, \{y :=0; \mathbf{while}\ y\neq x\ \mathbf{do}\ y:=y+1\ \mathbf{od} \}\,(y=x) &&
\end{eqnarray} </math> 

These are essentially the axioms of the successor theory. 
The ATN1 formula states that 0 is not the successor of any natural number. 
The ATN2 formula states that the successor is a one-to-one function. 
The formula ATN3 states that every natural number is ''reachable'' from zero by adding a finite number of ones. 
In this theory, one can write definitions for addition, multiplication, and any computable function.

==Analiza formuły stopu==
xxx

==Trójki ==
Spostrzeżenie (wynikłe z przygladania się formule stopu). 

<math>\forall_{n \neq 0} \exists_{x,y,z}\ n \cdot 3^x+y=2^z </math>

==Drzewo Collatza==
[[Plik:StratDrzewoCollatza.png|thumb|center |750px| Rys. 1 Fragmenty warstw <math>W_0, \dots W_4 </math> drzewa Collatza ]]

==Własności obliczeń na trójkach==
Tutaj napiszemy więcej 
==Kalejdoskop==

Oglądaj rysunki, wykonuj obliczenia, rozwiązuj zadania, formułuj swoje zdanie, próbuj je uzasadnić, ... 

Tu znajdziesz .... 
===Obliczenia utemperowane===
[[Plik:ObliczN19.pdf.png|thumb|center|750px|Utemperowane obliczenie dla n=76]]
Trzy zadania. Odpowiedz czy są one jakos powiązane? 
* Masz do dyspozycji bardzo wiele trójkątnych płytek, w dwu kolorach.
Czy potrafisz ułożyć chodnik łączący posesje o numerze n z numerem 1?
*[[Ułamek piętrowy]]
* Czy obliczenie 3x+1 jest skończone dla każdej liczby naturalnej?

===Struktury algebraiczne===
Struktura liczb naturalnych. 
Algebra Jaśkowskiego. 
===Teorie===
elementarna teoria liczb naturalnych z dodawaniem. 
algorytmiczna teoria liczb naturalnych 
===Zadania===

<math>\alpha</math> 

== Archiwum kolejnych wersji pracy ==
[CollatzConjecturebecomesTheorem11Aug23 http://lem12.uksw.edu.pl/images/3/3b/CollatzConjecturebecomesTheorem11Aug23.pdf]

[https://dx.doi.org/10.2139/ssrn.4158238 \On Collatz theorem II.pdf wersja z 5 czerwca 2022 ]

][http://lem12.uksw.edu.pl/images/a/ab/On-Collatz-thm17-09-21.pdf wersja z 20 wrzesnia 2021]

[http://lem12.uksw.edu.pl/images/7/7d/Algorytmy-bliskie-Collatzowi.pdf algorytmy wokół Collatzowe]

[http://lem12.uksw.edu.pl/images/c/c0/On-Collatz-thm-27-09-21.pdf wersja z 27 wrzesnia 2021]

[http://lem12.uksw.edu.pl/images/8/8f/On-Collatz-thm-7-10-21.pdf wersja z 7 pażdziernika 2021]