Visszalépéses keresés

Legyenek U_{1}, U_{2}, ..., U_{n} tetszőleges véges halmazok. Legyen

U = U_{1} × U_{2} × ... × U_{n}

Legyenek ρ_{0}, ρ_{1}, ρ_{2}, ..., ρ_{n} állítások U-n:

ρ_{i} : U → 𝕃, i = 0, 1, 2, ..., n, ρ_{0} = T RUE,

és amelyekre

ρ_{i+1} ⇒ ρ_{i}, i = 0, 1, 2, ..., n − 1

Legyen ρ = ρ_{n}.

Legyen u′, u′′ ∈ U, ahol

u′ = (u′_{1}, u′_{2}, ..., u′_{n}) és u′′ = (u′′_{1}, u′′_{2}, ..., u′′_{n})

Tegyük fel, hogy a ρ_{i} csak az első i változótól függ, azaz

∀i ∈ [1..n] : ∀u′ ∈ U : ∀u′′ ∈ U : (∀j ∈ [1..i] : u′_{j} = u′′_{j}) → (ρ_{i}(u′_{1}, u′_{2}, ..., u′_{i}, u′_{i+1}, ..., u′_{n}) ↔ ρ_{i}(u′′_{1}, u′′_{2}, ..., u′′_{i}, u′′_{i+1}, ..., u′′_{n}))

Keressünk olyan u ∈ U, amelyre ρ(u)!

A feladat megoldását nehezíti, hogy az U halmaz nem rendezett. Legyen |U_{i}| = σ_{i}, i = 1, 2, ..., n, ekkor léteznek a

ϕ_{i} : [0, σ_{i} − 1] → U_{i}, i = 1, 2, ..., n,

kölcsönösen egyértelmű leképezések. Legyen

ϕ_{j}(i) = u_{i}^{(j)}, i ∈ [0, σ_{j} − 1], j = 1, 2, ..., n

Tekintsük a Σ_{k} = [0, σ_{1} − 1] × [0, σ_{2} − 1] × ... × [0, σ_{k} − 1], k = 1, 2, ..., n, halmazokat. Legyen Σ = Σ_{n}.

Vezessük be a Σ halmazon \overline{ρ}_{i} állításokat a következő módon:

\overline{ρ}_{i}(i_{1}, i_{2}, ..., i_{n}) = ρ_{i}(u_{i_{1}}^{(1)}, u_{i_{2}}^{(2)}, ..., u_{i_{n}}^{(n)}), i = 0, 1, 2, ..., n

Legyen \overline{ρ} = \overline{ρ}_{n} Az eredeti feladat ekvivalens a következő feladattal:

Typeset by A_{M}S-TEX

Keressünk olyan i ∈ Σ , amelyre \overline{ρ}(i)!

Ha a Σ halmazt valamilyen formában rendezetté tesszük, akkor a feladat a lineáris keresés 2.8 tételére vezethető vissza. Könnyen ellenőrízhetők a következő összefüggések:

ρ(u) ↔ ¬∃m ∈ [1, n] : ¬ρ_{m}(u)

illetve

\overline{ρ}(u) ↔ ¬∃m ∈ [1, n] : ¬\overline{ρ}_{m}(i)

A ρ(u) ↔, illetve a \overline{ρ}(u) állítások ilyen átfogalmazását első közelítésban azért célszerű választani, hogy a kitranszformálásuk közvetlen visszavezethető legyen a lineáris keresés tételére. Mind látni fogjuk, a későbbiekben célszerű lesz inkább az állításoknak a

ρ(u) ↔ ∀m ∈ [1, n] : ρ_{m}(u)

illetve

\overline{ρ}(u) ↔ ∀m ∈ [1, n] : \overline{ρ}_{m}(u)

érvényes formulák alapján származtatott ekvivalens alakját alkalmazni, ezek kitranszformálásához azonban külön tétel alkalmazására lesz szükség.

Tegyük fel, hogy Σ valamilyen formában már rendezett és a keresésben már eljutottunk valamely i pontig és \overline{ρ}(i) nem teljesül. Akkor az \overline{ρ}(i) fenti előállításából következik, hogy egyérteműen létezik olyan j ∈ [1..n] index, amelyre \overline{ρ}_{j}(i) nem teljesül, de

