Mátrixtükrözés a melléká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_{(m.hib−(j−m.lob))(m.hib−(i−m.lob))} ∧ ∧ m′.lob = m.lob ∧ m′.hib = m.hib)

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

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

1. Q ⇏ P, de Q ⇒ P^{k←m.hib+1}.

Innen adódik, hogy

Q ⇒ lf(k := m.hib + 1, P)

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

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

4. és 5. Belátható, hogy P ∧ k > m.lob ⇒ 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..m.hib + 1] ∧ k > m.lob ∧ l ∈ [m.lob − 1..m.lob + (m.hib − (k − 1)] ∧ ∧ ∀i ∈ [k..m.hib] : ∀j ∈ [m.lob..m.lob + (m.hib − k)] : m′_{ij} = m_{(m.hib−(j−m.lob))(m.hib−(i−m.lob))} ∧ ∧ ∀i ∈ [m.lob..l] : (m′_{k−1i} = m_{(m.hib−(i−m.lob))(m.hib−((k−1)−m.lob)} ∧ ∧ m′_{(m.hib−(i−m.lob))(m.hib−((k−1)−m.lob)} = m_{k−1i}) ∧ ∧ ∀(i, j) ∈ ([m.lob..m.hib] × [m.lob..m.hib] \ \([k..m.hib] × [m.lob..m.lob + (m.hib − k)] ∪ {k − 1} × [m.lob..l] ∪ ∪[m.hib − (l − m.lob)..m.hib] × {m.hib − (k − 1 − m.lob)})) : m′_{ij} = m_{ij} ∧ ∧ m′.lob = m.lob ∧ m′.hib = m.hib)

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

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

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

3