Mátrixtükrözés a főátlóra

A feladat specifikációja:

Legyen 𝕄 : vekt(ℕ, vekt(ℕ, ℝ)) és 𝕄′ = {m ∈ 𝕄|∀j ∈ [m.lob..m.hib] : m_{j}.lob = m.lob ∧ m_{j}.hib = m.hib}

A ={𝕄′ \atop m}

B ={𝕄′ \atop m′}

Q : (m = m′)

R : (∀i ∈ [m.lob..m.hib] : ∀j ∈ [m.lob..m.hib] : m′_{ij} = m_{ji} ∧ ∧ m′.lob = m.lob ∧ m′.hib = m.hib)

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

P : (k ∈ [m.lob − 1..m.hib] ∧ ∧ ∀i ∈ [m.lob..k] : ∀j ∈ [m.lob..k] : m′_{ij} = m_{ji} ∧ ∧ ∀(i, j) ∈ [m.lob..m.hib] × [m.lob..m.hib] \ [m.lob..k] × [m.lob..k] : m′_{ij} = m_{ij} ∧ ∧ m′.lob = m.lob ∧ m′.hib = m.hib)

1. Q ⇏ P, de Q ⇒ P^{k←m.lob−1}.

Innen adódik, hogy Q ⇒ lf(k := m.lob − 1, P)

2. A ciklus levezetési szabálya második feltétele: P ∧ ¬π ⇒ R teljesül, ha ¬π : (k ≥ m.hib). Ezért π : (k < m.hib) alkalmas választás.

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

4. és 5. Belátható, hogy P ∧ k < m.hib ⇒ lf(S_{0}^{1}, P^{k←k+1}) esetén a (S_{0}^{1}; k := k + 1) program alkalmas ciklusmag.

Legyen

\overline{P} : (k ∈ [m.lob − 1..m.hib] ∧ k < m.hib ∧ l ∈ [m.lob − 1..k + 1] ∧ ∧ ∀i ∈ [m.lob..k] : ∀j ∈ [m.lob..k] : m′_{ij} = m_{ji} ∧ ∧ ∀i ∈ [m.lob..l] : (m′_{k+1i} = m_{ik+1} ∧ m′_{ik+1} = m_{k+1i}∧) ∧ ∀(i, j) ∈ [m.lob..m.hib] × [m.lob..m.hib] \ \([m.lob..k] × [m.lob..k] ∪ [m.lob..l] × {k + 1} ∪ ∪{k + 1} × [m.lob..l]) : m′_{ij} = m_{ij} ∧ ∧ m′.lob = m.lob ∧ m′.hib = m.hib)

Ekkor P ∧ k < m.hib ⇒ \overline{P}^{l←m.lob−1} \overline{P} ∧ ¬\overline{π} ⇒ P^{k←k+1} teljesül, ha ¬\overline{π} : l ≥ k + 1, tehát \overline{π} : l < k + 1 alkalmas választás. \overline{P} ∧ \overline{π} ⇒ \overline{t} > 0 teljesül, ha \overline{t} : k + 1 − l. Látható, hogy \overline{P} ∧ \overline{π} ⇒ (k ∈ [m.lob − 1..m.hib] ∧ k < m.hib ∧ l + 1 ∈ [m.lob − 1..k + 1] ∧ ∧ ∀i ∈ [m.lob..k] : ∀j ∈ [m.lob..k] : m′_{ij} = m_{ji} ∧ ∧ ∀i ∈ [m.lob..l] : (m′_{k+1i} = m_{ik+1} ∧ m′_{ik+1} = m_{k+1i}∧) ∧ m′_{k+1l+1} = m_{k+1l+1} ∧ m′_{l+1k+1} = m_{l+1k+1} ∧ ∀(i, j) ∈ [m.lob..m.hib] × [m.lob..m.hib] \ \([m.lob..k] × [m.lob..k] ∪ [m.lob..l + 1] × {k + 1} ∪ ∪{k + 1} × [m.lob..l + 1]) : m′_{ij} = m_{ij} ∧ ∧ m′.lob = m.lob ∧ m′.hib = m.hib) Ezért \overline{P} ∧ \overline{π} ⇒ \overline{P}^{l←l+1}^{m_{k+1,l+1},m_{l+1,k+1}←m_{l+1,k+1},m_{k+1,l+1}} Tehát \overline{P} ∧ \overline{π} ⇒ lf(\overline{S}_{0}^{1}, \overline{P}^{l←l+1}) Teljesul, ha \overline{S}_{0}^{1} : m_{k+1,l+1}, m_{l+1,k+1} := m_{l+1,k+1}, m_{k+1,l+1}

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

k := m.lob − 1 ; k < m.hib ; \overline{l := m.lob − 1 ; l < k + 1 ; \overline{\frac{m_{k+1,l+1}, m_{l+1,k+1} := m_{l+1,k+1}, m_{k+1,l+1}}{l := l + 1}} ; k := k + 1}