∀k ∈ [1..j − 1] : \overline{ρ}_{k}(i)

Figyelembe véve a

ρ_{i+1} ⇒ ρ_{i}, i = 0, 1, 2, ..., n − 1

tulajdonságokat, következik, hogy a \overline{ρ}(i′) biztosan nem teljesül, ha i és i′ az első j komponensben nem tér el. Rendezzük általában a Σ_{k} halmazokat úgy, ha i′, i′′ ∈ Σ_{k},

i′ = (i′_{1}, i′_{2}, ..., i′_{k}) és i′′ = (i′′_{1}, i′′_{2}, ..., i′′_{k})

akkor i′ ≤ i′′ akkor és csak akkor, ha ∀j ∈ [1, k] : (∀l ∈ [1, j − 1] : i′_{l} = i′′_{l}) → i′_{j} ≤ i′′_{j}

Könnyen látható, hogy ezen rendezés mellett azok az elemek, amelyekről biztosan tudjuk, hogy ott a \overline{ρ} értéke hamis, egy zárt intervallumot alkotnak i-től kezdve, ezért átléphetők a keresésben és meg tudjuk adni, azt az elemet is, ahol a keresést folytatni kell, feltéve, hogy ilyen elem még létezik.

Természetesen maradhatnánk az eredeti feladatnál is, mivel az U halmaz is rendezhető, például a Σ halmazban így bevezetett rendezés alapján. Mégis indokolt az állapottér transzformáció, mivel a Σ halmaz rendezettsége közvetlenül az N_{0} halmazon értelmezett rendezésre épül, amelyre viszont általában lehet hivatkozni a programokban.

Feltételezzük, hogy a ρ_{i}, i = 0, 1, 2, ..., n, feltételek megengedettek.

Tekintsük az I halmazt, amelyet úgy kapunk, hogy a Σ halmazt a −1 (extra) elemmel kiegészítjük, amely minden Σ-beli elemnél kisebb.

I = {−1} ∪ Σ és ∀i ∈ Σ : −1 ≤ i

Legyen i ∈ I. Jelölje i^{+} és i^{−}, az i után közvetlen következő, ill. az i-t közvetlen megelőző elemet a Σ_{k}-ban a bevezetett rendezés szerint feltéve, hogy ilyen elem létezik.

Alkalmazzuk a lineáris keresés 2.8 tételt a következő visszavezetéssel:

m ∼ −1, n ∼ (σ_{1} − 1, σ_{2} − 1, ..., σ_{n} − 1), γ ∼ \overline{ρ},

ahol \overline{ρ} kitranszformálandó feltétel a fenti formula alapján, szintén a lineáris keresés 2.8 tétel alkalmazásával.

Mindezeknek megfelelően a keresett program a következő:

i, u := −1, ↓ ; ¬u ∧ i < (σ_{1} − 1, σ_{2} − 1, ..., σ_{n} − 1) ; \overline{m, l := 0, ↓ ; m < n ∧ ¬l ; \overline{\frac{l := ¬\overline{ρ}_{m+1}(i^{+})}{m := m + 1}} ; u := ¬l ; i := i^{+}}

Ha kihasználjuk a beágyazott lineáris keresés 2.8 tétel által szolgáltatott plusz információt, és a \overline{ρ}_{i}, i = 0, 1, 2, ..., n, rendszernek a bevezető részben deklarált tulajdonságait, akkor a keresést az előzőekben mondottak alapján lényegesen meggyorsíthatjuk. Ha egy adott i^{+} keresési pontnál \overline{ρ}(i^{+}) nem teljesül, akkor pontosan meg tudjuk mondani azt az intervallumot i^{+}-tól kezdődően, amelyben \overline{ρ} biztosan nem teljesül..

A lineáris keresés 2.8 tétel utófeltétele a következő:

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

Könnyen belátható, hogy igaz a tétel akkor is, ha a következő R′ utófeltételt tekintjük:

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

Tehát, ha a beágyazott lineáris keresés 2.8 tételnek megfelelő program eredményeként l hamis, akkor m = n, ha viszont l igaz, akkor ∀j ∈ [1, m) : \overline{ρ}_{j}(i^{+}) teljesül, és \overline{ρ}_{m}(i^{+}) nem teljesül.

