Definíciók és tételek

1. Felhasznált matematikai fogalmak

Jelölés

1. ℕ: a természetes 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} > 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. 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.

3. Legyen α^{1}, α^{2},…, α^{n−1} ∈ A^{∗}, α^{n} ∈ A^{∗∗}.

χ_{n}(α^{1}, α^{2},…, α^{n}) =^{def} red(kon(α^{1}, α^{2},…, α^{n}))

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

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

6. Legyen A_{i} tetszőleges halmaz (i = 1,…, n) (n ∈ ℕ).

×_{i=1}^{n} A_{i} =^{def} A_{1} ×… × A_{n} =^{def} {(a_{1}, a_{2},…, a_{n}) | a_{i} ∈ A_{i} (i = 1,…, n)}

7. 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 halmaz az A halmaz altere, ha J ⊆ I.

8. 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 altér kiegészítő altere az A-ra: B′ =^{def} ×_{k∈(I\J)} A_{k}.

9. Legyen a ∈ A és B altere A-nak. Ekkor a-nak a B-re vett projekciója

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

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

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

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

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

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

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

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

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

18. Az R ⊆ A × B reláció komplemense: R̃ =^{def} {(a, b) ∈ A × B | (a, b) ∉ R}.

19. 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}}.

20. 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}}.

21. R ⊆ A × A. id_{A} =^{def} R^{0} =^{def} A × A.

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

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

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

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

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

25. 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}}.

26. 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})}.

27. 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_{0})\}.

28. 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_{0})\}.

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

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

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

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

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

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

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

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

34. \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 véges vagy megszámlálható 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. A p(S) ⊆ A × A reláció az S ⊆ A × A^{∗∗} program programfüggvénye, ha 1. D_{p(S)} = {a ∈ A | S(a) ⊆ A^{∗}}

2. ∀a ∈ D_{p(S)} : p(S)(a) = {b ∈ A | ∃α ∈ S(a) : τ(α) = b}.

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, ha pr_{B×B}(p(S_{1})) = pr_{B×B}(p(S_{2})).

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

13. Legyen B′ altere A-nak. A G ⊆ A × A feladat bővített identitás a B′ altér felett, ha ∀(a_{1}, a_{3}) ∈ G : ∃(a_{1}, a_{4}) ∈ G : (pr_{B′}(a_{4}) = pr_{B′}(a_{1}) ∧ pr_{B}(a_{3}) = pr_{B}(a_{4})).

Á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, S_{1} program A-n, G ⊆ A × A feladat, G_{1} = pr_{B×B}(G), és legyen S_{1} és S ekvivalens B-n.

1. S′ megoldja G-t ⇒ S megoldja G_{1}-et

2. S_{1} megoldja F′-t ⇒ S megoldja F -et

3. S′ megoldja F′-t ⇔ S megoldja F -et

4. S megoldja G_{1}-et, G vetítéstartó B felett, és bővített identitás B′ felett ⇒ S′ megoldja G-t.

3. A típus

Definíció

1. Legyen T tetszőleges nem üres, véges vagy megszámlálható halmaz I_{S} : A → 𝕃 specifikációs invariáns, T_{S} = [I_{S}] 𝔽 = {F_{1},…, F_{n}} feladatok halmaza:

∀i ∈ [1, n] : F_{i} ⊆ A_{i} × A_{i} (A_{i} = A_{i_{1}} ×… × A_{i_{n_{i}}}) ∃j ∈ [1, n_{i}] : A_{i_{j}} = T_{S}

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

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

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

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

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

2. ∀F ∈ F : ∃S ∈ SS a ϱ-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,…, n)

γ ⊆ A^{S} × A^{F′}, ahol

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

S ⊆ A^{S} × (A^{S})^{∗∗} a ϱ-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 kiterjesztettje 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. Ha Q ⇒ R, akkor lf(S, Q) ⇒ lf(S, R) (monotonitás)

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

7. S megoldja F -et ⇔ ∀H ⊆ D_{F^{−1}} : F^{−1}(H) ⊆ [lf(S, P (H))]

8. A specifikáció tétele:

