Programozási tételek

1. Összegzés

Legyen H egy tetszőleges halmaz, amelyen értelmezett az összeadás művelete. Tegyük fel, hogy létezik neutrális eleme a H-nak az összeadásra nézve (jelölje ezt 0), valamint adott az f : ℤ → H függvény. Adott [m, n] ⊂ ℤ intervallumon összegezzük az f függvény

értékeit! Legyen ∑_{i=m}^{n} f(i) = 0, ha n < m.

A =ℤ m×ℤ n×H s

B ={ℤ \atop m′}×{ℤ \atop n′}

Q : (m = m′ ∧ n = n′)

R : (Q ∧ s = ∑_{i=m′}^{n′} f(i))

Keressük a megoldást adó programot ciklus formában, ahol

P : (Q ∧ k ∈ [m..n] ∪ {m − 1} ∧ s = ∑_{i=m}^{k} f(i))

1. A ciklus levezetési szabálya második feltétele: P ∧ ¬π ⇒ R teljesül, ha ¬π : (k ≥ n). Ha ugyanis n < m akkor, ha P ∧ ¬π, akkor k = m − 1 és ezért P ∧ ¬π ⇒ R teljesül, mivel n < m esetén ∑_{i=m}^{n} f(i) = ∑_{i=m}^{m−1} f(i) = 0.

Ha viszont n ≥ m, akkor, ha P ∧ ¬π, akkor k = n és ezért P ∧ ¬π ⇒ R nyilván teljesül. Tehát π : k < n alkalmas választás.

2. A ciklus levezetési szabálya harmadik feltétele: P ∧ π ⇒ t > 0 teljesül, ha t = n − k a π választása miatt.

3. Célszerű a ciklusmagot S_{0} : (S_{1}; S_{2}) szekvencia fomában keresni, ahol S_{2} = (k := k + 1) abból a meggondolásból, hogy a ciklus levezetési szabályának 5. feltétele is teljesüljön. Alkalmazva a szekvencia leggyengébb előfeltételére ismert tételt, P ∧ π ⇒ lf(S_{0}, P) ⇔ lf(S_{1}, lf(S_{2}, P)) teljesül, ha P ∧ π ⇒ lf(S_{1}, P^{k←k+1}), mivel lf(k := k + 1, P) ⇔ P^{k←k+1}.

P^{k←k+1} : (Q ∧ k + 1 ∈ [m..n] ∪ {m − 1} ∧ s = ∑_{i=m}^{k+1} f(i)),

ugyanakkor

P ∧ π ⇒ Q ∧ k + 1 ∈ [m..n] ∪ {m − 1} ∧ s + f(k + 1) = ∑_{i=m}^{k+1} f(i),

ahonnan P ∧ π ⇒ P^{k←k+1}^{s←s+f(k+1)}. Ezért P ∧ π ⇒ lf(s := s + f(k + 1), P^{k←k+1}). Tehát S_{0} = (s := s + f(k + 1); k := k + 1) alkalmas választás a ciklus levezetési szabálya negyedik feltétele teljesüléséhez.

4. A ciklus levezetési szabálya ötödik feltétele: P ∧ π ∧ t ≤ t_{0} + 1 ⇒ lf(S_{0}, t ≤ t_{0}) minden t_{0} ∈ ℤ-re. Mivel lf(S_{0}, t ≤ t_{0}) ⇔ (t ≤ t_{0})^{k←k+1}^{s←s+f(k+1)} ⇔ n−k ≤ t_{0}+1 ⇔ t ≤ t_{0}+1 tetszőleges t_{0} ∈ ℤ-re, ezért a ciklus levezetési szabályának ötödik feltétele is teljesül.

5. Könnyen ellenőrizhető, hogy Q ⇒ P nem teljesül. Ugyanakkor látható, hogy Q ⇒ P^{k,s←m−1,0} fennáll, mivel

P^{k,s←m−1,0} : (Q ∧ m − 1 ∈ [m..n] ∪ {m − 1} ∧ 0 = ∑_{i=m}^{m−1} f(i)),

és

(m − 1 ∈ [m..n] ∪ {m − 1} ∧ 0 = ∑_{i=m}^{m−1} f(i)) ⇔ true.

Tehát Q ⇒ lf(k, s := m − 1, 0, P). Ugyanakkor a ciklus levezetési szabálya első feltétele: P ⇒ P nyilván teljesül, ezért P ⇒ lf(DO, R) is igaz, ahol DO = (k < n, S_{0}). Alkalmazva a szekvenciával kapcsolatos levezetési szabályt, kapjuk: Q ⇒ lf((k, s := m − 1, 0; DO), R)

Egy lehetséges megoldás tehát a következő program:

k, s := m − 1, 0 ; k < n ; \overline{\frac{s := s + f(k + 1)}{k := k + 1}}

2. Számlálás

Legyen β : ℤ → 𝕃, m, n ∈ ℤ. Számoljuk meg, hány helyen igaz β az [m, n] ⊂ ℤ

intervallumban. Legyen ∑_{i=m}^{n} χ(β(i)) = 0, ha n < m.

A =ℤ m×ℤ n×{ℕ_{0} \atop s}

B ={ℤ \atop m′}×{ℤ \atop n′}

Q : (m = m′ ∧ n = n′)

R : (Q ∧ s = ∑_{i=m′}^{n′} χ(β(i)))

Keressük a megoldást adó programot ciklus formában, ahol

P : (Q ∧ k ∈ [m..n] ∪ {m − 1} ∧ s = ∑_{i=m}^{k} χ(β(i)))

ahol χ : 𝕃 → ℕ_{0}, χ(a) = \{ \begin{matrix}1 & , a =↑ \\ 0 & , a =↓ \end{matrix} .

A levezetés lépései megegyeznek az Összegzés tétele levezetésénél alkalmazott lépésekkel, kivéve a 3. és a 4. pontokat, amelyek az alábbiak szerint módosulnak:

3’. Célszerű a ciklusmagot S_{0} : (S_{1}; S_{2}) szekvencia fomában keresni, ahol S_{2} = (k := k + 1) abból a meggondolásból, hogy a ciklus levezetési szabályának 5. feltétele is teljesüljön. Alkalmazva a szekvencia leggyengébb előfeltételére ismert tételt, P ∧ π ⇒ lf(S_{0}, P) ⇔ lf(S_{1}, lf(S_{2}, P)) teljesül, ha P ∧ π ⇒ lf(S_{1}, P^{k←k+1}), mivel lf(k := k + 1, P) ⇔ P^{k←k+1}.

P^{k←k+1} : (Q ∧ k + 1 ∈ [m..n] ∪ {m − 1} ∧ s = ∑_{i=m}^{k+1} χ(β(i))),

ugyanakkor

P ∧ π ∧ β(k + 1) ⇒ Q ∧ k + 1 ∈ [m..n] ∪ {m − 1} ∧ s + 1 = ∑_{i=m}^{k+1} χ(β(i)) ⇔

P^{k←k+1}^{s←s+1}. Ezért P ∧ π ∧ β(k + 1) ⇒ lf(s := s + 1, P^{k←k+1}). Hasonlóan

P ∧ π ∧ ¬β(k + 1) ⇒ Q ∧ k + 1 ∈ [m..n] ∪ {m − 1} ∧ s = ∑_{i=m}^{k+1} χ(β(i)),

tehát P ∧ π ∧ β(k + 1) ⇒ lf(SKIP, P^{k←k+1}). Felhasználva az elágazásra érvényes levezetési szabályt, kapjuk: P ∧ π ∧ (β(k + 1) ∨ (¬β(k + 1))) ⇒ lf(IF, P^{k←k+1}), ahol IF : (β(k + 1) : s := s + 1, ¬β(k + 1) : SKIP). (β(k + 1) ∨ (¬β(k + 1))) ⇔ true miatt adódik: P ∧ π ⇒ lf(IF, P^{k←k+1}). Tehát S_{0} = (IF; k := k + 1) alkalmas választás a ciklus levezetési szabálya negyedik feltétele teljesüléséhez.

4’. A ciklus levezetési szabálya ötödik feltétele: P ∧ π ∧ t ≤ t_{0} + 1 ⇒ lf(S_{0}, t ≤ t_{0}) minden t_{0} ∈ ℤ-re. Mivel lf(S_{0}, t ≤ t_{0}) ⇔ lf(IF, (t ≤ t_{0})^{k←k+1}) ⇔ n − k ≤ t_{0} + 1 ⇔ t ≤ t_{0} + 1 tetszőleges t_{0} ∈ ℤ-re, ezért a ciklus levezetési szabályának ötödik feltétele is teljesül.

Egy lehetséges megoldás tehát a következő program:

k, s := m − 1, 0 ; k < n ; \overline{\  β(k + 1)  / ; \begin{aligned}s := s + 1 \\ & SKIP \end{aligned} ; k := k + 1}

Második megoldás

. . .

3”. Legyen P′ : (P ∧ π ∧ (u ↔ ∃j ∈ [k + 1..n] : β(j)) ∧ (u → i ∈ [k + 1..n] ∧ β(i) ∧ ∀j ∈ [k + 1..i) : ¬β(j))). Keressünk olyan \overline{S} programot, amelyre P ∧ π ⇒ lf(\overline{S}, P′). A feltételnek eleget tesz a lin.ker.2.8 (k + 1, n) program. Ennek bizonyításához ld. a Lineáris keresés 2.8 tétel levezetését. Keressünk olyan programot, amelyre P′ ⇒ lf(\overline{\overline{S}}, P). Könnyen látható, hogy P′ ∧ u ⇒ P^{k,s←i,s+1} ⇔ lf(k, s := i, s + 1, P) és P′ ∧ ¬u ⇒ P^{k←n} ⇔ lf(k := n, P) Tehát a keresett program: \overline{\overline{S}} : IF (u : k, s := i, s + 1, ¬u : k := n) alkalmazva a szekvencia levezetési szabályának megfordítását, kapjuk hogy P ∧ π ⇒ lf((lin.ker.2.8 (k + 1, n); IF (u : k, s := i, s + 1, ¬u : k := n)), P) . . .

Egy lehetséges megoldás tehát a következő program:

k, s := m − 1, 0 ; k < n ; \overline{lin.ker.2.8 (k + 1, n) ; \  u  / ; \begin{aligned}k, s := i, s + 1 \\ & k := n \end{aligned}}

3. Feltételes összegzés

Legyen β : ℤ → 𝕃, f : ℤ → ℤ, m, n ∈ ℤ. Összegezzük az f függvény értékeit az [m..n] intervallum azon pontjaiban, amelyekben β feltétel igaz. Legyen ∑_{i=m}^{n} χ(β(i)) ∗ f(i) = 0, ha n < m.

A =ℤ m×ℤ n×{ℕ_{0} \atop s}

B ={ℤ \atop m′}×{ℤ \atop n′}

Q : (m = m′ ∧ n = n)

R : (Q ∧ s = ∑_{i=m′}^{n′} χ(β(i)) ∗ f(i))

Keressük a megoldást adó programot ciklus formában, ahol

P : (Q ∧ k ∈ [m..n] ∪ {m − 1} ∧ s = ∑_{i=m}^{k} χ(β(i)) ∗ f(i))

Vegyük észre, ha az f speciálisan f : ℤ → {1}, akkor a Számlálás tételéhez jutunk. A levezetés logikája megegyezik a Számlálás tételénél alkalmazottakkal. Az értelemszerű módosításokat az olvasó könnyen elvégezheti.

Egy lehetséges megoldás tehát a következő program:

ahol χ : 𝕃 → ℕ_{0}, χ(a) = \{ \begin{matrix}1 & , a =↑ \\ 0 & , a =↓ \end{matrix} .

k, s := m − 1, 0 ; k < n ; \overline{\  β(k + 1)  / ; \begin{aligned}s := s + f(k + 1) \\ & SKIP \end{aligned} ; k := k + 1}

4. Maximumkeresés

Legyen (H, ≤) egy tetszőleges halmaz és f : ℤ → H egy függvény. Keressük meg az f függvény maximumát és egy olyan helyet, ahol ezt a maximumértéket felveszi egy adott [m, n] ⊂ ℤ intervallumban.

A =ℤ m×ℤ n×H h×ℤ i

B ={ℤ \atop m′}×{ℤ \atop n′}

Q : (m = m′ ∧ n = n′ ∧ m ≤ n)

R : (Q ∧ i ∈ [m..n] ∧ f(i) = h ∧ ∀j ∈ [m..n] : f(j) ≤ f(i))

Keressük a megoldást adó programot ciklus formában, ahol

P : (Q ∧ k ∈ [m..n] ∧ i ∈ [m, k] ∧ f(i) = h ∧ ∀j ∈ [m, k] : f(j) ≤ f(i))

1. A ciklus levezetési szabálya második feltétele: P ∧ ¬π ⇒ R teljesül, ha ¬π : (k = n). Tehát π : k ≠ n alkalmas választás.

2. A ciklus levezetési szabálya harmadik feltétele: P ∧ π ⇒ t > 0 teljesül, ha t = n − k a π választása miatt.

3. Célszerű a ciklusmagot S_{0} : (S_{1}; S_{2}) szekvencia fomában keresni, ahol S_{2} = (k := k + 1) abból a meggondolásból, hogy a ciklus levezetési szabályának 5. feltétele is teljesüljön. Alkalmazva a szekvencia leggyengébb előfeltételére ismert tételt, P ∧ π ⇒ lf(S_{0}, P) ⇔ lf(S_{1}, lf(S_{2}, P)) teljesül, ha P ∧ π ⇒ lf(S_{1}, P^{k←k+1}), mivel lf(k := k + 1, P) ⇔ P^{k←k+1}. P^{k←k+1} : (Q ∧ k + 1 ∈ [m..n] ∧ i ∈ [m, k + 1] ∧ f(i) = h ∧ ∀j ∈ [m, k + 1] : f(j) ≤ f(i)), ugyanakkor P ∧ π ∧ h < f(k + 1) ⇒ Q ∧ k + 1 ∈ [m..n] ∧ k + 1 ∈ [m, k + 1] ∧ f(k + 1) = f(k + 1) ∧ ∧ ∀j ∈ [m, k + 1] : f(j) ≤ f(k + 1)) ⇔ P^{k←k+1}^{i,h←k+1,f(k+1)}, ahonnan P ∧ π ∧ h < f(k + 1) ⇒ P^{k←k+1}^{i,h←k+1,f(k+1)}. Ezért P ∧ π ∧ h < f(k + 1) ⇒ lf(i, h := k + 1, f(k + 1), P^{k←k+1}). Ugyanakkor P ∧ π ∧ h ≥ f(k + 1) ⇒ Q ∧ k + 1 ∈ [m..n] ∧ i ∈ [m, k + 1] ∧ f(i) = h ∧ ∀j ∈ [m, k + 1] : f(j) ≤ f(i)) ⇔ P^{k←k+1}, ahonnan P ∧ π ∧ h ≥ f(k + 1) ⇒ P^{k←k+1}, ezért P ∧ π ∧ h ≥ f(k + 1) ⇒ lf(SKIP, P^{k←k+1}). Alkalmazva az elágazásra vonatkozó levezetési szabályt, kapjuk: P ∧ π ⇔ P ∧ π ∧ (h < f(k + 1) ∨ h ≥ f(k + 1)) ⇒ lf(IF, P^{k←k+1}), ahol IF : (h < f(k + 1) : i, h := k + 1, f(k + 1), h ≥ f(k + 1) : SKIP). Tehát S_{0} = ((h < f(k + 1) : i, h := k + 1, f(k + 1), h ≥ f(k + 1) : SKIP), k := k + 1) alkalmas választás a ciklus levezetési szabálya negyedik feltétele teljesüléséhez.