Vezessük be i ∈ Σ, i = (i_{1}, i_{2}, ..., i_{n}),valamint k ∈ [1, n] esetén

[i_{1..k}] = (i_{1}, i_{2}, ..., i_{k})

jelölést.

Ha tehát l igaz, akkor

\overline{ρ}_{i+1} ⇒ \overline{ρ}_{i}, i = 0, 1, 2, ..., n − 1,

miatt a \overline{ρ} biztosan hamis az

[i^{+}, [i_{1..m}^{+}]^{+}, 0, ..., 0)

intervallumban, ha [i_{1..m}^{+}]^{+} létezik, ugyanis itt az az \overline{ρ}_{m} biztosan hamis, mivel az index vektor első m komponense változatlan és \overline{ρ}_{m}(i), m = 1, 2, ..., n, a feltevés szerint i-nek csak az első m komponensétől függ.

Hasonló meggondolaásból \overline{ρ} biztosan hamis az

[i^{+}, (σ_{1} − 1, ..., σ_{n} − 1)]

intervallumban, ha már [i_{1..m}^{+}]^{+} nem létezik. Tehát a következő ellenőrizendő argumentum:

([i_{1..m}^{+}]^{+}, 0, ..., 0) feltéve, hogy ez az argumentum létezik. Ennek megfelően a keresés

hatékonyabb formája:

i, u := −1, ↓ ; ¬u ∧ i < (σ_{1} − 1, σ_{2} − 1, ..., σ_{n} − 1) ; \overline{m, l := 0, ↓ ; m < n ∧ ¬l ; \overline{\frac{l := ¬\overline{ρ}_{m+1}(i^{+})}{m := m + 1}} ; u := ¬l ; \ [i_{1..m}^{+}] = (σ_{1} − 1, σ_{2} − 1, ..., σ_{m} − 1) / ; {i := \atop (σ_{1} − 1, ..., σ_{n} − 1)} ; i := ; ([i_{1..m}^{+}]^{+}, 0, ..., 0)^{−}}

mivel az elmondottak szerint a módosított ciklusmag is alkalmas választás ebben az eseben a lineáris keresés 2.8 tételének levezetéséhez.

Könnyen belátható, hogy a lineáris keresés 2.8 tétel igaz a következő formában is feltéve, hogy a γ megengedett feltétel:

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

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

∧ (¬u → i = n))

P : (Q ∧ i ∈ [m..n] ∪ {m − 1} ∧ u = (∃j ∈ [m..i] : γ(j)) ∧ ∀j ∈ [m..i) : ¬γ(j))

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

Ezen tétel szerint az i-re rákövetkező előre is kiszámítható, és ezért előnyösebb a keresési probléma megoldását ezen tétere visszavezetni. Maga a levezetés alapvetően a

P^{i←i+1}^{u←γ(i+1)} ⇔ P^{u←γ(i)}^{i←i+1}

érvényességén múlik, ami a jelen esetben teljesül. Ezt felhasználva a feladat megoldását a következő program adja:

i := (0, 0, ..., 0) ; m, l := 0, ↓ ; m < n ∧ ¬l ; \overline{\frac{l := ¬\overline{ρ}_{m+1}(i)}{m := m + 1}} ; u := ¬l ; ¬u ∧ i ≠ (σ_{1} − 1, σ_{2} − 1, ..., σ_{n} − 1) ; \overline{i := i^{+} ; m, l := 0, ↓ ; m < n ∧ ¬l ; \overline{\frac{l := ¬\overline{ρ}_{m+1}(i)}{m := m + 1}} ; u := ¬l}

Ha figyelembe vesszük az u := ¬lértékadást, az l változó használatát megspórolhatjuk, és az u := ¬l értékadást elhagyhatjuk, ha helyette alkalmasan magát az u változót használjuk. Ennek megfelelően a \overline{ρ} értéket kitranszformáló program és az u := ¬l helyett a következő programot használhatjuk:

m, u := 0, ↑ ; m < n ∧ u ; \overline{\frac{u := \overline{ρ}_{m+1}(i)}{m := m + 1}}

