Winograda mnożenie macierzy - Historia wersji

AndrzejSalwicki: /* Dowód lematu 1 */

2015-11-05T20:15:35Z

‎Dowód lematu 1

AndrzejSalwicki: /* Dowód poprawności */

2015-11-04T19:22:54Z

‎Dowód poprawności

AndrzejSalwicki: /* Dowód poprawności */

2015-11-04T16:19:37Z

‎Dowód poprawności

AndrzejSalwicki: /* Dowód poprawności */

2015-11-04T16:11:28Z

‎Dowód poprawności

AndrzejSalwicki: /* Dowód poprawności */

2015-11-04T16:09:09Z

‎Dowód poprawności

AndrzejSalwicki: /* Dowód poprawności */

2015-11-04T16:04:17Z

‎Dowód poprawności

AndrzejSalwicki: /* Dowód poprawności */

2015-11-04T16:01:28Z

‎Dowód poprawności

AndrzejSalwicki: /* Dowód poprawności */

2015-11-04T16:00:15Z

‎Dowód poprawności

AndrzejSalwicki o 15:50, 4 lis 2015

2015-11-04T15:50:22Z

AndrzejSalwicki: Utworzono nową stronę "Przedstawiamy algorytm Winograda i dowód jego poprawności. Wprowadzenie ============ Algorytm Winograda może być stosowany do obliczania iloczynu macierzy kwadrato..."

2015-11-04T14:28:02Z

Utworzono nową stronę "Przedstawiamy algorytm Winograda i dowód jego poprawności. Wprowadzenie ============ Algorytm Winograda może być stosowany do obliczania iloczynu macierzy kwadrato..."

Nowa strona

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ę
$$\mathrm{Precondition} \Rightarrow [\mathrm{Algorytm\ Winograda}]\mathrm{Postcondition}$$
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,

2. 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 $j, 1\leq j \leq n$, i $m=n \div 2$ zachodzi $$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 )$$

lub to samo spostrzeżenie zapisane nieco inaczej

Dla $m=n \div 2$ zachodzi $$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 )$$

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

@@ Linia 241: / Linia 241: @@
-W dowodzie wykorzystujemy następującą własność programów **for**:\
+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 />
@@ Linia 253: / Linia 253: @@
 \right \}\left (s =\sum\limits_{i=0}^{n} \omega(i)  \right )</math><br />
 Pozostaje
-skorzystać z aksjomatu instrukcji przypisania
+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 ===
-Dowody lematów 2 i 3 przebiegają podobnie.
+W tym dowodzie korzystamy z pomocniczej reguły wnioskowania<br />
 === Dowód lematu 5 ===

