\binom{n}{k} kiszámítása

\begin{matrix}A : & N_{0} & × & N_{0}( & × & N & × & N × ...) & × & N \\ n & k & v_{1} & v_{2} & v_{n−k+1} \end{matrix}

\begin{aligned}B : & N_{0} & × & N_{0} \\ & n′ & k′ \end{aligned}

Q : (n = n′ ∧ k = k′ ∧ k ≤ n)
R : (Q ∧ v_{n−k+1} = \binom{n′}{k′})

A feladat megoldásához ciklust használunk a következő invariánssal:

P : (Q ∧ i ∈ [0, k] ∧ ∀j ∈ [1, n − k + 1] : v_{j} = \binom{j + i − 1}{i})

Könnyen látható, hogy

Q ⇒ P^{i,v_{1},v_{2},...,v_{n−k+1}←0,1,1,...,1} = lf(i, v_{1}, v_{2}, ..., v_{n−k+1} := 0, 1, 1, ..., 1; P ) Emiatt a keresett program a következő szekvencia lesz:

(i, v_{1}, v_{2}, ..., v_{n−k+1} := 0, 1, 1, ..., 1; DO)

ahol a DO ciklust kell alkalmasan megválasztani. 1. P ⇒ P nyilván teljesül.

2. P ∧ ¬π ⇒ R feltétel teljesíthető, ha ¬π : i = k, hiszen v_{n−k+1} = \binom{n−k+1+k−1}{k} = \binom{n}{k}. Ennek megfelően

π : i ≠ k

3. P ∧ π ⇒ t > 0 feltétel kielégíthető, ha

t : k − i Typeset by A_{M}S-TEX A t termináló függvény választása miatt keressük a ciklusmagot

S : (S_{1}; i := i + 1)

alakban.

5. ∀t_{0} ∈ Z : P ∧ π ∧ t ≤ t_{0} + 1 ⇒ lf(S; t ≤ t_{0}) feltétel teljesül, ha az i projekció az S_{1} programra nézve konstans függvény.

4. P ∧ π ⇒ lf(S; P ) feltétel kielégítéséhez elegendő, ha olyan S_{1} programot keresünk, amelyre

P ∧ π ⇒ lf(S_{1}; P^{i←i+1})

Keressük az S_{1} programot ciklus formában, amely invariánsa:

\overline{P} : (Q ∧ i + 1 ∈ [0, k] ∧ l ∈ [1, n − k + 1] ∧ ∀j ∈ [1, l] : v_{j} = \binom{j + (i + 1) − 1}{i + 1}∧

∧ ∀j ∈ [l + 1, n − k + 1] : v_{j} = \binom{j + i − 1}{i})

Könnyen látható, hogy

P ∧ π ⇒ \overline{P}^{l←1} = lf(l := 1; \overline{P} )

teljesül. Ezért S_{1}-et

S_{1} : (l := 1; \overline{DO})

alakban kell keresnünk.

1.a \overline{P} ⇒ \overline{P} nyilván teljesül. 2.a \overline{P} ∧¬\overline{π} ⇒ P^{i←i+1} feltétel teljesül, ahol P^{i←i+1} \overline{R}-nek felel meg, ha ¬\overline{π} : l = n−k+1

tehát, ha

\overline{π} : l ≠ n − k + 1

3.a \overline{P} ∧ \overline{π} → \overline{t} > 0 teljesül,ha

\overline{t} : (n − k + 1) − l

A \overline{t} termináló függvény választása miatt keressük a ciklusmagot

\overline{S} : (\overline{S}_{1}; l := l + 1)

alakban.

5.a ∀\overline{t}_{0} ∈ Z : \overline{P} ∧ \overline{π} ∧ \overline{t} ≤ \overline{t}_{0} + 1 ⇒ lf(\overline{S}; \overline{t} ≤ \overline{t}_{0}) feltétel teljesül, ha az l projekció az \overline{S}_{1} programra nézve konstans függvény.

4.a \overline{P} ∧ \overline{π} ⇒ lf(\overline{S}; \overline{P} ) feltétel kielégítéséhez elegendő, ha olyan \overline{S}_{1} programot keresünk, amelyre

\overline{P} ∧ \overline{π} ⇒ lf(\overline{S}_{1}; \overline{P}^{l←l+1})

\overline{P} ∧ \overline{π} : (Q ∧ i + 1 ∈ [0, k] ∧ l ∈ [1, n − k + 1] ∧ l ≠ n − k + 1∧

∧ ∀j ∈ [1, l] : v_{j} = \binom{j + (i + 1) − 1}{i + 1}∧

∧ ∀j ∈ [l + 1, n − k + 1] : v_{j} = \binom{j + i − 1}{i})

alapján könnyen látható:

\overline{P} ∧ \overline{π} = (Q ∧ i + 1 ∈ [0, k] ∧ l ∈ [1, n − k + 1] ∧ l ≠ n − k + 1∧

∧ ∀j ∈ [1, l] : v_{j} = \binom{j + (i + 1) − 1}{i + 1}∧

∧ \binom{l + 1 + (i + 1) − 1}{i + 1} = v_{l} + v_{l+1}∧

∧ ∀j ∈ [l + 2, n − k + 1] : v_{j} = \binom{j + i − 1}{i})

Ebből következik, hogy

\overline{P} ∧ \overline{π} = (\overline{P}^{l←l+1})^{v_{l+1}←v_{l+1}+v_{l}} = lf(v_{l+1} := v_{l+1} + v_{l}; \overline{P}^{l←l+1})

Könnyen belátható, hogy az l projekció az \overline{S}_{1} programra nézve konstans függvény, ugyanúgy az i projekció az S_{1} programra nézve konstans függvény.

Összegezve a kapott eredményeket, a következő program megoldja a feladatot:

i, v_{1}, v_{2}, ..., v_{n−k+1} := 0, 1, 1, ..., 1 ; i ≠ k ; \overline{l := 1 ; l ≠ n − k + 1 ; \overline{\frac{v_{l+1} := v_{l+1} + v_{l}}{l := l + 1}} ; i := i + 1}