Ezt a programot KERESŐ programnak nevezhetjük. Ugyanezt a programot

m ∼ 1, n ∼ m, i ∼ m, γ(m) ∼ \overline{ρ}_{m}()

visszavezetéssel is megkaphatjuk az alábbi tételből:

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

∧ (u → i = n))

P : (Q ∧ i ∈ [m..n] ∪ {m − 1} ∧ ∀j ∈ [m..i) : γ(j) ∧ u = (∀j ∈ [m..i] : γ(j)))

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

Az utófeltétel alapján valóban u ↔ \overline{ρ}(i). Felhasználva ezt, és a következő ellenőrizendő argumentumra tett előző megállapítást,

a feladat megoldását jelentő program:

i := (0, 0, ..., 0) ; m, u := 0, ↑ ; m < n ∧ u ; \overline{\frac{u := \overline{ρ}_{m+1}(i)}{m := m + 1}} ; ¬u ∧ i ≠ (σ_{1} − 1, σ_{2} − 1, ..., σ_{n} − 1) ; \overline{\ [i_{1..m}] = (σ_{1} − 1, σ_{2} − 1, ..., σ_{m} − 1) / ; {i := \atop (σ_{1} − 1, ..., σ_{n} − 1)} ; i := ; ([i_{1..m}]^{+}, 0, ..., 0) ; m, u := 0, ↑ ; m < n ∧ u ; \overline{\frac{u := \overline{ρ}_{m+1}(i)}{m := m + 1}}}

Az alábbi

\frac{\ [i_{1..m}] = (σ_{1} − 1, σ_{2} − 1, ..., σ_{m} − 1) /}{{i := \atop (σ_{1} − 1, ..., σ_{n} − 1)} ; i := ; ([i_{1..m}]^{+}, 0, ..., 0)}

programot ELŐRELÉPŐ programnak nevezhetjük. Az i^{+} művelet nem megengedett, ezért ezt a programot tovább kell finomítani a következők szerint.

Az ELŐRELÉPŐ programban a Σ_{m}-ben bevezetett rendezés alapján az [i_{1..m}]^{+} meghatározásához a következő specifikációval megadott feladatot kell megoldani:

A : Σ ,  B : Σ ,  m ∈ [1, n] a feladat paramétere
i  i′

Q : ([i_{1..m}] = [i′_{1..m}])

R : (([i′_{1..m}] = (σ_{1} − 1, σ_{2} − 1, ..., σ_{m} − 1) → i = (σ_{1} − 1, σ_{2} − 1, ..., σ_{n} − 1))∧
∧ ((∃j ∈ [1, m] : i′_{j} ≠ σ_{j} − 1) →
→ ∀j ∈ [1, m] : ((∀k ∈ [j + 1, m] : i′_{k} = σ_{k} − 1) ∧ i′_{j} ≠ σ_{j} − 1) →
→ (i_{j} = i′_{j} + 1 ∧ ∀k ∈ [j + 1, m] : i_{k} = 0 ∧ ∀k ∈ [1, j − 1] : i_{k} = i′_{k})))

Könnyen látható, hogy

Q ∧ [i_{1..m}] = (σ_{1} − 1, σ_{2} − 1, ..., σ_{m} − 1) ⇒ R^{i←(σ_{1}−1,...,σ_{n}−1)}

Legyen

Q′ : (Q ∧ ∃j ∈ [1, m] : i′_{j} ≠ σ_{j} − 1)

és

P : (Q′ ∧ h ∈ [0..m + 1]∧
∧ ∀k ∈ [h + 1, m] : i′_{k} = σ_{k} − 1 ∧ ∀k ∈ [h + 1, m] : i_{k} = 0 ∧
∧ (l ↔ ∃k ∈ [h, m] : i′_{k} ≠ σ_{k} − 1) ∧
∧ (l ∧ h ≠ m + 1 → i_{h} = i′_{h} + 1) ∧
∧ (¬l ∧ h ≠ m + 1 → i_{h} = 0) ∧
∧ ∀k ∈ [1, h) : i′_{k} = i_{k})

1. Q′ ⇒ P^{l,k←m+1,↓} teljesül.

2. P ∧ ¬π ⇒ R teljesül, ha π : l.

