Algorithmic Logic: Różnice pomiędzy wersjami

Z Lem
Skocz do: nawigacji, wyszukiwania
(→‎Bibliography)
(→‎Algorithmic theories)
 
(Nie pokazano 78 pośrednich wersji utworzonych przez tego samego użytkownika)
Linia 1: Linia 1:
 +
<big><big><span style="color: Red">This page is under construction</span></big></big><br />
 +
<p style="text-align: right;"><small>''Felix qui potuit rerum cognoscere causas'' </small> </p>
 +
 
Algorithmic logic is a calculus in which one can express the semantical properties of programs and it allows to construct proofs of the formulas. In this way one can prove property like correctness by proving the corresponding formula that express the property.
 
Algorithmic logic is a calculus in which one can express the semantical properties of programs and it allows to construct proofs of the formulas. In this way one can prove property like correctness by proving the corresponding formula that express the property.
 +
 +
== Introduction ==
 +
Algorithmic logic is a calculus of logic, moreover it is also a calculus of programs. It is an attractive workplace for software engineers as well as for mathematically oriented people. It is quite reasonable to give it another name ''calculus of programs''.
 +
[[Plik:4logiki.jpg|thumb|center |750px| Fig. 1  Four logical systems and their sets of well formed expressions ]]
 +
Figure 1 shows relations among four logical calculi. An arrow    <math>\mathcal{L}\rightarrow\mathcal{L}'</math> between two logical calculi <math>\mathcal{L}</math> and <math>\mathcal{L}'</math> has following meaning: ''Every tautology'' <math>\alpha</math> ''of calculus'' <math>\mathcal{L}</math> ''becmes a tatutology of calculus ''<math>\mathcal{L}</math>' ''when atoms of formula '' <math>\alpha</math> '' are replaced by formulas of calculus'' <math>\mathcal{L}</math>. More insight can be gained by comparison of sets of well formed formulas  <math>\mathcal{WFF} </math>.  <br />
 +
The languages of four calculi differ. Each language is a pair <alphabet, WFF the set of well formed expressions>. Note,  in each case the structure of the set of well formed expression  <math>\mathcal{WFF} </math> (''ang''. well formed formulas) is different.  <br />
 +
Legend: <math>\mathcal{L}</math> - language, <math>\mathcal{A}</math> - alphabet, <math>\mathcal{T}</math> - set of terms (arithmetical, object, string, ... expressions), <math>\mathcal{F}</math> - set of formulas, <math>\mathcal{P}</math> - set of programs.
 +
[[Plik:AxiomPL.jpg|thumb|750px| Fig. 2  Axioms of propositional calculus ]]
 +
[[Plik:axiomsFOL-AL.jpg|thumb |750px|  Fig. 3  Axioms of predicate calculus (Ax<sub>12</sub>, Ax<sub>13</sub>) and program calculus ]]
 +
[[Plik:inferenceRules.jpg| thumb  |750px| Fig. 4 Inference rules ]]
 +
Set of formulas of algorithmic logic contains all formulas of first-order logic. Moreover it contains formulas which consist of program preceding a formula.  If  <math>\alpha</math> is a formula and  <math>K</math> is a program, then the expression of the form  <math>K\alpha</math> is a formula of the language of algorithmic logic. In short, an algorithmic formula.  <br />
 +
Such a formula <math>K\alpha</math> is evaluated to false or true according to the diagram Fig.5.
 +
[[Plik:Kalfa.jpg |thumb|left|300px|Fig. 5  Meaning of formula <math>K\alpha</math> is determined by commutativity of this diagram]]
 +
