Tekst źródłowy strony Winograda mnożenie macierzy

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:

#  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<br />

'''Lemat 1'''<br />
Dla każdego <math>j, 1\leq j \leq n</math>,\ i\ <math>m=n \div 2</math> zachodzi <br />
<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<br />

'''Lemat 2'''<br />
Dla <math>m=n \div 2</math> zachodzi<br />
<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ń.<br />

'''Lemat 3'''<br />
Dla każdego <math>j, 1\leq j \leq n</math>, i <math>m=n \div 2</math> zachodzi<br />
<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<br />

'''Lemat 4'''<br />
<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\<br />

'''Lemat 5'''<br />
<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\<br />

'''Lemat 6'''<br />
<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ć)<br />
<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><br />
Pozostaje
skorzystać z aksjomatu instrukcji przypisania<br />

<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<br />
<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><br />

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><br />
 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>.<br />
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>.<br />
<math>C_{i,j} = 
\sum\limits_{k=1}^{n} A_{i,k} *B_{k,j}</math>.<br />
 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