4. A ciklus levezetési szabálya ötödik feltétele: P ∧ π ∧ t ≤ t_{0} + 1 ⇒ lf(S_{0}, t ≤ t_{0}) minden t_{0} ∈ ℤ-re. Mivel lf(S_{0}, t ≤ t_{0}) ⇔ lf(IF, lf(k := k + 1, t ≤ t_{0})) ⇔ lf(IF, t − 1 ≤ t_{0}) a szekvencia leggyengébb előfeltételére vonatkozó ismert tétel, és t választása miatt, ezért elegendő belátni, hogy P ∧ π ∧ t ≤ t_{0} + 1 ⇒ lf(IF, t − 1 ≤ t_{0})

Alkalmazva az elágazás levezetési szabályának megfordítását, ehhez elegendő belátni, hogy P ∧π∧t ≤ t_{0}+1∧h < f(k+1) ⇒ lf(i, h := k+1, f(k+1), t−1 ≤ t_{0}) ⇔ t−1 ≤ t_{0}, valamint P ∧ π ∧ t ≤ t_{0} + 1 ∧ h ≥ f(k + 1) ⇒ lf(SKIP, t − 1 ≤ t_{0}) ⇔ t − 1 ≤ t_{0}. Könnyen látható, hogy mindkét állítás teljesül, ezért a ciklus levezetési szabályának ötödik feltétele is teljesül.

5. Könnyen ellenőrizhető, hogy Q ⇒ P nem teljesül. Ugyanakkor látható, hogy Q ⇒ P^{i,k,h←m,m,f(m)} fennáll, mivel P^{i,k,h←m,m,f(m)} : (Q ∧ m ∈ [m..n] ∧ m ∈ [m, m] ∧ f(m) = f(m) ∧ ∀j ∈ [m, m] : f(j) ≤ f(m)) és (m ∈ [m..n] ∧ m ∈ [m, m] ∧ f(m) = f(m) ∧ ∀j ∈ [m, m] : f(j) ≤ f(m)) ⇔ true. Tehát Q ⇒ lf(i, k, h := m, m, f(m), P). Ugyanakkor a ciklus levezetési szabálya első feltétele: P ⇒ P nyilván teljesül, ezért P ⇒ lf(DO, R) is igaz, ahol DO = (k ≠ n, S_{0}). Alkalmazva a szekvenciával kapcsolatos levezetési szabályt, kapjuk: Q ⇒ lf((i, k, h := m, m, f(m), DO), R)

Egy lehetséges megoldás tehát a következő program:

i, k, h := m, m, f(m) ; k ≠ n ; \overline{\begin{aligned}\ h ≤ f(k + 1) \\ & \ h ≥ f(k + 1) \end{aligned} ; \begin{aligned}i, h := k + 1, f(k + 1) \\ & SKIP \end{aligned} ; k := k + 1}

5. Feltételes maximumkeresés

Legyen (H, ≤) tetszőleges halmaz és f : Z → H egy függvény, m, n ∈ ℤ és β : ℤ → 𝕃. Határozzuk meg, hogy van-e az [m, n] intervallumban olyan i pont, ahol β(i) érvényes, és ha van ilyen pont, akkor határozzuk meg a [β] ∩ [m, n] halmaz felett az f függvény maximumát és a halmaz egy olyan pontját, ahol f a maximum értékét felveszi.

A =ℤ m×ℤ n×ℤ i×H h×𝕃 l

B ={ℤ \atop m′}×{ℤ \atop n′}

Q : (m = m′ ∧ n = n′)

R : (Q ∧ (l ↔ (∃i ∈ [m..n] : β(i))) ∧ (l → (ε(m, n, i) ∧ f(i) = h)))

ahol ε(m, k, i) : (i ∈ [m, k] ∧ β(i) ∧ ∀j ∈ [m, k] : (β(j) → f(j) ≤ f(i))).

Keressük a megoldást adó programot ciklus formában, ahol

P : (Q∧k ∈ [m..n]∪{m−1}∧(l ↔ (∃i ∈ [m, k] : β(i)))∧(l → (ε(m, k, i)∧f(i) = h)))

1. A ciklus levezetési szabálya második feltétele: P ∧ ¬π ⇒ R teljesül, ha ¬π := (k ≥ n). Ha ugyanis n < m akkor, ha P ∧ ¬π, akkor k = m − 1 és ezért P ∧ ¬π ⇒ R teljesül, mivel n < m esetén a ∃i ∈ [m, m − 1] : β(i) és a ∃i ∈ [m, n] : β(i) formulák értéke egyaránt hamis, és abból, hogy l ↔ ∃i ∈ [m, m − 1] : β(i) következik, hogy l ↔ ∃i ∈ [m, n] : β(i) is igaz és l hamis. Ez utóbbiból viszont következik, hogy l → (ε(m, n, i) ∧ f(i) = h)) biztosan igaz. Tehát R igaz. Ha viszont n ≥ m, akkor, ha P ∧ ¬π, akkor k = n és ezért P ∧ ¬π ⇒ R nyilván teljesül. Tehát π : k < n alkalmas választás.

2. A ciklus levezetési szabálya harmadik feltétele: P ∧ π ⇒ t > 0 teljesül, ha t = n − k a π választása miatt.

3. Célszerű a ciklusmagot S_{0} : (S_{1}; S_{2}) szekvencia fomában keresni, ahol S_{2} = (k := k + 1) abból a meggondolásból, hogy a ciklus levezetési szabályának 5. feltétele is teljesüljön. Alkalmazva a szekvencia leggyengébb előfeltételére ismert tételt, P ∧ π ⇒ lf(S_{0}, P) ⇔ lf(S_{1}, lf(S_{2}, P)) teljesül, ha P ∧ π ⇒ lf(S_{1}, P^{k←k+1}), mivel lf(k := k + 1, P) ⇔ P^{k←k+1}. P^{k←k+1} : (Q ∧ k + 1 ∈ [m..n] ∪ {m − 1} ∧ ∧(l ↔ (∃i ∈ [m, k + 1] : β(i))) ∧ ∧(l → (ε(m, k + 1, i) ∧ f(i) = h))), ugyanakkor P ∧ π ∧ β(k + 1) ∧ l ∧ h ≤ f(k + 1) ⇒ Q ∧ k + 1 ∈ [m..n] ∪ {m − 1} ∧ ∧(l ↔ (∃j ∈ [m, k + 1] : β(j))) ∧ ∧(l → (ε(m, k + 1, k + 1) ∧ f(k + 1) = f(k + 1))) ⇔ P^{k←k+1}^{i,h←k+1,f(k+1)} ⇔ ⇔ lf(i, h := k + 1, f(k + 1), P^{k←k+1}), valamint P ∧ π ∧ β(k + 1) ∧ l ∧ h ≥ f(k + 1) ⇒ Q ∧ k + 1 ∈ [m..n] ∪ {m − 1} ∧ ∧(l ↔ (∃i ∈ [m, k + 1] : β(i))) ∧ ∧(l → (ε(m, k + 1, i) ∧ f(i) = h)) ⇔ P^{k←k+1} ⇔ ⇔ lf(SKIP, P^{k←k+1}). Alkalmazva az elágazásra érvényes levezetési szabályt, kapjuk: P ∧ π ∧ β(k + 1) ∧ l ⇔ lf(IF, P^{k←k+1}), ahol IF : (h ≤ f(k + 1) : i, h := k + 1, f(k + 1), h ≥ f(k + 1) : SKIP). Hasonlóan P ∧ π ∧ β(k + 1) ∧ ¬l ⇒ Q ∧ k + 1 ∈ [m..n] ∪ {m − 1} ∧ ∧(↑↔ (∃j ∈ [m, k + 1] : β(j))) ∧ ∧(↑→ (ε(m, k + 1, k + 1) ∧ f(k + 1) = f(k + 1))) ⇔ P^{k←k+1}^{l,i,h:=↑,k+1,f(k+1)} ⇔ ⇔ lf(l, i, h :=↑, k + 1, f(k + 1), P^{k←k+1}), valamint P ∧ π ∧ ¬β(k + 1) ⇒ Q ∧ k + 1 ∈ [m..n] ∪ {m − 1} ∧ ∧(l ↔ (∃i ∈ [m, k + 1] : β(i))) ∧ ∧(l → (ε(m, k + 1, i) ∧ f(i) = h)) ⇔ P^{k←k+1} ⇔ ⇔ lf(SKIP, P^{k←k+1}). Ismételten alkalmazva az elágazás levezetési szabályát, adódik: P ∧ π ⇒ lf(IF_{1}, P^{k←k+1}), ahol IF_{1}: (¬β(k + 1) : SKIP, β(k + 1) ∧ l : IF, β(k + 1) ∧ ¬l : l, i, h :=↑, k + 1, f(k + 1)). Tehát S_{0} = ( (¬β(k + 1) : SKIP, β(k + 1) ∧ l : IF, β(k + 1) ∧ ¬l : l, i, h :=↑, k + 1, f(k + 1)); k := k + 1) alkalmas választás a ciklus levezetési szabálya negyedik feltétele teljesüléséhez.

4. A ciklus levezetési szabálya ötödik feltétele: P ∧ π ∧ t ≤ t_{0} + 1 ⇒ lf(S_{0}, t ≤ t_{0}) minden t_{0} ∈ ℤ-re.

Belátható, hogy lf(S_{0}, t ≤ t_{0}) ⇔ lf(S_{1}, (t ≤ t_{0})^{k←k+1}) ⇔ n − k ≤ t_{0} + 1 ⇔ t ≤ t_{0} + 1 tetszőleges t_{0} ∈ ℤ-re, ezért a ciklus levezetési szabályának ötödik feltétele is teljesül.

5. Könnyen ellenőrizhető, hogy Q ⇒ P nem teljesül. Ugyanakkor látható, hogy Q ⇒ P^{k,l←m−1,↓} fennáll, mivel P^{k,l←m−1,↓} : (Q ∧ m − 1 ∈ [m..n] ∪ {m − 1} ∧ ∧(↓↔ (∃i ∈ [m, m − 1] : β(i))) ∧ ∧(↓→ (ε(m, m − 1, i) ∧ f(i) = h))), ugyanakkor (m − 1 ∈ [m..n] ∪ {m − 1} ∧ ∧(↓↔ (∃i ∈ [m, m − 1] : β(i))) ∧ ∧(↓→ (ε(m, m − 1, i) ∧ f(i) = h))) ⇔ true. Tehát Q ⇒ lf(k, l := m − 1, ↓, P). Ugyanakkor a ciklus levezetési szabálya első feltétele: P ⇒ P nyilván teljesül, ezért P ⇒ lf(DO, R) is igaz, ahol DO = (k < n, S_{0}). Alkalmazva a szekvenciával kapcsolatos levezetési szabályt, kapjuk: Q ⇒ lf((k, l := m − 1, ↓; DO), R)

Egy lehetséges megoldás tehát a következő program:

k, l := m − 1, ↓ ; k < n ; \overline{\¬β(k + 1) \  β(k + 1) ∧ l  \  β(k + 1) ∧ ¬l ; SKIP \frac{\begin{aligned}\  h ≤ f(k + 1) \\ & \ h ≥ f(k + 1) \end{aligned}}{\begin{aligned}i, h := k + 1, f(k + 1) \\ & SKIP \end{aligned}} l, i, h :=↑, k + 1, f(k + 1) ; k := k + 1}

6. Lineáris keresés

Legyen m ∈ ℤ, β : ℤ → 𝕃. Keressük meg azt a legkisebb β tulajdonságú egész számot, amely nem kisebb mint m. 6.1.

A =ℤ m×ℤ i

B ={Z \atop m′}

Q : (m = m′ ∧ ∃j ≥ m : β(j))

R : (Q ∧ i ≥ m′ ∧ β(i) ∧ ∀j ∈ [m′, i) : ¬β(j))

6.1.1. Lineáris keresés 1. változat

Keressük a megoldást adó programot ciklus formában, ahol

P : (Q ∧ i ≥ m ∧ ∀j ∈ [m, i) : ¬β(j))

1. Könnyen látható, hogy a ciklus levezetési szabálya második feltétele: P ∧ ¬π ⇒ R teljesül, ha ¬π : β(i). Tehát π : ¬β(i) alkalmas választás.

2. A ciklus levezetési szabálya harmadik feltétele:

