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

Z Lem
Skocz do: nawigacji, wyszukiwania
(→‎Przykłady reguł wnioskowania)
 
(Nie pokazano 27 pośrednich wersji utworzonych przez tego samego użytkownika)
Linia 2: Linia 2:
 
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. <br />
 
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. <br />
 
Logikę algorytmiczną utożsamiać będziemy z rachunkiem programów.<br />
 
Logikę algorytmiczną utożsamiać będziemy z rachunkiem programów.<br />
−
<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><br />
+
<span style="color: Brown"><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></span><br />
 +
== Nieformalne wprowadzenie ==
 +
Każdy program można traktować jako operator modalności: ''formułę <span style="color: Blue"><math>P\alpha</math></span>, czytamy program <span style="color: Blue"><math>P</math></span> zakończył obliczenie i jego wyniki spełniają formułę <span style="color: Blue"><math>\alpha</math></span>.'' Rachunek programów jest splotem dwu algebr: algebry formuł i algebry programów. (zob. G. Mirkowska rozprawa doktorska 1972).<br />
 +
=== '''Przykłady''' praw rachunku programów ===
 +
W poniższych schematach rachunku programów możesz znaki  <span style="color: Blue"><math>K</math></span>  i <span style="color: Blue"><math> M </math></span> zastąpić przez programy, a znaki <span style="color: Blue"><math> \alpha, \beta, \gamma </math></span> przez formuły.(Formuła <math> \gamma </math>  powinna nie zawierać kwantyfikatorów)<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 />
+
<span style="color: Blue"><math> \vdash K\,(\alpha \land \beta) \equiv (K\,\alpha \land K\,\beta) \, </math></span><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 />
+
−
 
+
−
<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>\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 />
+
<span style="color: Blue"><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></span><br />
 
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 \land \alpha)) </math><br />
+
<span style="color: Blue"><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></span><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 />
+
<span style="color: Blue"><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></span><br />
 
Ponadto, każde prawo rachunku predykatów (a więc także każde prawo rachunku zdań) jest prawem rachunku programów.<br />
 
Ponadto, każde prawo rachunku predykatów (a więc także każde prawo rachunku zdań) jest prawem rachunku programów.<br />
 +
[[Axioms of algorithmic logic |Aksjomaty AL]]
 +
 +
=== Przykłady reguł wnioskowania ===
 +
<span style="color: Blue"><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></span>     
 +
i   
 +
<span style="color: Blue"><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></span><br />
 +
Obie te reguły wskazują na nieskończony charakter działań '''while''' oraz <math> \bigcup </math> kwantyfikatora iteracji.<br />
 +
Nie można nieskończonego zbioru przesłanek w tych regułach zastąpić jakimś skończonym jego podzbiorem. <br />
 +
'''Twierdzenie''' Rachunek programów AL nie cieszy się własnością zwartości!<br />
 +
Sens tego twierdzenia sprowadza się do stwierdzenia, że w wyżej przytoczonych regułach wnioskowania nie można zastąpić nieskończonego zbioru przesłanek przez jakiś skończony zbiór.<br />
 +
Przypomnijmy, że rachunek predykatów posiada własność zwartości. Jeśli jakieś zdanie jest logiczną konskwencją nieskończonego zbioru zdań to jest logiczną konsekwencją pewnego skończonego podzbioru tego zbioru.<br />
 +
 +
Poniżej znajdziesz
 +
[[inference rules|Komplet podstawowych reguł wnioskowania logiki algorytmicznej]]
 +
 +
=== 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 <br />
 +
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.<br />Oznacza to tyle, że własność WS zachodzi wtedy i tylko wtedy gdy formuła delta jest prawdziwa.
 +
 +
Przykłady.<br />
 +
... <br>
 +
 +
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
 +
 +
=== Przykłady dowodów ===
 +
 +
=== 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.
  
−
Przykład reguły wnioskowania.<br />
+
=== Czy ten rachunek jest kompletny? ===
−
<math>\frac{\{\{\textbf{if }\gamma \textbf{ then }K  \textbf{ fi} \}^i\,(\neg \gamma \land \alpha))\Rightarrow \beta\}_{i \in N}}{\big(\bigcup \{\textbf{if }\gamma \textbf{ then }K  \textbf{ fi} \}\,(\neg \gamma \land \alpha)\big) \Rightarrow \beta } </math>
+
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.

Aktualna wersja na dzień 11:32, 6 gru 2019

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łę [math]P\alpha[/math], czytamy program [math]P[/math] 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 zawierać 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.
Aksjomaty AL

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] kwantyfikatora iteracji.
Nie można nieskończonego zbioru przesłanek w tych regułach zastąpić jakimś skończonym jego podzbiorem.
Twierdzenie Rachunek programów AL nie cieszy się własnością zwartości!
Sens tego twierdzenia sprowadza się do stwierdzenia, że w wyżej przytoczonych regułach wnioskowania nie można zastąpić nieskończonego zbioru przesłanek przez jakiś skończony zbiór.
Przypomnijmy, że rachunek predykatów posiada własność zwartości. Jeśli jakieś zdanie jest logiczną konskwencją nieskończonego zbioru zdań to jest logiczną konsekwencją pewnego skończonego podzbioru tego zbioru.

Poniżej znajdziesz Komplet podstawowych reguł wnioskowania logiki algorytmicznej

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

Przykłady dowodów

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.

Źródło „http://lem12.uksw.edu.pl/index.php?title=Rachunek_programów&oldid=2705”