Logika Algorytmiczna: Różnice pomiędzy wersjami

Wersja z 22:41, 29 paź 2015

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

   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) 

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:

1. 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.
2. 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).
3. W procesie analizy musimy korzystać z własności otoczenia np. z przemienności i łączności dodawania.
4. Musimy też sobie zadawać sprawę, że wielu podstawowych własności nie da się wyrazić formułami pierwszego rzędu.
5. 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:

1. Czy można podać aksjomaty i reguły wnioskowania, które opiszą semantykę operacyjną języka programowania?
2. Czy (i jakie) własności struktur danych (systemów algebraicznych) są wyrażalne w języku logiki algorytmicznej?
3. 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.

Pytania

Czy logika Hoare'a nie jest narzędziem lepszym od logiki algorytmicznej?

1. Po pierwsze, logika Hoare'a jest fragmentem logiki algorytmicznej. By się o tym przekonać wystarczy zaobserwować, że

a) "trójki" w rachunku Hoare'a czyli formuły postaci [math] \{\alpha\} K \{\beta\} [/math] wyrażają to samo co formuły logiki algorytmicznej postaci [math] (\alpha \land K\,\mathbb{1}) \Rightarrow K \beta [/math], tj. własność semantycznej częściowej poprawności programu [math]K[/math] względem warunku początkowego [math] \alpha [/math] i warunku końcowego [math] \beta [/math], ponadto

b) każda reguła rachunku Hoare's jest wywodliwa (posiada dowód) w logice algorytmicznej zob [LogProg2 ↓] str. 250-260.

2. Język logiki Hoare'a nie ma środków do wyrażania pozostałych ważnych praktycznie własności semantycznch programów np. stop, całkowita poprawność, równoważność, etc.

3. Istnieją próby zmodyfikowania logiki Hoare'a w taki sposób by można było formułować własność całkowitej poprawności i dowodzić jej. Zob. książka Apt, de Boer i Olderog. Zauważmy jednak, że przyjęte w tym celu reguły wnioskowania mają sens tylko w dziedzinach arytmetycznych (tj. takich w których prawdziwa jest własność Archimedesa), w wielu istotnych dla informatyki strukturach danych np. stosy, kolejki, drzewa, kopce, etc. podejście takie jest nie do powtórzenia.

4. Powyższe uwagi mozna wypowiedzieć nieco ogólniej, logika Hoare'a nie wydaje się dobrą podstawą do rozwijania teorii struktur danych i w związku z tym nie rokuje nadziei na zastosowanie w programowaniu obiektowym.

5. Relatywna pełność logiki Hoare'a - czy to jest potrzebne?

System Hoare'a reguł wnioskowania o częściowej poprawności programów zbudowanych z instrukcji przypisania przy pomocy trzech konstrukcji programistycznych: składanie, instrukcja warunkowa oraz instrukcja while iteracji powstał wykorzystując wcześniejsza pracę R.W. Floyda (1967) i nie był wolny od błędów. Błędy te Hoare usuwał i co ważniejsze pokazywał, ze jego system może być wykorzystywany w dowodach częściowej poprawności programów np. quicksort. Nasuwało się kolejne pytanie: czy każda trójka wyrażająca prawdziwą własnośc częściowej poprawności posiada dowód w tym systemie. Na to pytanie S. Cook udzielił odpowiedzi w tzw. twierdzeniu o relatywnej pełności logiki Hoare'a:

Zauwazmy, że parę lat wcześniej w pracy [Góraj, Mirkowska i Paluszkiewicz 1970 ↓] udowodniono własność pełności systemu Floyda (zmodyfikowanego przez autorki) Twierdzenie. Opis programu P jest akceptowalny w teorii T wtedy i tylko wtedy gdy opis ten jest dopuszczalny w każdym modelu tej teorii.

Tę sama treść zawiera twierdzenie udowodnione przez L. Banachowskiego [LB1] Warunek weryfikacyjny VC programu P jest twierdzeniem teorii T wtedy i tylko wtedy gdy jest formułą prawdziwą w każdym modelu teorii T.

