Rachunek programów

Termin rachunek programów wydaje się lepiej pasować do znanych pojęć: rachunek zdań i rachunek predykatów. Rachunek programów zawiera w sobie oba rachunki i ponadto pozwala dokonywać "rachunków" na programach. Jak to zobaczymy często dowody semantycznych własności programów przybieraja postać rachunków na formułach algorytmicznych.
Logikę algorytmiczną utożsamiać będziemy z rachunkiem programów.
[math]\qquad \mbox{Rachunek zdań} \subset \left [\begin{array}{l} \mathrm{Rachunek\ predykatów} \\czyli \\ \mathrm{Logika\ pierwszego\ rzędu}\end{array}\right ] \subset \left [\begin{array}{l}\mathrm{Rachunek\ programów}\\czyli \\ \mbox{Logika algorytmiczna} \end{array}\right ] [/math]

Nieformalne wprowadzenie

Każdy program można traktować jako operator modalności: formułę P [math]\alpha[/math], czytamy program P zakończył obliczenie i jego wyniki spełniają formułę [math]\alpha[/math]. Rachunek programów jest splotem dwu algebr: algebry formuł i algebry programów. (zob. G. Mirkowska rozprawa doktorska 1972).

Przykłady praw rachunku programów

W poniższych schematach rachunku programów możesz znaki [math]K[/math] i [math] M [/math] zastąpić przez programy, a znaki [math] \alpha, \beta, \gamma [/math] przez formuły.(Formuła [math] \gamma [/math] powinna nie zawierac kwantyfikatorów)

[math] \vdash K\,(\alpha \land \beta) \equiv (K\,\alpha \land K\,\beta) \, [/math]
Program jest więc operatorem rozdzielnym z koniunkcja.

[math] \vdash \{\textbf{if }\gamma \textbf{ then }K \textbf{ else }M \textbf{ fi} \}\,\alpha \equiv ((\gamma \land K\,\alpha) \lor (\neg \gamma \land M\,\alpha)) [/math]
Tu natomiast widzimy możliwość eliminacji operatora if
Operator iteracji while nie może być wyeliminowany w taki sposób
[math] \vdash \{\textbf{while }\gamma \textbf{ do }K \textbf{ od} \}\,\alpha \equiv ((\gamma \land \{K;\,\textbf{while }\gamma \textbf{ do }K \textbf{ od}\}\,\alpha) \lor (\neg \gamma \land \alpha)) [/math]
Operator while jest działaniem nieskończonym, podobnie jak kwantyfikatory. Można go opisać przy pomocy kwantyfikatora iteracji.
[math]\vdash \{\textbf{while }\gamma \textbf{ do }K \textbf{ od} \}\,\alpha \equiv \bigcup \{\textbf{if }\gamma \textbf{ then }K \textbf{ fi} \}\,(\neg \gamma \land \alpha) [/math]
Ponadto, każde prawo rachunku predykatów (a więc także każde prawo rachunku zdań) jest prawem rachunku programów.

Przykłady reguł wnioskowania

[math]\frac{\big\{\{\textbf{if }\gamma \textbf{ then }K \textbf{ fi} \}^i\,(\neg \gamma \land \alpha))\Rightarrow \beta \big\}_{i \in N}}{\big(\bigcup \{\textbf{if }\gamma \textbf{ then }K \textbf{ fi} \}\,(\neg \gamma \land \alpha)\big) \Rightarrow \beta }\ \ \ \ [/math] i [math]\ \ \ \ \ \frac{\big\{\{\textbf{if }\gamma \textbf{ then }K \textbf{ fi} \}^i\,(\neg \gamma \land \alpha))\Rightarrow \beta \big\}_{i \in N}} {\big( \{\textbf{while }\gamma \textbf{ do }K \textbf{ od} \}\,(\neg \gamma \land \alpha)\big) \Rightarrow \beta } [/math]
Obie te reguły wskazują na nieskończony charakter działań while oraz [math] \bigcup [/math].
Nie można nieskończonego zbioru przesłanek w tych regułach zastapić jakims skończonym jego podzbiorem.
AL nie cieszy się własnością zwartości!

Jakie własności programów można wyrazić w języku logiki algorytmicznej?

Najpierw rozpatrzmy klasę programów iteracyjnych, deterministycznych. Trudno przecenic jej znaczenie poniewaz każda funkcja obliczalna jest programowalna za pomocą pewnego programu z tej klasy.

Nieformalna gramatyka
Programy iteracyjne to najmniejszy zbiów napisów zawierający instrukcje przypisania i zamkniety ze względu na składania i iterację(while).

Semantykę takich programów opisujemy definiując pojęcie obliczenia.

Każdą własność semantyczną WS programu tzn. jego obliczeń można wyrazić za pomocą pewnej formuły algorytmicznej delta.
Oznacza to tyle, że własność WS zachodzi wtedy i tylko wtedy gdy formuła delta jest prawdziwa.

Przykłady.
...

Z kolei, zamiast badać prawdziwość formuły delta możemy podjąć się jej udowodnienia. Jeśli to się nam uda to możemy być pewni, że badany program ma własność semantyczną WS.

Przykłady

Czy ten rachunek programów nie zawiera błędnych reguł wnioskowania? fałszywych aksjomatów?

Na to pytanie łatwo odpowiedzieć. Każdy aksjomat logiki algorytmicznej jest tautologia. Każda reguła wnioskowania jest poprawna tzn. z prawdziwych przesłanek reguła wyprowadza prawdziwe wnioski. Nie ma więc mozliwości wyprowadzenia sprzecznych wniosków.

Czy ten rachunek jest kompletny?

To jest istotne pytanie. Cóż nam po rachunku, który byłby niekompletny? Śpieszymy uspokoic czytelnika, że rachunek programów jest pełny tzn. każda prawdziwa semantycznie formuła posiada dowód.