Algorithmic Logic: Różnice pomiędzy wersjami

Wersja z 13:04, 2 sie 2017

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. It is an attractive workplace for software engineers as well as for mathematially oriented people. It is quite reasonable to give it another name calculus of programs.

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.

Rys. 2 Aksjomaty rachunku zdań

Rys. 3 Aksjomaty rachunku predykatów(2) i rachunku programów

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?

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 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.

Steps

1. Define syntax
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. find applications

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.

Floyd-Hoare logic

Paper of R.W. Floyd brought some light on proving programs correct. 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.

In the light of the paper [Goraj, Mirkowska, Paluszkiewicz ↓] this theorem is unnecessary. Theorem 5 of this paper states that notions of feasible and of acceptable description of program coincide. In other words if a verification condition of a program is valid in all models of a theory then it is provable from the axioms of the theory. For the details see [AL4software ↓] sections on Floyd's descriptions of programs and Hoare's logic of partial correctness.

Bibliography

1. [Mirkowska, Salwicki 1987] Grażyna Mirkowska, Andrzej Salwicki: Algorithmic Logic. Warszawa & Dordrecht: PWN & D.Reidel, s. 374.
2. [AL4software] Grażyna Mirkowska, Andrzej Salwicki: Algorithmic Logic for Software Construction and Verification. Dąbrowa Leśna: Dąbrowa Research, 2014, s. 154.
3. [Kreczmar 1977a] Antoni Kreczmar. Effectivity problems of Algorithmic Logic. „Fundamenta Informaticae”, 1977. 
4. [Kreczmar 1977b] Antoni Kreczmar. Programmability in Fields. „Fundamenta Informaticae”, s. 195-230, 1977. 
5. [Kreczmar 1979] Antoni Kreczmar: Some historical remarks on algorithmic logic. T. Algorithms in Modern Mathematics and Computer Science. Berlin: Springer Vlg, 1979, s. 999-1000, seria: LNCS. ISBN 0123456789.
6. [Banachowski i in.] 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. [1]
7. [Goraj, Mirkowska, Paluszkiewicz] Anna Goraj, Grażyna Mirkowska, Anna Paluszkiewicz. On the notion of the description of the program. „Bull. Pol. Acad. Sci. Ser. Astr. Math. Phys.”, s. 499-505, 1970. 
8. [Yanov 1959] Yuri I. Yanov. The Logical schemes in Algorithms. „Problems of Cybernetics”, s. 82-140, 1959. 
9. [Engeler 1967 ] Erwin Engeler. Algorithmic properties of Structures. „Math. System Theory”, s. 183-195, 1967.