Winograda mnożenie macierzy: Różnice pomiędzy wersjami

Aktualna wersja na dzień 21:15, 5 lis 2015

Przedstawiamy algorytm Winograda i dowód jego poprawności.

Wprowadzenie

Algorytm Winograda może być stosowany do obliczania iloczynu macierzy kwadratowych. Jego przydatność jest szczególnie widoczna gdy elementami macierzy są obiekty reprezentujące jakiś pierścień inny niż pierścień liczb rzeczywistych. Np. w przypadku gdy dany pierścień $\mathcal{C}$ jest zaimplementowane w programie przez klasę $C$.

Drugim i ważniejszym powodem do skreślenia tej notatki jest potrzeba zwrócenia uwagi na znikomą przydatność asercji i tzw. programowania przez kontrakt (*ang.* design by contract). Asercje są przydatne jako notatki, ale nie stanowią rozwiązania problemu zapewnienia poprawności algorytmu.

Zapraszam do czytania, zwłaszcza rozdziału Dowód poprawności.

Algorytm

W tym rozdziale pojawiają się dwa warunki:

- warunek wstępny – Precondition,

- warunek końcowy – Postcondition, oraz

- algorytm – algorytm Winograda.

Jak się upewnić, że algorytm jest poprawny ze względu na warunek początkowy i warunek końcowy? W literaturze proponowane są dwa podejścia:

- udowodnij częściową porawność sprawdzając pewne niezmienniki – jest

   to tzw. metoda Floyda-Hoare’a,

- wykonaj pewną liczbę obliczeń testowych i zaufaj, że w trakcie

   eksploatacji algorytmu nie okaże się, że jest on niepoprawny.

W obliczeniach testowych można w trakcie obliczeń sprawdzać wcześniej wstawione warunki – asercje. Czy rzeczywiście są one pomocne?

W następnym rozdziale pokażemy inną drogę - drogę dowodzenia lematów i w końcu twierdzenia o poprawności (całkowitej) algorytmu Winograda względem warunku początkowego Precondition i warunku końcowego Postcondition.

[1] $\mathbf{signal}\ Niezgoda;$

$\mathbf{unit}\ Winograd:\ \mathbf{procedure}(A,B: \mathbf{array\_of\ array\_of}\ real;\

            \ \mathbf{output}\ C: \mathbf{array\_of\ array\_of}\ real);$

wymagaj by A i B były macierzami kwadratowymi rozmiaru n x n zapewnij, że obliczona macierz C jest produktem macierzy A i B, C = A \* B $\mathbf{var}\ i,j,k,n,m: \mathbf{integer},\

      W,V: \mathbf{array\_of\ real}, 
      p: \mathbf{boolean}, 
      s: \mathbf{real}; $

$\mathbf{begin}$\ \ \ \

$raise\ Niezgoda$ ; i := upper(A); j := lower(A); n := i-j+1; raise Niezgoda ; ; sprawdzono: macierze są kwadratowe, rozmiaru n x n\

\

$p := (n\ mod\ 2) = 0;$ $m := n\ div\ 2;$ $\mathbf{array}\ W\ \mathbf{dim} (1:n);$ $\mathbf{array}\ V\ \mathbf{dim} (1:n);$ $ \mathbf{array} \ C\ \mathbf{dim} (1:n);$ $ \mathbf{array}\ C(i)\ \mathbf{dim} (1:n)$ ;\ \

s:=0; $  s := A[j,2*i-1] * A[j,2*i] +s;$ ; W[j] := s; ;

s:=0; ; V[j] := s; ;

\

s:= 0; s:= (A[i,2\*k-1]+B[2\*k,j]) \* (B[2\*k-1,j]+A[i,2\*k]) +s; ;\

$ C[i,j] :=s-W[i]-V[j];$

$C[i,j] := C[i,j] + A[i,n]*B[n,j];$ ;\

{ j } ; { i }\

\ $\mathbf{end}\ Winograd;$

Dowód poprawności

