Kikötjük, hogy bármely fixpontban az rendezett halmaz -es értéke éppen legyen (.), ahol az változó kezdeti értéke (.). Megköveteljük, hogy a program biztosan elérje valamelyik fixpontját (.).

, .

ahol elemenként feldolgozható.

Feltesszük, hogy és invariánsA halmazkivonás komponensenként értendő. módon az teljesen diszjunkt felbontása és -re már ismerjük az függvény értékét. Felhasználva az elemenként feldolgozható függvények azon tulajdonságát, hogy értékük az argumentum teljesen diszjunkt felbontása esetén komponensenkénti diszjunkt unióval meghatározható a (.)-(.) specifikáció fixpont feltételét az feltétellel helyettesíthetjük.

Biz.: A . lemma alapján. A bizonyításhoz szükséges matematikai meggondolások indoklása megtalálható [[???Fót 83]]-ban.

Definiáljuk az függvényt a következőképpen: ,

ahol az számok egy permutációja.

Jelöljük a és halmazok unióját -vel, ha . Hasonlóan, jelölje a halmazt, ha . A művelet egy nemdeterminisztikus feltételes értékadás, amely -nek értékül adja egy tetszőlegesen kiválasztott elemét, ha nem üres.

Biz.: A bizonyításhoz szükséges matematikai meggondolások indoklása megtalálható [[???Fót 83]]-ban.

Reprezentáljuk a továbbiakban az halmazokat olyan szigorúan növekvő monoton sorozatok formájában, amelyeknek elemei és részsorozatai közvetlenül hozzáférhetőek az indexek megadásávalFüggvény típusú reprezentációt választunk [[???Fót 86]].. első, legkisebb elemét jelölje . hosszát -mal jelöljük. -vel jelöljük azon részsorozatát, amely a indexű elemeket tartalmazza.

Feltételezve, hogy processzor áll rendelkezésünkre, felbontjuk -et páronként teljesen diszjunkt részre. A felbontás kiegyensúlyozott, ha a legnagyobb és a legkisebb rész méretének különbsége legfeljebb 1. Kiegyensúlyozott felbontás esetén processzor segítségével kb. -szeresére gyorsíthatjuk kiszámítását. Az egyes részekre kiszámított részeredményeket végül komponensenkénti diszjunkt unióval egyesíthetjük (. def.).

Megadjuk a páronként diszjunkt felbontás feladatának formális specifikációját:

, ,

ahol igaz, ha az mátrix páronként teljesen diszjunkt felbontását definiálja, azaz: .

Ahhoz, hogy egy páronként teljesen diszjunkt felbontásról eldönthessük, hogy kiegyensúlyozott-e, meg kell határoznunk nem feltétlenül diszjunkt halmazok uniójának számosságát. Nem diszjunkt halmazok uniója azonban elemenként feldolgozható függvény. Ha az unió elemeinek számát az unió elemenkénti feldolgozással történő kiszámítása útján határozzuk meg, akkor önmagában annak eldöntése, hogy a felbontás kiegyensúlyozott-e ugyanannyi számítási lépést igényel, mint a teljes elemenkénti feldolgozás. Ez a módszer nyilvánvalóan nem vezet eredményre. Nyitott kérdés, hogy más úton lehetséges-e (esetleg ) processzorral páronként teljesen diszjunkt és egyben kiegyensúlyozott felbontást hatékonyan előállítani.

A továbbiakban megmutatjuk hogyan lehet hatékonyan páronként teljesen diszjunkt felbontást előállítani anélkül, hogy a kiegyensúlyozottságot garantálnánk A [[???Fót Hor Kozs 95]] cikkben egy módszert mutattunk arra, hogy milyen módon oldható meg más úton az a feladat, hogy az egyes processzorok között a feladatmegosztást kiegyensúlyozzuk.. A felbontást a legnagyobb komponens egyenlő részekre osztásával definiáljuk, azaz ezen egyetlen komponens felosztását terjesztjük ki fokozatosan a többire oly módon, hogy a teljesen diszjunkt felbontás létrejöjjön.

Tegyük fel, hogy az legnagyobb elemszámú komponenseA legnagyobb elemszámú komponens megtalálása visszavezethető egy maximumkeresésre, amely asszociatív művelet. A . tétel szerint ezt a feladatot lépésben megoldhatjuk. A későbbiekben látjuk majd, hogy lépés elhanyagolható a megoldáshoz szükséges összes állapotváltozáshoz képest.. Bevezetjük a vektort, amely tájékoztat arról, hogy a páronként teljesen diszjunkt felbontás mely összetevőit ismerjük. Ezen összetevők együttesét részlegesen meghatározott páronként teljesen diszjunkt felbontásának nevezzük.

. Jelöljük -vel, ha az mátrix elemeivel és a vektor értékeivel meghatározott, az osztáspontokkal megadott, részleges felbontás megfelel a páronként teljesen diszjunkt felbontás követelményeinek, azaz: .