Legyen F ⊆ A × A, B az F egy paramétertere. Legyen b ∈ B és [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.

9. A specifikáció tétele nem megfordítható, azaz ∃F ⊆ A × A : ∃S ⊆ A × A^{∗∗} program amely megoldja F -t, és ∃b ∈ B : Q_{b} ⇏ lf(S, R_{b}).

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

S ={(a, red(a, b)) | a, b ∈ A ∧ a ∈ ⋂_{i=1}^{n} D_{F_{i}} ∧ b ∈ F (a)}∪

{(a, ABORT(a)) | a ∈ A ∧ a ∉ ⋂_{i=1}^{n} D_{F_{i}}}

Megjegyzés:

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

a) Ha D_{F} = A, akkor az S programot értékkiválasztásnak nevezzük és a :∈ F (a)-val jelöljük.

b) Ha az F reláció függvény. akkor az S programot értékadásnak nevezzük és a := F (a)-val jelöljük.

c) Ha D_{F} ⊂ A, akkor S parciális értékkiválasztás.

d) Ha D_{F} ⊂ A és F determinisztikus, akkor S parciális értékadás.

e) 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ű (általános) értékadás (egyébként szimultán).

Állítás

1. lf(SKIP, R) = R

2. lf(ABORT, R) = hamis

3. Ha S az F reláció által meghatározott értékadás, akkor lf(S, R) = F^{−1}([R])

6. Programkonstrukciók

Definíció

1. Legyenek S_{1}, S_{2} ⊆ A × A^{∗∗} programok. Az S ⊆ A × A^{∗∗} relációt az S_{1} és S_{2} szekvenciájának nevezzük, és (S_{1}; S_{2})-vel jelöljük, ha

\begin{matrix}∀a ∈ A : S(a) = & \{α ∈ A^{∞} | α ∈ S_{1}(a)\} ∪ \\ \{χ_{2}(α, β) ∈ A^{∗∗} | α ∈ S_{1}(a) ∩ A^{∗} ∧ β ∈ S_{2}(τ(α))\} \end{matrix}

2. Legyenek π_{1},…, π_{n} feltételek, S_{1},…, S_{n} programok A-n. Az IF ⊆ A × A^{∗∗} relációt az S_{i}-kből képzett elágazásnak nevezzük és (π_{1} : S_{1},…, π_{n} : S_{n})-nel jelöljük, ha

∀a ∈ A : 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(a) = \{ \begin{matrix}ABORT(a) & , ha a ∉ ⋃_{i=1}^{n}[π_{i}] \\ ∅ & , különben \end{matrix}

3. Legyen π feltétel és S_{0} program A-n. A DO ⊆ A × A^{∗∗} relációt az S_{0}-ból és π-ből képezett ciklusnak nevezzük, és (π, S_{0})-lal jelöljük, ha

∀a ∉ [π] : DO(a) = SKIP(a)
∀a ∈ [π] : DO(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^{∗} ∧ τ(α_{n}) ∉ [π]) ∨ (α_{n} ∈ A^{∞}))} ∪
{α ∈ A^{∞} | ∃α_{1},…, α_{k},… ∈ A^{∗} (α = χ_{∞}(α_{1},…, α_{k},…) ∧ α_{1} ∈ S_{0}(a) ∧
∀i ∈ ℕ : α_{i} ∈ A^{∗} ∧ α_{i+1} ∈ S_{0}(τ(α_{i})) ∧ τ(α_{i}) ∈ [π])}

Állítás

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

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

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}

4. p(DO(π; S_{0})) = \overline{p(S_{0})|_{π}} 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′) ∧ Q′ ⇒ lf(S_{2}, R).

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).

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 → Z függvény, amelyekre

1. Q ⇒ P

2. P ∧ ¬π ⇒ R

3. P ∧ π ⇒ t > 0

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

5. P ∧ π ∧ ∀t_{0} ∈ Z : t ≤ t_{0} + 1 ⇒ lf(S_{0}, t ≤ t_{0})

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

1. Q ⇒ lf(S_{1}, Q′)

2. Q′ ⇒ lf(S_{2}, R) akkor 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, R), akkor 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 → Z 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_{0} ∈ Z : t ≤ t_{0} + 1 ⇒ lf(S_{0}, t ≤ t_{0}) akkor Q ⇒ lf(DO, R).

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ámlá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}).