Rachunek programów: Różnice pomiędzy wersjami

Z Lem
Skocz do: nawigacji, wyszukiwania
Linia 8: Linia 8:
 
W poniższych schematach możesz znaki <math>K</math> i <math>M</math> zastąpić przez programy, a znaki <math>\alpha, \beta, \gamma</math> przez formuły.<br />
 
W poniższych schematach możesz znaki <math>K</math> i <math>M</math> zastąpić przez programy, a znaki <math>\alpha, \beta, \gamma</math> przez formuły.<br />
  
<math>K\,(\alpha \land \beta) \equiv (K\,\alpha \land K\,\beta) \,</math><br />
+
<math>\vdash K\,(\alpha \land \beta) \equiv (K\,\alpha \land K\,\beta) \,</math><br />
 
Program jest więc operatorem rozdzielnym z koniunkcja.<br />
 
Program jest więc operatorem rozdzielnym z koniunkcja.<br />
  
<math>\{\textbf{if }\gamma \textbf{ then }K \textbf{ else }M \textbf{ fi} \}\,\alpha \equiv ((\gamma \land K\,\alpha) \lor (\neg \gamma \land M\,\alpha)) </math><br />
+
<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><br />
 
Tu natomiast widzimy rozdzielnośc samego operatora '''if''' <br />
 
Tu natomiast widzimy rozdzielnośc samego operatora '''if''' <br />

Wersja z 21:47, 27 paź 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.
[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]

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]\alph[/math]. Rachunek programów jest splotem dwu algebr: algebry formuł i algebry programów. (zob. G. Mirkowska rozprawa doktorska 1972).
Przykłady
W poniższych schematach możesz znaki [math]K[/math] i [math]M[/math] zastąpić przez programy, a znaki [math]\alpha, \beta, \gamma[/math] przez formuły.

[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 rozdzielnośc samego operatora if