Függvény helyettesítés viszavezetés - Programtranszformácó
Feladat
\(f:\Z\to\Z\)
Keressük a legnagyobb olyan értéket annak helyével, ahol a függvény értéke mindkét szomszédjánál kissebb
\(A=\big(m:\Z,\;n:\Z,\;i:\Z,\;\max:\Z,\;\ell:\mathbb{L}\big)\)
\(B=\big(m':\Z,\;n':\Z\big)\)
\(Q=\big(m=m'\;\land\;n=n'\big)\)
\(R=\bigg(Q\land\green{\ell=}\green{\big(}\exists j\in[m+1..n-1]: \;f(j)<f(j-1)\land f(j)<f(j+1)\green{\big)} \\ \orange{\ell\supset\Big(}i\in[m+1..n-1]\land f(i)<f(i-1)\;\land\;f(i)<f(i+1)\;\land\;\max=f(i)\;\land\;\forall j\in[m+1..n-1]:{\color{#10B0FF}\big(f(i)<f(i-1)\;\land\;f(i)<f(i+1)\big)\supset} {\color{#10D0F0}f(j)\le f(i)}\orange{\Big)}\bigg)\)
Visszavezetés módszere
strukk?
┌──────────────────────────────────────────────────────────┐
│ k,l := m, hamis │
├──────────────────────────────────────────────────────────┤
│ k != n-1 │
│ ┌──────────────────────────────────────────────────────┤
│ │ u:= f(i)< f(i-1) ∧ f(i)<f(i+1) │
│ ├──────┬─────────────┬─────────────────────────────────┤
│ │\ ¬u │\ u ∧ ¬l │\ u ∧ l │
│ ├──────┼─────────────┼────────────────┬────────────────┤
│ │ │ i,max := │\ f(k+1) >= max │\ f(k+1) <= max │
│ ├──────┼─────────────┼────────────────┼────────────────┤
│ │ SKIP │ k+1, f(k+1) │ i,max := │ SKIP │
│ │ │ │ k+1, f(k+1) │ │
│ ├──────┴─────────────┴────────────────┴────────────────┤
│ │ k:= k+1 │
└───┴──────────────────────────────────────────────────────┘
A helyettesítéssel egy, a feltételes maximumkereséssel ekvivalens programot kaptunk (legalább az utófeltételben).
Viszont azt tudjuk még progelmből, hogy ha adott \(S\) program, ami megoldja az \(F_2\) feladatot ami szigorúbb, mint \(F_1\), akkor \(S\) biztosan megoldja \(F_1\)-et is.
Namost, ha az intervallumot is behelyettesítjük, egy tágabb intervallumot határozunk meg, így az eredeti specifikáció mindenképp teljesül a visszavezetéssel.