Rachunek programów: Różnice pomiędzy wersjami
| Linia 5: | Linia 5: | ||
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).<br /> | 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).<br /> | ||
| − | '''Przykłady'''<br /> | + | '''Przykłady''' praw rachunku programów<br /> |
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)<br /> | 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)<br /> | ||
| Linia 14: | Linia 14: | ||
Tu natomiast widzimy możliwość eliminacji operatora '''if''' <br /> | Tu natomiast widzimy możliwość eliminacji operatora '''if''' <br /> | ||
Operator iteracji '''while''' nie może być wyeliminowany w taki sposób <br /> | Operator iteracji '''while''' nie może być wyeliminowany w taki sposób <br /> | ||
| − | <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 \alpha)) </math><br /> | + | <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><br /> |
Operator while jest działaniem nieskończonym, podobnie jak kwantyfikatory. Można go opisać przy pomocy ''kwantyfikatora iteracji.<br /> | Operator while jest działaniem nieskończonym, podobnie jak kwantyfikatory. Można go opisać przy pomocy ''kwantyfikatora iteracji.<br /> | ||
<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><br /> | <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><br /> | ||
| + | Ponadto, każde prawo rachunku predykatów (a więc także każde prawo rachunku zdań) jest prawem rachunku programów. | ||
| + | Przykład reguły wnioskowania.<br /> | ||
| + | <math>\frac{\{\{\textbf{if }\gamma \textbf{ then }K \textbf{ fi} \}^i\,(\neg \gamma \land \alpha))\Rightarrow \beta\}_{i \in N}}{(\bigcup \{\textbf{if }\gamma \textbf{ then }K \textbf{ fi} \}\,(\neg \gamma \land \alpha)) \Rightarrow \beta } </math> | ||
Wersja z 08:35, 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.
[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 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ład reguły wnioskowania.
[math]\frac{\{\{\textbf{if }\gamma \textbf{ then }K \textbf{ fi} \}^i\,(\neg \gamma \land \alpha))\Rightarrow \beta\}_{i \in N}}{(\bigcup \{\textbf{if }\gamma \textbf{ then }K \textbf{ fi} \}\,(\neg \gamma \land \alpha)) \Rightarrow \beta } [/math]