3. P ∧ π ⇒ t > 0 teljesül, ha t : k.

4. P ∧ π ∧ i′_{h−1} = σ_{h−1} − 1 ⇒ P^{h←h−1}^{i_{h−1}←0} valamint P ∧ π ∧ i′_{h−1} ≠ σ_{h−1} − 1 ⇒ P^{h←h−1}^{l,i_{h−1}←↑,i_{h−1}+1} teljesülnek.

A fentiek alapján a megoldást a következő program adja, amely egyúttal kitranszformálja a ”rákövetkező” műveletet.

\frac{\ [i_{1..m}] = (σ_{1} − 1, σ_{2} − 1, ..., σ_{m} − 1) /}{{i := \atop (σ_{1} − 1, ..., σ_{n} − 1)} ; h, l := m + 1, ↓ ; ¬l ; \overline{\ i_{h−1} = σ_{h−1} − 1 / ; i_{h−1} := 0 ; i_{h−1} := ; i_{h−1} + 1 ; l :=↑ ; h := h − 1}}

Mindezeket figyelembe véve, a kiinduló feladat megoldását a következő program adja:

i := (0, 0, ..., 0) ; m, u := 0, ↑ ; m < n ∧ u ; \overline{\frac{u := \overline{ρ}_{m+1}(i)}{m := m + 1}} ; ¬u ∧ i ≠ (σ_{1} − 1, σ_{2} − 1, ..., σ_{n} − 1) ; \overline{\  [i_{1..m}] = (σ_{1} − 1, σ_{2} − 1, ..., σ_{m} − 1)  / ; {i := \atop (σ_{1} − 1, ..., σ_{n} − 1)} ; h, l := m + 1, ↓ ; ¬l ; \overline{\ i_{h−1} = σ_{h−1} − 1  / ; i_{h−1} := 0 ; i_{h−1} := ; i_{h−1} + 1 ; l :=↑ ; h := h − 1} ; m, u := 0, ↑ ; m < n ∧ u ; \overline{\frac{u := \overline{ρ}_{m+1}(i)}{m := m + 1}}}

Az ELŐRELÉPŐ program utófeltételéből következik, hogy a KERESŐ program

[i_{1..m}] ≠ (σ_{1} − 1, σ_{2} − 1, ..., σ_{m} − 1)

esetén elég, ha a [h, n] intervallumban keres, mivel az [1, h − 1] intervallumban az i index vektor komponensei nem változtak, és ebben az intervallumban \overline{ρ}_{k}(i) állítások biztosan igazak h − 1 < m miatt.

Hasonlóan, ha

[i_{1..m}] = (σ_{1} − 1, σ_{2} − 1, ..., σ_{m} − 1),

akkor a keresést elég m-től indítani, hiszen ebben az esetben csak az i_{m+1}, ..., i_{n} komponensek változtak, és a keresés az első lépésben véget fog érni.

Minden esetre m a kereséshez alkalmas értéket fogja felvenni, ha az ELŐRELÉPŐ program belső ciklusában a h váltzó helyett magát az m-et használjuk, és a KERESŐ programban a keresést az [m, n] itervallumra redukáljuk.

A fentiek alapján a keresett program végleges formája a következő:

i := (0, 0, ..., 0) ; m, u := 0, ↑ ; m < n ∧ u ; \overline{\frac{u := \overline{ρ}_{m+1}(i)}{m := m + 1}} ; ¬u ∧ i ≠ (σ_{1} − 1, σ_{2} − 1, ..., σ_{n} − 1) ; \overline{\  [i_{1..m}] = (σ_{1} − 1, σ_{2} − 1, ..., σ_{m} − 1)  / ; {i := \atop (σ_{1} − 1, ..., σ_{n} − 1)} ; m, l := m + 1, ↓ ; ¬l ; \overline{\ i_{m−1} = σ_{m−1} − 1  / ; i_{m−1} := 0 ; i_{m−1} := ; i_{m−1} + 1 ; l :=↑ ; m := m − 1} ; m, u := m − 1, ↑ ; m < n ∧ u ; \overline{\frac{u := \overline{ρ}_{m+1}(i)}{m := m + 1}}}

10