\documentclass[a4paper]{article}
\usepackage{progm}
\analpacks
\analoldal{2. feladatsor, log. ker. \nyil lin. ker. 3.}
\newcommand{\Hh}{\ensuremath{\mathcal{H}}}
\begin{document}
\noindent
\emph{Feladat:} Adott az $f:\Z\nyil\Hh$ monoton növő függvény és az
$[m..n]\subset\Z$ intervallum, valamint a $h\in\Hh$ érték.  Döntsük
el, hogy van-e az intervallumban olyan érték, amire $f(i)=h$!

Ez a feladat a logaritmikus keresés.  Próbáljunk meg olyan
specifikációt és visszavezetést adni, ami a lineáris keresés
3. verziójára vezet!

\begin{gather*}
\varphi\colon\No\nyil\Z\times\Z\times\L\\
\varphi(0):=(m,n,\hamis)\\
\forall i\ge1: \varphi(i):=F(i,\varphi(i-1)) \\
F(i,z):=\begin{cases}
(\star, \star, \igaz) & \text{ha } z.1\le z.2 \es f(\star)=h \\
(\star+1, z.2, \hamis) & \text{ha } z.1\le z.2 \es f(\star)<h \\
(z.1, \star-1, \hamis) & \text{ha } z.1\le z.2 \es f(\star)>h \\
z & \text{ha } z.1> z.2
\end{cases} \qquad\left(\text{ahol } \star = \left\lceil\frac{z.1+z.2}{2}\right\rceil \right) \\
\gamma(i):=\varphi(i).3 \qquad (i\ge0)\\
\delta(i):=\varphi(i).1>\varphi(i).2 \qquad (i\ge0)\\
\beta(i):=\gamma(i)\vagy\delta(i) \qquad (i\ge0)
\end{gather*}

Mivel a $\varphi$ rekurzív függvény első két eredménykomponense által
megadott intervallum folyamatosan csökken, amíg a harmadik komponens
hamis, $\beta$ biztosan teljesül elég nagy $i$-re.  Feladatunk, hogy
megállapítsuk, van-e olyan természetes szám, ahol $\gamma$ igaz.  Ha
van ilyen $\gamma$, akkor $\delta$ előtte sehol nem igaz, hiszen, ha
$\delta$ egyszer teljesül, akkor a rekurzív függvény onnantól kezdve
folyamatosan ugyanazt az értéket veszi fel, ami pedig nem $\gamma$
tulajdonságú.

\emph{Specifikáció:}\\
$\mathbb D=(\Z:a, \Z:b, \L:l)$ rekord, így $\varphi$ felfogható, mint $\varphi:\No\nyil\mathbb D$ függvény.\\
$A = \alatt{\Z}{m} \times \alatt{\Z}{n} \times \alatt{\Hh}{h} \times \alatt{\L}{l}$ \\
$B = \alatt{\Z}{m'} \times \alatt{\Z}{n'}$ \\
$Q = ( m=m' \es n=n' \es m\le n \es \forall k,j\in[m,n]:(k<j)\nyil(f(k)\le f(j)) \es \exists j\ge 1: \beta(j))$ \\
$R = ( Q \es l=(\exists j\ge 1: \gamma(j) \es \forall k\in [m..j-1]:\nem\delta(k)))$

\begin{tabular}{cccl}
  feladat &  & lin. ker. 3 & \\
  \hline
  $1$ & \knyil & $m$ & (alteres, konstanssal helyettesítés) \\
  $l$ & \knyil & $u$ \\
  $-$ & \knyil & $i$ & (alteres, általánosított)
\end{tabular}

A visszavezetés általánosított amiatt is, mert az előfeltétel
szigorúbb, a lineáris keresés nem követeli meg egy függvény
monotonságát.

\begin{stuki}[8cm]
  \stm{i,l,v:=0,\hamis,\hamis}
  \begin{WHILE}{2}{\stm{\nem l \es \nem v}}
    \stm{l,v:=\varphi(i+1).3, \varphi(i+1).1 >\varphi(i+1).2}
    \stm{i:=i+1}
  \end{WHILE}
\end{stuki}

Helyettesítsük a $\varphi$ rekurzívfüggvény a $z$ változóval, amely $\mathbb D$ típusú:
\begin{stuki}[6cm]
  \stm{i,l,v,z:=0,\hamis,\hamis,(m,n.\hamis)}
  \begin{WHILE}{3}{\stm{\nem l \es \nem v}}
    \stm{z:=F(i+1, z)}
    \stm{l,v:=z.l, z.a >z.b}
    \stm{i:=i+1}
  \end{WHILE}
\end{stuki}

