\input amstex
\documentstyle{amsppt}

\NoRunningHeads


\magnification=1200
\hsize=160 truemm
\vsize=220 truemm
\font\term=cmr10
\font\il=cmbx10

\input menv
\input stuki
\input border
\input scaling



\document

\centerline{\scaling 3 {\cimf $\binom nk$ kisz\'am\'\i t\'asa}}

\bigskip
Legyen $\text{\bf X}:vekt(\text{\bf N},\text{\bf N})$.



$$
\xxalignat 2
&
\alignedat 3
\quad \text{\bf A}: \quad &\text{\bf N}_0& \times &\text{\bf N}_0 &\times &\text{\bf X} \\
 &n & &k & &x
\endalignedat
&&
\endxxalignat
$$
$$
\xxalignat 2
&
\alignedat 2
\quad \text{\bf B}: \quad &\text{\bf N}_0& \times &\text{\bf N}_0  \\
 &n^\prime & &k^\prime
\endalignedat
&&
\endxxalignat
$$
$$
\xxalignat 2
\quad Q&:\bigl(n=n^\prime \land k=k^\prime \land k \le n \bigr) &&
\endxxalignat
$$
$$
\xxalignat 2
\quad R&:\bigl(Q \land x.hiv = \binom {n^\prime}{k^\prime} \bigr) &&
\endxxalignat
$$

A feladat megold\'as\'ahoz ciklust haszn\'alunk a k\"ovetkez\H o invari\'anssal:
$$
\xxalignat 2
\quad P&:\bigl(Q \land x.dom = n-k+1 \land i \in [0..k]
    \land \forall j \in [x.lob..x.hib]: x[j] = \binom {j-x.lob+i}i \bigr) &&
\endxxalignat
$$
\bigskip

K\"onnyen l\'athat\'o, hogy
$$
Q\Rightarrow P^{i,x \leftarrow 0,(1,<1_1,1_2,...,1_{n-k+1}>)}\Leftrightarrow
   lf\bigl(i,x := 0,(1,<1_1,1_2,...,1_{n-k+1}>);P\bigr)
$$
Emiatt a keresett program a k\"ovetkez\H o szekvencia lesz:
$$
\bigl(i,x := 0,(1,<1_1,1_2,...,1_{n-k+1}>); DO\bigr)
$$
ahol a $DO$ ciklust kell alkalmasan megv\'alasztani.
\bigskip

{\bf 1.} $P \Rightarrow P$ nyilv\'an teljes\"ul.
\bigskip

{\bf 2.} $P  \land \lnot \pi \Rightarrow R$ felt\'etel teljes\'\i thet\H o,
ha $\lnot \pi: i\ge k $, hiszen
$x.hiv = \binom {x.hib-x.lob+k}k = \binom nk $. Ennek megfel\H oen
$$\pi: i < k$$
\bigskip

{\bf 3.} $P \land \pi \Rightarrow t > 0$ felt\'etel kiel\'eg\'\i thet\H o, ha
$$t: k-i$$
\bigskip

A $t$ termin\'al\'o f\"uggv\'eny v\'alaszt\'asa miatt keress\"uk a ciklusmagot
$$
   S: \bigl(S_1;i:=i+1\bigr)
$$
alakban.
\bigskip

{\bf 5.} $\forall t_0 \in \text{\bf Z}: P \land \pi \land t \le t_0+1 \Rightarrow
           lf\bigl(S;t\le t_0 \bigr)$ felt\'etel teljes\"ul, ha az $i$ projekci\'o
az $S_1$ programra n\'ezve konstans f\"uggv\'eny.
\bigskip

{\bf 4.} $P \land \pi \Rightarrow lf\bigl(S;P\bigr)$ felt\'etel kiel\'eg\'\i t\'es\'ehez
elegend\H o, ha olyan $S_1$ programot keres\"unk, amelyre
$$
    P \land \pi \Rightarrow lf \bigl(S_1;P^{i\leftarrow i+1}\bigr)
$$
%\newpage

Keress\"uk az $S_1$ programot ciklus form\'aban, amely invari\'ansa:
$$
\xxalignat 2
 \quad \overline{P}:\bigl(Q &\land x.dom=n-k+1 \land i+1 \in [0..k] \land l \in [x.lob..x.hib] \land&& \\
      &\land \forall j \in [x.lob..l]: x[j] = \binom  {j-x.lob+(i+1)}{i+1} \land && \\
      &\land \forall j \in [l+1..x.hib]: x[j] = \binom {j-x.lob+i}i
               \bigr) &&
\endxxalignat
$$
\bigskip

K\"onnyen l\'athat\'o, hogy
$$
P \land \pi \Rightarrow \overline{P}^{l\leftarrow 1}\Leftrightarrow
                  lf\bigl(l:=1;\overline{P}\bigr)
$$
teljes\"ul. Ez\'ert $S_1$-et
$$
   S_1:\bigl(l:=1;\overline{DO}\bigr)
$$
alakban kell keresn\"unk.
\bigskip

{\bf 1.a} $\overline{P}\Rightarrow \overline{P}$ nyilv\'an teljes\"ul.
\bigskip

{\bf 2.a} $\overline{P} \land \lnot \overline{\pi}
\Rightarrow P^{i\leftarrow i+1}$ felt\'etel teljes\"ul, ahol
$P^{i\leftarrow i+1}$ $\overline{R}$-nek felel meg, ha
$\lnot \overline{\pi} : l\ge x.hib$ teh\'at, ha
$$
\overline{\pi} : l< x.hib
$$

{\bf 3.a} $\overline{P} \land \overline{\pi} \rightarrow \overline{t} > 0$ teljes\"ul,ha
$$
  \overline{t}: x.hib-l
$$
A $\overline{t}$ termin\'al\'o f\"uggv\'eny v\'alaszt\'asa miatt keress\"uk a ciklusmagot
$$
   \overline{S}: \bigl(\overline{S}_1;l:=l+1\bigr)
$$
alakban.
\bigskip

{\bf 5.a} $\forall \overline{t}_0 \in \text{\bf Z}: \overline{P} \land \overline{\pi} \land \overline{t} \le \overline{t}_0+1 \Rightarrow
           lf\bigl(\overline{S};\overline{t}\le \overline{t}_0 \bigr)$ felt\'etel teljes\"ul, ha az $l$ projekci\'o
az $\overline{S}_1$ programra n\'ezve konstans f\"uggv\'eny.
\bigskip

{\bf 4.a} $\overline{P} \land \overline{\pi} \Rightarrow lf\bigl(\overline{S};\overline{P}\bigr)$ felt\'etel kiel\'eg\'\i t\'es\'ehez
elegend\H o, ha olyan $\overline{S}_1$ programot keres\"unk, amelyre
$$
    \overline{P} \land \overline{\pi} \Rightarrow lf \bigl(\overline{S}_1;\overline{P}^{l\leftarrow l+1}\bigr)
$$
$$
\xxalignat 2
 \quad \overline{P}\land \overline{\pi}:\bigl(Q \land x.dom=n-k+1 &\land i+1 \in [0..k] \land l \in [x.lob..x.hib] \land l <x.hib \land && \\
      &\land \forall j \in [x.lob..l]: x[j] = \binom  {j-x.lob+(i+1)}{i+1} \land && \\
      &\land \forall j \in [l+1..x.hib]: x[j] = \binom {j-x.lob+i}i
               \bigr) &&
\endxxalignat
$$
alapj\'an k\"onnyen l\'athat\'o:
$$
\xxalignat 2
 \quad \overline{P}\land \overline{\pi}\Rightarrow\bigl(Q \land x.dom=n-k+1 &\land i+1 \in [0..k] \land l+1 \in [x.lob..x.hib] \land && \\
      &\land \forall j \in [x.lob..l]: x[j] = \binom  {j-x.lob+(i+1)}{i+1} \land && \\
      &\land \binom {(l+1)-x.lob+(i+1)}{i+1} = x[l] + x[l+1] \land && \\
      &\land \forall j \in [l+2..x.hib]: x[j] = \binom {j-x.hib+i}i
               \bigr)  &&
\endxxalignat
$$

Ebb\H ol k\"ovetkezik, hogy
$$
 \quad \overline{P}\land \overline{\pi}= \bigl(\overline{P}^{l\leftarrow l+1}\bigr)^{x[l+1]\leftarrow x[l+1]+ x[l]}=
   lf\bigl(x[l+1]:= x[l+1]+ x[l]; \overline{P}^{l\leftarrow l+1}\bigr)
$$

K\"onnyen bel\'athat\'o, hogy az $l$ projekci\'o az $\overline{S}_1$ programra n\'ezve
konstans f\"uggv\'eny, ugyan\'ugy az $i$ projekci\'o az $S_1$ programra n\'ezve
konstans f\"uggv\'eny.

\"Osszegezve a kapott eredm\'enyeket, a k\"ovetkez\H o program megoldja a feladatot:

\bigskip
\centerline{
\loopindent=90
\STRUC 230pt :
     \Stm $i,x:= 0,(1,<1_1,1_2,...,1_{n-k+1}>)$;
     \Rule
     \WHILE \Stm $i < k$; DO
        \Stm $l:=1$;
        \Rule
        {
        \WHILE \Stm $l < x.hib$; DO
           \Stm $x[l+1]:= x[l+1]+ x[l]$;
           \Rule
           \Stm $l:=l+1 $;
        \ENDDO
         }
        \Rule
        \Stm $ i := i+1$;
     \ENDDO
\END. }


\enddocument
