Logika algorytmiczna

Logika algorytmiczna – rachunek logiczny, ale także rachunek programów. Każdy program możemy rozpatrywać jako modalność. Jeśli ${\displaystyle K}$ jest programem, a ${\displaystyle \alpha }$ jest formułą, to wyrażenie postaci ${\displaystyle 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 ${\displaystyle K\alpha }$ jest wyznaczone gdy znamy znaczenie (tj. semantykę) programu ${\displaystyle K}$ i znaczenie formuły ${\displaystyle \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 ${\displaystyle K\alpha }$ możemy opisać w następujący sposób: dla danego wartościowania zmiennych ${\displaystyle v}$ należy najpierw wyznaczyć wynik ${\displaystyle v'}$ obliczenia programu ${\displaystyle K}$ i z kolei obliczyć wartość formuły ${\displaystyle \alpha }$ dla wartościowania ${\displaystyle v'.}$ W przypadku gdy obliczenie programu ${\displaystyle K}$ dla wartościowania ${\displaystyle v}$ nie daje wyniku, przyjmujemy, że wartością formuły ${\displaystyle 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 ${\displaystyle P}$ jest poprawny względem warunku początkowego ${\displaystyle \alpha }$ i warunku końcowego ${\displaystyle \beta .}$ Formuła taka ma postać implikacji ${\displaystyle (\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].