P ∧ π ⇒ t > 0 teljesül, ha t = τ(m) − i, ahol a τ(m) függvényre: m ≤ τ(m) ∧ β(τ(m)). P ⇒ Q, viszont Q-ból következik, hogy ilyen m-től függő τ mindig létezik, ezért P -ből is következik, hogy ilyen m-től függő τ létezik. Könnyen látható, hogy P ∧ π ⇒ t > 0, mivel P ∧ π ⇒ ∀j ∈ [m, i] : ¬β(j), ezért P ∧ π ⇒ τ(m) > i.

3. Célszerű a ciklusmagot S_{0} : (S_{1}; S_{2}) szekvencia fomában keresni, ahol S_{2} = (i := i + 1) abból a meggondolásból, hogy a ciklus levezetési szabályának 5. feltétele is teljesüljön. Alkalmazva a szekvencia leggyengébb előfeltételére ismert tételt, P ∧ π ⇒ lf(S_{0}, P) ⇔ lf(S_{1}, lf(S_{2}, P)) teljesül, ha P ∧ π ⇒ lf(S_{1}, P^{i←i+1}), mivel lf(i := i + 1, P) ⇔ P^{i←i+1}. P^{i←i+1} : (Q ∧ i + 1 ≥ m ∧ ∀j ∈ [m, i + 1) : ¬β(j)), ugyanakkor P ∧ π ⇒ Q ∧ i ≥ m ∧ ∀j ∈ [m, i) : ¬β(j) ∧ ¬β(i) ⇒ Q ∧ i + 1 ≥ m ∧ ∀j ∈ [m, i + 1) : ¬β(j), ahonnan P ∧ π ⇒ P^{i←i+1}. Tehát már S_{0} = (i := i + 1) is alkalmas választás a ciklus levezetési szabálya negyedik feltétele teljesüléséhez.

4. A ciklus levezetési szabálya ötödik feltétele:

P ∧ π ∧ t ≤ t_{0} + 1 ⇒ lf(S_{0}, t ≤ t_{0}) minden t_{0} ∈ ℤ-re. Mivel lf(S_{0}, t ≤ t_{0}) ⇔ (t ≤ t_{0})^{i←i+1} ⇔ τ(m) − i ≤ t_{0} + 1 ⇔ t ≤ t_{0} + 1 tetszőleges t_{0} ∈ ℤ-re, ezért a ciklus levezetési szabályának ötödik feltétele is teljesül.

5. Könnyen ellenőrizhető, hogy Q ⇒ P nem teljesül. Ugyanakkor látható, hogy Q ⇒ P^{i←m} fennáll, mivel P^{i←m} : (Q ∧ m ≥ m ∧ ∀j ∈ [m, m) : ¬β(j)), és (m ≥ m ∧ ∀j ∈ [m, m) : ¬β(j)) ⇔ true. Tehát Q ⇒ lf(i := m, P). Ugyanakkor a ciklus levezetési szabálya első feltétele: P ⇒ P nyilván teljesül, ezért P ⇒ lf(DO, R) is igaz, ahol DO = (¬β(i), S_{0}). Alkalmazva a szekvenciával kapcsolatos levezetési szabályt, kapjuk: Q ⇒ lf((i := m; DO), R)

Egy lehetséges megoldás tehát a következő program:

i := m ; ¬β(i) ; \overline{i := i + 1}

6.1.2. Lineáris keresés 2. változat

Keressük a megoldást adó programot ciklus formában, ahol

P : (Q ∧ i ≥ m − 1 ∧ (∀j ∈ [m, i) : ¬β(j)) ∧ l = ∃j ∈ [m, i] : β(j))

1. Könnyen látható, hogy a ciklus levezetési szabálya második feltétele: P ∧ ¬π ⇒ R teljesül, ha ¬π : l. Tehát π : ¬l alkalmas választás.

2. A ciklus levezetési szabálya harmadik feltétele: P ∧ π ⇒ t > 0 teljesül, ha t = τ(m) − i, ahol a τ(m) függvényre: m ≤ τ(m) ∧ β(τ(m)). P ⇒ Q, viszont Q-ból következik, hogy ilyen m-től függő τ mindig létezik, ezért P -ből is következik, hogy ilyen m-től függő τ létezik. Könnyen látható, hogy P ∧ π ⇒ t > 0, mivel P ∧ π ⇒ ∀j ∈ [m, i] : ¬β(j), ezért P ∧ π ⇒ τ(m) > i.

3. Célszerű a ciklusmagot S_{0} : (S_{1}; S_{2}) szekvencia fomában keresni, ahol S_{2} = (i := i + 1) abból a meggondolásból, hogy a ciklus levezetési szabályának 5. feltétele is teljesüljön. Alkalmazva a szekvencia leggyengébb előfeltételére ismert tételt, P ∧ π ⇒ lf(S_{0}, P) ⇔ lf(S_{1}, lf(S_{2}, P)) teljesül, ha P ∧ π ⇒ lf(S_{1}, P^{i←i+1}), mivel lf(i := i + 1, P) ⇔ P^{i←i+1}. P^{i←i+1} : (Q∧i+1 ≥ m−1∧(∀j ∈ [m, i+1) : ¬β(j))∧l = ∃j ∈ [m, i+1] : β(j)), ugyanakkor P ∧ π ⇒ Q ∧ i ≥ m − 1 ∧ (∀j ∈ [m, i) : ¬β(j)) ∧ l = ∃j ∈ [m, i] : β(j) ∧ ¬β(i) ⇒ Q ∧ i + 1 ≥ m ∧ ∀j ∈ [m, i + 1) : ¬β(j) ∧ β(i + 1) = ∃j ∈ [m, i + 1] : β(j), ahonnan P ∧ π ⇒ P^{i←i+1}^{l←β(i+1)}. Ezért P ∧ π ⇒ lf(l := β(i + 1), P^{i←i+1}). Tehát S_{0} = (l := β(i + 1); i := i + 1) is alkalmas választás a ciklus levezetési szabálya negyedik feltétele teljesüléséhez.

4. A ciklus levezetési szabálya ötödik feltétele: P ∧ π ∧ t ≤ t_{0} + 1 ⇒ lf(S_{0}, t ≤ t_{0}) minden t_{0} ∈ ℤ-re. Mivel lf(S_{0}, t ≤ t_{0}) ⇔ (t ≤ t_{0})^{i←i+1} ⇔ τ(m) − i ≤ t_{0} + 1 ⇔ t ≤ t_{0} + 1 tetszőleges t_{0} ∈ ℤ-re, ezért a ciklus levezetési szabályának ötödik feltétele is teljesül.

5. Könnyen ellenőrizhető, hogy Q ⇒ P nem teljesül. Ugyanakkor látható, hogy Q ⇒ P^{i,l←m−1,↓} fennáll, mivel P^{i,l←m−1,↓} : (Q∧m−1 ≥ m−1∧(∀j ∈ [m, m−1) : ¬β(j))∧ ↓= ∃j ∈ [m, m−1] : β(j)), és (m − 1 ≥ m − 1 ∧ (∀j ∈ [m, m − 1) : ¬β(j))∧ ↓= ∃j ∈ [m, m − 1] : β(j)) ⇔ true. Tehát Q ⇒ lf(i, l := m, ↓, P). Ugyanakkor a ciklus levezetési szabálya első feltétele: P ⇒ P nyilván teljesül, ezért P ⇒ lf(DO, R) is igaz, ahol DO = (¬l, S_{0}). Alkalmazva a szekvenciával kapcsolatos levezetési szabályt, kapjuk: Q ⇒ lf((i, l := m − 1, ↓; DO), R)

Egy lehetséges megoldás tehát a következő program:

i, l := m − 1, ↓ ; ¬l ; \overline{\frac{l := β(i + 1)}{i := i + 1}}

6.2.

Tegyük fel, hogy β = γ ∨ δ és létezik i ≥ m, hogy δ(i). Állapítsuk meg, hogy van-e olyan i ≥ m, amelyre γ(i) igaz és az [m..i) intervallumban a δ mindenütt hamis. Ha van ilyen tulajdonságú i, akkor keressük meg a ezek közül a legkisebbet.

6.2.1. Lineáris keresés 3. változat

A =ℤ m×ℤ i×𝕃 u

B ={ℤ \atop m′}

Q : (m = m′ ∧ ∃j ≥ m : δ(j))

R : (Q ∧ (u ↔ ∃j ≥ m′ : (γ(j) ∧ ∀k ∈ [m′, j) : ¬δ(k))) ∧ ∧(u → (i ≥ m′ ∧ γ(i) ∧ ∀j ∈ [m′, i) : ¬β(j)))

Keressük a megoldást adó programot ciklus formában, ahol P : (Q ∧ i ≥ m − 1 ∧ (u ↔ (∃j ∈ [m, i] : γ(j))) ∧ (v ↔ (∃j ∈ [m, i] : δ(j))) ∧ ∧ ∀j ∈ [m, i) : ¬β(j)).

1. Belátható, hogy a ciklus levezetési szabálya második feltétele: P ∧ ¬π ⇒ R teljesül, ha ¬π : u ∨ v. Tegyük fel, hogy P ∧u teljesül, akkor nyilván Q teljesül, hiszen P -ben Q konjunkciós tag. Mivel u igaz a feltevés szerint és (u ↔ (∃j ∈ [m, i] : γ(j))) igaz, mert konjunkciós tag P -ben, ezért (∃j ∈ [m, i] : γ(j)) is igaz. De ∀j ∈ [m, i) : ¬β(j) is teljesül, mivel konjunkciós tag P -ben. E két utóbbi állításból következik, hogy γ(i) igaz, i ≥ m és ∀j ∈ [m, i) : ¬δ(j) is teljesül, mivel ha ¬β(j) igaz, akkor ¬δ(j) is igaz. Tehát ∃j ≥ m′ : (γ(j) ∧ ∀k ∈ [m′, j) : ¬δ(k)) is igaz, mert m = m′ igaz és i ≥ m ∧ (γ(i) ∧ ∀k ∈ [m, i) : ¬δ(k)) igaz. Ezért (u ↔ ∃j ≥ m′ : (γ(j) ∧ ∀k ∈ [m′, j) : ¬δ(k))) igaz, hiszen az ekvivalencia logikai műveletében mindkét tag igaz. A (i ≥ m′ ∧ γ(i) ∧ ∀j ∈ [m′, i) : ¬β(j)) állítást már az elzőekben beláttuk, ezért az (u → (i ≥ m′ ∧ γ(i) ∧ ∀j ∈ [m′, i) : ¬β(j))) állítás is igaz, mivel az implikáció logikai műveletében mindkét tag igaz. Adódott tehát, hogy P ∧ u ⇒ R Tegyük fel, hogy P ∧ ¬u ∧ v teljesül, akkor nyilván Q teljesül, hiszen P -ben Q konjunkciós tag. Ekkor (u → (i ≥ m′ ∧ γ(i) ∧ ∀j ∈ [m′, i) : ¬β(j))) nyilván igaz, mert u hamis, és ezért az implikáció biztosan igaz. A ∃j ≥ m′ : (γ(j) ∧ ∀k ∈ [m′, j) : ¬δ(k))) állítás viszont hamis, mert a (∃j ∈ [m, i] : γ(j)) állítás hamis, hiszen a (u ↔ (∃j ∈ [m, i] : γ(j))) ekvivalencia igaz, mivel konjunkciós tag P -ben és u hamis. Hasolóan, a (v ↔ (∃j ∈ [m, i] : δ(j))) ekvivalencia igaz, mivel konjunkciós tag P -ben. Ebből következik a v igaz feltétel miatt, hogy (∃j ∈ [m, i] : δ(j)) igaz és ezért i ≥ m. A ∀j ∈ [m, i) : ¬β(j) állítás is igaz, mert konjunkciós tag P -ben. Ebből viszont az következik, hogy i ≥ m ∧ δ(i) ∧ ¬γ(i) ∧ ∀j ∈ [m, i) : ¬β(j), tehát a ∃j ≥ m′ : (γ(j) ∧ ∀k ∈ [m′, j) : ¬δ(k))) biztosan hamis, mivel m = m′ és az i ≥ m pontokban a δ tulajdonság előbb teljesült, mint a γ tulajdonság. Ezért (u ↔ ∃j ≥ m′ : (γ(j) ∧ ∀k ∈ [m′, j) : ¬δ(k))) igaz, hiszen az ekvivalencia logikai műveletében mindkét tag hamis. Adódott tehát, hogy P ∧ ¬u ∧ v ⇒ R. Összegezve a fentieket, kapjuk, hogy P ∧ (u ∨ v) ⇒ R. Tehát π : ¬u ∧ ¬v alkalmas választás.

2. A ciklus levezetési szabálya harmadik feltétele:

P ∧ π ⇒ t > 0 teljesül, ha t = τ(m) − i, ahol a τ(m) függvényre: m ≤ τ(m) ∧ β(τ(m)). P ⇒ Q, viszont Q-ból következik, hogy ilyen m-től függő τ mindig létezik, ezért P -ből is következik, hogy ilyen m-től függő τ létezik. Könnyen látható, hogy P ∧ π ⇒ t > 0, mivel P ∧ π ⇒ ∀j ∈ [m, i] : ¬β(j), ezért P ∧ π ⇒ τ(m) > i.