Figure  5 should be self explanatory. It remains to decide what to do when a computation of program K does not bring a result . It may happen that computation of program K is infinite or another error occurred.  In such case it is impossible to assert that ''for  data v the computation of program K ends successfully and the results satisfy the condition '' <math>\alpha</math>'. Hence in this case the value of formula  <math>K\alpha</math> is '''false'''..<br />
 +
 +
We can also say that algorithmic logic is a calculus of programs. The language of algorithmic logic contains programs and algorithmic formulas. It is important that each semantic property of programs, e.g. correctness, equivalence, termination of computations or, conversely, looping, ... may be expressed by an appropriate formula. This allows us to turn the task of proving that a certain program
 +
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. <br />'''Przykład''' <br />
 +
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 ... <br />
 +
 +
 +
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.
 +
 
== Structure of AL ==
 
== Structure of AL ==
 
An algorithmic logic is a pair <math>\mathcal{AL} = \langle \mathcal{L}, \mathcal{C} \rangle </math>, where <math>\mathcal{L} </math> is  a formalized language of algorithmic logic and <math>\mathcal{C} </math> is i a logical consequence operation defined by the notions of logical axioms, inference rules and the notion of (formal) proof.
 
An algorithmic logic is a pair <math>\mathcal{AL} = \langle \mathcal{L}, \mathcal{C} \rangle </math>, where <math>\mathcal{L} </math> is  a formalized language of algorithmic logic and <math>\mathcal{C} </math> is i a logical consequence operation defined by the notions of logical axioms, inference rules and the notion of (formal) proof.
−
An algorithmic language <math>\mathcal{L} </math> is a pair consisting of the alphabet of <math>\mathcal{L} </math> and the set of weel-formed expressions, <math>\mathcal{L} = \langle A, WFF \rangle </math>, where <math> A </math> is the alphabet, i.e. the set of admissible symbols and <math> WFF </math> is the set of well formed expressions of the language.
+
An algorithmic language <math>\mathcal{L} </math> is a pair consisting of the alphabet of <math>\mathcal{L} </math> and the set of well-formed expressions, <math>\mathcal{L} = \langle A, WFF \rangle </math>, where <math> A </math> is the alphabet, i.e. the set of admissible symbols and <math> WFF </math> is the set of well formed expressions of the language.
 +
 
 +
 
 +
Structure
 +
 
 +
# Define syntax - of expressions(terms), formulas and programs.
 +
# Define semantics - partially using the Tarski's scheme: each term defines a function and each formula defines ...<br />
 +
::partially through the notion of computation ...
 +
# Make a catalogue of semantical properties of programs: halting property, correctness, partial correctness, ...
 +
# Define ''algorithmic formulas'' -- show that semantical properties of programs are expressible in the language of algorithmic formulas,
 +
# Find the axioms and inference rules of algorithmic logic
 +
# Show the completeness property of AL,
 +
# Show applications
 +
 
 +
== Algorithmic theories ==
 +
Here we shall collect axiomatizations of various algorithmic theories. Each set <math>S</math> of this collection may be conceived as specification of a class <math>C</math>  that implements the set  <math>S</math>.<br />
 +
 
 +
[[Algorithmic theory of natural numbers  ]]<br />
 +
[[Algorithmic theory of integers]]<br />
 +
[[Algorithmic theory of rational numbers]]<br />
 +
<br />
 +
[[Algorithmic theory of stacks]]<br />
 +
 
 +
[[Algorithmic theory of FIFO queues]]<br />
 +
 
 +
[[Algorithmic theory of binary trees]]<br />
 +
 
 +
[[Algorithmic theory of binary search trees BST]]<br />
 +
 
 +
[[Algorithmic theory of heaps]]<br />
 +
 
 +
[[Algorithmic theory of dictionaries - i.e. finite sets]]<br />
 +
 
 +
[[Algorithmic theory of priority queues]]<br />
 +
<br />
  
 
== History ==
 
== History ==
−
The origins of algorithmic logic go to papers of Yanov, H. Thiele, Erwin Engeler.
+
The first papers on properties of programs appeared in the 50-ies of XX century. To mention a few: Yanov, Sh. Igarashi.
−
In 1969 the program of research was formulated in the Ph.D.  thesis of A. Salwicki.
+
Later the papers of Helmut Thiele and of Erwin Engeler are important ones.
−
== pre algorithmic logic ==
+
 
−
Paper of R.W. Floyd brought some light on proving programs correct.
+
In 1969 the program of research of algorithmic logic was formulated in the Ph.D.  thesis of A. Salwicki.
−
Later C.A.R. Hoare proposed another formalization based on the ideas of Floyd.
+
 
−
S. Cook addressed the problem of completeness of Floyd-Hoare calculus and formulated the so called relative completeness theorem.
+
== Other logics of programs ==
 +
You may ask how calculus of programs is related to other calculi: e.g. Floyd, Hoare, Dijkstra, dynamic logic, etc.?<br />
  
−
In the light of the papers of A., Goraj, G. Mirkowska and A. Paluszkiewicz this theorem is unnecessary. Theorem 5 of this paper states that notion of feasible and of acceptable desciption of program coincide. In other words if a verification condition of a program is valid in allmodels of a theory then it is provable from the axioms of the theory.
+
[[calculus of Floyd]]<br />
 +
[[logic of Hoare]]<br />
 +
[[calculus of weakest precondition of Dijkstra]]<br />
 +
[[dynamic logic]]<br />
  
 
== Bibliography ==
 
== Bibliography ==
−
# [Mirkowska, Salwicki 1987] {{Cytuj książkę | odn=tak | nazwisko=Mirkowska |imię= Grażyna | tytuł = Algorithmic Logic | nazwisko2= Salwicki |imię2=Andrzej | wydawca =PWN & D.Reidel | miejsce= Warszawa & Dordrecht | strony= 374 }} [[Media:Algorithmic Logic.pdf]]
+
Books
−
# [Kreczmar 1977a] {{Cytuj pismo |odn=tak |odn=a | nazwisko = Kreczmar | imię = Antoni | tytuł = Effectivity problems of Algorithmic Logic | czasopismo = Fundamenta Informaticae | rok = 1977}}
+
−
# [Kreczmar 1977b] {{Cytuj pismo| odn=tak |odn=b | imię=Antoni | nazwisko=Kreczmar |tytuł=Programmability in Fields |czasopismo=Fundamenta Informaticae |strony=195-230 |rok=1977}}
+
−
# [Kreczmar 1979] {{Cytuj książkę|odn=tak | nazwisko = Kreczmar | imię = Antoni | tytuł = Some historical remarks on algorithmic logic | wydawca = Springer Vlg | miejsce = Berlin | data = 1979 | seria = LNCS | strony = 999-1000 | isbn = 0123456789 | tytuł tomu = Algorithms in Modern Mathematics and Computer Science}}
+
−
# [Banachowski i in.] {{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}} [[http://matwbn.icm.edu.pl/ksiazki/bcp/bcp2/bcp211.pdf]]
+
−
# [Goraj, Mirkowska, Paluszkiewicz] {{Cytuj pismo|odn=tak| nazwisko= Goraj| imię = Anna|tytuł= On the notion of the description of the program | nazwisko2=Mirkowska| imię2=Grażyna | nazwisko3=Paluszkiewicz| imię3=Anna| czasopismo= Bull. Pol. Acad. Sci. Ser. Astr. Math. Phys.|rok=1970| strony=499-505 }} [[Media:GMP1970.pdf]]
+
  
 +
# [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
 +
# [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 }}
 +
A choice of publications
 +
# [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-Black.pdf | {{Cytuj pismo| odn=nie| nazwisko=Salwicki| imię=Andrzej| tytuł=A new proof of Euclid's algorithm | czasopismo= }}]]
 +
Other papers
 +
# [Yanov 1959] {{Cytuj pismo | odn=tak | imię=Yuri I. |nazwisko= Yanov |tytuł = The Logical schemes in Algorithms| czasopismo= Problems of Cybernetics| rok=1959| strony=82-140 |volumin=1}}
 +
# [Engeler 1967 ] {{Cytuj pismo| odn=tak| autor= Erwin Engeler | tytuł= Algorithmic properties of Structures | czasopismo=Math. System Theory| rok=1967 | strony=183-195 }}
 
[[Category:Algorithmic Logic]]
 
[[Category:Algorithmic Logic]]

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

This page is under construction

Felix qui potuit rerum cognoscere causas

Algorithmic logic is a calculus in which one can express the semantical properties of programs and it allows to construct proofs of the formulas. In this way one can prove property like correctness by proving the corresponding formula that express the property.

Introduction

Algorithmic logic is a calculus of logic, moreover it is also a calculus of programs. It is an attractive workplace for software engineers as well as for mathematically oriented people. It is quite reasonable to give it another name calculus of programs.

Fig. 1 Four logical systems and their sets of well formed expressions

Figure 1 shows relations among four logical calculi. An arrow [math]\mathcal{L}\rightarrow\mathcal{L}'[/math] between two logical calculi [math]\mathcal{L}[/math] and [math]\mathcal{L}'[/math] has following meaning: Every tautology [math]\alpha[/math] of calculus [math]\mathcal{L}[/math] becmes a tatutology of calculus [math]\mathcal{L}[/math]' when atoms of formula [math]\alpha[/math] are replaced by formulas of calculus [math]\mathcal{L}[/math]. More insight can be gained by comparison of sets of well formed formulas [math]\mathcal{WFF} [/math].
The languages of four calculi differ. Each language is a pair <alphabet, WFF the set of well formed expressions>. Note, in each case the structure of the set of well formed expression [math]\mathcal{WFF} [/math] (ang. well formed formulas) is different.
Legend: [math]\mathcal{L}[/math] - language, [math]\mathcal{A}[/math] - alphabet, [math]\mathcal{T}[/math] - set of terms (arithmetical, object, string, ... expressions), [math]\mathcal{F}[/math] - set of formulas, [math]\mathcal{P}[/math] - set of programs.

Fig. 2 Axioms of propositional calculus
Fig. 3 Axioms of predicate calculus (Ax12, Ax13) and program calculus
Fig. 4 Inference rules

Set of formulas of algorithmic logic contains all formulas of first-order logic. Moreover it contains formulas which consist of program preceding a formula. If [math]\alpha[/math] is a formula and [math]K[/math] is a program, then the expression of the form [math]K\alpha[/math] is a formula of the language of algorithmic logic. In short, an algorithmic formula.
Such a formula [math]K\alpha[/math] is evaluated to false or true according to the diagram Fig.5.

Fig. 5 Meaning of formula [math]K\alpha[/math] is determined by commutativity of this diagram

Figure 5 should be self explanatory. It remains to decide what to do when a computation of program K does not bring a result . It may happen that computation of program K is infinite or another error occurred. In such case it is impossible to assert that for data v the computation of program K ends successfully and the results satisfy the condition [math]\alpha[/math]'. Hence in this case the value of formula [math]K\alpha[/math] is false..

We can also say that algorithmic logic is a calculus of programs. The language of algorithmic logic contains programs and algorithmic formulas. It is important that each semantic property of programs, e.g. correctness, equivalence, termination of computations or, conversely, looping, ... may be expressed by an appropriate formula. This allows us to turn the task of proving that a certain program O logice algorytmicznej możemy też powiedzieć, że jest 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.

Structure of AL

An algorithmic logic is a pair [math]\mathcal{AL} = \langle \mathcal{L}, \mathcal{C} \rangle [/math], where [math]\mathcal{L} [/math] is a formalized language of algorithmic logic and [math]\mathcal{C} [/math] is i a logical consequence operation defined by the notions of logical axioms, inference rules and the notion of (formal) proof. An algorithmic language [math]\mathcal{L} [/math] is a pair consisting of the alphabet of [math]\mathcal{L} [/math] and the set of well-formed expressions, [math]\mathcal{L} = \langle A, WFF \rangle [/math], where [math] A [/math] is the alphabet, i.e. the set of admissible symbols and [math] WFF [/math] is the set of well formed expressions of the language.


Structure

  1. Define syntax - of expressions(terms), formulas and programs.
  2. Define semantics - partially using the Tarski's scheme: each term defines a function and each formula defines ...
partially through the notion of computation ...
  1. Make a catalogue of semantical properties of programs: halting property, correctness, partial correctness, ...
  2. Define algorithmic formulas -- show that semantical properties of programs are expressible in the language of algorithmic formulas,
  3. Find the axioms and inference rules of algorithmic logic
  4. Show the completeness property of AL,
  5. Show applications

Algorithmic theories

Here we shall collect axiomatizations of various algorithmic theories. Each set [math]S[/math] of this collection may be conceived as specification of a class [math]C[/math] that implements the set [math]S[/math].

Algorithmic theory of natural numbers
Algorithmic theory of integers
Algorithmic theory of rational numbers

Algorithmic theory of stacks

Algorithmic theory of FIFO queues

Algorithmic theory of binary trees

Algorithmic theory of binary search trees BST

Algorithmic theory of heaps

Algorithmic theory of dictionaries - i.e. finite sets

Algorithmic theory of priority queues

History

The first papers on properties of programs appeared in the 50-ies of XX century. To mention a few: Yanov, Sh. Igarashi. Later the papers of Helmut Thiele and of Erwin Engeler are important ones.

In 1969 the program of research of algorithmic logic was formulated in the Ph.D. thesis of A. Salwicki.

Other logics of programs

You may ask how calculus of programs is related to other calculi: e.g. Floyd, Hoare, Dijkstra, dynamic logic, etc.?

calculus of Floyd
logic of Hoare
calculus of weakest precondition of Dijkstra
dynamic logic

Bibliography

Books

  1. [AlgoLog] Grażyna Mirkowska, Andrzej Salwicki: Algorithmic Logic. Warszawa: PWN, 1987, s. 345.
  2. [LogProg1] Grażyna Mirkowska, Andrzej Salwicki: Logika Algorytmiczna dla Programistów. Warszawa: WNT, 1992, s. 294. cz.1
  3. [LogProg2] Grażyna Mirkowska, Andrzej Salwicki: Logika Algorytmiczna dla Programistów. Warszawa: WNT, 1992, s. 294. cz.2
  4. [AL4software] Grażyna Mirkowska, Andrzej Salwicki: Algorithmic Logic for Software Construction and Verification. Dąbrowa Leśna: Dąbrowa Research, 2014, s. 154.
  5. [CentrumBanachAL] Lech Banachowski, Antoni Kreczmar, Grażyna Mirkowska, Helena Rasiowa, Andrzej Salwicki: An introduction to Algorithmic Logic - Metamathematical Investigations of Theory of Programs. T. 2: Banach Center Publications. Warszawa: PWN, 1977, s. 7-99, seria: Banach Center Publications. ISBN 123.
  6. [HRAL] Helena Rasiowa: Algorithmic Logic - Notes from Seminar in Simon Fraser University. T. 281. Warsaw: 1975, seria: Reports of Institute of Computer Science PAS.
  7. [AB] Andrzej Biela: Algorithmic structural completeness and a retrieval system for proving theorems in algorithmic theories. T. 1901. Katowice: Wydawnictwo Uniwersytetu Śląskiego, 2000, s. 122.

A choice of publications

  1. [GMP] Anna Góraj, Grazyna Mirkowska, Anna Paluszkiewicz. On the notion of description of program. „Bull. Acad. Polon. Sci. Ser. Math. Astr. Phys.”, s. 499 - 505, 1970. 
  2. [GM1971] Grażyna Mirkowska. On Formalized Systems of Algorithmic Logic. „Bull. Polish Academy Sciences, Ser. Math. Phys.”, s. 421-428, 1971. 
  3. [GM1] Grazyna Mirkowska. Algorithmic logic and its applications in the theory of programs I. „Fundamenta Informaticae”, s. 1-17, 1977. 
  4. [GM2] Grazyna Mirkowska. Algorithmic logic and its applications in the theory of programs II. „Fundamenta Informaticae”, s. 147-165, 1977. 
  5. [AS1] Andrzej Salwicki. Formalized Algorithmic Languages. „Bull. Acad. Polon. Sci. Ser. Math. Astr. Phys.”, s. 227-232, 1970. 
  6. [AS3] Andrzej Salwicki. On the predicate calculi with iteration quantifiers. „Bull. Acad. Polon. Sci. Ser. Math. Astr. Phys.”, s. 279-285, 1970. 
  7. [LB1] Lech Banachowski. Investigations of Properties of Programs by means of Extended Algorithmic Logic I. „Fundamenta Informaticae”, s. 93-119, 1977. 
  8. [LB2] Lech Banachowski. Investigations of Properties of Programs by means of Extended Algorithmic Logic II. „Fundamenta Informaticae”, s. 167-193, 1977. 
  9. [LB3] Lech Banachowski. An Axiomatic Approach to the Theory of Data Structures. „Bull. Acad. Polon. Sci. Ser. Math. Astr. Phys.”, s. 315-323, 1975. 
  10. [AK1] Antoni Kreczmar. Programmability in Fields. „Fundamenta Informaticae”, s. 195-230, 1977. 
  11. [AK2] Antoni Kreczmar. Effectivity problems of Algorithmic Logic. „Fundamenta Informaticae”, s. 19-32, 1977. 
  12. [MSS2009] Grażyna Mirkowska, Andrzej Salwicki, Oskar Świda. Verifying a Class: combining Testing and Proving. „Fundamenta Informaticae”, s. 305-324, 2009. 
  13. [AS2017] Andrzej Salwicki. A new proof of Euclid's algorithm. . 

Other papers

  1. [Yanov 1959] Yuri I. Yanov. The Logical schemes in Algorithms. „Problems of Cybernetics”, s. 82-140, 1959. 
  2. [Engeler 1967 ] Erwin Engeler. Algorithmic properties of Structures. „Math. System Theory”, s. 183-195, 1967. 
Źródło „http://lem12.uksw.edu.pl/index.php?title=Algorithmic_Logic&oldid=3048”