1. Lineáris keresés

1.0.1. Lineáris keresés 2.9 változat

Legyen m ∈ ℤ, β : ℤ → 𝕃, γ : ℤ → 𝕃. Keressük meg azt a legkisebb β tulajdonságú i egész számot, ha van ilyen, amelyre i ≥ m, és az [m..i] minden elemére γ hamis.

A =ℤ m×ℤ i

B ={Z \atop m′}

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

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

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

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

1. Könnyen ellenőrizhető, hogy Q ⇒ P nem teljesül. Ugyanakkor látható, hogy Q ⇒ P^{u,i←β(m)∧¬γ(m),m} fennáll, mivel P^{u,i←β(m)∧¬γ(m),m} : (Q ∧ m ≥ m ∧ ∀j ∈ [m, m) : ¬γ(j) ∧ ∀j ∈ [m, m) : ¬β(j) ∧ ∧(β(m) ∧ ¬γ(m) ↔ ∃j ∈ [m, m] : β(j) ∧ ∀j ∈ [m, m] : ¬γ(j))), és (m ≥ m ∧ ∀j ∈ [m, m) : ¬γ(j) ∧ ∀j ∈ [m, m) : ¬β(j) ∧ ∧(β(m) ∧ ¬γ(m) ↔ ∃j ∈ [m, m] : β(j) ∧ ∀j ∈ [m, m] : ¬γ(j))) ⇔ true. Tehát Q ⇒ lf(u, i := β(m) ∧ ¬γ(m), m, P). Ugyanakkor P ⇒ P nyilván teljesül.

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

3. A ciklus levezetési szabálya harmadik feltétele …

4. 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. P^{i←i+1} : (Q ∧ i + 1 ≥ m ∧ ∀j ∈ [m, i + 1) : ¬γ(j) ∧ ∀j ∈ [m, i + 1) : ¬β(j) ∧ ∧(u ↔ ∃j ∈ [m, i + 1] : β(j) ∧ ∀j ∈ [m, i + 1] : ¬γ(j))), ugyanakkor P ∧¬u∧¬γ(i) ⇒ (Q∧i+1 ≥ m∧∀j ∈ [m, i+1) : ¬γ(j)∧∀j ∈ [m, i+1) : ¬β(j)∧ ∧((β(i + 1) ∧ ¬γ(i + 1)) ↔ ∃j ∈ [m, i + 1] : β(j) ∧ ∀j ∈ [m, i + 1] : ¬γ(j))), ahonnan P ∧ ¬u ∧ ¬γ(i) ⇒ lf(S_{1}, P^{i←i+1}), ahol S_{1} : u := β(i + 1) ∧ ¬γ(i + 1).

5. A ciklus levezetésének ötödik feltétele ...

Tehát a keresett program:

u, i := β(m) ∧ ¬γ(m), m ; ¬u ∧ ¬γ(i) ; \overline{\frac{u := β(i + 1) ∧ ¬γ(i + 1)}{i := i + 1}}

A tétel közvetlen alkalmazható lináris keresésre szekvenciális input file esetén, ahol γ(i) : sa = abnorm, ha a ciklusmagban a szekvencia sorendjét felcseréljük. Könnyen belátható, hogy ez jelen esetben megengedett transzformáció.

A típustranszformációnak megfelelő transzformált program a következő:

sa, da, a : read ; \  sa = norm  / ; \begin{aligned}u := β(da) \\ & u :=↓ \end{aligned} ; ¬u ∧ sa = norm ; \overline{sa, da, a : read ; \  sa = norm  / ; \begin{aligned}u := β(da) \\ & u :=↓ \end{aligned}}