Definíciók és tételek

1. Felhasznált matematikai fogalmak

Jelölés

1. ℕ: a természetes számok halmaza, ℤ: az egész számok halmaza

2. 𝕃: a logikai értékek halmaza, 𝕃 =^{def} { igaz, hamis }

3. véges sorozat: α = < α_{1},…, α_{n} >, értelmezési tartománya: D_{α} = {1,…, n}

4. az α =< α_{1},…, α_{n} > véges sorozat hossza: |α| = n

5. végtelen sorozat: α = < α_{1},… >, értelmezési tartománya: D_{α} = ℕ

6. az A halmaz elemeiből képzett véges sorozatok halmaza: A^{∗}

7. az A halmaz elemeiből képzett végtelen sorozatok halmaza: A^{∞}

8. az A halmaz elemeiből képzett véges és végtelen sorozatok halmaza: A^{∗∗}

Definíció

1. az α ∈ A^{∗} és a β ∈ A^{∗∗} sorozatok konkatenáltja: kon(α, β) =^{def} < α_{1},…, α_{n}, β_{1} … >, ahol n = |α|

2. Legyen α^{1}, α^{2},…, α^{n−1} ∈ A^{∗}, α^{n} ∈ A^{∗∗}. kon(α^{1},…, α^{n}) = kon(α^{1}, kon(α^{2},…, α^{n}))

3. Az α ∈ A^{∗∗} redukáltjának nevezzük, és red(α)-val jelöljük azt a sorozatot, amit úgy kapunk, hogy az α minden azonos elemekből álló véges részsorozatát a részsorozat egyetlen elemével helyettesítjük.

4. Legyen α^{1}, α^{2},…, α^{n−1} ∈ A^{∗}, α^{n} ∈ A^{∗∗}. χ_{n}(α^{1},…, α^{n}) =^{def} red(kon(α^{1},…, α^{n}))