Az $F$ függvény kiszámítható elágazással:
\begin{stuki}[16cm]
  \stm{i,l,v,z:=0,\hamis,\hamis,(m,n.\hamis)}
  \begin{WHILE}{4}{\stm{\nem l \es \nem v}}
    \begin{CASE}{1}{4}
      \WHEN{\stm{z.a\le z.b \es f(\star)=h}}
      \stm{z:=(\star, \star, \igaz)}
      \WHEN{\stm{z.a\le z.b \es f(\star)<h}}
      \stm{z:=(\star+1, z.b, \hamis)}
      \WHEN{\stm{z.a\le z.b \es f(\star)>h}}
      \stm{z:=(z.a, \star-1, \hamis)}
      \WHEN{\stm{z.a> z.b}}
      \SKIP
    \end{CASE}
    \stm{l,v:=z.l, z.a >z.b}
    \stm{i:=i+1}
  \end{WHILE}
\end{stuki}

$i$ sosem szerepel értékadás jobb oldalán vagy feltételben, így
elhagyható, $z.l$ pedig pont ugyanazt az értéket veszi fel mindig,
mint $l$, így $l$ helyettesíthető $z.l$-lel, $v$ úgy küszöbölhető ki,
ha a ``nem megengedett ciklusfeltétel kitranszformálása''
programtranszformációt alkalmazzuk visszafele.  Mindezen átalakítások
közben a $z$ rekordváltozót helyettesítsük az $a,b,e$ változókkal!

\begin{stuki}[16cm]
  \stm{a,b,e:=m,n.\hamis}
  \begin{WHILE}{2}{\stm{\nem e \es a\le b}}
    \begin{CASE}{1}{4}
      \WHEN{\stm{a\le b \es f(\star)=h}}
      \stm{a,b,e:=\star, \star, \igaz}
      \WHEN{\stm{a\le b \es f(\star)<h}}
      \stm{a,b,e:=\star+1, b, \hamis}
      \WHEN{\stm{a\le b \es f(\star)>h}}
      \stm{a,b,e:=a, \star-1, \hamis}
      \WHEN{\stm{a> b}}
      \SKIP
    \end{CASE}
  \end{WHILE}
\end{stuki}

A program kis egyszerű átalakításokkal (a fölösleges szimultán
értékadásrészek elhagyásával, a $\star$ jelölés egy külön $i$
változóval való helyettesítésével, a sosem végrehajtódó utolsó
elágazáság elhagyásával) lényegében a logaritmikus keresés programjává
transzformálható.

A programról látható, hogy az $e$ változót csak akkor állítja igazra,
ha mellette az $a$ értéket olyanra állítja, hogy $f(a)=h$.  Ezzel a
meggondolással a keresett elem megtalálására is felhasználhatjuk a
programunkat nem csak a létezés megállapítására.

Annyiban csaltunk, hogy a rekurzív függvényről, amit csak úgy
kitaláltunk, illene bebizonyítani, hogy tényleg akkor vesz fel valahol
a harmadik komponensében igaz értéket, ha az eredeti függvény felvesz
az $[m..n]$ intervallumon $h$ értéket.

\begin{itemize}
\item $\exists i\ge 1:\varphi(i).3 \kovkerdes \exists i\in[m..n]: f(i)=h$

Trivialitás, ugyanis az $F$ függvény úgy van definiálva, hogy a $\star$ pont egy ilyen $i$.

\item $\exists i\in[m..n]:f(i)=h \kovkerdes \exists i\ge 1: \varphi(i).3$

  Tegyük fel, hogy $\forall x\ge 1: \nem \varphi(x).3$.

  Ekkor teljes indukcióval belátjuk, hogy $\varphi(x)=(a,b,\hamis)$ esetén $f(a)\le h=f(i)\le f(b)$ és $a\le b$.\\
  Ez igaz $\varphi(0)=(m,n,\hamis)$-ra felhasználva a tétel feltételrészét és $f$ monotonitását. \\
  Rögzített $x$ mellett $\varphi(x+1)$-re az $f(\star)$ függvényértéktől függően az alábbi teljesülhet:
  \begin{itemize}
    \item $f(\star)=h$, ekkor $\varphi(x+1).3=\igaz$, ami ellentmondás.
    \item $f(\star)<h$, ekkor tudjuk $f$ monotonitásából, hogy
      $\forall j\in[a,\star]: f(j)<h$, ezért $x+1$-re is teljesül az
      elvárt $f(\star+1)\le h \le f(b)$ állítás.  És $\star+1\le
      b$-nek is teljesülnie kell $f$ monotonitása miatt, hiszen $b$
      fölött már a $h$-nál nagyobb értékek vannak és a tételben
      feltettük, hogy található $h$ érték az $f$ értékei között.
    \item $f(\star)>h$ esetén hasonlóan belátható, hogy vagy
      ellentmondásra jutunk vagy igaz a indukció.
  \end{itemize}
  Tehát kiderült, hogy minden $x$-re $\varphi(x)=(a,b,hamis)$ mellett
  $a\le b$, ami viszont lehetetlen, hiszen az $a,b$ intervallum
  folyamatosan szűkűl és kezdetben csak véges nagy volt.  Az eredeti
  feltételezésünk helytelen volt, tehát amennyiben az $f$ függvényben
  megtalálható a $h$ érték, akkor a $\varphi$ függvény harmadik
  komponense előbb-utóbb igaz értéket vesz fel.
\end{itemize}

\end{document}