3. Célszerű a ciklusmagot S_{0} : (S_{1}; S_{2}) szekvencia fomában keresni, ahol S_{2} = (i := i + 1) abból a meggondolásból, hogy a ciklus levezetési szabályának 5. feltétele is teljesüljön. Alkalmazva a szekvencia leggyengébb előfeltételére ismert tételt, P ∧ π ⇒ lf(S_{0}, P) ⇔ lf(S_{1}, lf(S_{2}, P)) teljesül, ha P ∧ π ⇒ lf(S_{1}, P^{i←i+1}), mivel lf(i := i + 1, P) ⇔ P^{i←i+1}. P^{i←i+1} : (Q ∧ i + 1 ≥ m − 1 ∧ (u ↔ (∃j ∈ [m, i + 1] : γ(j))) ∧ (v ↔ (∃j ∈ [m, i + 1] : δ(j))) ∧ ∧ ∀j ∈ [m, i + 1) : ¬β(j)), ugyanakkor P ∧ π ⇒ Q ∧ i ≥ m − 1 ∧ (u ↔ (∃j ∈ [m, i] : γ(j))) ∧ (v ↔ (∃j ∈ [m, i] : δ(j))) ∧ ∧ ∀j ∈ [m, i) : ¬β(j) ∧ ¬γ(i) ∧ ¬δ(i) ⇒ Q ∧ i + 1 ≥ m − 1 ∧ ∧(γ(i + 1) ↔ (∃j ∈ [m, i + 1] : γ(j))) ∧ (δ(i + 1) ↔ (∃j ∈ [m, i + 1] : δ(j))) ∧ ∧ ∀j ∈ [m, i + 1) : ¬β(j), ahonnan P ∧ π ⇒ P^{i←i+1}^{u,v←γ(i+1),δ(i+1)}. Ezért P ∧ π ⇒ lf(u, v := γ(i + 1), δ(i + 1), P^{i←i+1}). Tehát S_{0} = (u, v := γ(i + 1), δ(i + 1); i := i + 1) is alkalmas választás a ciklus levezetési szabálya negyedik feltétele teljesüléséhez.

4. A ciklus levezetési szabálya ötödik feltétele: P ∧ π ∧ t ≤ t_{0} + 1 ⇒ lf(S_{0}, t ≤ t_{0}) minden t_{0} ∈ ℤ-re. Mivel lf(S_{0}, t ≤ t_{0}) ⇔ (t ≤ t_{0})^{i←i+1} ⇔ τ(m) − i ≤ t_{0} + 1 ⇔ t ≤ t_{0} + 1 tetszőleges t_{0} ∈ ℤ-re, ezért a ciklus levezetési szabályának ötödik feltétele is teljesül.

5. Könnyen ellenőrizhető, hogy Q ⇒ P nem teljesül. Ugyanakkor látható, hogy Q ⇒ P^{i,u,v←m−1,↓,↓} fennáll, mivel P^{i,u,v←m−1,↓,↓} : (Q∧m−1 ≥ m−1∧(↓↔ (∃j ∈ [m, m−1] : γ(j)))∧(↓↔ (∃j ∈ [m, m−1] : δ(j)))∧ ∧ ∀j ∈ [m, m − 1) : ¬β(j)), és (m − 1 ≥ m − 1 ∧ (↓↔ (∃j ∈ [m, m − 1] : γ(j))) ∧ (↓↔ (∃j ∈ [m, m − 1] : δ(j))) ∧ ∧ ∀j ∈ [m, m − 1) : ¬β(j)) ⇔ true. Tehát Q ⇒ lf(i, u, v := m, ↓, ↓, P). Ugyanakkor a ciklus levezetési szabálya első feltétele: P ⇒ P nyilván teljesül, ezért P ⇒ lf(DO, R) is igaz, ahol DO = (¬u ∧ ¬v, S_{0}). Alkalmazva a szekvenciával kapcsolatos levezetési szabályt, kapjuk: Q ⇒ lf((i, u, v := m − 1, ↓, ↓; DO), R)

Egy lehetséges megoldás tehát a következő program:

i, u, v := m − 1, ↓, ↓ ; ¬u ∧ ¬v ; \overline{\frac{u, v := γ(i + 1), δ(i + 1)}{i := i + 1}}

6.2.2. Lineáris keresés 2.8. változat

Legyen m ∈ ℤ, n ∈ ℤ β : ℤ → 𝕃. Határozzuk meg, hogy van-e az [m, n] intervallumban β tulajdoságú egész szám és ha van, akkor keressük meg ezek közül a legkisebbet. Látható, hogy a Lineáris keresés 3. változatának speciális esetéről van szó, hiszen γ = β és δ = j ≥ n választásával a feladat visszavezethető a Lineáris keresés 3. változatára. A feladat direkt megoldása a következő:

A =ℤ m×ℤ n×ℤ i×𝕃 u

B ={ℤ \atop m′}×{ℤ \atop n′}

Q : (m = m′ ∧ n = n′ ∧ n + 1 ≥ m)

