Reprezentáljuk az sorozatot és a függvényt egy-egy vektorral, amelyeket -val, illetve -vel jelölünk. A vektorok elemei -beli értékek. Kikötjük, hogy fixpontban a vektor . eleme éppen legyen (.), illetve a program biztosan elérje egy fixpontját (.).

Megállapíthatjuk, hogy a függvény helyen felvett értékének meghatározását megkönnyíti, ha ismerjük értékét bármely intervallum elemeivel indexelt részsorozatra.A lépésenkénti finomítás során alkalmazzuk a [[???Qui 87]] 3-2. pontjában és [[???Cha Mis 89]] 23. fejezetében ill. 24.9. pontjában bemutatott megoldási módszerek egyes elemeit. Megfigyelhetjük azt is, hogy egy részsorozatra kapott eredményt bármely, a részsorozatot tartalmazó részsorozatra vonatkozó eredmény meghatározásánál hasznosíthatjuk.

Ezen gondolatmenet alapján bővítsük a feladat állapoterét és finomítsuk a specifikációt. Vezessük be a függvényt oly módon, hogy jelentse értékét azon részsorozatára, amelynek utolsó eleme és hossza vagy éppen vagy az első eleme, ha . A kétdimenziós vektort azért vezetjük be, hogy segítségével a függvényt változóval helyettesítsük [[???Fót 83]]. A változók és kapcsolatát invariáns állítással írjuk le (.)-(.). Ugyanezt jelenítjük meg szemléletes alakban a . ábrán. Az ábrán szereplő vonalak a mátrix elemei között fennálló kapcsolatot írják le a . lemma alapján, azaz , ha . egy értéke legfeljebb hosszú kezdősorozatra.

Megadjuk a parciális függvény pontos definícióját:

Válasszuk a variánsfüggvényt a következőképpen:

ahol . , . A variánsfüggvény lényegében azt adja meg, hogy a mátrix egyes oszlopaiban összesen hány olyan elem van, amely nem azonos a függvény megfelelő helyen felvett értékével, illetve a vektor értéke hány helyen különbözik a függvény értékétől.

Bizonyítás: Fixpontban (.) szerint és , tehát a . lemma és (.) alapján . , így definícióját felhasználva , így a (.) invariáns tulajdonság és . lemma alkalmazásával igazoltuk, hogy a (.),(.),(.) feltételek együttesen finomítják a (.) feltételt.

Bizonyítás: Tudjuk, hogy , tehát = . Ha , akkor Ekkor asszociativitása miatt . Ha , akkor asszocivitása miatt .

Bizonyítás:

(.): A programban elemeire vonatkozó értékadás nincs. Így a (.) kezdeti feltétel egyben invariáns tulajdonság is.

(.): -ben: és , tehát a feltétel kezdetben teljesül. Az értékadások mindegyike együtt változtatja és értékét, ezért a (.) feltétel invariáns tulajdonság.

(.): , mert . , mert kezdetben .

Értékadás leggyengébb előfeltételének meghatározása után elég azt megmutatni, hogy

. Az első esetben: miatt , miatt . A második esetben: miatt , miatt . Mindkét esetben a . lemma alkalmazásával kapjuk a bizonyítandó állítást.

A . megj. szerint (.),(.) és (.) feltételeinek konjunkciója invariáns tulajdonság.

(.): (.),(.),(.) feltételeinek konjunkciójából következik, hogy , így: . A . lemma szerint elegendő belátni, hogy a program minden utasítására igaz, hogy vagy pontosan 1-gyel csökkenti a variáns függvényt, vagy nem okoz állapotváltozást. Ha a program nincs fixpontban, akkor van olyan és megfelelő értékadás, amely értékét növeli, vagy van olyan , hogy és még nem vette fel a értéket.

(.): a fixpont definíciója (.,. def.) alapján

