Rachunek programów: Różnice pomiędzy wersjami
Linia 24: | Linia 24: | ||
<math>\ \ \ \ \ \frac{\big\{\{\textbf{if }\gamma \textbf{ then }K \textbf{ fi} \}^i\,(\neg \gamma \land \alpha))\Rightarrow \beta \big\}_{i \in N}} | <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><br /> | {\big( \{\textbf{while }\gamma \textbf{ do }K \textbf{ od} \}\,(\neg \gamma \land \alpha)\big) \Rightarrow \beta } </math><br /> | ||
− | Obie te reguły wskazują na nieskończony charakter działań '''while''' oraz <math> \bigcup </math>. Nie można nieskończonego | + | 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! |
Wersja z 20:58, 2 lis 2015
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.
Rachunek zdań⊂[Rachunek predykatówczyliLogika pierwszego rzędu]⊂[Rachunek programówczyliLogika algorytmiczna]
Każdy program można traktować jako operator modalności: formułę P α, czytamy program P zakończył obliczenie i jego wyniki spełniają formułę \alph. 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 K i M zastąpić przez programy, a znaki α,β,γ przez formuły.(Formuła γ powinna nie zawierac kwantyfikatorów)
⊢K(α∧β)≡(Kα∧Kβ)
Program jest więc operatorem rozdzielnym z koniunkcja.
⊢{if γ then K else M fi}α≡((γ∧Kα)∨(¬γ∧Mα))
Tu natomiast widzimy możliwość eliminacji operatora if
Operator iteracji while nie może być wyeliminowany w taki sposób
⊢{while γ do K od}α≡((γ∧{K;while γ do K od}α)∨(¬γ∧α))
Operator while jest działaniem nieskończonym, podobnie jak kwantyfikatory. Można go opisać przy pomocy kwantyfikatora iteracji.
⊢{while γ do K od}α≡⋃{if γ then K fi}(¬γ∧α)
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.
{{if γ then K fi}i(¬γ∧α))⇒β}i∈N(⋃{if γ then K fi}(¬γ∧α))⇒β
i
{{if γ then K fi}i(¬γ∧α))⇒β}i∈N({while γ do K od}(¬γ∧α))⇒β
Obie te reguły wskazują na nieskończony charakter działań while oraz ⋃. 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!