Stosy - struktura algebraiczna: Różnice pomiędzy wersjami
| Linia 6: | Linia 6: | ||
<math>w\colon E \times S \rightarrow S </math><br /> | <math>w\colon E \times S \rightarrow S </math><br /> | ||
<math>u\colon S \rightarrow S </math><br /> | <math>u\colon S \rightarrow S </math><br /> | ||
| − | <math> | + | <math>n\colon S \rightarrow E </math><br /> |
<math>e\colon S \rightarrow \{true, false\}</math><br /> | <math>e\colon S \rightarrow \{true, false\}</math><br /> | ||
<math>=_E \colon E \times E \rightarrow \{true, false\} </math><br /> | <math>=_E \colon E \times E \rightarrow \{true, false\} </math><br /> | ||
| − | + | <math>=_S \colon S \times S \rightarrow \{true, false\} </math><br /> | |
| − | <math>\forall_{e \in E}\,\forall_{s \in S} \lnot e(w(e,s)) </math><br /> | + | które zapewniają prawdziwość następującego zbioru aksjomatów <br /> |
| + | <math>\forall_{e \in E}\,\forall_{s \in S} \lnot n(w(e,s)) </math><br /> | ||
| + | <math>\forall_{e \in E}\,\forall_{s \in S} p(w(e,s)) =_E e </math><br /> | ||
| + | <math>\forall_{e \in E}\,\forall_{s \in S} u(w(e,s)) =_S s </math><br /> | ||
| + | <math>\forall_{e \in E}\,\forall_{s \in S} \lnot n(s) \implies w(p(s),u(s)) =_S s </math><br /> | ||
| + | <math>\forall_{s \in S} \{'''while'''\ \lnot n(s) \ do \ s:= u(s) \ od\}\<n(s)</math> | ||
Wersja z 09:20, 12 mar 2017
Stosy to struktura algebraiczna znajdująca wiele zastosowań w informatyce.
Definicja
Struktura algebraiczna
której uniwersum jest sumą dwu rozłącznych zbiorów [math]E[/math] i [math]S[/math], z działaniami
[math]w\colon E \times S \rightarrow S [/math]
[math]u\colon S \rightarrow S [/math]
[math]n\colon S \rightarrow E [/math]
[math]e\colon S \rightarrow \{true, false\}[/math]
[math]=_E \colon E \times E \rightarrow \{true, false\} [/math]
[math]=_S \colon S \times S \rightarrow \{true, false\} [/math]
które zapewniają prawdziwość następującego zbioru aksjomatów
[math]\forall_{e \in E}\,\forall_{s \in S} \lnot n(w(e,s)) [/math]
[math]\forall_{e \in E}\,\forall_{s \in S} p(w(e,s)) =_E e [/math]
[math]\forall_{e \in E}\,\forall_{s \in S} u(w(e,s)) =_S s [/math]
[math]\forall_{e \in E}\,\forall_{s \in S} \lnot n(s) \implies w(p(s),u(s)) =_S s [/math]
[math]\forall_{s \in S} \{'''while'''\ \lnot n(s) \ do \ s:= u(s) \ od\}\\ltn(s)[/math]