Ebből szerinti indukcióval . -re: (.)-ből következik . Tegyük fel, hogy . ezért ellentmond az indukciós feltételnek. Így (.) az feltétellel helyettesíthető. Ha , akkor , különben (.) nem teljesül. Az indukciós feltétel szerint miatt , tehát: . Ez azonban ellentmond a kezdeti feltételnek. Tehát: . , különben (.) nem teljesül. . A (.) feltétel (invariánstulajdonság része) miatt . Ekkor (.) alapján: is.

Tegyük fel, hogy processzor párhzamosan hajtja végre a kapott programot. A vektorok . komponenseire vonatkozó értékadásokat az . logikai processzorra képezhetjük le. A variáns függvény definiciójából és a fenti bizonyításból közvetlenül adódik, hogy a program legkésőbb állapotváltozás után fixpontba jut. Az egyes logikai processzorok egymáshoz képest aszinkron és szinkron módon is működhetnek.

A program jelenlegi alakjában azonban még nem felel meg sem a finom atomicitás szabályának [[???And 91]](2.4), sem az osztott változós sémának [[???Cha Mis 89]], ezért további komponensekkel bővítjük az állapotteret. Célszerű a logaritmus függvényt is kitranszformálni.

Jelöljük gst(i)-vel , -vel , -vel értékét, ha az szükséges és ismert az . processzor számára és értéke elegendően nagy ahhoz, hogy a mátrix . oszlopának következő ( .) elemét meghatározhassuk (.). Vezessük be a logikai vátozókat a segédvektorok kezelésének megkönnyítésére. A segédvektorok . komponense lokális az . processzorra nézve. A transzformált program esetén teljesül majd, hogy minden egyes értékadásban pontosan legfeljebb egy olyan változóra (vektorkomponensre) hivatkozunk, amely nem lokális az . processzorra nézve.

A (.)-(.) specifikációt bővítjük az alábbi invariánsokkal:

Bizonyítás: az (.)-(.) invariánsok teljesülését a leggyengébb előfeltételek és kiszámolásával könnyen igazolhatjuk. A (.),(.)-(.) kikötések a transzformált programra is teljesülnek, mert a kikötésekben szereplő változókra vonatkozó értékadások a (.)-(.) invariáns állítások miatt ekvivalensek az eredetiekkel. A (.) fixpontfeltétel teljesüléséhez azt kell megmutatni, hogy ha a transzformált program fixpontba jut, akkor az eredeti is fixpontban van és a (.)-(.) feltételek teljesülnek.

A fenti megoldás egyszerűen implementálható szinkron, aszinkron arhitektúrán is, és osztott rendszerben is [[???Cha Mis 89]]. Szinkron arhitektúra esetén egyszerűsíthető a megoldás, kevesebb új változó bevezetésével is megoldható a feladat. Osztott rendszer esetén csak akkor hatékony ez a megoldás, ha elegendően sok, legalább csatorna áll rendelkezésre processzoronként és a kommunikációs költség alacsony. Ilyen architektúra pl. a hiperkocka [[???Qui 87]]. Adatcsatornás megoldásra mutat hatékony megoldást [[???Loy Vor 90]].

A tétel segítségével nagyon sok klasszikusnak számító feladatot oldhatunk meg egyszerű visszavezetéssel Az asszociatív függvény kiszámításának tételét eddig már kb. 200 egyetemi hallgató alkalmazta a gyakorlatban is sikeresen konrét feladatok megoldása során. PowerXplorer típusú, 16 processzoros, párhuzamos számítógépen, PVM-ben implementált aszinkron, párhuzamos, konkrét program futási ideje a felhasznált processzorok számának emelése mellett egyre rövidebb, ha a művelet elvégzéséhez szükséges processzoridő elegendően nagy a kommunikációs költségekhez képest. [[???Fót 86]]. Pl.: párhuzamos összeadás, emelkedő számsorozatok összehasonlítása [[???Cha Mis 89]], stb.