Naszym zadaniem jest wykazać nastepującą implikację [math]\mathrm{Precondition} \Rightarrow [\mathrm{Algorytm\ Winograda}]\mathrm{Postcondition}[/math] co się czyta tak: *jeśli dane spełniają warunek wstępny to algorytm Winograda kończy obliczenia nie sygnalizując błędu i wyniki spełniają warunek końcowy*.

Sprawdzenie czy warunek wstępny jest spełniony przez dane może być w części wykonane przez kompilator. Kompilator może sprawdzić czy parametry aktualne sa tablicami dwuwymiarowymi. Druga część warunku, że rozmiary tablic są równe $n \times n$ nie może być sprawdzona przed wywołaniem procedury Winograd, nie może też być udowodniona. Wobec tego wykonywanie procedury rozpoczynamy od (dynamicznego) sprawdzania kształtu i rozmiaru tablic[^1]. Można rozważać czy nie dałoby się udowodnić, o programie stosującym procedurę Winograd, że warunek wstępny jest spełniony za każdym razem gdy procedura Winograd jest wywoływana w naszym programie. Ale czy można zagwarantować, że każdy program stosujący algorytm Winograda będzie sprawdzał warunek wstępny? lub go dowodził? Lepiej więc zostawić sprawdzanie warunku wstępnego procedurze Winograd.\

Do algorytmu Winograd wstawiliśmy asercje. Mają one za zadanie:

1. umożliwić sygnalizację naruszenia warunku asercji w trakcie wykonywania programu,

1. ułatwić argumentację na rzecz tezy o poprawności algorytmu.

W tym przypadku trudno mówić o dynamiczej weryfikacji: ażeby sprawdzić warunek wyliczony w asercji trzeba powtórzyć obliczenia – to niewiele nam daje. Ponadto, tu uwaga natury ogólnej, zamiana asercji na instrukcję warunkową\ $$\mathbf{if}\ warunek\_ asercji\ \mathbf{then}\ \mbox{wrzuć\_ wyjątek}\ \mathbf{fi}$$ zapewnia tylko tyle, że podczas wykonywania algorytmu zostanie zasygnalizowany błąd. Nie mamy nawet gwarancji, że zdarzy się to zawsze gdy program zawiera błędy.\

Natomiast asercje możemy zastąpić lematami i udowodnić je

Lemat 1
Dla każdego [math]j, 1\leq j \leq n[/math],\ i\ [math]m=n \div 2[/math] zachodzi
[math]K: \left \{ \begin{array}{l} \quad s:=0; \\ \quad \mathbf{for}\ i:=1\ \mathbf{to}\ m \\ \quad \mathbf{do} \\ \qquad s := A[j, 2*i-1] * A[j,2*i]+s; \\ \quad \mathbf{od} ; \\ \quad W[j]:=s; \end{array} \right \} \left (W_j=\sum\limits_{i=1}^{n \div 2} A_{j,2i-1}*A_{j,2i}\right )[/math]

lub to samo spostrzeżenie zapisane nieco inaczej

Lemat 2
Dla [math]m=n \div 2[/math] zachodzi
[math]M: \left \{ \begin{array}{l} \textbf{for }j:=1\textbf{ to } n \textbf{ do} \\ \quad s:=0; \\ \quad \mathbf{for}\ i:=1\ \mathbf{to}\ m \\ \quad \mathbf{do} \\ \qquad s := A[j, 2*i-1] * A[j,2*i]+s; \\ \quad \mathbf{od} ; \\ \quad W[j]:=s; \\ \textbf{od} \end{array} \right \} \left ( \forall_{1\leq j \leq n}\,W_j=\sum\limits_{i=1}^{n \div 2} A_{j,2i-1}*A_{j,2i}\right )[/math]

Zwróć uwagę na to, że zewnętrzna instrukcja for oblicza kwantyfikator ograniczony, a wewnętrzna instrukcja for oblicza sumę. Instrukcja for ma jeszcze wiele innych zastosowań.

