Winograda mnożenie macierzy
Przedstawiamy algorytm Winograda i dowód jego poprawności.
Spis treś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:
- umożliwić sygnalizację naruszenia warunku asercji w trakcie wykonywania programu,
- 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
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
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ń.
Dla każdego $j, 1\leq j \leq n$, i $m=n \div 2$ zachodzi $$\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 )$$
Kolejny lemat
$\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 )$
\ 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 nastepująca formuła algorytmiczna\ $$\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 )$$
\ Z prawdziwości lematów 1 i 2 wynika, że następująca formuła jest prawdziwa\ $\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 )$
Dowody lematów
Dowód lematu 1
W dowodzie wykorzystujemy następującą własność programów **for**:\ niech napis $\omega(i)$ oznacza wyrażenie arytmetyczne (zmienna $i$ może, ale nie musi, w nim wystepować) $$\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 )$$ Pozostaje skorzystać z aksjomatu instrukcji przypisania $$\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 )$$
$\Box$
Dowody lematów 2 i 3 przebiegają podobnie.
Dowód lematu 5
Należy udowodnić $$(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})$$ Rozwińmy mnożenie i zastosujmy rozdzielność mnożenia wzgledem dodawania $$\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}$$ Skorzystamy z lematów 1 oraz 2 $$\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}$$ Wykorzystujemy przemienność mnożenia i łączność dodawania $$\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}$$
Dowód lematu 6
Trzeba wykazać, że $$(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} )$$ Pamiętamy, że p= (n mod 2 =0). Jeżeli n jest liczbą parzystą to $2(n \div 2)=n$. $$C_{i,j} = \sum\limits_{k=1}^{n} A_{i,k} *B_{k,j}$$ W przeciwnym przypadku (tzn. gdy **not** $p$) sumowanie zakonczyło się dla $k=n-1$. Trzeba więc dodać wartość $A[i,n]*B[n,j]$\
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
