Logika algorytmiczna

Logika algorytmiczna – rachunek logiczny, ale także rachunek programów. Każdy program możemy rozpatrywać jako modalność. Jeśli $K$ jest programem, a $\alpha$ jest formułą, to wyrażenie postaci $K\alpha$ jest formułą algorytmiczną. W ten sposób mamy do czynienia ze splotem dwu algebr: algebry Boole’a i algebry programów. Znaczenie formuły $K\alpha$ jest wyznaczone gdy znamy znaczenie (tj. semantykę) programu $K$ i znaczenie formuły $\alpha .$ Przypomnijmy, że znaczeniem formuły (pierwszego rzędu) jest funkcja ze zbioru wartościowań zmiennych w zbiór {true, false} wartości logicznych. Znaczeniem programu jest funkcja (częściowa) ze zbioru wartościowań w ten sam zbiór. Teraz znaczenie formuły $K\alpha$ możemy opisać w następujący sposób: dla danego wartościowania zmiennych $v$ należy najpierw wyznaczyć wynik $v'$ obliczenia programu $K$ i z kolei obliczyć wartość formuły $\alpha$ dla wartościowania $v'.$ W przypadku gdy obliczenie programu $K$ dla wartościowania $v$ nie daje wyniku, przyjmujemy, że wartością formuły $K\alpha$ jest false.

W języku logiki algorytmicznej można wyrażać semantyczne własności programów. Aksjomaty i reguły wnioskowania AL pozwalają na dowodzenie prawdziwych (semantycznie) formuł algorytmicznych. Oznacza to, że uzyskujemy możliwość dowodzenia faktów postaci: ten program $P$ jest poprawny względem warunku początkowego $\alpha$ i warunku końcowego $\beta .$ Formuła taka ma postać implikacji $(\alpha \Rightarrow P\,\beta ).$

Zastosowania AL

• w inżynierii oprogramowania możemy zapisywać specyfikacje oprogramowania i dokonywać weryfikacji poprzez dowody [Mirkowska Salwicki 1987 ↓ ],
• w projektowaniu języków programowania można opisać semantykę języka, podając odpowiednie aksjomaty i reguły wnioskowania,
• w opisie abstrakcyjnych struktur danych (co łączy się ze specyfikowaniem klas w językach programowania obiektowego) formuły algorytmiczne pozwalają w pełni scharakteryzować pewne struktury i klasy struktur.

Język określa się, podając jego alfabet i zbiór wyrażeń poprawnie zbudowanych WFF. W zbiorze wyrażeń poprawnie zbudowanych wyróżniamy trzy podzbiory: zbiór termów (albo zbiór wyrażeń nazwowych), zbiór formuł (zbiór wyrażeń logicznych) i zbiór programów (algorytmów).

Język logiki algorytmicznej jest konwolucją języka logiki pierwszego rzędu i języka programów.

Bibliografia

• Grażyna Mirkowska, Andrzej Salwicki: Algorithmic Logic. Warszawa: PWN, 1987, s. 345.
• Grażyna Mirkowska, Andrzej Salwicki: Logika Algorytmiczna dla Programistów cz. 1. Warszawa: WNT, 1992, s. 294.
• Grażyna Mirkowska, Andrzej Salwicki: Logika Algorytmiczna dla Programistów cz. 2. Warszawa: WNT, 1992, s. 294.
• 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.
• Helena Rasiowa: Algorithmic Logic – Notes from Seminar in Simon Fraser University. T. 281. Warsaw: 1975, seria: Reports of Institute of Computer Science Polish Academy of Sciences.
• repozytorium logiki algorytmicznej. 2013. [dostęp 2018-10-07].