Lemat 3
Dla każdego [math]j, 1\leq j \leq n[/math], i [math]m=n \div 2[/math] zachodzi
[math]\left \{ \begin{array}{l} \quad s:=0; \\ \quad \mathbf{for}\ i:=1\ \mathbf{to}\ m \\ \quad \mathbf{do} \\ \qquad s := B[2*i-1,j] * B[2*i,j]+s; \\ \quad \mathbf{od} ; \\ \quad V[j]:=s; \end{array} \right \} \left (V_j=\sum\limits_{i=1}^{n \div 2} B_{2i-1,j}*B_{2i,j}\right )[/math]

Kolejny lemat

Lemat 4
[math]\forall_{1\leq i \leq n},\forall_{1\leq j \leq n}\ \left \{ \begin{array}{l} s:= 0; \\ \mathbf{for} \ k:= 1\ \mathbf{to}\ m \\ \mathbf{do} \\ \quad s:= (A[i,2*k-1]+B[2*k,j]) \\ \qquad * (B[2*k-1,j]+A[i,2*k]) +s;\\ \mathbf{od};\end{array} \right \} \left (s = \sum\limits_{k=1}^{n \div 2} (A_{i,2k-1}+B_{2k,j})*(B_{2k-1,j}+A_{i,2k}) \right )[/math]

\ Przy założeniu, że tablice A i B są macierzami kwadratowymi rozmiaru n x n i że zachodzą lematy 1 oraz 2, prawdziwa jest następująca formuła algorytmiczna\

Lemat 5
[math]\forall_{1\leq i \leq n},\forall_{1\leq j \leq n} \left \{ \begin{array}{l} s:= 0; \\ \mathbf{for} \ k:= 1\ \mathbf{to}\ m \\ \mathbf{do} \\ \quad s:= (A[i,2*k-1]+B[2*k,j]) \\ \qquad * (B[2*k-1,j]+A[i,2*k]) +s;\\ \mathbf{od};\\ C[i,j] := s -W[i] -V[j]; \\ \end{array} \right \} \left (s = \sum\limits_{k=1}^{2*(n \div 2)} A_{i,k}*B_{k,j} \right )[/math]

\ Z prawdziwości lematów 1 i 2 wynika, że następująca formuła jest prawdziwa\

Lemat 6
[math]\left \{ \begin{array}{l} \mathbf{for} \ i:=1\ to \ n \\ \mathbf{do} \\ \quad \mathbf{for} \ j:=1\ to \ n \\ \quad \mathbf{do} \\ \quad \quad s:= 0; \\ \quad \quad \mathbf{for} \ $k:= 1$\ \mathbf{to}\ $m$ \\ \quad \quad \mathbf{do} \\ \quad \quad \quad s:= (A[i,2*k-1]+B[2*k,j]) \\ \quad \quad \qquad * (B[2*k-1,j]+A[i,2*k]) +s;\\ \quad \quad \mathbf{od};\\ \quad \quad C[i,j] := s -W[i] -V[j]; \\ \quad \quad \mathbf{if} \ \mathbf{not} \ p \\ \quad \quad \mathbf{then} \\ \quad \quad \qquad C[i,j] :=C[i,j] + A[i,n]*B[n,j]\\ \quad \quad \mathbf{fi}; \\ \quad \mathbf{od} \\ \mathbf{od} \\ \end{array} \right \} \ \left (\forall_{1\leq i \leq n},\forall_{1\leq j \leq n}\,C_{i,j} = \sum\limits_{k=1}^{n} A_{i,k} *B_{k,j} \right )[/math]

Dowody lematów

Dowód lematu 1

