Rachunek programów - Historia wersji

AndrzejSalwicki: /* Przykłady reguł wnioskowania */

2019-12-06T10:32:48Z

‎Przykłady reguł wnioskowania

AndrzejSalwicki: /* Przykłady reguł wnioskowania */

2016-03-06T02:21:31Z

‎Przykłady reguł wnioskowania

AndrzejSalwicki: /* Przykłady reguł wnioskowania */

2016-03-06T02:20:42Z

‎Przykłady reguł wnioskowania

AndrzejSalwicki: /* Przykłady reguł wnioskowania */

2016-03-06T02:19:51Z

‎Przykłady reguł wnioskowania

AndrzejSalwicki: /* Przykłady praw rachunku programów */

2015-11-19T15:40:59Z

‎Przykłady praw rachunku programów

AndrzejSalwicki: /* Przykłady reguł wnioskowania */

2015-11-19T08:24:24Z

‎Przykłady reguł wnioskowania

AndrzejSalwicki: /* Nieformalne wprowadzenie */

2015-11-17T09:06:50Z

‎Nieformalne wprowadzenie

AndrzejSalwicki: /* Nieformalne wprowadzenie */

2015-11-17T09:05:49Z

‎Nieformalne wprowadzenie

AndrzejSalwicki o 09:02, 17 lis 2015

2015-11-17T09:02:44Z

AndrzejSalwicki: /* Przykłady praw rachunku programów */

2015-11-17T08:59:14Z

‎Przykłady praw rachunku programów

@@ Linia 27: / Linia 27: @@
 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!
+'''Twierdzenie''' Rachunek programów AL nie cieszy się własnością zwartości!<br />
 [[inference rules|Komplet podstawowych reguł wnioskowania logiki algorytmicznej]]

@@ Linia 27: / Linia 27: @@
 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!
+'''Twierdzenie''' Rachunek programów AL nie cieszy się własnością zwartości!
 [[inference rules|Komplet podstawowych reguł wnioskowania logiki algorytmicznej]]

@@ Linia 27: / Linia 27: @@
 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!
+===Twierdzenie=== Rachunek programów AL nie cieszy się własnością zwartości!
 [[inference rules|Komplet podstawowych reguł wnioskowania logiki algorytmicznej]]

@@ Linia 25: / Linia 25: @@
 <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>.<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 zastapić jakims skończonym jego podzbiorem. <br />
+Nie można nieskończonego zbioru przesłanek w tych regułach zastąpić jakimś skończonym jego podzbiorem. <br />
-AL nie cieszy się własnością zwartości!
+---Twierdzenie--- Rachunek programów AL nie cieszy się własnością zwartości!
 [[inference rules|Komplet podstawowych reguł wnioskowania logiki algorytmicznej]]

@@ Linia 18: / Linia 18: @@
 <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 />
 === Przykłady reguł wnioskowania ===

@@ Linia 4: / Linia 4: @@
 <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 P 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 />
+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 />

@@ 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 />
 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łę 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).<br />