R : (Q ∧ (u ↔ ∃j ∈ [m′, n′] : β(j)) ∧ ∧(u → (i ∈ [m′, n′] ∧ β(i) ∧ ∀j ∈ [m′, i) : ¬β(j)))

Keressük a megoldást adó programot ciklus formában, ahol

P : (Q ∧ i ∈ [m − 1, n] ∧ (u ↔ (∃j ∈ [m, i] : β(j))) ∧ ∧ ∀j ∈ [m, i) : ¬β(j)).

1. Könnyen látható, hogy a ciklus levezetési szabálya második feltétele: P ∧ ¬π ⇒ R teljesül, ha ¬π : u ∨ i ≥ n. Tehát π : ¬u ∧ i < n alkalmas választás.

2. A ciklus levezetési szabálya harmadik feltétele:

P ∧ π ⇒ t > 0 teljesül, ha t : n − i.

3. Célszerű a ciklusmagot S_{0} : (S_{1}; S_{2}) szekvencia fomában keresni, ahol S_{2} = (i := i + 1) abból a meggondolásból, hogy a ciklus levezetési szabályának 5. feltétele is teljesüljön. Alkalmazva a szekvencia leggyengébb előfeltételére ismert tételt, P ∧ π ⇒ lf(S_{0}, P) ⇔ lf(S_{1}, lf(S_{2}, P)) teljesül, ha P ∧ π ⇒ lf(S_{1}, P^{i←i+1}), mivel lf(i := i + 1, P) ⇔ P^{i←i+1}. P^{i←i+1} : (Q ∧ i + 1 ∈ [m − 1, n] ∧ (u ↔ (∃j ∈ [m, i + 1] : β(j))) ∧ ∧ ∀j ∈ [m, i + 1) : ¬β(j), ugyanakkor P ∧ π ⇒ Q ∧ i + 1 ∈ [m − 1, n] ∧ (β(i + 1) ↔ (∃j ∈ [m, i + 1] : β(j))) ∧ ∧ (∀j ∈ [m, i + 1) : ¬β(j), ahonnan P ∧ π ⇒ P^{i←i+1}^{u←β(i+1)}. Ezért P ∧ π ⇒ lf(u := β(i + 1), P^{i←i+1}). Tehát S_{0} = (u := β(i + 1); i := i + 1) is alkalmas választás a ciklus levezetési szabálya negyedik feltétele teljesüléséhez.

4. A ciklus levezetési szabálya ötödik feltétele:

P ∧ π ∧ t ≤ t_{0} + 1 ⇒ lf(S_{0}, t ≤ t_{0}) minden t_{0} ∈ ℤ-re. Mivel lf(S_{0}, t ≤ t_{0}) ⇔ (t ≤ t_{0})^{i←i+1} ⇔ n−i ≤ t_{0} +1 ⇔ t ≤ t_{0} +1 tetszőleges t_{0} ∈ ℤ-re, ezért a ciklus levezetési szabályának ötödik feltétele is teljesül.

5. Könnyen ellenőrizhető, hogy Q ⇒ P nem teljesül. Ugyanakkor látható, hogy Q ∧ m ≤ n ⇒ P^{i,u←m−1,↓} fennáll, mivel P^{i,u←m−1,↓} :

(Q ∧ m − 1 ∈ [m − 1, n] ∧ (↓↔ (∃j ∈ [m, m − 1] : β(j))) ∧ ∧∀j ∈ [m, m − 1) : ¬β(j)), és (m − 1 ≥ m − 1 ∧ (↓↔ (∃j ∈ [m, m − 1] : β(j))) ∧ ∀j ∈ [m, m − 1) : ¬β(j)) ⇔ true. Tehát Q ∧ m ≤ n ⇒ lf(i, u := m − 1, ↓, P). Ugyanakkor a ciklus levezetési szabálya első feltétele: P ⇒ P nyilván teljesül, ezért P ⇒ lf(DO, R) is igaz, ahol DO = (¬u ∧ i < n, S_{0}). Alkalmazva a szekvenciával kapcsolatos levezetési szabályt, kapjuk: Q ⇒ lf((i, u := m − 1, ↓; DO), R).

Egy lehetséges megoldás tehát a következő program:

i, u := m − 1, ↓ ; ¬u ∧ i < n ; \overline{\frac{u := β(i + 1)}{i := i + 1}}

Megjegyzés I.

A Lineáris keresés 3. változatának a következő feladatot is szokták tekinteni: Tegyük fel, hogy β = γ ∨ δ és létezik i ≥ m, hogy β(i). Keressük meg a legkisebb olyan i-t, amire i ≥ m és β(i), és adjuk meg azt is, hogy γ(i), illetve δ(i) igaz-e!

A =ℤ m×ℤ i×𝕃 u×𝕃 v

B ={ℤ \atop m′}

Q : (m = m′ ∧ ∃j ≥ m′ : β(j))

R : (Q ∧ i ≥ m′ ∧ β(i) ∧ ∀j ∈ [m′, i) : ¬β(j) ∧ ∧ (u ↔ γ(i)) ∧ (v ↔ δ(i)))

Keressük a megoldást adó programot ciklus formában, ahol

P : (Q ∧ i ≥ m − 1 ∧ (u ↔ (∃j ∈ [m, i] : γ(j))) ∧ (v ↔ (∃j ∈ [m, i] : δ(j))) ∧ ∧ ∀j ∈ [m, i) : ¬β(j))

.

1. Könnyen látható, hogy a ciklus levezetési szabálya második feltétele: P ∧ ¬π ⇒ R teljesül, ha ¬π : u ∨ v. Tehát π : ¬u ∧ ¬v alkalmas választás.

2. A ciklus levezetési szabálya harmadik feltétele: P ∧ π ⇒ t > 0 teljesül, ha t = τ(m) − i, ahol a τ(m) függvényre: m ≤ τ(m) ∧ β(τ(m)). P ⇒ Q, viszont Q-ból következik, hogy ilyen m-től függő τ mindig létezik, ezért P -ből is következik, hogy ilyen m-től függő τ létezik. Könnyen látható, hogy P ∧ π ⇒ t > 0, mivel P ∧ π ⇒ ∀j ∈ [m, i] : ¬β(j), ezért P ∧ π ⇒ τ(m) > i.

3. Célszerű a ciklusmagot S_{0} : (S_{1}; S_{2}) szekvencia fomában keresni, ahol S_{2} = (i := i + 1) abból a meggondolásból, hogy a ciklus levezetési szabályának 5. feltétele is teljesüljön. Alkalmazva a szekvencia leggyengébb előfeltételére ismert tételt, P ∧ π ⇒ lf(S_{0}, P) ⇔ lf(S_{1}, lf(S_{2}, P)) teljesül, ha P ∧ π ⇒ lf(S_{1}, P^{i←i+1}), mivel lf(i := i + 1, P) ⇔ P^{i←i+1}. P^{i←i+1} : (Q ∧ i + 1 ≥ m − 1 ∧ (u ↔ (∃j ∈ [m, i + 1] : γ(j))) ∧ (v ↔ (∃j ∈ [m, i + 1] : δ(j))) ∧ ∧ ∀j ∈ [m, i + 1) : ¬β(j)), ugyanakkor P ∧ π ⇒ Q ∧ i ≥ m − 1 ∧ (u ↔ (∃j ∈ [m, i] : γ(j))) ∧ (v ↔ (∃j ∈ [m, i] : δ(j))) ∧ ∧ ∀j ∈ [m, i) : ¬β(j) ∧ ¬γ(i) ∧ ¬δ(i) ⇒ Q ∧ i + 1 ≥ m − 1 ∧ ∧(γ(i + 1) ↔ (∃j ∈ [m, i + 1] : γ(j))) ∧ (δ(i + 1) ↔ (∃j ∈ [m, i + 1] : δ(j))) ∧ ∧ ∀j ∈ [m, i + 1) : ¬β(j), ahonnan P ∧ π ⇒ P^{i←i+1}^{u,v←γ(i+1),δ(i+1)}. Ezért P ∧ π ⇒ lf(u, v := γ(i + 1), δ(i + 1), P^{i←i+1}). Tehát S_{0} = (u, v := γ(i + 1), δ(i + 1); i := i + 1) is alkalmas választás a ciklus levezetési szabálya negyedik feltétele teljesüléséhez.

4. A ciklus levezetési szabálya ötödik feltétele: P ∧ π ∧ t ≤ t_{0} + 1 ⇒ lf(S_{0}, t ≤ t_{0}) minden t_{0} ∈ ℤ-re.

Mivel lf(S_{0}, t ≤ t_{0}) ⇔ (t ≤ t_{0})^{i←i+1} ⇔ τ(m) − i ≤ t_{0} + 1 ⇔ t ≤ t_{0} + 1 tetszőleges t_{0} ∈ ℤ-re, ezért a ciklus levezetési szabályának ötödik feltétele is teljesül.

5. Könnyen ellenőrizhető, hogy Q ⇒ P nem teljesül. Ugyanakkor látható, hogy Q ⇒ P^{i,u,v←m−1,↓,↓} fennáll, mivel P^{i,u,v←m−1,↓,↓} : (Q∧m−1 ≥ m−1∧(↓↔ (∃j ∈ [m, m−1] : γ(j)))∧(↓↔ (∃j ∈ [m, m−1] : δ(j)))∧ ∧ ∀j ∈ [m, m − 1) : ¬β(j)), és (m − 1 ≥ m − 1 ∧ (↓↔ (∃j ∈ [m, m − 1] : γ(j))) ∧ (↓↔ (∃j ∈ [m, m − 1] : δ(j))) ∧ ∧ ∀j ∈ [m, m − 1) : ¬β(j)) ⇔ true. Tehát Q ⇒ lf(i, u, v := m, ↓, ↓, P). Ugyanakkor a ciklus levezetési szabálya első feltétele: P ⇒ P nyilván teljesül, ezért P ⇒ lf(DO, R) is igaz, ahol DO = (¬u ∧ ¬v, S_{0}). Alkalmazva a szekvenciával kapcsolatos levezetési szabályt, kapjuk: Q ⇒ lf((i, u, v := m − 1, ↓, ↓; DO), R)

Egy lehetséges megoldás tehát a következő program:

i, u, v := m − 1, ↓, ↓ ; ¬u ∧ ¬v ; \overline{\frac{u, v := γ(i + 1), δ(i + 1)}{i := i + 1}}

Megjegyzés II.:

Nyilvánvaló, hogy (Q ∧ i ≥ m′ ∧ β(i) ∧ ∀j ∈ [m′, i) : ¬β(j) ∧ (u ↔ γ(i)) ∧ (v ↔ δ(i))) ⇒ (Q ∧ i ≥ m′ ∧ β(i) ∧ ∀j ∈ [m′, i) : ¬β(j) ∧ (u ↔ γ(i))), valamint (Q ∧ i ≥ m′ ∧ β(i) ∧ ∀j ∈ [m′, i) : ¬β(j) ∧ (u ↔ γ(i)) ∧ (v ↔ δ(i))) ⇒ (Q ∧ i ≥ m′ ∧ β(i) ∧ ∀j ∈ [m′, i) : ¬β(j) ∧ (v ↔ δ(i))). Ezért a fenti program

R′ : (Q ∧ i ≥ m′ ∧ β(i) ∧ ∀j ∈ [m′, i) : ¬β(j) ∧ (u ↔ γ(i))), illetve

R′ : (Q ∧ i ≥ m′ ∧ β(i) ∧ ∀j ∈ [m′, i) : ¬β(j) ∧ (u ↔ γ(i)))

feltétel mellett is megoldja a feladatot.

A Lineáris keresés 2.8-as változata a az előző 3. változat speciális esete δ(j) = (j ≥ n) választással. Ennek megfelelően a következők érvényesek:

A =ℤ m×ℤ n×ℤ i×𝕃 u

B ={ℤ \atop m′}×{ℤ \atop n′}

Q : (m = m′ ∧ n = n′)

R : (Q ∧ i ≥ m′ ∧ (γ(i) ∨ i ≥ n′) ∧ ((∀j ∈ [m′, i) : ¬γ(j)) ∧ (∀j ∈ [m′, i) : j < n)) ∧ ∧ (u ↔ γ(i)))

Keressük a megoldást adó programot ciklus formában, ahol

P : (Q ∧ m ≤ n ∧ i ≥ m − 1 ∧ (u ↔ (∃j ∈ [m, i] : γ(j))) ∧ ∧ ((∀j ∈ [m, i) : ¬γ(j)) ∧ (∀j ∈ [m, i) : j < n)))

1. Könnyen látható, hogy a ciklus levezetési szabálya második feltétele: P ∧ ¬π ⇒ R teljesül, ha ¬π : u ∨ i ≥ n. Tehát π : ¬u ∧ i < n alkalmas választás.

2. A ciklus levezetési szabálya harmadik feltétele:

P ∧ π ⇒ t > 0 teljesül, ha t = τ(m, n) − i, ahol a τ(m, n) függvényre: m ≤ τ(m, n) ∧ β(τ(m, n)). β = γ ∨ δ és δ(j) = (j ≥ n) miatt ilyen m-től és n-től függő τ mindig létezik. Könnyen látható, hogy P ∧ π ⇒ t > 0, mivel P ∧ π ⇒ ∀j ∈ [m, i] : ¬β(j), ezért P ∧ π ⇒ τ(m) > i.

3. Célszerű a ciklusmagot S_{0} : (S_{1}; S_{2}) szekvencia fomában keresni, ahol S_{2} = (i := i + 1) abból a meggondolásból, hogy a ciklus levezetési szabályának 5. feltétele is teljesüljön. Alkalmazva a szekvencia leggyengébb előfeltételére ismert tételt, P ∧ π ⇒ lf(S_{0}, P) ⇔ lf(S_{1}, lf(S_{2}, P)) teljesül, ha P ∧ π ⇒ lf(S_{1}, P^{i←i+1}), mivel lf(i := i + 1, P) ⇔ P^{i←i+1}. P^{i←i+1} : (Q ∧ m ≤ n ∧ i + 1 ≥ m − 1 ∧ (u ↔ (∃j ∈ [m, i + 1] : γ(j))) ∧ ∧ ((∀j ∈ [m, i + 1) : ¬γ(j)) ∧ i + 1 ≤ n)), ugyanakkor P ∧ π ⇒ Q ∧ m ≤ n ∧ i + 1 ≥ m − 1 ∧ (γ(i + 1) ↔ (∃j ∈ [m, i + 1] : γ(j))) ∧ ∧ ((∀j ∈ [m, i + 1) : ¬γ(j)) ∧ (∀j ∈ [m, i + 1) : j < n)), ahonnan P ∧ π ⇒ P^{i←i+1}^{u←γ(i+1)}. Ezért P ∧ π ⇒ lf(u := γ(i + 1), P^{i←i+1}). Tehát S_{0} = (u := γ(i + 1); i := i + 1) is alkalmas választás a ciklus levezetési szabálya negyedik feltétele teljesüléséhez.

4. A ciklus levezetési szabálya ötödik feltétele: P ∧ π ∧ t ≤ t_{0} + 1 ⇒ lf(S_{0}, t ≤ t_{0}) minden t_{0} ∈ ℤ-re. Mivel lf(S_{0}, t ≤ t_{0}) ⇔ (t ≤ t_{0})^{i←i+1} ⇔ τ(m) − i ≤ t_{0} + 1 ⇔ t ≤ t_{0} + 1 tetszőleges t_{0} ∈ ℤ-re, ezért a ciklus levezetési szabályának ötödik feltétele is teljesül.

5. Könnyen ellenőrizhető, hogy Q ⇒ P nem teljesül. Ugyanakkor látható, hogy Q ∧ m ≤ n ⇒ P^{i,u←m−1,↓} fennáll, mivel P^{i,u←m−1,↓} : (Q ∧ m ≤ n ∧ m − 1 ≥ m − 1 ∧ (↓↔ (∃j ∈ [m, m − 1] : γ(j))) ∧ ∧ ((∀j ∈ [m, m − 1) : ¬γ(j)) ∧ (∀j ∈ [m, m − 1) : j < n)), és (m − 1 ≥ m − 1 ∧ (↓↔ (∃j ∈ [m, m − 1] : γ(j))) ∧ ∧ ((∀j ∈ [m, m − 1) : ¬γ(j)) ∧ (∀j ∈ [m, m − 1) : j < n)) ⇔ true. Tehát Q ∧ m ≤ n ⇒ lf(i, u := m − 1, ↓, P). Ugyanakkor a ciklus levezetési szabálya első feltétele: P ⇒ P nyilván teljesül, ezért P ⇒ lf(DO, R) is igaz, ahol DO = (¬u ∧ i < n, S_{0}). Alkalmazva a szekvenciával kapcsolatos levezetési szabályt, kapjuk: Q ∧ m ≤ n ⇒ lf((i, u := m − 1, ↓; DO), R). Ugyanakkor

Q ∧ m > n ⇒ R^{i,u←m,γ(m)},
mivel R^{i,u←m,γ(m)} ⇔

Q∧m ≥ m′∧(γ(m)∨m ≥ n′)∧((∀j ∈ [m′, m) : ¬γ(m))∧(∀j ∈ [m′, m) : j < n))∧

∧ (γ(m) ↔ γ(m)).

Egy lehetséges megoldás tehát a következő program:

\frac{\  m ≤ n  /}{i, u := m − 1, ↓ ; ¬u ∧ i < n ; \overline{\frac{u := γ(i + 1)}{i := i + 1}} ; i, u := m, γ(m)}

Ha valódi intervallumban keresünk, azaz

Q : (m = m′ ∧ n = n′ ∧ m ≤ n)

feltételből indulunk ki, akkor az előzőek alapján, a keresett program:

i, u := m − 1, ↓ ; ¬u ∧ i < n ; \overline{\frac{u := γ(i + 1)}{i := i + 1}}

Ebben az esetben könnyen belátható, hogy

(Q ∧ i ≥ m′ ∧ (γ(i) ∨ i ≥ n′) ∧ ((∀j ∈ [m′, i) : ¬γ(j)) ∧ (∀j ∈ [m′, i) : j < n)) ∧ ∧ (u ↔ γ(i))) ⇒ (Q ∧ (u ↔ ∃j ∈ [m′..n′] : γ(j)) ∧ (u → (i ∈ [m′..n′] ∧ γ(i) ∧ ∀j ∈ [m′..i) : ¬γ(j)))), valamint (Q ∧ i ≥ m′ ∧ (γ(i) ∨ i ≥ n′) ∧ ((∀j ∈ [m′, i) : ¬γ(j)) ∧ (∀j ∈ [m′, i) : j < n)) ∧ ∧ (u ↔ γ(i))) ⇒ (Q ∧ (u ↔ ∃j ∈ [m′..n′] : γ(j)) ∧ ∧(u → (i ∈ [m′..n′] ∧ γ(i) ∧ ∀j ∈ [m′..i) : ¬γ(j))) ∧ (¬u → i = n′)).

Tehát a fenti program

R′ : (Q ∧ (u ↔ ∃j ∈ [m′..n′] : γ(j)) ∧ (u → (i ∈ [m′..n′] ∧ γ(i) ∧ ∀j ∈ [m′..i) : ¬γ(j)))),

valamint

R′ : (Q ∧ (u ↔ ∃j ∈ [m′..n′] : γ(j)) ∧ ∧(u → (i ∈ [m′..n′] ∧ γ(i) ∧ ∀j ∈ [m′..i) : ¬γ(j))) ∧ (¬u → i = n′)) feltételek mellett is megoldja a feladatot, ugyanakkor ez utóbbi feltételek direkt módon fejezi ki a megoldandó problémát. Természtesen ez utóbbi feltételekből kiindulva a levezetések a lineáris keresés 3. változatára történő visszautalás nélkül is elkészíthetőek.

7. Logaritmikus keresés

Legyen H egy olyan halmaz, amin értelmezve van egy rendezési reláció. Legyen f : ℤ → H monoton növekedő függvény. Döntsük el egy adott h ∈ H értékről, hogy felveszi-e azt az f függvény egy adott [m, n] ⊂ ℤ intervallumon, és ha igen, akkor adjuk meg egy olyan pontját, ahol a függvényérték h.

A =ℤ m×ℤ n×ℤ i×H h×𝕃 l

B ={ℤ \atop m′}×{ℤ \atop n′}×{H \atop h′}

Q : (m = m′ ∧ n = n′ ∧ h = h′ ∧ ∀j, k ∈ [m′..n′] : j ≤ k → f(j) ≤ f(k))

R : (Q ∧ l = (∃j ∈ [m′..n′] : f(j) = h′) ∧ (l → (i ∈ [m′..n′] ∧ f(i) = h′)))

Keressük a megoldást adó programot ciklus formában, ahol

P : (Q ∧ [u, v] ⊆ [m..n] ∧ ∀j ∈ [m..n] \ [u, v] : f(j) ≠ h ∧ (l → (i ∈ [u, v] ∧ f(i) = h)))

1. A ciklus levezetési szabálya második feltétele:

P ∧ ¬π ⇒ R teljesül, ha ¬π : l ∨ u > v. Tehát π : ¬l ∧ u ≤ v alkalmas választás.

2. A ciklus levezetési szabálya harmadik feltétele:

P ∧ π ⇒ t > 0 teljesül, ha t : v − u + 1 − χ(l).

3. Az f függvény monotonitására tett feltételt kihasználva rendre igazolhatók a következő állítások: P ∧ (¬l ∧ u ≤ v) ∧ i = [(u + v)/2] ∧ f(i) < h ⇒ P^{u←i+1}, P ∧ (¬l ∧ u ≤ v) ∧ i = [(u + v)/2] ∧ f(i) > h ⇒ P^{v←i−1}, valamint P ∧ (¬l ∧ u ≤ v) ∧ i = [(u + v)/2] ∧ f(i) = h ⇒ P^{l←↑}. Alkalmazva az elágazás levezetési szabályát, kapjuk: P ∧ (¬l ∧ u ≤ v) ∧ i = [(u + v)/2] ⇒ lf(IF, P), ahol IF : (f(i) < h : u := i + 1, f(i) > h : v := i − 1, f(i) = h : l :=↑). Ugyanakkor P ∧ (¬l ∧ u ≤ v) ⇔ lf(i := [(u + v)/2], P ∧ (¬l ∧ u ≤ v) ∧ i = [(u + v)/2]), mivel lf(i := [(u + v)/2], P ∧ (¬l ∧ u ≤ v) ∧ i = [(u + v)/2]) ⇔ P ∧ (¬l ∧ u ≤ v) ∧ i = [(u + v)/2]^{i←[(u+v)/2]} ⇔ P ∧ (¬l ∧ u ≤ v).

Alkalmazva a szekvencia leggyengébb előfeltételére az ismert tételt, kapjuk: P ∧ (¬l ∧ u ≤ v) ⇒ lf((i := [(u + v)/2]; IF), P), tehát S_{0} : (i := [(u + v)/2]; IF) alkalmas választás a ciklus levezetési szabálya negyedik feltételének teljesítéséhez.

4. A ciklus levezetési szabálya ötödik feltétele: P ∧ π ∧ t ≤ t_{0} + 1 ⇒ lf(S_{0}, t ≤ t_{0}) minden t_{0} ∈ ℤ-re. Alkalmazva a szekvencia levezetési szabályának megfordítását, ha belátjuk, hogy P ∧ π ∧ t ≤ t_{0} + 1 ∧ i = [(u + v)/2] ⇒ lf(IF, t ≤ t_{0}) tetszőleges t_{0} ∈ ℤ-re, akkor a ciklus levezetési szabályának ötödik feltétele is teljesül, mivel P ∧ π ∧ t ≤ t_{0} + 1 ⇔ lf(i := [(u + v)/2], P ∧ π ∧ t ≤ t_{0} + 1 ∧ i = [(u + v)/2]). Alkalmazva az elágazás levezetési szabályának megfordítását, ha belátjuk, hogy P ∧ π ∧ t ≤ t_{0} + 1 ∧ i = [(u + v)/2] ∧ f(i) < h ⇒ lf(u := i + 1, t ≤ t_{0}), P ∧ π ∧ t ≤ t_{0} + 1 ∧ i = [(u + v)/2] ∧ f(i) > h ⇒ lf(v := i − 1, t ≤ t_{0}), valamint P ∧ π ∧ t ≤ t_{0} + 1 ∧ i = [(u + v)/2] ∧ f(i) = h ⇒ lf(l :=↑, t ≤ t_{0}), akkor P ∧ π ∧ t ≤ t_{0} + 1 ∧ i = [(u + v)/2] ⇒ lf(IF, t ≤ t_{0}) tetszőleges t_{0} ∈ ℤ-re, és ezért a ciklus levezetési szabályának ötödik feltétele is teljesül. Egyszerű belátni, hogy a t választása miatt mindhárom fenti állítás igaz.

5. Könnyen ellenőrizhető, hogy Q ⇒ P nem teljesül. Ugyanakkor látható, hogy Q ⇒ P^{u,v,l←m,n,↓} fennáll, mivel P^{u,v,l←m,n,↓} : (Q∧[m, n] ⊆ [m..n]∧∀j ∈ [m..n]\[m, n] : f(j) ≠ h∧(↓→ (i ∈ [m, n]∧f(i) = h))), és ([m, n] ⊆ [m..n] ∧ ∀j ∈ [m..n] \ [m, n] : f(j) ≠ h ∧ (↓→ (i ∈ [m, n] ∧ f(i) = h))) ⇔ true. Tehát Q ⇒ lf(u, v, l := m, n, ↓, P). Ugyanakkor a ciklus levezetési szabálya első feltétele: P ⇒ P nyilván teljesül, ezért P ⇒ lf(DO, R) is igaz, ahol DO = (¬l ∧ u ≤ v, S_{0}). Alkalmazva a szekvenciával kapcsolatos levezetési szabályt, kapjuk: Q ⇒ lf((u, v, l := m, n, ↓; DO), R)

Egy lehetséges megoldás tehát a következő program:

u, v, l := m, n, ↓ ; ¬l ∧ (u ≤ v) ; \overline{i := [(u + v)/2] ; \ f(i) < h \ f(i) > h \ f(i) = h ; u := i + 1  v := i − 1  l :=↑}

Megjegyzés:

3’ Az i = [(u + v)/2] feltétel a P ∧ (¬l ∧ u ≤ v) ∧ i = [(u + v)/2] ∧ f(i) < h ⇒ P^{u←i+1}, P ∧ (¬l ∧ u ≤ v) ∧ i = [(u + v)/2] ∧ f(i) > h ⇒ P^{v←i−1}, valamint P ∧ (¬l ∧ u ≤ v) ∧ i = [(u + v)/2] ∧ f(i) = h ⇒ P^{l←↑} állításokban nem tűnik természetesnek első látásra. Valóban, a levezetés mögött húzódó matematikai meggondolás alapján, mely szerint az [u, v] intervallum fokozatos szűkítése a cél, az alábbi összefüggések adódnak közvetlenül: P ∧ (¬l ∧ u ≤ v) ∧ f([(u + v)/2]) < h ⇒ P^{u←[(u+v)/2]+1}, P ∧ (¬l ∧ u ≤ v) ∧ f([(u + v)/2]) > h ⇒ P^{v←[(u+v)/2]−1}, valamint P ∧ (¬l ∧ u ≤ v) ∧ f([(u + v)/2]) = h ⇒ P^{i,l←[(u+v)/2],↑}. A fentiek alapján S_{0} : (f([(u + v)/2]) < h : u := [(u + v)/2] + 1, f([(u + v)/2]) > h : v := [(u + v)/2] − 1, f([(u + v)/2]) = h : i, l := [(u + v)/2], ↑) alkalmas választás a ciklus levezetési szabálya negyedik feltételének teljesítéséhez. A levezetés többi lépése változatlanul érvényes. Gyakorlati szempontból azonban a fenti módszer nem tűnik gazdaságosnak, mivel valahányszor hivatkozás történik a [(u+v)/2] értékre, mindannyiszor ki kell azt számolni. Az eredetileg alkalmazott módszer éppen ezt küszöböli ki. E feledatban a gyakran hivatkozott aritmetikai kifejezés értékének előre történő kiszámítására láttunk példát.

8. Speciális formában adott függvény értékének kiszámítása adott helyen

8.1. Függvénykompozícióval definiált függvény

Legyenek H_{1}, H_{2}, H_{3} tetszőleges halmazok, továbbá f : H_{1} → H_{3}, g : H_{1} → H_{2}, h : H_{2} → H_{3} olyan függvények, hogy f = h ∘ g. Határozzuk meg az f függvény v ∈ H_{1} helyen felvett értékét.

A ={H_{1} \atop v}×{H_{3} \atop z}

B ={H_{1} \atop v′}

Q : (v = v′)

R : (Q ∧ z = f(v′))

Legyen R′ : (Q ∧ z = h(w) ∧ w = g(v)). Könnyen látható, hogy R′ ⇒ R. Ugyanakkor Q ⇒ (R′^{z←h(w)})^{w←g(v)} is teljesül. Ezért a szekvencia leggyengébb előfeltételére ismert összefüggés alapján Q ⇒ lf((w := g(v); z := h(w)), R′). R′ ⇒ R miatt Q ⇒ lf((w := g(v); z := h(w)), R) is teljesül.

Egy lehetséges megoldás tehát a következő program:

\frac{w := g(v)}{z := h(w)}

8.2. Esetszétválasztásos függvény

Legyen H egy tetszőleges halmaz, f : ℤ → H, h_{1},…, h_{k} : ℤ → H, π_{1},…, π_{k} : ℤ → 𝕃, amelyekre

f(i) := \{ \begin{matrix}h_{1}(i) & , ha π_{1}(i) \\ ⋮ & ⋮ \\ h_{k}(i) & , ha π_{k}(i) \end{matrix}

Határozzuk meg az f parciális függvény v helyen felvett értékét!

A =ℤ v×H z

B ={ℤ \atop v′}

Q : (v = v′ ∧ v′ ∈ ⋃_{j=1}^{k}[π_{j}])

R : (Q ∧ z = f(v′))

A feltételek alapjan Q ∧ π_{i}(v) ⇒ Q ∧ h_{i}(v) = f(v) ⇔ (Q ∧ z = f(v))^{z←h_{i}(v)}. Tehát minden i ∈ [1..k] esetén Q ∧ π_{i}(v) ⇒ lf(z := h_{i}(v), R).

Alkalmazva az elágazás levezetési szabályát, adódik: Q ∧ (∨_{i=1}^{k}π_{i}(v)) ⇒ lf(IF, R), De nyilván Q ∧ (∨_{i=1}^{k}π_{i}(v)) ⇔ Q, ezért Q ⇒ lf(IF, R), ahol IF : (π_{1} : z := h_{1}, ..., π_{k} : z := h_{k}).

Egy lehetséges megoldás tehát a következő program:

\frac{\ π_{1}(v)  \ … \ π_{k}(v)}{z := h_{1}(v)  …  z := h_{k}(v)}

8.3. Rekurzív formulával definiált függvény

Legyen H egy tetszőleges halmaz, k ∈ ℕ, f : ℤ → H, h : ℤ × H^{k} → H olyan függvények, hogy f(t_{0}) = f_{0}, f(t_{0} − 1) = f_{−1}, …, f(t_{0} − k + 1) = f_{−k+1} (t_{0} ∈ ℤ) és ∀i ≥ t_{0} : f(i + 1) = h(i + 1, f(i),…, f(i − k + 1)). Határozzuk meg az f függvény n > t_{0} helyen felvett értékét.

A =ℤ n×H z

B ={ℤ \atop n′}

Q : (n = n′ ∧ n ≥ t_{0})

R : (Q ∧ z = f(n′))

Keressük a megoldást adó programot ciklus formában, ahol

P : (Q ∧ t_{0} ≤ i ≤ n ∧ z = f(i) ∧ z_{−1} = f(i − 1) ∧… ∧ z_{−k+1} = f(i − k + 1))

1. Könnyen látható, hogy a ciklus levezetési szabálya második feltétele: P ∧ ¬π ⇒ R teljesül, ha ¬π : (i = n). Tehát π : i ≠ n alkalmas választás.

2. A ciklus levezetési szabálya harmadik feltétele:

P ∧ π ⇒ t > 0 teljesül, ha t = n − i, a π választása és amiatt, hogy P ∧ π ⇒ t_{0} ≤ i ≤ n ∧ i ≠ n ⇒ i < n.

3. Célszerű a ciklusmagot S_{0} : (S_{1}; S_{2}) szekvencia fomában keresni, ahol S_{2} = (i := i + 1) abból a meggondolásból, hogy a ciklus levezetési szabályának 5. feltétele is teljesüljön. Alkalmazva a szekvencia leggyengébb előfeltételére ismert tételt, P ∧ π ⇒ lf(S_{0}, P) ⇔ lf(S_{1}, lf(S_{2}, P)) teljesül, ha P ∧ π ⇒ lf(S_{1}, P^{i←i+1}), mivel lf(i := i + 1, P) ⇔ P^{i←i+1}. P^{i←i+1} : (Q∧t_{0} ≤ i+1 ≤ n∧z = f(i+1)∧z_{−1} = f(i)∧…∧z_{−k+1} = f(i−k+2)), ugyanakkor P ∧ π ⇒ ⇒ Q ∧ t_{0} ≤ i + 1 ≤ n ∧ h(i + 1, z, z_{−1},…, z_{−k+1}) = f(i + 1) ∧ ∧z = f(i) ∧… ∧ z_{−k+2} = f(i − k + 2) ⇔ ⇔ P^{i←i+1}^{z,z_{−1},...,z_{−k+1}←h(i+1,z,z_{−1},...,z_{−k+1}),z,z_{−1},...,z_{−k+2}}. Mivel P^{i←i+1}^{z,z_{−1},...,z_{−k+1}←h(i+1,z,z_{−1},...,z_{−k+1}),z,z_{−1},...,z_{−k+2}} ⇔ ⇔ lf(z, z_{−1},…, z_{−k+1} := h(i + 1, z, z_{−1},…, z_{−k+1}), z, z_{−1},…, z_{−k+2}, P^{i←i+1}), ezért S_{1} : (z, z_{−1},…, z_{−k+1} := h(i + 1, z, z_{−1},…, z_{−k+1}), z, z_{−1},…, z_{−k+2}) alkalmas választás.

4. A ciklus levezetési szabálya ötödik feltétele: P ∧ π ∧ t ≤ t_{0} + 1 ⇒ lf(S_{0}, t ≤ t_{0}) minden t_{0} ∈ ℤ-re. Mivel lf(S_{0}, t ≤ t_{0}) ⇔ (t ≤ t_{0})^{i←i+1}^{z,z_{−1},...,z_{−k+1}←h(i+1,z,z_{−1},...,z_{−k+1}),z,z_{−1},...,z_{−k+2}} ⇔ ⇔ n − i ≤ t_{0} + 1 ⇔ t ≤ t_{0} + 1 tetszőleges t_{0} ∈ ℤ-re, ezért a ciklus levezetési szabályának ötödik feltétele is teljesül.

5. Könnyen ellenőrizhető, hogy Q ⇒ P nem teljesül. Ugyanakkor látható, hogy Q ⇒ P^{i,z,z_{−1},...,z_{−k+1}←t_{0},f_{0},f_{−1},...,f_{−k+1}} fennáll, mivel P^{i,z,z_{−1},...,z_{−k+1}←t_{0},f_{0},f_{−1},...,f_{−k+1}} ⇔ ⇔ Q ∧ t_{0} ≤ t_{0} ≤ n ∧ f_{0} = f(t_{0}) ∧ f_{−1} = f(t_{0} − 1) ∧… ∧ f_{−k+1} = f(t_{0} − k + 1) és (f_{0} = f(t_{0}) ∧ f_{−1} = f(t_{0} − 1) ∧… ∧ f_{−k+1} = f(t_{0} − k + 1) ⇔ true. és Q ⇒ Q ∧ t_{0} ≤ t_{0} ≤ n a Q választása miatt. Tehát Q ⇒ lf(i, z, z_{−1},…, z_{−k+1} := t_{0}, f_{0}, f_{−1},…, f_{−k+1}, P). Ugyanakkor a ciklus levezetési szabálya első feltétele: P ⇒ P nyilván teljesül, ezért P ⇒ lf(DO, R) is igaz, ahol DO = (i ≠ n, S_{0}). Alkalmazva a szekvenciával kapcsolatos levezetési szabályt, kapjuk: Q ⇒ lf((i, z, z_{−1},…, z_{−k+1} := t_{0}, f_{0}, f_{−1},…, f_{−k+1}; DO), R)

Egy lehetséges megoldás tehát a következő program:

i, z, z_{−1}, .., z_{−k+1} := t_{0}, f_{0}, f_{−1}, .., f_{−k+1} ; i ≠ n ; \overline{\frac{z, z_{−1}, .., z_{−k+1} := h(i + 1, z,…, z_{−k+1}), z, .., z_{−k+2}}{i := i + 1}}

8.4. Elemenként feldolgozható függvény Legyenek E, F_{i} (i = 1,…, m) tetszőleges halmazok, m, n ∈ ℕ tetszőlegesek.

\begin{matrix}X = & X_{1} ×… × X_{n}  (X_{i} ⊆ 2^{E} (i = 1,…, n)) \\ Y = & Y_{1} ×… × Y_{m}  (Y_{i} ⊆ 2^{F_{i}} (i = 1,…, m)) \end{matrix}

Definíció: Azt mondjuk, hogy \overline{x}, \overline{\overline{x}} ∈ X teljesen diszjunkt felbontása x ∈ X-nek, ha i) ∀i ∈ [1, n] : x_{i} = \overline{x}_{i} ∪ \overline{\overline{x}}_{i} és ii) ∀i, j ∈ [1, n] : \overline{x}_{i} ∩ \overline{\overline{x}}_{j} = ∅.

Definíció: Legyen f : X → Y. Ha bármely x ∈ X bármely \overline{x}, \overline{\overline{x}} teljesen diszjunkt felbontására

i) f(\overline{x}) ∪ f(\overline{\overline{x}}) = f(x) és ii) f(\overline{x}) ∩ f(\overline{\overline{x}}) = (∅, ..., ∅), akkor f-et elemenként feldolgozhatónak nevezzük.

Megjegyzés:

1. Az ∪ és ∩ műveletek komponensenként értendők.

2. f(x) = (f_{1}(x),…, f_{m}(x)) jelölést alkalmazva, ahol

f_{j}(x) : X → Y_{j}, j = 1,…, m ,

könnyen látható, hogy az f_{1}(x),…, f_{m}(x) függvénnek mind elemenként feldolgozhatóak.

8.4.1. Egyváltozós egyértékű elemenkénti feldolgozás

Legyen f : X → Y (n = 1, m = 1) elemenként feldolgozható függvény. Határozzuk meg az f függvény értékét valamely x ∈ X pontban.

A =X x×Y y

B ={X \atop x′}

Q : (x = x′) R : (y = f(x′))

Keressük a megoldást adó programot ciklus formában, ahol P : (y ∪ f(x) = f(x′) ∧ y ∩ f(x) = ∅)

1. A ciklus levezetési szabályának második feltétele: P ∧ ¬π ⇒ R teljesül, ha ¬π : x = ∅. Ha ugyanis x = ∅, akkor az elemenként feldolgozható tulajdonság miatt f(x) = ∅. Tehát π : x ≠ ∅ alkalmas választás.

2. A ciklus levezetési szabálya harmadik feltétele: P ∧ π ⇒ t > 0 teljesül, ha t = |x| (|x| jelenti x elemeinek számát) a π választása miatt.

3. Célszerű a ciklusmagot S_{0} : (S_{1}; S_{2}) szekvencia fomában keresni, ahol S_{2} azon egyszerű parciális értékadás, amelyre D_{F_{1}} = {(x, y, e)|e ∈ x} és F_{1}((x, y, e)) = {x ≃ {e}} minden (x, y, e) ∈ D_{F_{1}}, abból a meggondolásból, hogy a ciklus levezetési szabályának 5. feltétele is teljesüljön. Alkalmazva a szekvencia leggyengébb előfeltételére ismert tételt, P ∧ π ⇒ lf(S_{0}, P) ⇔ lf(S_{1}, lf(S_{2}, P)) teljesül, ha P ∧ π ⇒ lf(S_{1}, lf(S_{2}, P)) ⇔ lf(S_{1}, P^{x←x≃{e}} ∧ e ∈ x) mivel lf(S_{2}, P) ⇔ P^{x←x≃{e}} ∧ e ∈ x. P^{x←x≃{e}} ∧ e ∈ x : (y ∪ f(x ≃ {e}) = f(x′) ∧ y ∩ f(x ≃ {e}) = ∅ ∧ e ∈ x). Ugyanakkor P ∧ π ∧ e ∈ x ⇒ (y ∪ f(x ≃ {e}) ∪ f({e}) = f(x′) ∧ y ∩ (f(x ≃ {e}) ∪ f({e})) = ∅ ∧ e ∈ x), ugyanis e ∈ x, valamint a ≃ művetel tulajdonsága miatt x-nek x ≃ {e} és {e} diszjunkt felbontása, ezért f(x) = f(x ≃ {e})˜∪f({e}). Ugyanakkor a teljesen diszjunkt felbontás miatt f(x ≃ {e}) ∩ f({e}) = ∅ is teljesül, ezért e ∈ x esetén y ∩ (f(x ≃ {e}) ∪ f({e})) = ∅ ⇒ (y˜∪f({e})) ∩ f(x ≃ {e}) = ∅, tehát P ∧ π ∧ e ∈ x ⇒ (y ∪ f(x ≃ {e}) ∪ f({e}) = f(x′) ∧ (y˜∪f({e})) ∩ f(x ≃ {e}) = ∅ ∧ y ∩ f({e}) = ∅ ∧ e ∈ x) ⇔ lf(S_{1,2}, P^{x←x≃{e}} ∧ e ∈ x), ahol S_{1,2} azon egyszerű parciális értékadás, amelyre D_{F_{2}} = {(x, y, e)|y ∩ f({e}) = ∅ és F_{2}((x, y, e)) = {y˜∪f({e})} minden (x, y, e) ∈ D_{F_{2}}.

Látható viszont, hogy P ∧ π ⇏ P ∧ π ∧ e ∈ x, ezért egy olyan S_{1,1} programra van szükség, amelyre P ∧ π ⇒ lf(S_{1,1}, P ∧ π ∧ e ∈ x). Az ilyen tulajdonságú programokat x bizonyos elemeit kiválasztó programoknak nevezzük. S_{1,1} prgramra alkalmas választás lehet az S_{1,1} : e :∈ (x) értékkiválasztás (ez x minden elemét kiválasztja!), ugyanis könnyen belátható, hogy lf(e :∈ (x), P ∧ π ∧ e ∈ x) ⇔ P ∧ π az e :∈ x értékkiválasztásnak adott utófeltétel mellett, a leggyengébb előfeltételére vonatkozó tétele alapján. A S_{1,2} : y := y˜∪f({e}) jelölést használva, tehát beláttuk, hogy az S_{1} : (S_{1,1}; S_{1,2}) alkalmas választás.

4. A ciklus levezetési szabálya ötödik feltétele: P ∧ π ∧ t ≤ t_{0} + 1 ⇒ lf(S_{0}, t ≤ t_{0}) minden t_{0} ∈ ℤ-re. Alkalmazva a szekvencia levezetési szabályát, adódik: lf(S_{0}, t ≤ t_{0}) ⇔ lf(S_{1,1}, lf(S_{1,2}, lf(S_{2}, t ≤ t_{0}))) ⇔ lf(S_{1,1}, lf(S_{1,2}, e ∈ x ∧ Cardinal(x ≃ {e}) ≤ t_{0})) ⇔ lf(S_{1,1}, lf(S_{1,2}, e ∈ x ∧ t − 1 ≤ t_{0})) ⇔ lf(S_{1,1}, y ∩ f({e}) = ∅ ∧ e ∈ x ∧ t − 1 ≤ t_{0}). Felhasználva az f függvény elemenként feldolgozható tulajdonságát, belátható, hogy P ∧ π ∧ t ≤ t_{0} + 1 ⇒ lf(S_{1,1}, y ∩ f({e}) = ∅ ∧ e ∈ x ∧ t − 1 ≤ t_{0}) tetszőleges t_{0} ∈ ℤ-re, ugyanis lf(S_{1,1}, y ∩ f({e}) = ∅ ∧ e ∈ x ∧ t − 1 ≤ t_{0}) ⇔ x ≠ ∅ ∧ ∀e ∈ x : (y ∩ f({e}) = ∅ ∧ e ∈ x ∧ t − 1 ≤ t_{0}), és egyszerűen belátható, hogy P ∧ π ∧ t ≤ t_{0} + 1 ⇒ x ≠ ∅ ∧ ∀e ∈ x : (y ∩ f({e}) = ∅ ∧ e ∈ x ∧ t − 1 ≤ t_{0}) ezért a ciklus levezetési szabályának ötödik feltétele is teljesül.

5. Könnyen ellenőrizhető, hogy Q ⇒ P nem teljesül. Ugyanakkor látható, hogy Q ⇒ P^{y←∅} fennáll, mivel P^{y←∅} : (∅ ∪ f(x) = f(x′) ∧ ∅ ∩ f(x) = ∅) ⇔ (f(x) = f(x′)), ugyanis ∅ ∩ f(x) = ∅ ⇔ true nyilván teljesül. Tehát Q ⇒ lf(y := ∅, P). Ugyanakkor a ciklus levezetési szabálya első feltétele: P ⇒ P nyilván teljesül, ezért P ⇒ lf(DO, R) is igaz, ahol DO = (x ≠ ∅, S_{0}). Alkalmazva a szekvenciával kapcsolatos levezetési szabályt, kapjuk: Q ⇒ lf((y := ∅; DO), R)

Egy lehetséges megoldás tehát a következő program:

y := ∅ ; x ≠ ∅ ; \overline{e :∈ (x) ; y := y˜∪f(\{e\}) ; x := x ≃ \{e\}}

Megjegyzés: ˜∪ a diszjunkt unió, ≃ valamely halmaz és egy eleme, mint halmaz közötti különbség műveletét jejöli. 8.4.2. Kétváltozós egyértékű elemenkénti feldolgozás

Legyen f : X → Y (n = 2, m = 1) elemenként feldolgozható függvény.

A ={X_{1} \atop x_{1}}×{X_{2} \atop x_{2}}×Y y

B ={X_{1} \atop x′_{1}}×{X_{2} \atop x′_{2}}

Q : (x_{1} = x′_{1} ∧ x_{2} = x′_{2})

R : (y = f(x′_{1}, x′_{2}))

Keressük a megoldást adó programot ciklus formában, ahol

P : (y ∪ f(x_{1}, x_{2}) = f(x′_{1}, x′_{2}) ∧ y ∩ f(x_{1}, x_{2}) = ∅)

1. A ciklus levezetési szabályának második feltétele: P ∧ ¬π ⇒ R teljesül, ha ¬π : x = (∅, ∅). Ha ugyanis x = (∅, ∅), akkor az elemenként feldolgozható tulajdonság miatt f(x) = ∅. Tehát π : x ≠ (∅, ∅), vagy π : x ≠ (∅, ∅) ⇔ x_{1} ≠ ∅ ∨ x_{2} ≠ ∅ miatt π : x_{1} ≠ ∅ ∨ x_{2} ≠ ∅ egyaránt alkalmas választás.

2. A ciklus levezetési szabálya harmadik feltétele: P ∧ π ⇒ t > 0 teljesül, ha t = |x_{1} ∪ x_{2}| (|x| jelenti valamely x halmaz elemeinek számát) a π választása miatt.

3. Vegyük észre, hogy P ∧ π ∧ e ∈ x_{1} ∪ x_{2} ∧ (e ∈ x_{1} ∧ e ∉ x_{2}) ⇒ (y ∪ f(x_{1} ≃ {e}, x_{2}) ∪ f({e}, ∅) = f(x′) ∧ y ∩ (f(x_{1} ≃ {e}, x_{2}) ∪ f({e}, ∅)) = ∅), ugyanis e ∈ x_{1} ∧ e ∉ x_{2}, valamint a ≃ művetel tulajdonsága miatt (x_{1}, x_{2})-nek (x_{1} ≃ {e}, x_{2}) és ({e}, ∅) teljesen diszjunkt felbontása, ezért f((x_{1}, x_{2})) = f((x_{1} ≃ {e}, x_{2}))˜∪f(({e}, ∅)). Ugyanakkor a teljesen diszjunkt felbontás miatt f((x_{1} ≃ {e}, x_{2})) ∩ f(({e}, ∅)) = ∅ is teljesül, ezért e ∈ x_{1} ∧ e ∉ x_{2} esetén y ∩ (f((x_{1} ≃ {e}, x_{2})) ∪ f(({e}, ∅))) = ∅ ⇒ (y˜∪f(({e}, ∅))) ∩ f((x_{1} ≃ {e}, x_{2})) = ∅, tehát P ∧ π ∧ e ∈ x_{1} ∪ x_{2} ∧ (e ∈ x_{1} ∧ e ∉ x_{2}) ⇒ (y ∪ f((x_{1} ≃ {e}, x_{2})) ∪ f(({e}, ∅)) = f(x′) ∧ ∧(y˜∪f(({e}, ∅))) ∩ f((x_{1} ≃ {e}, x_{2})) = ∅ ∧ ∧e ∈ x_{1} ∪ x_{2} ∧ (e ∈ x_{1} ∧ e ∉ x_{2}) ∧ y ∩ f(({e}, ∅)) = ∅) ⇔

P^{x_{1}←x_{1}≃{e}}^{y←y_{∪}f(({e},∅))} ∧

∧e ∈ x_{1} ∪ x_{2} ∧ (e ∈ x_{1} ∧ e ∉ x_{2}) ∧ y ∪ f(({e}, ∅)) = ∅. Hasonlóan belátható, hogy P ∧ π ∧ e ∈ x_{1} ∪ x_{2} ∧ (e ∉ x_{1} ∧ e ∈ x_{2}) ⇒ (y ∪ f((x_{1}, x_{2} ≃ {e})) ∪ f((∅, {e})) = f(x′) ∧ ∧(y˜∪f((∅, {e}))) ∩ f((x_{1}, x_{2} ≃ {e})) = ∅ ∧ ∧e ∈ x_{1} ∪ x_{2} ∧ (e ∉ x_{1} ∧ e ∈ x_{2}) ∧ y ∩ f((∅, {e})) = ∅) ⇔

P^{x_{2}←x_{2}≃{e}}^{y←y_{∪}f((∅,{e}))} ∧

∧e ∈ x_{1} ∪ x_{2} ∧ (e ∉ x_{1} ∧ e ∈ x_{2}) ∧ y ∩ f((∅, {e})) = ∅, és P ∧ π ∧ e ∈ x_{1} ∪ x_{2} ∧ (e ∈ x_{1} ∧ e ∈ x_{2}) ⇒ (y ∪ f((x_{1} ≃ {e}, x_{2} ≃ {e})) ∪ f(({e}, {e})) = f(x′) ∧ ∧(y˜∪f(({e}, {e}))) ∩ f((x_{1} ≃ {e}, x_{2} ≃ {e})) = ∅ ∧ ∧e ∈ x_{1} ∪ x_{2} ∧ (e ∈ x_{1} ∧ e ∈ x_{2}) ∧ y ∩ f(({e}, {e})) = ∅) ⇔

P^{x_{1},x_{2}←x_{1}≃{e},x_{2}≃{e}}^{y←y_{∪}f(({e},{e}))} ∧

∧e ∈ x_{1} ∪ x_{2} ∧ (e ∈ x_{1} ∧ e ∈ x_{2}) ∧ y ∩ f(({e}, {e})) = ∅. Alkalmazva az elágazás levezetési szabályát, valamint a e ∈ x_{1} ∪ x_{2} ⇔ e ∈ x_{1} ∪ x_{2} ∧ ((e ∈ x_{1} ∧ e ∈ x_{2}) ∨ (e ∉ x_{1} ∧ e ∈ x_{2}) ∨ (e ∈ x_{1} ∧ e ∉ x_{2})) összefüggést, kapjuk: P ∧ π ∧ e ∈ x_{1} ∪ x_{2} ⇒ lf(IF, P), ahol IF : (e ∈ x_{1} ∧ e ∉ x_{2} : S_{2,1}, e ∉ x_{1} ∧ e ∈ x_{2} : S_{2,2}, e ∈ x_{1} ∧ e ∈ x_{2} : S_{2,3}), ahol S_{2,1} szimultán parciális értékadás, amelyre D_{F_{1}} = {(x_{1}, x_{2}, y, e)| e ∈ x_{1} ∧ e ∉ x_{2}} és F_{1}((x_{1}, x_{2}, y, e)) = {x_{1} ≃ {e}} minden (x_{1}, x_{2}, y, e) ∈ D_{F_{1}}, valamint D_{F_{3}} = {(x_{1}, x_{2}, y, e)|y ∩ f(({e}, ∅)) = ∅} és F_{3}((x_{1}, x_{2}, y, e)) = {y˜∪f(({e}, ∅))} minden (x_{1}, x_{2}, y, e) ∈ D_{F_{3}}, S_{2,2} szimultán parciális értékadás, amelyre D_{F_{2}} = {(x_{1}, x_{2}, y, e)| e ∉ x_{1} ∧ e ∈ x_{2}} és F_{2}((x_{1}, x_{2}, y, e)) = {x_{2} ≃ {e}} minden (x_{1}, x_{2}, y, e) ∈ D_{F_{2}}, valamint D_{F_{3}} = {(x_{1}, x_{2}, y, e)|y ∩ f((∅, {e})) = ∅} és F_{3}((x_{1}, x_{2}, y, e)) = {y˜∪f((∅, {e}))} minden (x_{1}, x_{2}, y, e) ∈ D_{F_{3}}, S_{2,3} szimultán parciális értékadás, amelyre D_{F_{1}} = {(x_{1}, x_{2}, y, e)| e ∈ x_{1} ∧ e ∈ x_{2}} és F_{1}((x_{1}, x_{2}, y, e)) = {x_{1} ≃ {e}} minden (x_{1}, x_{2}, y, e) ∈ D_{F_{1}}, valamint D_{F_{2}} = {(x_{1}, x_{2}, y, e)| e ∈ x_{1} ∧ e ∈ x_{2}} és F_{2}((x_{1}, x_{2}, y, e)) = {x_{2} ≃ {e}} minden (x_{1}, x_{2}, y, e) ∈ D_{F_{2}}, valamint D_{F_{3}} = {(x_{1}, x_{2}, y, e)|y ∩ f(({e}, {e})) = ∅} és F_{3}((x_{1}, x_{2}, y, e)) = {y˜∪f(({e}, {e}))} minden (x_{1}, x_{2}, y, e) ∈ D_{F_{3}}. Látható viszont, hogy P ∧ π¬ ⇒ P ∧ π ∧ e ∈ x_{1} ∪ x_{2}, ezért egy olyan S_{1} programra van szükség, amelyre P ∧ π ⇒ lf(S_{1}, P ∧ π ∧ e ∈ x_{1} ∪ x_{2}). Az ilyen tulajdonságú programokat x_{1} ∪ x_{2} bizonyos elemeit kiválasztó programoknak nevezzük. S_{1} prgramra alkalmas választás lehet az S_{1} : e :∈ (x_{1} ∪ x_{2}) értékkiválasztás (ez x_{1} ∪ x_{2} minden elemét kiválasztja!), ugyanis könnyen belátható, hogy lf(e :∈ (x_{1} ∪ x_{2}), P ∧ π ∧ e ∈ x_{1} ∪ x_{2}) ⇔ P ∧ π az e :∈ (x_{1} ∪ x_{2}) értékkiválasztásnak adott utófeltétel mellett, a leggyengébb előfeltételére vonatkozó tétele alapján. Alkalmazva a szekvenciára vonatkozó levezetési szabályt, kapjuk: P ∧ π ⇒ lf((e :∈ (x_{1} ∪ x_{2}); IF), P). Tehát S_{0} : (e :∈ (x_{1} ∪ x_{2}); IF) választás esetén a ciklus levezetési szabálya harmadik feltétele is teljesül, és ugyanakkor látható, hogy a t termináló függvény értékei is csökken S_{0} végrehajtásakor.

4. A ciklus levezetési szabálya ötödik feltétele: P ∧ π ∧ t ≤ t_{0} + 1 ⇒ lf(S_{0}, t ≤ t_{0}) minden t_{0} ∈ ℤ-re. Alkalmazva a szekvencia és az elágazás levezetési szabályainak megfordítását, ha belátjuk, hogy P ∧ π ∧ t ≤ t_{0} + 1 ⇒ lf(e :∈ (x_{1} ∪ x_{2}), P ∧ π ∧ t ≤ t_{0} + 1 ∧ e ∈ x_{1} ∪ x_{2}, és P ∧ π ∧ t ≤ t_{0} + 1 ∧ e ∈ x_{1} ∪ x_{2} ∧ (e ∈ x_{1} ∧ e ∉ x_{2}) ⇒ lf(S_{2,1}, t ≤ t_{0}), valamint P ∧ π ∧ t ≤ t_{0} + 1 ∧ e ∈ x_{1} ∪ x_{2} ∧ (e ∉ x_{1} ∧ e ∈ x_{2}) ⇒ lf(S_{2,2}, t ≤ t_{0}), valamint P ∧ π ∧ t ≤ t_{0} + 1 ∧ e ∈ x_{1} ∪ x_{2} ∧ (e ∈ x_{1} ∧ e ∈ x_{2}) ⇒ lf(S_{2,3}, t ≤ t_{0}), tetszőleges t_{0} ∈ ℤ-re, akkor a ciklus levezetési szabályának ötödik feltétele is teljesül. Az első összefüggés következik abból, hogy az értékkiválasztás leggyengébb előfeltételére: P ∧ π ∧ t ≤ t_{0} + 1 ⇔ lf(e :∈ (x_{1} ∪ x_{2}), P ∧ π ∧ t ≤ t_{0} + 1 ∧ e ∈ x_{1} ∪ x_{2}. Ugyanakkor lf(S_{2,1}, t ≤ t_{0}) ⇔ (t ≤ t_{0})^{x_{2}←x_{2}≃{e}} ∧ (e ∈ x_{1} ∧ e ∉ x_{2}) ∧ y ∪ f(({e}, ∅)) = ∅ ⇔ Cardinal(x_{1} ∪ (x_{2} ≃ {e})) ≤ t_{0} ∧ (e ∈ x_{1} ∧ e ∉ x_{2}) ∧ y ∪ f(({e}, ∅)) = ∅ ⇔ Cardinal(x_{1} ∪ x_{2}) − 1 ≤ t_{0} ∧ (e ∈ x_{1} ∧ e ∉ x_{2}) ∧ y ∪ f(({e}, ∅)) = ∅ ⇔ t ≤ t_{0} + 1 ∧ (e ∈ x_{1} ∧ e ∉ x_{2}) ∧ y ∪ f(({e}, ∅)) = ∅. Könnyen látható, hogy P ∧ π ∧ t ≤ t_{0} + 1 ∧ e ∈ x_{1} ∪ x_{2} ∧ (e ∈ x_{1} ∧ e ∉ x_{2}) ⇒ t ≤ t_{0} + 1 ∧ (e ∈ x_{1} ∧ e ∉ x_{2}) ∧ y ∪ f(({e}, ∅)) = ∅, tehát P ∧ π ∧ t ≤ t_{0} + 1 ∧ e ∈ x_{1} ∪ x_{2} ∧ (e ∈ x_{1} ∧ e ∉ x_{2}) ⇒ lf(S_{2,1}, t ≤ t_{0}). Hasonlóan látható be a másik két leggyengébb előfeltételre vonatkozó összefüggés is.

5. Könnyen ellenőrizhető, hogy Q ⇒ P nem teljesül. Ugyanakkor látható, hogy Q ⇒ P^{y←∅} fennáll, mivel P^{y←∅} : (∅ ∪ f(x) = f(x′) ∧ ∅ ∩ f(x) = ∅) ⇔ (f(x) = f(x′)), ugyanis ∅ ∩ f(x) = ∅ ⇔ true nyilván teljesül. Tehát Q ⇒ lf(y := ∅, P). Ugyanakkor a ciklus levezetési szabálya első feltétele:

P ⇒ P nyilván teljesül, ezért P ⇒ lf(DO, R) is igaz, ahol DO = (x_{1} ≠ ∅ ∨ x_{1} ≠ ∅, S_{0}). Alkalmazva a szekvenciával kapcsolatos levezetési szabályt, kapjuk: Q ⇒ lf((y := ∅; DO), R)

Egy lehetséges megoldás tehát a következő program:

y := ∅ ; x_{1} ≠ ∅ ∨ x_{1} ≠ ∅ ; \overline{e :∈ (x_{1} ∪ x_{2}) ; \ e ∈ x_{1} ∧ e ∉ x_{2} \ e ∉ x_{1} ∧ e ∈ x_{2} \ e ∈ x_{1} ∧ e ∈ x_{2} ; y, x_{1} := ; y˜∪f(\{e\}, ∅), ; x_{1} ≃ \{e\}  y, x_{2} := ; y˜∪f(∅, \{e\}), ; x_{2} ≃ \{e\}  y, x_{1}, x_{2} := ; y˜∪f(\{e\}, \{e\}), ; x_{1} ≃ \{e\}, ; x_{2} ≃ \{e\}}

8.4.3. Egyváltozós kétértékű elemenkénti feldolgozás

Legyen f : X → Y (n = 1, m = 2), elemenként feldolgozható függvény, f_{1} : X → Y_{1}, f_{2} : X → Y_{2}, f = (f_{1}, f_{2}).

A =X x×{Y_{1} \atop y_{1}}×{Y_{2} \atop y_{2}}

B ={X \atop x′}

Q : (x = x′)

R : (y_{1} = f_{1}(x′) ∧ y_{2} = f_{2}(x′))

Keressük a megoldást adó programot ciklus formában, ahol

P : (y_{1} ∪ f_{1}(x) = f_{1}(x′) ∧ y_{1} ∩ f_{1}(x) = ∅ ∧ y_{2} ∪ f_{2}(x) = f_{2}(x′) ∧ y_{2} ∩ f_{2}(x) = ∅)

Vegyük figyelembe, hogy az f(x) = (f_{1}(x), f_{2}(x)) függvény f_{1}(x) és f_{2}(x) komponensei egyváltozós egyértékű elemenkénk feldolgozható függvények. Ennek alapján a levezetés és a programkonstrukció az egyváltozós egyértékű elemenként feldolgozható függvény esetén alkalmazott módszerrel és meggondolásokkal analóg módon elvégezhető. Mindezek alapján a következő program a feladat egy lehetséges megoldása:

y_{1}, y_{2} := ∅, ∅ ; x ≠ ∅ ; \overline{e :∈ (x) ; y_{1}, y_{2} := y_{1}˜∪f_{1}(\{e\}), y_{2}˜∪f_{2}(\{e\}) ; x := x ≃ \{e\}}

8.4.4. n változós, m értékű elemenkénti feldolgozás

Legyen f : X → Y (n, m ∈ ℕ), elemenként feldolgozható függvény, f_{1} : X → Y_{1},…, f_{n} : X → Y_{n}, f = (f_{1},…, f_{n}).

A ={X_{1} \atop x_{1}}× ⋯×{X_{n} \atop x_{n}} ×{Y_{1} \atop y_{1}}× ⋯×{Y_{m} \atop y_{m}}

B ={X_{1} \atop x′_{1}}× ⋯×{X_{n} \atop x′_{n}}

Q : (x_{1} = x′_{1} ∧ ⋯ ∧ x_{n} = x′_{n})

R : (y_{1} = f_{1}(x′_{1},…, x′_{n}) ∧ ⋯ ∧ y_{m} = f_{m}(x′_{1},…, x′_{n}))

Keressük a megoldást adó programot ciklus formában, ahol

P : (∀j ∈ [1..m] : (y_{j} ∪ f_{j}(x_{1},…, x_{n}) = f_{j}(x′_{1},…, x′_{n}) ∧ y_{j} ∩ f_{j}(x_{1},…, x_{n}) = ∅)

A programkonstrukció és a levezetés a kétváltozós egyértékű elemenként feldolozható függvény esetében alkalmazott módszer többváltozós esetre történő általánosításával, valamint annak figyelembe vételével kapható meg, hogy az f(x) = (f_{1}(x),…, f_{m}(x)) jelölést alkalmazva, ahol

f_{j}(x) : X → Y_{j}, j = 1,…, m ,

az f_{1}(x),…, f_{m}(x) függvénnek mind n változós egyértékű elemenként feldolgozható függvények. Mindezek alapján a következő program a feladat egy lehetséges megoldása:

y_{1},…, y_{m} := ∅,…, ∅ ; ∨_{i=1}^{n}x_{i} ≠ ∅ ; \overline{e :∈ ( ⋃_{i=1}^{n} x_{i}) ; \… \  e ∈ x_{i_{1}} ∧… e ∈ x_{i_{k}} ∧ e ∉ x_{i_{k+1}} ∧ e ∉ x_{i_{n}}  \…; …  y_{1},…, y_{m}, x_{i_{1}},…, x_{i_{k}} := ; y_{1}˜∪f_{1}(sl(x, e)),…, y_{m}˜∪f_{m}(sl(x, e)), ; x_{i_{1}} ≃ \{e\},…, x_{i_{k}} ≃ \{e\}  …}

ahol i_{1},…, i_{k} ∈ {1,…, n} különbözőek, sl : X × E → X,

sl(x, e)_{i} = \{ \begin{matrix}\{e\}, & ha e ∈ x_{i} \\ ∅, & különben \end{matrix}

Az elágazás ”ágainak” száma 2^{n} − 1.