Logika Algorytmiczna
Felix qui potuit rerum cognoscere causas
Logika algorytmiczna jest jeszcze jednym, rachunkiem logicznym. 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.
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.
Przykład Rozpatrzmy prosty program
(* 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. 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żne jest stwierdzenie, ż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ą priorytettową
- d jest strukturą słownika (ang. dictionary)
- k jest kopcem
itd.
Bibliografia
Książki
- [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.
- [AlgoLog] Grażyna Mirkowska, Andrzej Salwicki: Algorithmic Logic. Warszawa: PWN, 1987, s. 345.
- [LogProg] Grażyna Mirkowska, Andrzej Salwicki: Logika Algorytmiczna dla Programistów. Warszawa: WNT, 1992, s. 294. cz.1
- [LogProg] Grażyna Mirkowska, Andrzej Salwicki: Logika Algorytmiczna dla Programistów. Warszawa: WNT, 1992, s. 294. cz.1
- [AL4software] Grażyna Mirkowska, Andrzej Salwicki: Algorithmic Logic for Software Construction and Verification. Dąbrowa Leśna: Dąbrowa Research, 2014, s. 154.
Artykuły