@@ Linia 168: / Linia 168: @@
 '''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 \{
+<math>\left \{
 \begin{array}{l}
 \quad s:=0; \\
@@ Linia 193: / Linia 193: @@
+\
-Przy założeniu, że tablice A i B są macierzami kwadratowymi rozmiaru n x
+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
-n i że zachodzą lematy 1 oraz 2, prawdziwa jest nastepująca formuła
 algorytmiczna\<br />
@@ Linia 234: / Linia 233: @@
 \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>
+\sum\limits_{k=1}^{n} A_{i,k} *B_{k,j}  \right )</math>
 == Dowody lematów ==
@@ Linia 243: / Linia 242: @@
 W dowodzie wykorzystujemy następującą własność programów **for**:\
-niech napis $\omega(i)$ oznacza wyrażenie arytmetyczne (zmienna $i$
+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}
@@ Linia 255: / Linia 254: @@
 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 )$$
+<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>
-$\Box$
+<math>\Box</math>
 Dowody lematów 2 i 3 przebiegają podobnie.
@@ Linia 265: / Linia 264: @@
 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})$$
+<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
-$$\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}) \\
+<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}+
@@ Linia 276: / Linia 276: @@
 \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
+\end{array}</math><br />
-$$\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]=
+ Skorzystamy z lematów 1 oraz 2
   \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
+\sum\limits_{k=1}^{n \div 2} B_{2k,j}*A_{i,2k}</math>.<br />
 przemienność mnożenia i łączność dodawania
-$$\sum\limits_{k=1}^{n \div 2} A_{i,2k-1}*B_{2*k-1,j}+
+<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}$$
+  \sum\limits_{k=1}^{2(n \div 2)} A_{i,k}*B_{k,j}</math>
 === Dowód lematu 6 ===
@@ Linia 289: / Linia 291: @@
 Trzeba wykazać, że
-$$(s= \sum\limits_{k=1}^{2(n \div 2)} A_{i,k}*B_{k,j}  )\Rightarrow\left \{ \begin{array}{l}
+<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} )$$
+\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
-$2(n \div 2)=n$. $$C_{i,j} =
+<math>2(n \div 2)=n</math>.<br />
-\sum\limits_{k=1}^{n} A_{i,k} *B_{k,j}$$ W przeciwnym przypadku (tzn.
+<math>C_{i,j} =
-gdy **not** $p$) sumowanie zakonczyło się dla $k=n-1$. Trzeba więc dodać
+\sum\limits_{k=1}^{n} A_{i,k} *B_{k,j}</math>.<br />
-wartość $A[i,n]*B[n,j]$\
+ W przeciwnym przypadku (tzn.
 == A można inaczej ==

@@ Linia 128: / Linia 128: @@
 gdy program zawiera błędy.\
-Natomiast asercje możemy zastąpić lematami i udowodnić je
+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 />
@@ Linia 143: / Linia 144: @@
 \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
+lub to samo spostrzeżenie zapisane nieco inaczej<br />
 '''Lemat 2'''<br />
 Dla <math>m=n \div 2</math> zachodzi<br />
@@ Linia 162: / Linia 164: @@
 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ń.
+Instrukcja '''for''' ma jeszcze wiele innych zastosowań.<br />
 '''Lemat 3'''<br />
 Dla każdego $j, 1\leq j \leq n$, i $m=n \div 2$ zachodzi $$\left \{
@@ Linia 176: / Linia 179: @@
 \left (V_j=\sum\limits_{i=1}^{n \div 2} B_{2i-1,j}*B_{2i,j}\right )$$
-Kolejny lemat
+Kolejny lemat<br />
 '''Lemat 4'''<br />
 $\forall_{1\leq i \leq n},\forall_{1\leq j \leq n}$\
@@ Linia 190: / Linia 194: @@
 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\
+algorytmiczna\<br />
 '''Lemat 5'''<br />
 $$\forall_{1\leq i \leq n},\forall_{1\leq j \leq n}
@@ Linia 205: / Linia 210: @@
+\
 Z prawdziwości lematów 1 i 2 wynika, że następująca formuła jest
-prawdziwa\
+prawdziwa\<br />
 '''Lemat 6'''<br />
-$\left \{ \begin{array}{l}
+<math>\left \{ \begin{array}{l}
 \mathbf{for} \ i:=1\ to \ n \\
 \mathbf{do} \\
@@ Linia 227: / Linia 233: @@
 \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 )$
+\sum\limits_{k=1}^{n} A_{i,k} *B_{k,j}  \right )/math>
 == Dowody lematów ==

@@ Linia 129: / Linia 129: @@
 Natomiast asercje możemy zastąpić lematami i udowodnić je
+'''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 \{
@@ Linia 144: / Linia 144: @@
 lub to samo spostrzeżenie zapisane nieco inaczej
+'''Lemat 2'''<br />
 Dla <math>m=n \div 2</math> zachodzi<br />
 <math>M: \left \{
@@ Linia 163: / Linia 163: @@
 kwantyfikator ograniczony, a wewnętrzna instrukcja '''for''' oblicza sumę.
 Instrukcja '''for''' ma jeszcze wiele innych zastosowań.
+'''Lemat 3'''<br />
 Dla każdego $j, 1\leq j \leq n$, i $m=n \div 2$ zachodzi $$\left \{
 \begin{array}{l}
@@ Linia 177: / Linia 177: @@
 Kolejny lemat
+'''Lemat 4'''<br />
 $\forall_{1\leq i \leq n},\forall_{1\leq j \leq n}$\
 $\left \{ \begin{array}{l}    s:= 0; \\
@@ Linia 191: / Linia 191: @@
 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; \\
@@ Linia 205: / Linia 206: @@
 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 \\

@@ Linia 146: / Linia 146: @@
 Dla <math>m=n \div 2</math> zachodzi<br />
- <math>M: \left \{
+<math>M: \left \{
 \begin{array}{l}
 \textbf{for }j:=1\textbf{ to } n \textbf{ do} \\

@@ Linia 115: / Linia 115: @@
 Do algorytmu Winograd wstawiliśmy asercje. Mają one za zadanie:
-.  umożliwić sygnalizację naruszenia warunku asercji w trakcie
+#  umożliwić sygnalizację naruszenia warunku asercji w trakcie wykonywania programu,
-    wykonywania programu,
-.  ułatwić argumentację na rzecz tezy o poprawności algorytmu.
+#  ułatwić argumentację na rzecz tezy o poprawności algorytmu.
 W tym przypadku trudno mówić o dynamiczej weryfikacji: ażeby sprawdzić
@@ Linia 131: / Linia 130: @@
 Natomiast asercje możemy zastąpić lematami i udowodnić je
-Dla każdego <math>j, 1\leq j \leq n$,\ i\ $m=n \div 2</math> zachodzi
+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}
@@ Linia 146: / Linia 145: @@
 lub to samo spostrzeżenie zapisane nieco inaczej
-Dla $m=n \div 2$ zachodzi $$M: \left \{
+Dla <math>m=n \div 2</math> zachodzi<br />
 \begin{array}{l}
 \textbf{for }j:=1\textbf{ to } n \textbf{ do} \\
@@ Linia 158: / Linia 158: @@
 \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 )$$
+\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
+Zwróć uwagę na to, że zewnętrzna instrukcja '''for''' oblicza
-kwantyfikator ograniczony, a wewnętrzna instrukcja **for** oblicza sumę.
+kwantyfikator ograniczony, a wewnętrzna instrukcja '''for''' oblicza sumę.
-Instrukcja **for** ma jeszcze wiele innych zastosowań.
+Instrukcja '''for''' ma jeszcze wiele innych zastosowań.
 Dla każdego $j, 1\leq j \leq n$, i $m=n \div 2$ zachodzi $$\left \{
@@ Linia 227: / Linia 227: @@
 \sum\limits_{k=1}^{n} A_{i,k} *B_{k,j}  \right )$
-Dowody lematów
+== Dowody lematów ==
-==============
 W dowodzie wykorzystujemy następującą własność programów **for**:\
@@ Linia 250: / Linia 250: @@
 Dowody lematów 2 i 3 przebiegają podobnie.
-Dowód lematu 5
+=== Dowód lematu 5 ===
---------------
 Należy udowodnić
@@ Linia 274: / Linia 274: @@
   \sum\limits_{k=1}^{2(n \div 2)} A_{i,k}*B_{k,j}$$
-Dowód lematu 6
+=== Dowód lematu 6 ===
---------------
 Trzeba wykazać, że
@@ Linia 290: / Linia 290: @@
 wartość $A[i,n]*B[n,j]$\
-A można inaczej
+== A można inaczej ==
-===============
 To jest próba innego przedstawienia algorytmu Winograda.
-Śmiało stosujmy symbole matematyczne
+=== Śmiało stosujmy symbole matematyczne ===
-------------------------------------
 Programista może napisać $$x \leftarrow \sum\limits_{i=1}^{n}\,a_i$$
@@ Linia 351: / Linia 351: @@
 zapisuje wynik w elemencie $C_{i,j}$ tablicy $C$.
-Uwagi końcowe
+== Uwagi końcowe ==
-=============
 . Zauważ, że algorytm ten pozwala mnożyć macierze liczb zespolonych,

@@ Linia 1: / Linia 1: @@
 Przedstawiamy algorytm Winograda i dowód jego poprawności.
-Wprowadzenie
+== Wprowadzenie ==
-============
 Algorytm Winograda może być stosowany do obliczania iloczynu macierzy
@@ Linia 18: / Linia 18: @@
 Zapraszam do czytania, zwłaszcza rozdziału Dowód poprawności.
-Algorytm
+== Algorytm ==
-========
 W tym rozdziale pojawiają się dwa warunki:
@@ Linia 44: / Linia 44: @@
 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
+względem warunku początkowego ''Precondition'' i warunku końcowego
-**Postcondition**.
+''Postcondition''.
 [1] $\mathbf{signal}\  Niezgoda;$
@@ Linia 90: / Linia 90: @@
 $\mathbf{end}\ Winograd;$
-Dowód poprawności
+== Dowód poprawności ==
-=================
 Naszym zadaniem jest wykazać nastepującą implikację
-$$\mathrm{Precondition} \Rightarrow [\mathrm{Algorytm\ Winograda}]\mathrm{Postcondition}$$
+<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ą
@@ Linia 131: / Linia 131: @@
 Natomiast asercje możemy zastąpić lematami i udowodnić je
-Dla każdego $j, 1\leq j \leq n$, i $m=n \div 2$ zachodzi $$K: \left \{
+Dla każdego <math>j, 1\leq j \leq n$,\ i\ $m=n \div 2</math> zachodzi
 \begin{array}{l}
 \quad s:=0; \\
@@ Linia 141: / Linia 142: @@
 \end{array}
 \right \}
-\left (W_j=\sum\limits_{i=1}^{n \div 2} A_{j,2i-1}*A_{j,2i}\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