5. Legyen α^{i} ∈ A^{∗} (i ∈ ℕ). χ_{∞}(α^{1}, α^{2},…) =^{def} red(kon(α^{1}, α^{2},…)

6. Ha α =< α_{1},…, α_{n} >∈ A^{∗}, akkor τ(α) =^{def} α_{n}

7. Legyen I = {i_{1}, i_{2},…, i_{n}} ⊂ ℕ. Legyen A_{i} tetszőleges halmaz (i ∈ I).

×_{i∈I}^{n} A_{i} =^{def} A_{i_{1}} × … × A_{i_{n}} =^{def} {(a_{i_{1}}, a_{i_{2}},…, a_{i_{n}}) | a_{i_{j}} ∈ A_{i_{j}} ∧ i_{j} ∈ I}, ahol

i_{1} < i_{2} < … < i_{n}.

8. Legyen I = {i_{1}, i_{2},…, i_{n}} ⊂ ℕ, J = {j_{1}, j_{2},…, j_{m}} ⊂ ℕ (m, n ∈ ℕ).

A = ×_{k=1}^{n} A_{i_{k}}, B = ×_{k=1}^{m} A_{j_{k}}. A B halmaz az A halmaz altere, ha J ⊆ I.

9. Legyen I = {i_{1}, i_{2},…, i_{n}} ⊂ ℕ, J = {j_{1}, j_{2},…, j_{m}} ⊂ ℕ (m, n ∈ ℕ, m < n). A = ×_{k=1}^{n} A_{i_{k}}, B = ×_{k=1}^{m} A_{j_{k}}. A B tér kiegészítő altere az A-ra: B′ =^{def} ×_{k∈(I\J)} A_{k}.

10. Legyen a ∈ A és B altere A-nak a J = {j_{1}, j_{2},…, j_{m}} ⊂ ℕ indexhalmazzal. Ekkor a-nak a B-re vett projekciója

pr_{B}(a) =^{def} (a_{j_{1}}, a_{j_{2}},…, a_{j_{m}}).

11. Legyen B altér A-ban és legyen B′ a B kiegészítő altere A-hoz. ”⊗” bináris művelet: ⊗ : B × B′ → A. Tetszőleges b ∈ B és b′ ∈ B′ esetén b ⊗ b′ A azon eleme, amelyre pr_{B}(b ⊗ b′) = b és pr_{B′}(b ⊗ b′) = b′.

12. Legyen α ∈ A^{∗∗}. pr_{B}(α) =^{def} < pr_{B}(α_{1}), pr_{B}(α_{2}),… >∈ B^{∗∗}.

13. Legyen R ⊆ C × D, A altere C-nek, B altere D-nek.

pr_{A×B}(R) =^{def} {(pr_{A}(c), pr_{B}(d)) | (c, d) ∈ R}.

14. Legyen R ⊆ A × A, B altere A-nak. pr_{B}(R) =^{def} pr_{B×B}(R).

15. Legyen R ⊆ A × A^{∗∗}, B altere A-nak. pr_{B}(R) =^{def} pr_{B×B^{∗∗}}(R).

16. Az R ⊆ A × B halmazt bináris relációnak nevezzük.

17. Az R ⊆ A × B reláció képe a ∈ A pontban: R(a) =^{def} {b ∈ B | (a, b) ∈ R}.

18. Az R ⊆ A×B reláció képe H ⊆ A halmazon: R(H) =^{def} {b ∈ B | ∃a ∈ H : (a, b) ∈ R}.

19. Az R ⊆ A × B reláció értelmezési tartománya: D_{R} =^{def} {a ∈ A | ∃b ∈ B : (a, b) ∈ R}.

20. Az R ⊆ A × B reláció értékkészlete: R_{R} =^{def} {b ∈ B | ∃a ∈ A : (a, b) ∈ R}.

21. Az R ⊆ A × B reláció determinisztikus reláció (parciális függvény), ha ∀a ∈ D_{R} : |R(a)| = 1.

22. Az R ⊆ A × B reláció függvény, ha R parciális függvény és D_{R} = A.

23. Az R ⊆ A × B reláció inverze: R^{(−1)} =^{def} {(b, a) ∈ B × A | (a, b) ∈ R}.

24. A H ⊆ B halmaz R ⊆ A × B reláció szerinti inverz képe:

R^{(−1)}(H) =^{def} {a ∈ A | ∃h ∈ H : (a, h) ∈ R}.

25. Az R ⊆ A × B reláció komplementere: \overline{R} =^{def} \{(a, b) ∈ A × B | (a, b) ∉ R\}.

26. Az R_{1} ⊆ A × B és az R_{2} ⊆ B × C relációk kompozicíója:

R_{2} ∘ R_{1} =^{def} {(a, c) ∈ A × C | ∃b ∈ B : (a, b) ∈ R_{1} ∧ (b, c) ∈ R_{2}}.

27. Az R_{1} ⊆ A × B és az R_{2} ⊆ B × C relációk szigorú kompozíciója:

R_{2} ⊙ R_{1} =^{def} {(a, c) ∈ A × C | R_{1}(a) ⊆ D_{R_{2}} ∧ ∃b ∈ B : (a, b) ∈ R_{1} ∧ (b, c) ∈ R_{2}}.

28. R ⊆ A × A. id_{A} =^{def} R^{0} =^{def} {(a, a) ∈ A × A}.

29. Az R ⊆ A × A reláció n. hatványa: R^{n} =^{def} R ∘ R^{n−1} (n ∈ ℕ).

30. A H ⊆ B halmaz R ⊆ A × B reláció szerinti ősképe:

R^{−1}(H) =^{def} {a ∈ A | R(a) ⊆ H ∧ R(a) ≠ ∅}.

31. Az R ⊆ A × A reláció α_{0} ∈ A kezdőpontú, véges pontláncainak halmaza:

L_{R}(α_{0}) =^{def} {< α_{0}, α_{1},…, α_{q} >∈ A^{∗} | q ∈ ℕ_{0} ∧ ∀i ∈ [1, q] : α_{i} ∈ R(α_{i−1}) ∧ α_{q} ∉ D_{R}}.

32. Az R ⊆ A × A reláció α_{0} ∈ A kezdőpontú végtelen pontláncainak halmaza:

L_{R}^{∞}(α_{0}) =^{def} {< α_{0}, α_{1},… >∈ A^{∞} | ∀i ∈ ℕ : α_{i} ∈ R(α_{i−1})}.

33. Az R ⊆ A × A reláció lezártja:

D\overline{R} =^{def} \{a ∈ A | L_{R}^{∞}(a) = ∅\} és ∀a ∈ D\overline{R} : \overline{R}(a) =^{def} \{τ(α) | α ∈ L_{R}(a)\}.

34. Az R ⊆ A × A reláció korlátos lezártja:

D\overline{\overline{R}} =^{def} \{a ∈ A | L_{R}^{∞}(a) = ∅ ∧ ∃n_{a} ∈ ℕ : ∀α ∈ L_{R}(a) : |α| ≤ n_{a}\} és

∀a ∈ D\overline{\overline{R}} : \overline{\overline{R(a)}} =^{def} \{τ(α) | α ∈ L_{R}(a)\}.

35. Az f ⊆ A × 𝕃 reláció logikai függvény (állítás), ha függvény.

36. Az f logikai függvény igazsághalmaza: [f] =^{def} {a ∈ A | f(a) = igaz}.

37. A H ⊆ A halmaz indikátorfüggvénye: P (H) : A → 𝕃, P (H)(a) =^{def} a ∈ H (a ∈ A).

38. Az R ⊆ A × 𝕃 reláció igazsághalmaza: [R] =^{def} R^{−1}({ igaz }).

39. Legyen R ⊆ A × B, H ⊆ A. Az R reláció leszűkítése a H halmazra:

R|_{H} =^{def} (R ∩ (H × B)).

40. Legyen R ⊆ A × A és π : A → 𝕃. Az R reláció megszorítása a π feltételre:

R|_{π} =^{def} (R ∩ ([π] × A)) ∪ {(a, a) ∈ A × A | a ∈ [π] \ D_{R}}.

Megjegyzés: R|_{π} ≠ R|_{[π]}!

41. \overline{R|_{π}} az R reláció π feltételre vonatkozó lezártja, \overline{\overline{R|_{π}}} az R reláció π feltételre vonatkozó korlátos lezártja.

Állítás

1. [f] = f^{−1}({ igaz }).

2. Ha ∀n ∈ ℕ : |A| > n, akkor ∃R ⊆ A × A : \overline{R} ≠ \overline{\overline{R}}.

2. Alapvető definíciók és tételek

Definíció

1. Legyen n ∈ ℕ és A_{1},…, A_{n} tetszőleges halmaz. Az A =^{def} A_{1} × … × A_{n} halmazt állapottérnek, az A_{i} halmazokat típusértékhalmazoknak nevezzük.

2. Az állapottér elemeit (az a = (a_{1},…, a_{n}) ∈ A pontokat) állapotoknak nevezzük.

3. Az a_{i} : A → A_{i} projekciókat változóknak nevezzük (i = 1,…, n).

4. Az F ⊆ A × A relációt feladatnak nevezzük.

5. Az S ⊆ A × A^{∗∗} relációt programnak nevezzük, ha 1. D_{S} = A

2. ∀a ∈ A : ∀α ∈ S(a) : α_{1} = a

3. ∀α ∈ R_{S} : α = red(α)

6. Legyen S ⊆ A × A^{∗∗} program. A p(S) ⊆ A × A relációt, amelyre 1. D_{p(S)} = {a ∈ A | S(a) ⊆ A^{∗}}

2. ∀a ∈ D_{p(S)} : p(S)(a) = {b ∈ A | ∃α ∈ S(a) : τ(α) = b} az S program programfüggvényének nevezzük.

7. Az S ⊆ A × A^{∗∗} program megoldja az F ⊆ A × A feladatot, ha 1. D_{F} ⊆ D_{p(S)}

2. ∀a ∈ D_{F} : p(S)(a) ⊆ F (a).

8. S_{1}, S_{2} ⊆ A × A^{∗∗} programok. S_{1} és S_{2} ekvivalensek, ha p(S_{1}) = p(S_{2}).

9. Legyen B altere az A állapottérnek. Az F ⊆ B × B feladat kiterjesztése az A térre: F′ = {(a_{1}, a_{2}) ∈ A × A | (pr_{B}(a_{1}), pr_{B}(a_{2})) ∈ F }.

10. Legyen B altere az A állapottérnek, B′ a B altér kiegészítő altere az A-ra. Az S ⊆ B × B^{∗∗} program kiterjesztése A-ra: S′ = {(a, α) ∈ A × A^{∗∗} | (pr_{B}(a), pr_{B}(α)) ∈ S ∧ ∀i ∈ D_{α} : pr_{B′}(α_{i}) = pr_{B′}(a)}.

11. Legyen B közös altere A_{1}-nek és A_{2}-nek. S_{1} program A_{1}-en, S_{2} program A_{2}-n. S_{1} és S_{2} ekvivalensek B-n, ha pr_{B}(p(S_{1})) = pr_{B}(p(S_{2})).

12. Legyen B altere A-nak. A G ⊆ A × A feladat vetítéstartó a B altér felett, ha minden a_{1}, a_{2} ∈ D_{G}-re: ha pr_{B}(a_{1}) = pr_{B}(a_{2}) akkor pr_{B}(G(a_{1})) = pr_{B}(G(a_{2})).

13. Legyen B altere A-nak és legyen B′ kiegészítő altér B-hez A-ban. A G ⊆ A×A feladat bővített identitás a B altér és a B′ kiegészítő altér felett, ha minden (a_{1}, a_{2}) ∈ G esetén (a_{1}, a_{3}) ∈ G is teljesül, ahol pr_{B}(a_{3}) = pr_{B}(a_{2}) és pr_{B′}(a_{3}) = pr_{B′}(a_{1}).

Állítás

Legyen B altere A-nak, B′ B kiegészítő altere A-ra, S program B-n, F ⊆ B×B feladat, S′ illetve F′ S-nek, illetve F -nek kiterjesztése A-ra, \overline{S} ⊆ A × A^{∗∗} S-sel ekvivalens program B-n, \overline{F} ⊆ A × A feladat és F = pr_{B}(\overline{F}).

1. S′ megoldja F′-t akkor és csak akkor, ha S megoldja F -et.

Bizonyítás

Tekintettel arra, hogy S′ ekvivalens S-sel B-n, pr_{B}(F′) = F, valamint F′ vetítéstartó B felett és bővített identitás B és B′ felett, ezért a tétel állítása következik a a változó bevezetésének tétele és a részfeladat kiválasztásának tételé-ből.

2. Ha \overline{S} megoldja F′-t, akkor S megoldja F -et (a változó bevezetésének tétele).

Bizonyítás

Először belátjuk, hogy D_{F} ⊆ D_{p(S)}. Legyen a ∈ D_{F} tetszőleges. Ekkor D_{F} definíciójából következik, hogy van olyan b ∈ B, amelyre (a, b) ∈ F. pr_{B}(F′) = F miatt van olyan \overline{a}, \overline{b} ∈ A, amelyre (\overline{a}, \overline{b}) ∈ F′ és pr_{B}(\overline{a}) = a és pr_{B}(\overline{b}) = b. (\overline{a}, \overline{b}) ∈ F′ miatt \overline{a} ∈ D_{F′}. A feltétel szerint \overline{S} megoldja az F′ feladatot, ezért \overline{a} ∈ D_{p(\overline{S})}. Ebből következik, hogy van

olyan \overline{\overline{b}} ∈ A, amleyre, (\overline{a}, \overline{\overline{b}}) ∈ p(\overline{S}), de pr_{B}(\overline{S}) = p(S) igaz a feltevések szerint, ezért (pr_{B}(\overline{a}), pr_{B}(\overline{\overline{b}})) ∈ p(S). mivel pr_{B}(\overline{a}) = a, ezért (a, pr_{B}(\overline{\overline{b}})) ∈ p(S), tehát a ∈ D_{p}(S). Mivel a ∈ D_{F} tetszőleges volt, D_{F} ⊆ D_{p}(S) igaz.

Az állítás igazolásához be kell még látni, hogy minden a ∈ D_{F} -re: p(S)(a) ⊆ F (a). Legyen a ∈ D_{F} tetszőleges. Az előzőek miatt a ∈ D_{p}(S) is teljesül. Legyen b ∈ p(S)(a) tetszőleges. Ebből nyilván következik, hogy (a, b) ∈ p(S). A pr_{B}(p(\overline{S})) = p(S) eqvivalencia feltétel miatt van olyan \overline{a}, \overline{b} ∈ A, amelyre (\overline{a}, \overline{b}) ∈ p(\overline{S}) és pr_{B}(\overline{a}) = a, valamint pr_{B}(\overline{b}) = b. pr_{B}(\overline{a}) = a-ból és a ∈ D_{F} következik, hogy \overline{a} ∈ D_{F′}, mert a ∈ D_{F} -ből következik, hogy van olyan b ∈ B, amelyre (a, b) ∈ F és F′ definíciója miatt, ha \overline{\overline{b}} ∈ A olyan, amelyre pr_{B}(\overline{\overline{b}}) = b, akkor (\overline{a}, \overline{\overline{b}}) ∈ F′. Ilyen \overline{\overline{b}} biztosan létezik, tehát \overline{a} ∈ D_{F′}. A feltevés szerint \overline{S} megoldja F′-et, ezért \overline{a} ∈ D_{p}(\overline{S}) is igaz, és (\overline{a}, \overline{b}) ∈ F′ is teljesül a p(\overline{S})(\overline{a}) ⊆ F′(\overline{a}) tartalmazás miatt. Ha viszont (\overline{a}, \overline{b}) ∈ F′, akkor pr_{B}(F′) = F miatt (pr_{B}(\overline{a}), pr_{B}(\overline{b})) ∈ F, azaz (a, b) ∈ F, tehát b ∈ F (a). Mivel b ∈ p(S)(a) tetszőleges volt, beláttuk, hogy tetszőleges a ∈ D_{F} -re: p(S)(a) ⊆ F (a). Amit bizonyítani kellett.

3. Ha S′ megoldja \overline{F} -et, akkor S megoldja F -et.

Bizonyítás

D_{F} ⊆ D_{p(S)} bizonyítása pontosan úgy történik, mint a a változó bevezetésének tétele bizonyítása esetén. A pr_{B}(p(S′) = p(S) és pr_{B}(\overline{F}) = F feltételek teljesülnek, valamint S′ megoldja az \overline{F} feladatot, és a a változó bevezetésének tétele bizonyításának megfelelő részében csak ezeket a tulajdonságokat használtuk ki.

Az állítás igazolásához be kell még látni, hogy minden a ∈ D_{F} -re: p(S)(a) ⊆ F (a). Legyen a ∈ D_{F} tetszőleges. Az előzőek miatt a ∈ D_{p}(S) is teljesül. Legyen b ∈ p(S)(a) tetszőleges. a ∈ D_{F} miatt van olyan b^{∗} ∈ B, amelyre (a, b^{∗}) ∈ F. A pr_{B}(\overline{F}) = F feltétel miatt van olyan \overline{a}, \overline{b} ∈ A, amelyre (\overline{a}, \overline{b}) ∈ \overline{F} és pr_{B}(\overline{a}) = a, valamint pr_{B}(\overline{b}) = b^{∗}. Abból a feltevésből, hogy S′ megoldja \overline{F} -et következik, hogy \overline{a} ∈ D\overline{F} miatt \overline{a} ∈ D_{p(S′)} is teljesül. p(S′) = \{(\overline{a}, \overline{b}) ∈ A × A|(pr_{B}(\overline{a}), pr_{B}(\overline{b})) ∈ p(S) és pr_{B′}(\overline{a}) = pr_{B′}(\overline{b})\} összefüggés miatt (\overline{a}, b ⊗ pr_{B′}(\overline{a})) ∈ p(S′). Abból, hogy S′ megoldja \overline{(}F)-et és \overline{a} ∈ D_{F′} következik, hogy (\overline{a}, b ⊗ pr_{B′}(\overline{a})) ∈ \overline{F}. Ugyanakkor pr_{B}(\overline{F}) = F miatt (pr_{B}(\overline{a}), pr_{B}(b ⊗ pr_{B′}(\overline{a}))) ∈ F, azaz pr_{B}(\overline{a}) = a, valamint pr_{B}(b ⊗ pr_{B′}(\overline{a})) = b miatt (a, b) ∈ F, tehát b ∈ F (a). Mivel b ∈ p(S)(a) tetszőleges volt, beláttuk, hogy tetszőleges a ∈ D_{F} -re: p(S)(a) ⊆ F (a). Amit bizonyítani kellett.

4. Ha S megoldja F -et, \overline{F} vetítéstartó B felett, és bővített identitás B és B′ felett, akkor S′ megoldja \overline{F} -et (részfeladat kiválasztásának tétele).

Bizonyítás

Először belátjuk, hogy D\overline{F} ⊆ D_{p(S′)}. Legyen \overline{a} ∈ D\overline{F} tetszőleges. Ekkor D\overline{F} definíciójából következik, hogy van olyan \overline{b} ∈ A, amelyre (\overline{a}, \overline{b}) ∈ \overline{F}. pr_{B}(\overline{F}) = F miatt (pr_{B}(\overline{a}), pr_{B}(\overline{b})) ∈ F, tehát pr_{B}(\overline{a}) ∈ D_{F}. A feltétel szerint S megoldja az F feladatot, ezért pr_{B}(\overline{a}) ∈ D_{p(S)}. Ez azt jelenti, hogy van olyan b ∈ B, amelyre (pr_{B}(\overline{a}), b) ∈ p(S). Mivel p(S′) = \{(\overline{a}, \overline{b}) ∈ A × A|(pr_{B}(\overline{a}), pr_{B}(\overline{b})) ∈ p(S) és pr_{B′}(\overline{a}) = pr_{B′}(\overline{b})\}, ezért (\overline{a}, b ⊗ pr_{B′}(\overline{a})) ∈ p(S′), tehát \overline{a} ∈ D_{p(S′)}. Mivel \overline{a} ∈ D\overline{F} tetszőleges volt, D\overline{F} ⊆ D_{p(S′)} igaz.

Az állítás igazolásához be kell még látni, hogy minden \overline{a} ∈ D\overline{F} -re: p(S′)(\overline{a}) ⊆ \overline{F} (\overline{a}). Legyen \overline{a} ∈ D\overline{F} tetszőleges. Az előzőek miatt \overline{a} ∈ D_{p}(S′) is teljesül. Legyen \overline{b} ∈ p(S′)(\overline{a}) tetszőleges. Ekkor (\overline{a}, \overline{b}) ∈ p(S′). Felhasználva a p(S) és a p(S′) között a már említett összefüggést, adódik, hogy pr_{B′}(\overline{a}) = pr_{B′}(\overline{b}) és (pr_{B}(\overline{a}), pr_{B}(\overline{b})) ∈ p(S).

Ha lenne olyan \overline{\overline{b}} ∈ A, amelyre (\overline{a}, \overline{\overline{b}}) ∈ \overline{F} és pr_{B}(\overline{b}) = pr_{B}(\overline{\overline{b}}), akkor a bővített identitás feltétele miatt (\overline{a}, \overline{b}) ∈ \overline{F} is teljesülne és akkor \overline{b} ∈ \overline{F} (a) is igaz lenne.

\overline{a} ∈ D\overline{F} feltevésből és abból, hogy pr_{B}(\overline{F}) = F következik, hogy pr_{B}(\overline{a}) ∈ D_{F}. Feltétel szerint S megoldja az F feladatot, ezért pr_{B}(\overline{a}) ∈ D_{F} és (pr_{B}(\overline{a}), pr_{B}(\overline{b})) ∈ p(S)-ből következik, hogy (pr_{B}(\overline{a}), pr_{B}(\overline{b})) ∈ F. A pr_{B}(\overline{F}) = F feltétel miatt van olyan (\overline{a}′, \overline{b}′) ∈ A × A, amelyre (\overline{a}′, \overline{b}′) ∈ \overline{F} és pr_{B}(\overline{a}′) = pr_{B}(\overline{a}), valamint pr_{B}(\overline{b}′) = pr_{B}(\overline{b}). Az \overline{F} feladat vetítéstartó tulajdonsága miatt pr_{B}(\overline{a}′) = pr_{B}(\overline{a})-ből következik, hogy pr_{B}(\overline{F} (\overline{a}′)) = pr_{B}(\overline{F} (\overline{a})), viszont \overline{b}′ ∈ \overline{F} (\overline{a}′) és ezért pr_{B}(\overline{b}′) ∈ pr_{B}(\overline{F} (\overline{a}′)). Ebből viszont \overline{F} vetítéstartás miatt következik, hogy van olyan \overline{b}′′ ∈ \overline{F} (\overline{a}), amelyre pr_{B}(\overline{b}′′) = pr_{B}(\overline{b}′) = pr_{B}(\overline{b}). \overline{F} bővített identitás tulajdonsága miatt (\overline{a}, pr_{B}(\overline{b}′′)⊗pr_{B′}(\overline{a})) ∈ \overline{F} is teljesül. pr_{B}(\overline{b}′′) = pr_{B}(\overline{b}) felhasználásával kapjuk, hogy (\overline{a}, pr_{B}(\overline{b})⊗pr_{B′}(\overline{a})) ∈ \overline{F}. pr_{B′}(\overline{a}) = pr_{B′}(\overline{b}) figyelembevételéval adódik, hogy (\overline{a}, pr_{B}(\overline{b}) ⊗ pr_{B′}(\overline{b})) ∈ \overline{F}, azaz (\overline{a}, \overline{b}) ∈ \overline{F}. Mivel \overline{b} ∈ p(S′)(\overline{a}) tetszőleges volt, beláttuk, hogy tetszőleges \overline{a} ∈ D\overline{F} -re: p(S′)(\overline{a}) ⊆ \overline{F} (\overline{a}). Amit bizonyítani kellett.

5. Ha \overline{S} megoldja \overline{F} -et és tetszőleges \overline{a} ∈ D_{p(\overline{S})}-ra: ha (pr_{B}(\overline{a}) ∈ D_{F} akkor \overline{a} ∈ D\overline{F}), akkor S megoldja F -et (a visszavezetés általánosításának tétele).

Bizonyítás

D_{F} ⊆ D_{p(S)} bizonyítása pontosan úgy történik, mint a a változó bevezetésének tétele bizonyítása esetén. A pr_{B}(p(\overline{S}) = p(S) és pr_{B}(\overline{F}) = F feltételek teljesülnek, valamint \overline{S} megoldja az \overline{F} feladatot, és a a változó bevezetésének tétele bizonyításának megfelelő részében csak ezeket a tulajdonságokat használtuk ki.

Az állítás igazolásához be kell még látni, hogy minden a ∈ D_{F} -re: p(S)(a) ⊆ F (a). Legyen a ∈ D_{F} tetszőleges. Az előzőek miatt a ∈ D_{p}(S) is teljesül. Legyen b ∈ p(S)(a) tetszőleges. pr_{B}(p(\overline{S})) = p(S) miatt van olyan \overline{a}, \overline{b} ∈ A, amelyekre (\overline{a}, \overline{b}) ∈ p(\overline{S}) és pr_{B}(\overline{a}) = a, valamint pr_{B}(\overline{b}) = b. Ebből következik, hogy \overline{a} ∈ D_{p(\overline{S})}. Kihasználva az állításban szereplő feltételt, \overline{a} ∈ D_{p(\overline{S})} és pr_{B}(\overline{a}) = a ∈ D_{F} -ből adódik, hogy \overline{a} ∈ D\overline{F}. Mivel \overline{S} megoldja az \overline{F} feladatot, ezért (\overline{a}, \overline{b}) ∈ \overline{F}. A pr_{B}(\overline{F}) = F feltétel miatt (pr_{B}(\overline{a}), pr_{B}(\overline{b})) ∈ F is teljesül, ahonnan (a, b) ∈ F következik. Mivel b ∈ p(S)(a) tetszőleges volt, beláttuk, hogy tetszőleges a ∈ D_{F} -re: p(S)(a) ⊆ F (a). Amit bizonyítani kellett.

3. A típus

Definíció

1. Legyen T tetszőleges halmaz I_{S} : T → 𝕃 specifikációs invariáns, T_{S} = [I_{S}] 𝔽 = {F_{1},…, F_{n}} feladatok halmaza:

∀i ∈ [1, n] : F_{i} ⊆ A^{F_{i}} × A^{F_{i}} (A^{F_{i}} = A_{1}^{F_{i}} ×… × A_{n_{i}}^{F_{i}}) ∃j ∈ [1..n_{i}] : A_{j}^{F_{i}} = T

A T_{S} = (T, I_{S}, 𝔽) hármast típusspecifikációnak nevezzük.

2. Legyen E tetszőleges halmaz, az elemi típusértékek halmaza ϱ ⊆ E^{∗} × H reprezentációs függvény, I : E^{∗} → 𝕃 típusinvariáns 𝕊 = {S_{1},…, S_{m}} programok halmaza:

∀i ∈ [1, m] : S_{i} ⊆ A^{S_{i}} × A^{S_{i}^{∗∗}} (A^{S_{i}} = A_{1}^{S_{i}} ×… × A_{m_{i}}^{S_{i}}) ∃j ∈ [1..m_{i}] : A_{j}^{S_{i}} = E^{∗}

A T = (ϱ, I, 𝕊) hármast típusnak nevezzük.

3. A T = (ϱ, I, 𝕊) típus megfelel a T_{S} = (T, I_{S}, 𝔽) típusspecifikációnak, ha 1. ϱ([I]) = T_{S}

2. ∀F ∈ 𝔽 : ∃S ∈ 𝕊 : S a ϱ_{|_{[I]}}-n keresztül megoldja F -et.

4. A^{S} = A_{1}^{S} ×… × A_{m}^{S}, S ⊆ A^{S} × (A^{S})^{∗∗} program, A^{F} = A_{1}^{F} ×… × A_{n}^{F}, F ⊆ A^{F} × A^{F} (m, n ∈ ℕ). Legyen A^{F′} = A_{1}^{F′} ×… × A_{m}^{F′}, ahol

A_{i}^{F′} := \{ \begin{matrix}T_{S} & ha A_{i}^{S} = E^{∗} \\ A_{i}^{S} & ha A_{i}^{S} ≠ E^{∗} \end{matrix} (i = 1,…, m)

γ ⊆ A^{S} × A^{F′}, ahol γ = (γ_{1},…, γ_{m}), γ_{i} ⊆ A_{i}^{S} × A_{i}^{F′},

γ_{i} = \{ \begin{matrix}ϱ_{|_{[I]}} & ha A_{i}^{S} = E^{∗} \\ id_{A_{i}^{S}} & ha A_{i}^{S} ≠ E^{∗} \end{matrix} (i = 1,…, m),

(γ_{1},…, γ_{m}) = {((a_{1}^{S}, a_{2}^{S},…, a_{m}^{S}), (a_{1}^{F′}, a_{2}^{F′},…, a_{m}^{F′})) | ∀i ∈ [1..m] : (a_{i}^{S}, a_{i}^{F′}) ∈ γ_{i}}

S ⊆ A^{S} × (A^{S})^{∗∗} a a ϱ_{|_{[I]}}-n keresztül megoldja F ⊆ A^{F} × A^{F} -et, ha

1. A^{F} altere A^{F′}-nek

2. D_{F′} ⊆ D_{γ⊙p(S)⊙γ^{(−1)}}

3. ∀a ∈ D_{F′} : γ ⊙ p(S) ⊙ γ^{(−1)}(a) ⊆ F′(a) ahol F′ az F kiterjesztése A^{F′}-re.

4. Specifikáció

Definíció

1. Az R ⊆ A×𝕃 utófeltétel S ⊆ A×A^{∗∗} programra vonatkozó leggyengébb előfeltételének nevezzük azt az lf(S, R) állítást, amelyre [lf(S, R)] = {a ∈ D_{p(S)} | p(S)(a) ⊆ [R]}.

2. B az F ⊆ A × A feladat paramétertere, ha ∃F_{1} ⊆ A × B : ∃F_{2} ⊆ B × A F = F_{2} ∘ F_{1}.

Állítás 1. [lf(S, R)] = p(S)^{−1}([R])

2. lf(S, hamis) = hamis (A csoda kizárásának elve.)

3. lf(S, P ∧ Q) = lf(S, P) ∧ lf(S, Q)

4. lf(S, P ∨ Q) ⇐ lf(S, P) ∨ lf(S, Q)

5. lf(S, ¬Q) ⇒ ¬lf(S, Q)

6. Ha Q ⇒ R, akkor lf(S, Q) ⇒ lf(S, R) (monotonitás)

7. S megoldja F -et ⇔ ∀a ∈ D_{F} : a ∈ [lf(S, P (F (a)))]

8. S megoldja F -et ⇔ ∀H ⊆ A : ∃a ∈ D_{F} : F (a) = H esetén: F^{−1}(H) = [lf(S, P (H))]

9. A specifikáció tétele:

Legyen A állapottér, F ⊆ A × A feladat, valamint S ⊆ A × A^{∗∗} program A-n. Legyen B az F paramétertere:

F = F_{2} ∘ F_{1}, ahol F_{1} ⊆ A × B és F_{2} ⊆ B × A.

Tetszőleges b ∈ B-re legyen Q_{b} és R_{b} állítások A-n, amelyekre

[Q_{b}] = F_{1}^{(−1)}(b) és [R_{b}] = F_{2}(b).

Ha ∀b ∈ B : Q_{b} ⇒ lf(S, R_{b}), akkor S megoldja F -et.

Bizonyítás

Legyen a ∈ D_{F} tetszőleges. Ekkor létezik olyan a′ ∈ A, amelyre (a, a′) ∈ F. F = F_{2} ∘ F_{1} miatt létezik olyan b ∈ B, amelyre (a, b) ∈ F_{1} és (b, a′) ∈ F_{2}. Legyenek Q_{b} és R_{b} állítások A-n, amelyekre [Q_{b}] = F_{1}^{(−1)}(b) és [R_{b}] = F_{2}(b). Ebből következik, hogy ∀a ∈ [Q_{b}] : [R_{b}] ⊆ F_{2} ∘ F_{1}(a). De F = F_{2} ∘ F_{1} miatt ∀a ∈ [Q_{b}] : [R_{b}] ⊆ F (a) is teljesül. A feltétel szerint Q_{b} ⇒ lf(S, R_{b}), ezért [Q_{b}] ⊆ D_{P (S)}. De (a, b) ∈ F_{1} miatt a ∈ [Q_{b}], ezért a ∈ D_{P (S)}. Q_{b} ⇒ lf(S, R_{b}) és a ∈ [Q_{b}]-ből következik, hogy P (S)(a) ⊆ [R_{b}] ⊆ F (a). Tehát P (S)(a) ⊆ F (a) is teljesül tetszőleges a ∈ D_{F} -re.

10. A specifikáció tétele nem megfordítható, azaz megadható olyan A állapottér, valamint F feladat és S program az A-n, továbbá olyan B paramétertér az F feladathoz, hogy bár S megoldja az F feladatot, mégis létezik olyan b ∈ B, amelyre Q_{b} ⇏ lf(S, R_{b}). Megjegyzés: ha F_{1} determinisztikus, akkor a specifikáció tétele megfordítható.

5. Elemi programok

Definíció

1. Eleminek nevezünk egy A állapottéren egy S programot, ha ∀a ∈ A : S(a) ⊆ {< a >, < a, a, a,… >, < a, b > | b ≠ a}.

2. Üresnek nevezzük, és SKIP-pel jelöljük azt a programot, amire ∀a ∈ A : SKIP(a) = {< a >}.

3. Törlődésnek nevezzük, és ABORT-tal jelöljük azt a programot, amire ∀a ∈ A : ABORT(a) = {< a, a, a,… >}.

4. Legyen A = A_{1}×…×A_{n}, F = (F_{1},…, F_{n}), ahol F_{i} ⊆ A×A_{i}. Az S program általános értékadás, ha

\begin{matrix}S = & \{(a, red(a, b)) | a, b ∈ A ∧ a ∈ ⋂_{i=1}^{n} D_{F_{i}} ∧ b ∈ F (a)\}∪ \\ \{(a, < a, a,… >) | a ∈ A ∧ a ∉ ⋂_{i=1}^{n} D_{F_{i}}\} \end{matrix}

Megjegyzés:

D_{F} = ⋂_{i=1}^{n} D_{F_{i}}, F (a) = F_{1}(a) × F_{2}(a) ×… × F_{n}(a)

a) Ha F nem determinisztikus, akkor az S programot értékkiválasztásnak nevezzük és a :∈ F (a)-val jelöljük, különben az S programot értékadásnak nevezzük és a := F (a)-val jelöljük.

b) Ha D_{F} ⊂ A, akkor S parciális (értékkiválasztás vagy értékadás), különben teljes.

c) Ha

\begin{matrix}∃i ∈ [1, n] : & F_{i}(a_{1}, .., a_{i}, .., a_{n}) ≠ a_{i}∧ \\ ∀j ∈ [1, n] : & i ≠ j → F_{j}(a_{1},…, a_{j},…, a_{n}) = a_{j} \end{matrix}

akkor S egyszerű (értékadás vagy értékkiválasztás), különben szimultán.

Állítás

1. A SKIP, az ABORT és az értékadás program.

2. p(SKIP) = id_{A}

3. p(ABORT) = ∅

4. p(a :∈ F (a)) = F

5. lf(SKIP, R) = R

6. lf(ABORT, R) = hamis

7. Ha S az F reláció által meghatározott általános értékadás, akkor lf(S, R) = P (D_{F}) ∧ R ∘ F

6. Programkonstrukciók

Definíció

1. Legyenek S_{1}, S_{2} ⊆ A × A^{∗∗} programok. Az S ⊆ A × A^{∗∗} relációt, amelyre tetszőleges a ∈ A-ra

S(a) ={χ_{2}(α, β) ∈ A^{∗} | α ∈ S_{1}(a) ∧ α ∈ A^{∗} ∧ β ∈ S_{2}(τ(α)) ∧ β ∈ A^{∗}} ∪
{α ∈ A^{∞} | α ∈ S_{1}(a)} ∪
{χ_{2}(α, β) ∈ A^{∞} | α ∈ S_{1}(a) ∧ α ∈ A^{∗} ∧ β ∈ S_{2}(τ(α)) ∧ β ∈ A^{∞}}

az S_{1} és S_{2} szekvenciájának nevezzük, és (S_{1}; S_{2})-vel jelöljük.

2. Legyenek π_{1},…, π_{n} feltételek (állítások), valamint S_{1},…, S_{n} programok A-n. Az IF ⊆ A × A^{∗∗} relációt, amelyre tetszőleges a ∈ A-ra

IF (a) = ⋃_{i=1}^{n} w_{i}(a) ∪ w_{0}(a),

ahol

w_{i}(a) = \{ \begin{matrix}S_{i}(a) & , ha a ∈ [π_{i}] \\ ∅ & , különben \end{matrix}

w_{0}(a) = \{ \begin{matrix}< a, a,… > & , ha a ∉ ⋃_{i=1}^{n}[π_{i}] \\ ∅ & , különben \end{matrix}

az S_{1}, S_{2}, ..., S_{n} programokból, valamint a π_{1}, π_{2}, ..., π_{n} feltételekből képzett elágazásnak nevezzük és (π_{1} : S_{1},…, π_{n} : S_{n})-nel jelöljük.

3. Legyen π feltétel és S_{0} program A-n. A DO ⊆ A × A^{∗∗} relációt, amelyre tetszőleges a ∈ A-ra

a ∈ [π] esetén : DO(a) = {α ∈ A^{∗} | ∃α_{1},…, α_{n} ∈ A^{∗} : (α = χ_{n}(α_{1},…, α_{n}) ∧ α_{1} ∈ S_{0}(a) ∧ ∀i ∈ [1, n − 1] : (α_{i+1} ∈ S_{0}(τ(α_{i})) ∧ τ(α_{i}) ∈ [π]) ∧ (τ(α_{n}) ∉ [π]))} ∪ {α ∈ A^{∞} | ∃α_{1},…, α_{n} ∈ A^{∗∗} : (α = χ_{n}(α_{1},…, α_{n}) ∧ α_{1} ∈ S_{0}(a) ∧ ∀i ∈ [1, n − 1] : (α_{i} ∈ A^{∗} ∧ α_{i+1} ∈ S_{0}(τ(α_{i})) ∧ τ(α_{i}) ∈ [π]) ∧ α_{n} ∈ A^{∞})} ∪ {α ∈ A^{∞} | ∃α_{1},…, α_{k},… ∈ A^{∗} : (α = χ_{∞}(α_{1},…, α_{k},…) ∧ α_{1} ∈ S_{0}(a) ∧ ∀i ∈ ℕ : (α_{i+1} ∈ S_{0}(τ(α_{i})) ∧ τ(α_{i}) ∈ [π]))}

és a ∉ [π] esetén : DO(a) = SKIP(a)

az S_{0}-ból és π-ből képezett ciklusnak nevezzük, és (π, S_{0})-lal jelöljük.

Állítás

1. A szekvencia, az elágazás és a ciklus program.

Bizonyítás

Az állítás közvetlen következik az egyes relációk definíciójából.

2. p((S_{1}; S_{2})) = p(S_{2}) ⊙ p(S_{1}).

Bizonyítás

Legyen (a, a′) ∈ p((S_{1}; S_{2})). Ebből következik, hogy
{α ∈ A^{∞} | α ∈ S_{1}(a)} = ∅

és

{χ_{2}(α, β) ∈ A^{∞} | α ∈ S_{1}(a) ∧ α ∈ A^{∗} ∧ β ∈ S_{2}(τ(α)) ∧ β ∈ A^{∞}} = ∅,

hiszen ebben az esetben (S_{1}; S_{2})(a) csak véges sorozatokat tartalmaz. Ebből következik, hogy a ∈ D_{p(S_{1})} és p(S_{1})(a) ⊆ D_{p(S_{2})}. A programfüggvény defníciójából közvetlen következik, hogy létezik olyan \overline{α} ∈ (S_{1}; S_{2})(a), hogy a′ = τ(\overline{α}). Ezért

S(a) = {χ_{2}(α, β) ∈ A^{∗} | α ∈ S_{1}(a) ∧ α ∈ A^{∗} ∧ β ∈ S_{2}(τ(α)) ∧ β ∈ A^{∗}}

miatt létezik olyan χ_{2}(α, β) ∈ A^{∗}, ahol α ∈ S_{1}(a) ∧ α ∈ A^{∗} ∧ β ∈ S_{2}(τ(α)) ∧ β ∈ A^{∗}, hogy a′ = τ(χ_{2}(α, β)). Ekkor viszont (a, τ(α)) ∈ p(S_{1}) és (τ(α), τ(β)) ∈ p(S_{2}). De τ(β) = τ(χ_{2}(α, β)), ezért (a, a′) ∈ p(S_{2}) ⊙ p(S_{1}).

Legyen (a, a′) ∈ p(S_{2}) ⊙ p(S_{1}). Ekkor a ∈ D_{p(S_{1})} és p(S_{1})(a) ⊆ D_{p(S_{2})}. Ezért

{α ∈ A^{∞} | α ∈ S_{1}(a)} = ∅

és

{χ_{2}(α, β) ∈ A^{∞} | α ∈ S_{1}(a) ∧ α ∈ A^{∗} ∧ β ∈ S_{2}(τ(α)) ∧ β ∈ A^{∞}} = ∅,

Tehát a ∈ D_{p((S_{1};S_{2}))}. (a, a′) ∈ p(S_{2}) ⊙ p(S_{1}) feltételből következik, hogy létezik olyan b ∈ A, amelyre (a, b) ∈ p(S_{1}) és (b, a′) ∈ p(S_{2}). Tekintettel a p(S_{1}) és p(S_{2}) definíciójára, következik, hogy létezik olyan α ∈ S_{1}(a) és β ∈ S_{2}(b), hogy τ(α) = b és τ(β) = a′. Ekkor viszont χ_{2}(α, β) ∈ (S_{1}; S_{2})(a). Ebből következik, hogy (a, τ(χ_{2}(α, β))) ∈ p((S_{1}; S_{2}))(a), de τ(χ_{2}(α, β)) = τ(β) = a′ miatt (a, a′) ∈ p((S_{1}; S_{2})).

3. D_{p(IF)} = {a ∈ A | a ∈ ⋃_{i=1}^{n}[π_{i}] ∧ ∀i ∈ [1, n] : a ∈ [π_{i}] → a ∈ D_{p(S_{i})}}

∀a ∈ D_{p(IF)} : p(IF)(a) = ⋃_{i=1}^{n} pw_{i}(a), ahol

pw_{i}(a) = \{ \begin{matrix}p(S_{i})(a) & , ha a ∈ [π_{i}] \\ ∅ & , különben \end{matrix}

Bizonyítás

A tétel állítása közvetlen következik a program, illetve a programfüggvény definíciójából.

4. p(DO(π; S_{0})) = \overline{p(S_{0})|_{π}}

Bizonyítás

p(DO(π; S_{0}))|_{A\[π]} = \overline{p(S_{0})|_{π}}|_{A\[π]}

nyilván teljesül.

Legyen (a, a′) ∈ p(DO(π; S_{0}))|_{[π]}.Ebből következik, hogy a ∈ [π], valamint

{α ∈ A^{∞} | ∃α_{1},…, α_{n} ∈ A^{∗∗} : (α = χ_{n}(α_{1},…, α_{n}) ∧ α_{1} ∈ S_{0}(a) ∧ ∀i ∈ [1, n − 1] : (α_{i} ∈ A^{∗} ∧ α_{i+1} ∈ S_{0}(τ(α_{i})) ∧ τ(α_{i}) ∈ [π]) ∧ α_{n} ∈ A^{∞})} = ∅

és

{α ∈ A^{∞} | ∃α_{1},…, α_{k},… ∈ A^{∗} : (α = χ_{∞}(α_{1},…, α_{k},…) ∧ α_{1} ∈ S_{0}(a) ∧ ∀i ∈ ℕ : (α_{i} ∈ A^{∗} ∧ α_{i+1} ∈ S_{0}(τ(α_{i})) ∧ τ(α_{i}) ∈ [π]))} = ∅

Legyen < a_{0}, a_{1},… >∈ A^{∞}, ahol ∀i ∈ ℕ_{0} : a_{i+1} ∈ p(S_{0})|_{π}(a_{i}) az p(S_{0})|_{π} reláció a_{0} kezdőpontú végtelen pontlánca, ahol a_{0} ∈ [π]. Ha ∀i ∈ ℕ_{0} : a_{i+1} ∈ p(S_{0})|_{[π]}(a_{i}), akkor legyen α_{i} ∈ S_{0}(a_{i−1}), amelyre τ(α_{i}) = a_{i}, i = 1, 2,. . .. Ekkor

χ_{∞}(α_{1},…, α_{k},…) ∈ {α ∈ A^{∞} | ∃α_{1},…, α_{k},… ∈ A^{∗} : (α = χ_{∞}(α_{1},…, α_{k},…) ∧ α_{1} ∈ S_{0}(a_{0}) ∧ ∀i ∈ ℕ_{0} : (α_{i} ∈ A^{∗} ∧ α_{i+1} ∈ S_{0}(τ(α_{i})) ∧ τ(α_{i}) ∈ [π]))}

Ha ∀i ∈ ℕ_{0} : a_{i+1} ∈ p(S_{0})|_{[π]}(a_{i}) nem teljesül, akkor van olyan i ∈ ℕ_{0}, amelyre a_{i+1} ∈ p(S_{0})|_{π}(a_{i}) úgy, a_{i} ∉ D_{p(S_{0})|_{[π]}} ∧ a_{i} ∈ [π]. Ekkor szükségképpen a_{i+1} = a_{i} a p(S_{0})|_{[π]} definíciója miatt. Legyen i_{0} az ilyen tulajdonságú indexek közül a legkisebb. Az i_{0} választása miatt ∀j ∈ [0..i_{0} − 1] : a_{j} ∈ D_{p(S_{0})} ∧ π[a_{j}], a_{i_{0}} ∉ D_{p}(S_{0}) ∧ π(a_{i_{0}}). Legyen α_{i+1} ∈ S_{0}(a_{i}), amelyre τ(α_{i+1}) = a_{i+1}, i = 0, 1,…, i_{0} − 1 és α_{i_{0}+1} ∈ S(a_{i}) ∩ A^{∞}. Ekkor

χ_{n}(α_{1},…, α_{i_{0}}, α_{i_{0}+1}) ∈ {α ∈ A^{∞} | ∃α_{1},…, α_{n} ∈ A^{∗∗} : (α = χ_{n}(α_{1},…, α_{n}) ∧ α_{1} ∈ S_{0}(a) ∧ ∀i ∈ [1, n − 1] : (α_{i} ∈ A^{∗} ∧ α_{i+1} ∈ S_{0}(τ(α_{i})) ∧ τ(α_{i}) ∈ [π]) ∧ α_{n} ∈ A^{∞})}.

Tehát (a, a′) ∈ p(DO(π; S_{0}))|_{[π]}-ból következik, hogy a ∈ D\overline{p(S_{0})|_{π}}. (a, a′) ∈ p(DO(π; S_{0}))|_{[π]}-ből következik, hogy létezik olyan

α_{1},…, α_{n} ∈ A^{∗} : (α_{1} ∈ S_{0}(a) ∧ a ∈ [π] ∧ ∀i ∈ [1, n − 1] : (α_{i} ∈ A^{∗} ∧ α_{i+1} ∈ S_{0}(τ(α_{i})) ∧ τ(α_{i}) ∈ [π]) ∧ (α_{n} ∈ A^{∗} ∧ τ(α_{n}) ∉ [π])) ∧ a′ = τ(χ_{n}(α_{1},…, α_{n}).

(a, a′) ∈ p(DO(π; S_{0}))|_{[π]}-ből ugyanakkor az is következik, hogy

S_{0}(a) ⊆ A^{∗} és ∀i ∈ [1, n − 1] : S_{0}(τ(α_{i})) ⊆ A^{∗}

is teljesül, mert ellenkező esetben a

{α ∈ A^{∞} | ∃α_{1},…, α_{n} ∈ A^{∗∗} : (α = χ_{n}(α_{1},…, α_{n}) ∧ α_{1} ∈ S_{0}(a) ∧ ∀i ∈ [1, n − 1] : (α_{i} ∈ A^{∗} ∧ α_{i+1} ∈ S_{0}(τ(α_{i})) ∧ τ(α_{i}) ∈ [π]) ∧ α_{n} ∈ A^{∞})} = ∅

nem teljesül. Legyen a_{0} = a, ∀i ∈ [1, n] : a_{i} = τ(α_{i}). Ekkor az < a_{0}, a_{1}, ..., a_{n} > sorozatra

∀i ∈ [1, n − 1] : (a_{i+1} ∈ p(S_{0})(a_{i}) ∧ π(a_{i})) ∧ ¬π(a_{n}).

Mivel τ(χ_{n}(α_{1},…, α_{n}) = τ(α_{n}), ezért (a, a′) ∈ \overline{p(S_{0})|_{π}}|_{[π]}.

Legyen (a, a′) ∈ \overline{p(S_{0})|_{π}}|_{[π]}. Ekkor a ∈ [π]. Ha

{α ∈ A^{∞} | ∃α_{1},…, α_{n} ∈ A^{∗∗} : (α = χ_{n}(α_{1},…, α_{n}) ∧ α_{1} ∈ S_{0}(a) ∧ ∀i ∈ [1, n − 1] : (α_{i} ∈ A^{∗} ∧ α_{i+1} ∈ S_{0}(τ(α_{i})) ∧ τ(α_{i}) ∈ [π]) ∧ α_{n} ∈ A^{∞})} ≠ ∅,

akkor legyen

α_{1},…, α_{n} ∈ A^{∗∗} : (α_{1} ∈ S_{0}(a) ∧ ∀i ∈ [1, n − 1] : (α_{i} ∈ A^{∗} ∧ α_{i+1} ∈ S_{0}(τ(α_{i})) ∧ τ(α_{i}) ∈ [π]) ∧ α_{n} ∈ A^{∞}).

Könnyen látható, hogy n = 1 esetén a ∉ D_{p(S_{0})}, valamint n > 1 esetén τ(α_{n−1}) ∉ D_{p(S_{0})} ∧ τ(α_{n−1}) ∈ [π]. Ebből következik, hogy L_{p(S_{0})|_{π}}^{∞}(a) ≠ ∅, ami ellentmondáshoz vezet. Ha viszont

{α ∈ A^{∞} | ∃α_{1},…, α_{k},… ∈ A^{∗} : (α = χ_{∞}(α_{1},…, α_{k},…) ∧ α_{1} ∈ S_{0}(a) ∧ ∀i ∈ ℕ : (α_{i} ∈ A^{∗} ∧ α_{i+1} ∈ S_{0}(τ(α_{i})) ∧ τ(α_{i}) ∈ [π]))} ≠ ∅,

akkor létezik olyan

α_{1},…, α_{k},… ∈ A^{∗} : (α_{1} ∈ S_{0}(a) ∧ ∀i ∈ ℕ : (α_{i} ∈ A^{∗} ∧ α_{i+1} ∈ S_{0}(τ(α_{i})) ∧ τ(α_{i}) ∈ [π])).

Ha a ∈ D_{p(S_{0})} ∧ ∀i ∈ ℕ : τ(α_{i}) ∈ D_{p(S_{0})}, akkor Legyen a_{0} = a, a_{1} = τ(α_{1}), a_{2} = τ(α_{2}),…, a_{n} = τ(α_{n}),. . .. Könnyen látható, hogy < a_{0}, a_{1},…, a_{n},… >∈ L_{p(S_{0})|_{π}}^{∞}(a), ami ellentmond annak, hogy (a, a′) ∈ \overline{p(S_{0})|_{π}}|_{[π]}. Ha viszont a ∈ D_{p(S_{0})} ∧ ∀i ∈ ℕ : τ(α_{i}) ∈ D_{p(S_{0})} nem teljesül, akkor vagy a ∉ D_{p(S_{0})} vagy ∃i ∈ ℕ : τ(α_{i}) ∉ D_{p(S_{0})}. Mindkét esetben következik, hogy L_{p(S_{0})|_{π}}^{∞}(a) ≠ ∅, ami szintén ellentmondáshoz vezet. Tehát (a, a′) ∈ \overline{p(S_{0})|_{π}}|_{[π]}-ból következik, hogy a ∈ D_{p(DO(π;S_{0}))}. Ha (a, a′) ∈ \overline{p(S_{0})|_{π}}|_{[π]}, akkor létezik olyan

a_{0} = a, a_{1},…, a_{n} : n ∈ ℕ_{0} ∧ ∀i ∈ [1, n] : a_{i} ∈ p(S_{0})|_{π}(a_{i−1}) ∧ a_{n} ∉ D_{p(S_{0})|_{π}} ∧ a′ = a_{n}. a ∈ [π] miatt n > 0. Ekkor szükségképpen ∀i ∈ [1, n] : a_{i−1} ∈ D(p(S_{0})) ∧ π(a_{i−1}), mivel ha lenne olyan i ∈ [1, n] : a_{i−1} ∉ D(p(S_{0})) ∧ π(a_{i−1}), akkor a sorozat ezen i indextől a_{i−1}, a_{i−1},…, a_{i−1},… ∈ L_{p(S_{0})|_{π}}^{∞}(a_{i−1}) sorozattal folytatható lenne, ebből viszont következne, hogy L_{p(S_{0})|_{π}}^{∞}(a) ≠ ∅, ami ellentmondás. Tehát létezik olyan

a_{0}, a_{1},…, a_{n} : ∀i ∈ [1, n] : a_{i} ∈ p(S_{0})(a_{i−1}) ∧ π(a_{i−1}) ∧ ¬π(a_{n}) ∧ a′ = a_{n}.

Ekkor viszont létezik olyan

α_{1},…, α_{n} ∈ A^{∗} : (α_{1} ∈ S_{0}(a) ∧
∀i ∈ [1, n − 1] : (α_{i} ∈ A^{∗} ∧ α_{i+1} ∈ S_{0}(τ(α_{i})) ∧ a_{i} = τ(α_{i}) ∧ τ(α_{i}) ∈ [π]) ∧
(α_{n} ∈ A^{∗} ∧ τ(α_{n}) ∉ [π]) ∧ a_{n} = τ(α_{n}) ),

tehát (a, χ_{n}(α_{1},…, α_{n}))) ∈ p(DO(S_{0}, π)). τ(χ_{n}(α_{1},…, α_{n})) = τ(α_{n}) = a′ miatt adódik, hogy (a, a′) = (a, τ(χ_{n}(α_{1},…, α_{n}))), tehát (a, a′) ∈ p(DO(S_{0}; π))|_{[π]} is teljesül.

5. Legyen S = (S_{1}; S_{2}), és Q, R olyan állítások A-n, amelyekre Q ⇒ lf(S, R). Ekkor létezik olyan Q′ állítás, amire Q ⇒ lf(S_{1}, Q′) és Q′ ⇒ lf(S_{2}, R).

Bizonyítás

Legyen

[Q′] = ⋃_{a∈[Q]} p(S_{1})(a).

Könnyen látható, hogy Q′ kielegítí a tétel állítását.

6. Legyen IF = (π_{1} : S_{1},…, π_{n} : S_{n}), és Q, R olyan állítások A-n, amelyekre

Q ∧ ( ⋁_{i=1}^{n} π_{i}) ⇒ lf(IF, R). Ekkor ∀i ∈ [1, n] : Q ∧ π_{i} ⇒ lf(S_{i}, R).

Bizonyítás

Legyen a ∈ [Q ∧ π_{i}]. Ekkor a ∈ [Q ∧ ( ⋁_{j=1}^{n} π_{j}]). Ebből következik, hogy a ∈ D_{p(IF)},

ezért a ∈ [Q ∧ π_{i}] miatt a ∈ D_{p(S_{i})}. p(S_{i})(a) ⊆ ⋃_{j=1}^{n} pw_{j}(a) = IF (a) ahol,

pw_{j}(a) = \{ \begin{matrix}p(S_{j})(a) & , ha a ∈ [π_{j}] \\ ∅ & , különben, \end{matrix}

mert a ∈ [π_{i}] miatt pw_{i}(a) = p(S_{i})(a). Ezért p(S_{i})(a) ⊆ [R] is tejesül. Tehát tetszőleges i-re Q ∧ π_{i} ⇒ lf(S_{i}, R).

7. Legyen DO = (π, S_{0}), és Q, R olyan állítások A-n, amelyekre Q ⇒ lf(DO, R), és tegyük fel, hogy ∀a ∈ D_{p(S_{0})} ∩ [π] : ∃k ∈ ℕ : p(S_{0})^{k}(a) = ∅. Ekkor létezik P állítás és t : A → ℤ függvény, amelyekre

1. Q ⇒ P 2. P ∧ ¬π ⇒ R

3. P ∧ π ⇒ t > 0

4. P ∧ π ⇒ lf(S_{0}, P)

5. P ∧ π ∧ t = t′ ⇒ lf(S_{0}, t ≤ t′ − 1)

Bizonyítás

Ismeretes, hogy p(DO(π; S_{0})) = \overline{p(S_{0})|_{π}}. A ∀a ∈ D_{p(S_{0})} ∩ [π] : ∃k ∈ ℕ : p(S_{0})^{k}(a) = ∅ feltételből következik, hogy A ∀a ∈ D\overline{p(S_{0})|_{π}} : ∃k ∈ ℕ : p(S_{0})|_{π}^{k}(a) = ∅, ugyanis ha a ∉ [π], akkor k = 1 már alkalmas választás. Legyen a ∈ [π] ∧ a ∈ D\overline{p(S_{0})|_{π}}. Ha < a_{0} = a, a_{1},…, a_{n} >∈ L\overline{p(S_{0})|_{π}}(a), akkor ∀i ∈ [0, n − 1] : a ∈ [π]. Ekkor viszont ∀i ∈ [0, n − 1] : a ∈ D_{p(S_{0})} is teljesül L_{p(S_{0})|_{π}}^{∞} = ∅ miatt. Ezért, ha p(S_{0})^{k}(a) = ∅, akkor az L\overline{p(S_{0})|_{π}}(a) minden lánca k-nál rövidebb, tehát p(S_{0})|_{π}^{k}(a) = ∅. Legyen

t(a) = \{ \begin{matrix}min_{k∈ℕ} p(S_{0})|_{π}^{k}(a) = ∅ & , ha a ∈ D\overline{p(S_{0})|_{π}} \\ 0 & , különben \end{matrix}

és legyen P olyan állítás, amelyre [P] = ⋃_{k=0}^{∞} p(S_{0})|_{π}^{k}[Q].

1. Q ⇒ P nyilván teljesül.

2. P ∧ ¬π ⇒ R teljesül, mert Q ⇒ lf(DO, R) és P ∧ ¬π a Q-ból p(S_{0})|_{π}-szerint kiinduló láncok végei.

3. P ∧ π ⇒ t > 0 teljesül, hiszen az ilyen pontokban az p(S_{0})|_{π}-szerinti láncok nem érnek véget és ezért Q ⇒ lf(DO, R) miatt [P ∧ π] ⊆ D\overline{p(S_{0})|_{π}}.

4. P ∧ π ⇒ lf(S_{0}, P) P definíciójából közvetlen következik.

5. P ∧ π ∧ t = t′ ⇒ lf(S_{0}, t ≤ t′ − 1) teljesül, mert ha egy pontból indul ki p(S_{0})|_{π} szerint lánc és e láncok hosszának van felső határa, akkor ha valamely láncon egy lépést előre megyünk p(S_{0})|_{π} szerint, akkor az abból p(S_{0})|_{π} szerint kiinduló láncok hosszának felső határa eggyel biztosan csökken.

7. Levezetési szabályok

Állítás

1. A szekvencia levezetési szabálya: Legyen S = (S_{1}; S_{2}), és adott Q, R és Q′ állítás A-n. Ha Q ⇒ lf(S_{1}, Q′) és Q′ ⇒ lf(S_{2}, R) akkor Q ⇒ lf(S, R).

Bizonyítás

Legyen a ∈ [Q]. A feltétel szerint, a ∈ D_{p(S_{1})} és p(S_{1})(a) ⊆ [Q′]. Q′ ⇒ lf(S_{2}, R) miatt [Q′] ⊆ D_{p(S_{2})}. Tehát p(S_{1})(a) ⊆ D_{p(S_{2})}, ezért a ∈ D_{p(S_{2})⊙p(S_{1})}.

Legyen b ∈ p(S_{2}) ⊙ p(S_{1})(a). Ekkor van olyan a′, amelyre a′ ∈ p(S_{1})(a) ∧ b ∈ p(S_{2})(a′). Ebből adódik, hogy a′ ∈ [Q′], ezért b ∈ [R]. Tehát p(S_{2}) ⊙ p(S_{1})(a) ⊆ [R]. Mivel a ∈ [Q] tetszőleges volt, adódik, hogy Q ⇒ lf(S, R).

2. Az elágazás levezetési szabálya: Legyen IF = (π_{1} : S_{1},…, π_{n} : S_{n}), és adott Q, R állítás A-n.

Ha ∀i ∈ [1, n] : Q ∧ π_{i} ⇒ lf(S_{i}, R), akkor Q ∧ ( ⋁_{i=1}^{n} π_{i}) ⇒ lf(IF, R).

Bizonyítás

Legyen a ∈ [Q∧( ⋁_{j=1}^{n} π_{j})]. Ha a ∈ [π_{i}], akkor a ∈ [Q∧π_{i}], amiből következik a ∈ D_{p(S_{i})}

a feltételek miatt. Az i tetszőleges választása miatt következik, hogy ha a ∈ [Q ∧ ( ⋁_{j=1}^{n} π_{j})],

akkor a ∈ D_{p(IF)} is teljesül. Definíció szerint ∀a ∈ D_{p(IF)} : p(IF)(a) = ⋃_{i=1}^{n} pw_{i}(a), ahol

pw_{i}(a) = \{ \begin{matrix}p(S_{i})(a) & , ha a ∈ [π_{i}] \\ ∅ & , különben \end{matrix}

Ugyanakkor a feltételek miatt pw_{i}(a) ⊆ [R], i = 1, 2,…, n, tehát p(IF)(a) ⊆ [R] is

teljesül. Mivel a ∈ [Q ∧ ( ⋁_{j=1}^{n} π_{j})] tetszőleges volt, adódik, hogy Q ∧ ( ⋁_{i=1}^{n} π_{i}) ⇒ lf(IF, R).

3. A ciklus levezetési szabálya: Adott P, Q, R állítás A-n, t : A → ℤ függvény és legyen DO = (π, S_{0}). Ha

1. Q ⇒ P

2. P ∧ ¬π ⇒ R

3. P ∧ π ⇒ t > 0

4. P ∧ π ⇒ lf(S_{0}, P)

5. P ∧ π ∧ t = t′ ⇒ lf(S_{0}, t ≤ t′ − 1)

akkor Q ⇒ lf(DO, R).

Bizonyítás

Ismeretes, hogy p(DO(π; S_{0})) = \overline{p(S_{0})|_{π}}. Legyen a ∈ [P]. Ha a ∉ [π], akkor 2. miatt a ∈ [R]. De \overline{p(S_{0})|_{π}}(a) = \{a\} a ∉ [π] miatt, ezért \overline{p(S_{0})|_{π}}(a) ⊆ [R].

Legyen a ∈ [P] és a ∈ [π]. Ekkor a ∈ D\overline{p(S_{0})|_{π}} és 3. miatt t(a) > 0. Legyen < a_{0} = a, a_{1},…, a_{n},… >∈ L∞ ; \overline{p(S_{0})|_{π}}(a). ∀i ∈ ℕ_{0} : a_{i} ∈ [π] nyilván teljesül, mivel D\overline{p(S_{0})|_{π}} = [π]. A 4. feltétel miatt teljes indukcióval könnyen belátható, hogy

∀i ∈ ℕ_{0} : a_{i} ∈ [P]

is teljesül. Ugyanakkor 5. és 3. miatt

∀i ∈ ℕ_{0} : t(a_{i+1}) < t(a_{i}) ∧ t(a_{i}) > 0,

ami lehetetlen. Tehát L∞ ; \overline{p(S_{0})|_{π}}(a) = ∅. Legyen < a_{0} = a, a_{1},…, a_{n} >∈ L\overline{p(S_{0})|_{π}}(a). Ebből következik, hogy ∀i ∈ [0, n − 1] : a_{i} ∈ [π] és a_{n} ∉ [π]. Hasonlóan az előzőekhez belátható, hogy ∀i ∈ [0, n] : a_{i} ∈ [P], tehát adódott a_{n} ∈ \overline{p(S_{0})|_{π}}(a)-ra, hogy a_{n} ∈ [P]∧a_{n} ∉ [π]. Ebből 2. miatt következik, hogy a_{n} ∈ [R]. Mivel < a_{0} = a, a_{1},…, a_{n} >∈ L\overline{p(S_{0})|_{π}}(a) tetszőleges volt, adódik, hogy \overline{p(S_{0})|_{π}}(a) ⊆ [R]. Összegezve a kapott eredményeket, kapjuk, hogy P ⇒ lf(DO, R). Ugyanakkor az 1. feltétel miatt Q ⇒ lf(DO, R) is nyilván teljesül.

8. Típuskonstrukciók

Legyenek T_{0}, T_{1},…, T_{n} típusértékhalmazok, E_{1},…, E_{n} nem üres, véges vagy megszám-

lálható halmazok, E = ⋃_{i=1}^{n} E_{i}, ϱ_{i} ⊂ E^{∗} × T_{i} (i = 1,…, n) reprezentációs függvények,

T_{i} = (ϱ_{i}, I_{i}, S_{i})(i = 0,…, n) típusok.

Definíció

1. Direktszorzat ϱ = ψ_{D} ∘ φ_{D}, ahol ψ_{D} ⊂ B × T, B = T_{1} ×… × T_{n}, φ_{D} = {(ε, b) ∈ E^{∗} × B | ∃ε_{1},…, ε_{n} ∈ E^{∗} ∀i ∈ [1, n] : (ε_{i}, b_{i}) ∈ ϱ_{i} ∧ ε = kon(ε_{1},…, ε_{n})} Jelölés: T = (T_{1},…, T_{n}). Ha ψ_{D} kölcsönösen egyértelmű, akkor T rekord típus.

2. Unió ϱ = ψ_{U} ∘ φ_{U}, ahol ψ_{U} ⊂ B × T, B = T_{1} ∪… ∪ T_{n}, φ_{U} = {(ε, b) ∈ E^{∗} × B | ∃i ∈ [1, n] : (ε, b) ∈ ϱ_{i}} Jelölés: T = (T_{1}; …; T_{n}). Ha ψ_{U} kölcsönösen egyértelmű, akkor T egyesítés.

3. Iterált ϱ = ψ_{I} ∘ φ_{I}, ahol ψ_{I} ⊂ T_{0}^{∗} × T, φ_{I} = {(ε, β) ∈ E^{∗} × T_{0}^{∗} | ∃α ∈ (E^{∗})^{∗} : |α| = |β| ∧ ∀i ∈ [1, |α|] : (α_{i}, β_{i}) ∈ ϱ_{0} ∧ ε = kon(α_{1},…, α_{|α|}} Jelölés: T = it(T_{0}). Ha ψ_{I} kölcsönösen egyértelmű, akkor T sorozat típus.

Jelölés: T = seq(T_{0}). Ha D_{ψ_{I}} = T_{0}^{∗} és (α, t), (β, t) ∈ ψ_{I} ⇔ α ∈ perm(β), akkor T kombináció típus.

Jelölés: T = com(T_{0}).

Ha D_{ψ_{I}} = T_{0}^{∗} és (α, t), (β, t) ∈ ψ_{I} ⇔ ⋃_{i=1}^{|α|}{α_{i}} = ⋃_{i=1}^{|β|}{β_{i}}, akkor T halmaz típus.

Jelölés: T = set(T_{0}).