A részlegesen meghatározott, páronként teljesen diszjunkt felbontás fogalmának bevezetésével fionomíthatjuk a (.)-(.) specifikációt.

Biz.: A korábbiakhoz hasonlóan a . lemma alapján.

Válasszuk a variáns függvényt a következőképpen: .

A variáns függvény értéke akkor csökken, ha a vektor elemeinek értéke nő. Ez azt jelenti, hogy a részlegesen meghatározott felbontást ki kell terjeszteni, az mátrix további elemei értékének meghatározásával.

Az (.) invariáns, igaz marad, ha -t azon -beli elem indexének választjuk, amely elem kisebb vagy egyenlő -nél, és amely elemre rákövetkező elem -ben nagyobb, mint . Jelöljük a logikai függvényt -vel. A (.) feltételt a

feltétellel finomítjuk.

Mivel monoton, a (.) feltétellel definiált feladat visszavezethető szekvenciális logaritmikus keresésre [[???Fót 83]].

Általánosítsuk a (.) feltétellel definiált feladatot. Legyen egy rendezett halmaz, az egész számok nem üres intervalluma és monoton növő függvény. Adott egy érték. Keressük meg azt egész számot, amelyre a tulajdonság teljesül, ahol .

Mivel az intervallum nem üres, ezért biztosan létezik olyan . Finomítsuk a specifikációt egy invariáns és egy variáns függvény bevezetésével. Az állapotteret két új komponsnes bevetetésével bővítjük. .

Válasszuk a variáns függvényt a következőképpen: .

Bizonyítás: A bizonyítás a [[???Fót 83]]-ban adott bizonyítás alapján elvégezhető.

Alkalmazzuk a logaritmikus keresés programját (. prg.) sorozatra (szuperpozíció), egyenként -szer (explicit szekvencializálás [[???Lam Sin 79]]). Ezzel a módszerrel meghatározhatjuk az mátrix értékét úgy, hogy az egy páronként teljesen diszjunkt felbontását definiálja, azaz megkapjuk azt a programot, amely megfelel a (.)-(.) specifikációnak. A megoldás helyességét a szuperpozíció és a szekvencia levezetési szabályára hivatkozva igazolhatjuk. folyamat szekvenciáját egyszerű transzformációval ciklussá alakítjuk.

Az elemenként feldolgozható függvény értékét a páronként teljesen diszjunkt felbontással kapott szeletekre függetlenül, párhuzamosan meghatározhatjuk. A teljes eredményt a szeletekre kapott eredmény diszjunkt uniójaként állítjuk elő (. def.).

Tegyük fel, hogy értékét ismerjük mind az páronként teljesen diszjunkt szeletére. Jelöljük a függvényértékeket rendre -nel, ahol . Tudjuk, hogy . Tetszőleges -re: . Ahhoz, hogy megkapjuk az értéket, ki kell számítanunk diszjunkt halmaz unióját minden -re. Tegyük fel, hogy a halmazok sorozatok formájában adottak, és a sorozatok elemei indexeik alapján elérhetőek. Az halmazok unióját, mint a sorozatok konkatenációját állítjuk elő. elemeit azon részsorozatába kell bemásolnunk, amelyik kezdőindexe , azaz meg kell határoznunk a sorozatok hosszából kapott szerint rendezett sorozat minden kezdőszeletének összegét. Az összeadás asszociatív művelet, így a feladat megoldható a . absztrakt program felhasználásával.

A fenti megoldás egyszerűen implementálható szinkron, aszinkron arhitektúrán is, és osztott rendszerben is [[???Cha Mis 89]]. Osztott rendszer esetén csak akkor hatékony ez a megoldás, ha elegendően sok, (logikai) csatorna áll rendelkezésre processzoronként és a kommunikációs költség alacsony. Tegyük fel, hogy processzoron implementáljuk az absztrakt programot, és sokkal nagyobb, mint . A párhuzamos teljesen diszjunkt felbontás eredményét processzor cseréli ki egymás között, hogy az egyes szeletekre megkezdődhessen az elemenkénti feldolgozás. Az elemenkénti feldolgozás eredményét ismét processzor cseréli ki egymás közöttEgyes párhuzamos gépek processzorai számára a filerendszer párhuzamosan is elérhető. Ebben az esetben a kommunikációs igény kisebb.. A kommunikációs lépések száma tehát processzoronként. A teljesen diszjunkt felbontáshoz szükséges lépések száma , a szelet elemenkénti feldolgozásához szükséges lépésszám: (kiegyensúlyozott felbontás esetén), a részeredmények konkatenációjához pedig lépés szükséges a részletösszegek kiszámítása miatt. Kevés változó ( ) és sok adat ( ) és kiegyensúlyozott felbontás esetén a függvényérték meghatározásának jellemző költsége: .

Elemenként feldolgoható függvény értékének kiszámítására vezethető vissza rendezett sorozatok összefésülése, halmazok uniója, az időszerűsítés [[???Fót Nyé 90]], Conway problémája [[???Cha Mis 89]] és még számos feladat.