Jak porównać te dwa twierdzenia z twierdzeniem Cooka o relatywnej pełności. Twierdzenie GMP mówi nam: jeśli znalazłeś właściwe formuły jako kandydatów na niezmienniki pętli to dowód częściowej poprawności sprowadza się do udowodnienia długiej koniunkcji formuł pierwsego rzędu.

Twierdzenie o relatywnej pełności ma nieco inną postać. Jeśli udowodnisz pewną liczbę formuł pierwszego rzędu to formuła wyrazająca własnośc częściowej poprawności posiada dowód.

Pozostają wątpliwości: rozpatrzmy algorytm Euklidesa. Jak wygląda dowód poprawności? (ROZWIŃ)

Co z logiką dynamiczną? Słyszałem, że teraz nie logika algorytmiczna lecz logika dynamiczna się liczy.

1. Autorzy książki Dynamic Logic uważają, że logika algorytmiczna jest logiką dynamiczną.

2. V. Pratt wynalazca logiki dynamicznej(1976) był zaskoczony gdy studenci pokazali mu prace z logiki algorytmicznej datujące się parę lat wcześniej.

3. Logika dynamiczna kładzie nacisk na niedeterminizm.

a) Oprócz zwykłych instrukcji przypisania postaci {x:=e}, język LD zawiera instrukcje niedeterministycznego wyboru {x:=?}. Odpowiedni aksjomat ma postać

[x:=?]φ ≡ ∀x φ

b) Instrukcja iteracji ma postać α* gdzie α jest programem.

c) Zauważ, że programy {x:=?} i {x:=0; (x:=x+1)*} są równoważne w tym sensie, że oba realizują niedeterministyczny wybór liczby naturalnej.

Obie te konstrukcje mogą być przydatne, w pewnym stopniu, do modelowania zjawisk zachodzących podczas obliczeń. Nie są jednak tożsame z programami. Dlaczego? Ponieważ nie istnieje żaden efektywny mechanizm, który gwarantowałby spełnienie jednocześnie dwu warunków: (i) nieograniczony wybór, i (ii) kończenie obliczeń. Argument ten podał E.W. Dijkstra w książce Umiejętność programowania, WNT, Warszawa,1985, str. 77-79.

Dla ciekawych: Intuicjonizm -- sposób uprawiania matematyki zapoczatkowany przez Brouwera -- nie zezwala na niekonstruktywne dowody zdań egzystencjalnych.

Podsumowując:

a) Język logiki dynamicznej dopuszcza jako programy pewne konstrukcje nieefektywne,

b) System logiki algorytmicznej cieszy się własnością pełności. Logika dynamiczna przez pewien czas zadowalała się twierdzeniem o tzw. arytmetycznej pełności. Dopiero po naszej krytyce w książce Dynamic Logic znalazł się system wzorowany na systemie aksjomatów i reguł wnioskowania G. Mirkowskiej [GM1].

c) Logika dynamiczna nie zajmuje się strukturami danych innymi niż standardowy system liczb naturalnych. Logika algorytmiczna jest systemem dedukcyjnym stosowanym w teoriach podstawowych struktur: algorytmiczna teoria stosów, algorytmiczna teoria kolejek FIFO, algorytmiczna teoria s łowników, algorytmiczna teoria kolejek priorytetowych, algorytmiczna teoria drzew binarnych, algorytmiczna teoria dzew BST binarnych poszukiwań, ...

d)

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.

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 i zwiększenia adresu.

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

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.

Artykuły

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.  W tej pracy zawarte jest twierdzenie. Niech P bedzie programem deterministycznym iteracyjnym. Niech o będzie odwzorowaniem przypisującym każdej krawedzi diagramu tego programu formułę pierwszego rzędu. Odwzorowanie to nazwiemy opisem programu P. Opis o jest twierdzeniem teorii T wtedy i tylko wtedy gdy jest dopuszczalny w każdym modelu tej teorii. Powyższe twierdzenie udowodniono wcześniej od tw. Cooka (1978) o relatywnej pełności logiki Hoare'a,
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”, 2009.