W dowodzie wykorzystujemy następującą własność programów for:\ niech napis [math]\omega(i)[/math] oznacza wyrażenie arytmetyczne (zmienna [math]i[/math] może, ale nie musi, w nim wystepować)
[math]\left \{ \begin{array}{l} s := 0\\ \mathbf{for}\ i:= 1\ \mathbf{to}\ n \\ \mathbf{do} \\ \quad s := \omega(i) +s \\ \mathbf{od} \end{array} \right \}\left (s =\sum\limits_{i=0}^{n} \omega(i) \right )[/math]
Pozostaje skorzystać z aksjomatu instrukcji przypisania

[math]\left (s =\sum\limits_{i=0}^{n} \omega(i) \right )\Rightarrow\{W[j] := s \}\left (W(j) =\sum\limits_{i=0}^{n} \omega(i) \right )[/math]

[math]\Box[/math]

Dowód Lematu 2

W tym dowodzie korzystamy z pomocniczej reguły wnioskowania
[math]\frac{\{\alpha_i \}_{1\leq i \leq n}}{} [/math] Dowody lematów 3 i 4 przebiegają podobnie.

Dowód lematu 5

Należy udowodnić [math](s = \sum\limits_{k=1}^{n \div 2} (A_{i,2k-1}+B_{2k,j})*(B_{2*k-1,j}+A_{i,2k})\Rightarrow(s-W[i]-V[j]=\sum\limits_{k=1}^{2(n \div 2)} A_{i,k}*B_{k,j})[/math]

Rozwińmy mnożenie i zastosujmy rozdzielność mnożenia wzgledem dodawania [math]\begin{array}{l} \sum\limits_{k=1}^{n \div 2} (A_{i,2k-1}+B_{2k,j})*(B_{2*k-1,j}+A_{i,2k}) \\ \quad = \sum\limits_{k=1}^{n \div 2} [A_{i,2k-1}*B_{2*k-1,j}+ A_{i,2k-1}*A_{i,2k}+ B_{2k,j}*B_{2k-1,j}+ B_{2k,j}*A_{i,2k} ] \\ \quad = \sum\limits_{k=1}^{n \div 2} A_{i,2k-1}*B_{2*k-1,j}+ \sum\limits_{k=1}^{n \div 2} A_{i,2k-1}*A_{i,2k}+ \sum\limits_{k=1}^{n \div 2} B_{2k,j}*B_{2k-1,j}+ \sum\limits_{=1}^{n \div 2} B_{2k,j}*A_{i,2k} \\ \end{array}[/math]

Skorzystamy z lematów 1 oraz 2

[math]\sum\limits_{k=1}^{n \div 2} (A_{i,2k-1}+B_{2k,j})*(B_{2*k-1,j}+A_{i,2k})-W[i]-V[j]= \sum\limits_{k=1}^{n \div 2} A_{i,2k-1}*B_{2*k-1,j}+ \sum\limits_{k=1}^{n \div 2} B_{2k,j}*A_{i,2k}[/math].
Wykorzystujemy przemienność mnożenia i łączność dodawania [math]\sum\limits_{k=1}^{n \div 2} A_{i,2k-1}*B_{2*k-1,j}+ \sum\limits_{k=1}^{n \div 2} B_{2k,j}*A_{i,2k}= \sum\limits_{k=1}^{2(n \div 2)} A_{i,k}*B_{k,j}[/math]

Dowód lematu 6

Trzeba wykazać, że [math](s= \sum\limits_{k=1}^{2(n \div 2)} A_{i,k}*B_{k,j} )\Rightarrow\left \{ \begin{array}{l} \mathbf{if} \ \mathbf{not} \ p \\ \mathbf{then} \\ \qquad C[i,j] :=C[i,j] + A[i,n]*B[n,j]\\ \mathbf{fi}; \end{array} \right \}(s= \sum\limits_{k=1}^{n} A_{i,k}*B_{k,j} )[/math] Pamiętamy, że p= (n mod 2 =0). Jeżeli n jest liczbą parzystą to [math]2(n \div 2)=n[/math].
[math]C_{i,j} = \sum\limits_{k=1}^{n} A_{i,k} *B_{k,j}[/math].

W przeciwnym przypadku (tzn.

gdy **not** [math]p[/math]) sumowanie zakonczyło się dla [math]k=n-1[/math]. Trzeba więc dodać wartość [math]A[i,n]*B[n,j][/math].

A można inaczej

To jest próba innego przedstawienia algorytmu Winograda.

Śmiało stosujmy symbole matematyczne

Programista może napisać $$x \leftarrow \sum\limits_{i=1}^{n}\,a_i$$ Program, w rodzaju, programu $tangle$ pozwol, stosując odpowiednie makro przekształcić tę linijkę w taki fragment kodu\

 ------------------------------------
 {int i;
  x:=0;
  for i:= 1 to n do x := x+a$_i$ od
  }
 ------------------------------------

Mamy do tego prawo ponieważ umiemy udowodnić, że

Po wykonaniu programu zachodzi równość\ $$\left \{ \begin{array}{l} \{int\ i; \\ \ x:=0;\\ \ \textbf{for }i:= 1\textbf{ to }n\textbf{ do }x := x+a_i\textbf{ od} \\ \ \}\\ \end{array} \right \}(x = \sum\limits_{i=1}^{n}\,a_i )$$

Podobnie, możemy stosować kwantyfikatory ograniczone. $$\bigwedge\limits_{i=1}^{n}\,\alpha(i)$$ ponieważ można dowieść

Po wykonaniu programu $S$ zachodzi formuła $\Sigma$\ $$\overbrace{\left \{ \begin{array}{l} \{\textbf{boolean}\ b;\ \textbf{int} \ i; \\ \ b:=\textsc{false};\\ \ \textbf{for }i:= 1\textbf{ to }n\textbf{ do }b := b \wedge \alpha(i)\textbf{ od} \\ \ \}\\ \end{array}\right \}} ^{\mathrm{program }S}\,(\overbrace{ \bigwedge\limits_{i=1}^{n}\,\alpha(i) )}^{\Sigma}$$

Łącząc te dwa fakty możemy dowieść, że

Po wykonaniu programu $S$ zachodzi formuła $\Sigma$\ $$\overbrace{\left \{ \begin{array}{l} \{ \textbf{int} \ i,\, j,\,k; \\ \quad \textbf{for }i:= 1\textbf{ to }n\textbf{ do } \\ \qquad \textbf{for }j:= 1\textbf{ to }n\textbf{ do } \\ \qquad \ \ s:=0; \\ \qquad \ \ \textbf{for }k:= 1\textbf{ to }n\textbf{ do } \\ \qquad \ \ \ \ \ s := s+ A_{i,k}*B_{k,j} \\ \qquad \ \ \textbf{od} \\ \qquad \ \ C_{i,j}:=s; \\ \qquad \textbf{od} \\ \quad \textbf{od} \\

\}\\  

\end{array}\right \}} ^{\mathrm{program }S}\,\overbrace{ \bigwedge\limits_{i=1}^{n}\,\bigwedge\limits_{j=1}^{n}\, (C_{i,j}=\sum\limits_{k=1}^{n}\,A_{i,k}*B_{k,j} )}^{\Sigma}$$

Dwie zewnętrzne instrukcje **for** obliczają ograniczone kwantyfikatory, pętla wewnętrzna oblicza wyrażenie $\sum_{k=1}^{n}\,A_{i,k}*B_{k,j} $ i zapisuje wynik w elemencie $C_{i,j}$ tablicy $C$.

Uwagi końcowe

​1. Zauważ, że algorytm ten pozwala mnożyć macierze liczb zespolonych, ... Zmieńmy nagłówek procedury\

• • unit** Winograd\_Generic: **procedure**( **type** T, **function**

add(x,y:T):T, **function** mult(x,y:T):T,\

• • function** subt(x,y:T):T, A, B: **array\_of array\_of** T, output C:
  • array\_of array\_of** T);\

i odpowiednio w treści procedury zapiszmy add(u,v) zamiast u+v, mult(u,v) zmiast u\*v, subt(u,v) zamiast u-v.,

Nasz warunek wstępny przybiera teraz inną postać\

• • Precondition**: Argumenty procedury Winograd\_Generic spełniaja

następujące warunki

1. pierwszy argument jest nazwą klasy,

2. kolejne trzy argumenty są nazwami funkcji, dwuargumentowych ze

   zbioru |T| obiektów typu T w zbiór |T|,

3. następne dwa argumenty to nazwy tablic kwadratowych jednakowego

   rozmiaru n x n,

4. ostatni argument także jest nazwą tablicy, tablica ta zostanie

   przekazana wywołującemu procedurę Winograd\_Generic,

5. zbiór |T| obiektów klasy T wraz z operacjami add, mult i subt jest

   *pierścieniem*.

• • Postcondition**: Algorytm zwraca tablicę C obiektów typu T, taką, że

dla każdych $i,j,\\ \ 1\leq i \leq n, 1 \leq j \leq n$ $$C_{i,j}= \add \limits_{k=0}^{n} (A_{i,k}\mult B_{k,j}) .$$

• • Poprzednia wersja dowodu lematu 1**\

Niech $j$ będzie liczbą naturalną taką, że $1\leq j \leq n$, niech $m=n \div 2$. Wykażemy, że po wykonaniu instrukcji ujętych w nawiasy zachodzi warunek $W_j=\sum\limits_{i=1}^{n \div 2} A_{j,2i-1}*A_{j,2i}$.\

• • Przypadek** $m=0$. Jeśli $m$ jest równe zero to na mocy aksjomatu

instrukcji for\

mamy równoważną jej formułę, $$\left \{ \begin{array}{l} \quad s:=0; \\ \quad W[j]:=s; \end{array} \right \} \left (W_j=\sum\limits_{k=1}^{n \div 2} A_{j,2i-1}*A_{j,2i}\right )$$ czyli $$\left \{

 s:=0;  
W[j]:=s; 

\right \} \left (W_j=\sum\limits_{k=1}^{n \div 2} A_{j,2i-1}*A_{j,2i}\right )$$ Jeśli dwukrotnie zastosujemy aksjomat instrukcji przypisania to otrzymamy najpierw $$\left \{ s:=0; \right \} \left (s=\sum\limits_{k=1}^{n \div 2} A_{j,2i-1}*A_{j,2i}\right )$$ a potem $$\left (0=\sum\limits_{k=1}^{n \div 2} A_{j,2i-1}*A_{j,2i}\right )$$ Równocześnie z własności sumy $ \Sigma$ wyrażenie po prawej znaku = ma wartość zero, co kończy analizę przypadku $m=0$ ponieważ wszystkie te formuły sa sobie równoważne.\

• • Krok indukcyjny** Załóżmy, że nasz lemat zachodzi dla wartości $m$

równej $k$. Wykażemy, że zachodzi on też dla $m=k+1$. Rozważmy formułę $$\left \{ \begin{array}{l} \quad s:=0; \\ \quad \mathbf{for}\ i:=1\ \mathbf{to}\ k+1 \\ \quad \mathbf{do} \\ \qquad s := A[j, 2*i-1] * A[j,2*i]+s; \\ \quad \mathbf{od} ; \\ \quad W[j]:=s; \end{array} \right \} \left (W_j=\sum\limits_{i=1}^{k+1} A_{j,2i-1}*A_{j,2i}\right )$$ Wykorzystamy inny aksjomat instrukcji for.

Z założenia indukcyjnego wiemy, że $$\left \{ \begin{array}{l} \quad s:=0; \\ \quad \mathbf{for}\ i:=1\ \mathbf{to}\ k \\ \quad \mathbf{do} \\ \qquad s := A[j, 2*i-1] * A[j,2*i]+s; \\ \quad \mathbf{od} ; \\ \end{array} \right \} \left (s=\sum\limits_{i=1}^{k } A_{j,2i-1}*A_{j,2i}\right )$$ Pozostaje do wykazania, że $$\left (s=\sum\limits_{i=1}^{k } A_{j,2i-1}*A_{j,2i}\right ) \Rightarrow \{i:=k+1; s:=A[j, 2*i-1] * A[j,2*i]+s \} (s=\sum\displaylimits_{i=1}^{k+1 } A_{j,2i-1}*A_{j,2i})$$ Dwukrotnie stosujemy aksjomat instrukcji przypisania, by otrzymać najpierw $$\left (s=\sum\limits_{i=1}^{k } A_{j,2i-1}*A_{j,2i}\right ) \Rightarrow \{i:=k+1 \} (A[j, 2*i-1] * A[j,2*i]+s=\sum\displaylimits_{i=1}^{k+1 } A_{j,2i-1}*A_{j,2i})$$ a później $$\left (s=\sum\limits_{i=1}^{k } A_{j,2i-1}*A_{j,2i}\right ) \Rightarrow (A[j, 2*(k+1)-1] * A[j,2*(k+1)]+s=\sum\displaylimits_{i=1}^{k+1 } A_{j,2i-1}*A_{j,2i})$$ Teraz już łatwo widać, że jeśli $s=\sum_{i=1}^{k } A_{j,2i-1}*A_{j,2i} $ to\ $A[j, 2*(k+1)-1] * A[j,2*(k+1)]+s=\sum\displaylimits_{i=1}^{k+1 } A_{j,2i-1}*A_{j,2i}$.\

Wynika to wprost z własności sumy. Wykazaliśmy prawdziwość implikacji $$\left (s=\sum\limits_{i=1}^{k } A_{j,2i-1}*A_{j,2i}\right ) \Rightarrow \{i:=k+1; s:=A[j, 2*i-1] * A[j,2*i]+s \} (s=\sum\displaylimits_{i=1}^{k+1 } A_{j,2i-1}*A_{j,2i})$$ Sorzystamy z reguły wnioskowania $$\frac{\phi \Rightarrow\psi}{M\phi \RightarrowM \psi}$$ by udowodnić $$\begin{array}{l} \left \{ \begin{array}{l}

s:=0; \\
\mathbf{for}\ i:=1\ \mathbf{to}\ k \\
\mathbf{do} \\

\ \ s := A[j, 2*i-1] * A[j,2*i]+s; \\

\mathbf{od} ; \\

\end{array} \right \} \\ (s=\sum\limits_{i=1}^{k } A_{j,2i-1}*A_{j,2i}) \end{array} \Rightarrow\begin{array}{l} \left \{ \begin{array}{l}

s:=0; \\
\mathbf{for}\ i:=1\ \mathbf{to}\ k \\
\mathbf{do} \\

\ \ s := A[j, 2*i-1] * A[j,2*i]+s; \\

\mathbf{od} ; \\
i:= k+1; \\
s:=A[j, 2*i-1] * A[j,2*i]+s; \\
\end{array}
\right \} \\

(s=\sum\limits_{i=1}^{k+1} A_{j,2i-1}*A_{j,2i}) \end{array}$$ Poprzednik tej implikacji odrywamy korzystając z reguły

• modus ponens* (tj. reguły odrywania). Program w formule następnika

implikacji upraszczamy stosując aksjomat instrukcji for. $$\begin{array}{l} \left \{ \begin{array}{l}

s:=0; \\
\mathbf{for}\ i:=1\ \mathbf{to}\ k+1 \\
\mathbf{do} \\

\ \ s := A[j, 2*i-1] * A[j,2*i]+s; \\

\mathbf{od} ; \\
\end{array}
\right \} \\

(s=\sum\limits_{i=1}^{k+1} A_{j,2i-1}*A_{j,2i}) \end{array}$$ Na tym możemy zakończyć (indukcyjny) dowód lematu 1.

$\Box$

[^1]: W loglanie’82 dwuwymiarowej tablicy możemy nadać kształt

   trójkatny, wstęgowy i oczywiście kształt kwadratowy