Hurok változat - Loop variant

Az informatikában a hurokváltozat egy olyan számítógépes program állapotterületén meghatározott matematikai függvény, amelynek értéke monoton csökken a (szigorú) jól megalapozott összefüggéshez képest egy ideig tartó ciklus iterációjával bizonyos invariáns körülmények között , ezáltal biztosítva annak megszűnését . Az a ciklusváltozat, amelynek tartománya a nem negatív egész számokra korlátozódik, kötött függvénynek is nevezik , mert ebben az esetben egy triviális felső korlátot biztosít a ciklus iterációinak számához, mielőtt befejeződik. Azonban egy ciklusváltozat lehet transzfinit , és így nem feltétlenül korlátozódik egész értékekre.

A jól megalapozott viszonyt az jellemzi, hogy a tartományának minden nem üres részhalmazából minimális elem létezik. A variáns létezése bizonyítja, hogy a számítógépes programban a while ciklus megalapozott leszármazással fejeződik be . A jól megalapozott kapcsolat alapvető tulajdonsága, hogy nincsenek végtelen leszálló láncai . Ezért egy variánst tartalmazó hurok véges számú iteráció után véget ér, amíg a teste minden alkalommal leáll.

A while ciklus , vagy általában egy számítógépes program, amely tartalmaz ciklus ciklusokat, teljesen helyesnek mondható, ha részben helyes és befejeződik.

Következtetési szabály a teljes helyesség érdekében

Annak érdekében, hogy hivatalosan kimondhassuk a következtetési szabályt a while ciklus lezárására, amit fentebb bemutatottunk, emlékezzünk arra, hogy a Floyd – Hoare logikában a while ciklus részleges helyességének kifejezésére vonatkozó szabály a következő:

{\ displaystyle {\ frac {\ {I \ land C \} \; S \; \ {I \}} {\ {I \} \; {\ mathtt {while}} \; C \; {\ mathtt { do}} \; S \; \ {I \ land \ l not C \}}},}

ahol $I$ jelentése az invariáns , C jelentése a feltétellel , és S jelentése a test a hurok. A teljes helyesség kifejezése érdekében ezt írjuk:

{\ displaystyle {\ frac {<{\ text {is megalapozott}}, \; [I \ land C \ land V = z] \; S \; [I \ land V <z]} {[I] \; {\ mathtt {while}} \; C \; {\ mathtt {do}} \; S \; [I \ land \ l not C]}},}

ahol ezenkívül V a változat , és egyezség szerint a kötetlen z szimbólumot univerzálisan számszerűsítettnek kell tekinteni .

Minden befejeződő ciklusnak van egy változata

A változat létezése azt jelenti, hogy a while ciklus véget ér. Meglepőnek tűnhet, de ez fordítva is igaz, amennyiben feltételezzük a választás axiómáját : minden egyes ciklusnak, amely befejeződik (tekintettel változatlanságára), van változata. Ennek bizonyítására tegyük fel, hogy a hurok

{\ displaystyle {\ mathtt {while}} \; C \; {\ mathtt {do}} \; S}

befejeződik, tekintettel az $I.$ invariánsra $,$ ahol megvan a teljes helyesség -állítás

{\ displaystyle [I \ land C] \; S \; [I].}

Tekintsük a „utódja” kapcsolatban az állapottér $Σ$ okozta a végrehajtás a nyilatkozat S egy állam megfelelő mind az invariáns $I$ és a feltétel C . Vagyis azt mondjuk, hogy egy $σ '$ állapot akkor és csak akkor $σ$ "utódja"

$I$ és C egyaránt igazak a $σ$ és a állapotban
$σ '$ az az állapot, amely az S utasítás $σ$ állapotban történő végrehajtásából adódik .

Megjegyezzük, hogy különben a ciklus nem fejeződik be. ${\ displaystyle \ sigma '\ neq \ sigma,}$

Ezután tekintsük az "utód" reláció reflexív, tranzitív lezárását. Hívja ezt iteráció : azt mondjuk, hogy egy állami $σ "$ egy hajtogat a $σ$ , ha bármelyik , vagy van egy véges lánc , úgyhogy és egy„utódja”az összes $I$ , ${\ displaystyle \ sigma '= \ sigma,}$ ${\ displaystyle \ sigma _ {0}, \ sigma _ {1}, \, \ dots \ ,, \ sigma _ {n}}$ ${\ displaystyle \ sigma _ {0} = \ sigma,}$ ${\ displaystyle \ sigma _ {n} = \ sigma '}$ ${\ displaystyle \ sigma _ {i+1}}$ ${\ displaystyle \ sigma _ {i};}$ ${\ displaystyle 0 \ leq i <n.}$

Megjegyezzük, hogy ha $σ$ és $σ '$ két különböző állapotok és $σ'$ jelentése hajtogat a $σ$ , akkor $σ$ nem lehet hajtogat a $σ ',$ az újra, különben a hurok nem tudnák megszüntetni. Más szóval, az iteráció antiszimmetrikus, és így részleges sorrend .

Most, mivel a while ciklus véges számú lépés után véget ér az $I$ változatlan helyzetben , és egyetlen állapotnak sincs utódja, hacsak nem $vagyok$ igaz ebben az állapotban, arra a következtetésre jutunk, hogy minden állapotnak csak véges sok iterációja van, minden csökkenő lánc az iteráció tekintetében csak véges sok különböző értékkel rendelkezik, és így nincs végtelen leszálló lánc , azaz a ciklus iteráció kielégíti a csökkenő lánc feltételt .

Ezért-feltételezve a választási axiómát-az eredetileg a ciklushoz definiált "utód" reláció jól megalapozott az állapottéren $Σ$ , mivel szigorú (nem reflexív) és az "iteráció" relációban található. Így ezen az állapottéren az azonosságfüggvény a while ciklus egyik változata, mivel kimutattuk, hogy az állapotnak szigorúan csökkentenie kell - „utódként” és „iterációként” - minden alkalommal, amikor az S testet végrehajtják, tekintettel az $I$ és $I$ változatra. a feltétel C .

Sőt, számolási érveléssel is kimutathatjuk, hogy bármelyik változat létezése magában foglalja egy existence ₁-es változat létezését , az első megszámlálhatatlan sorrendet , azaz

{\ displaystyle V: \ Sigma \ rightarrow \ omega _ {1}.}

Ennek az az oka, hogy a véges számítógépes program által véges számú lépésben elérhető állapotok gyűjteménye véges bemenetről megszámlálhatatlanul végtelen, és ω ₁ az összes jól rendezett típus felsorolása a megszámlálható halmazokon.

Gyakorlati szempontok

A gyakorlatban a ciklusváltozatokat gyakran nem negatív egész számoknak tekintik , vagy akár kötelezőnek is kell lenniük, de az a követelmény, hogy minden ciklusnak legyen egész számú változata, eltávolítja a programozási nyelv korlátlan iterációjának kifejező erejét . Hacsak egy ilyen (formailag ellenőrzött) nyelv nem tesz lehetővé végleges bizonyítást a lezárásról más, hasonlóan erős konstrukció, például rekurzív függvényhívás esetén , akkor már nem képes teljes μ-rekurzióra , hanem csak primitív rekurzióra . Ackermann függvénye egy kanonikus példa egy rekurzív függvényre, amely nem számítható ki egy ciklusban egész változattal .

Számítási bonyolultságukat tekintve azonban a nem primitív rekurzív funkciók messze túlmutatnak azon a területen, amit általában kezelhetőnek tartanak . Ha figyelembe vesszük még a hatványozás egyszerű esetét is primitív rekurzív függvényként, és azt, hogy a primitív rekurzív függvények összetétele primitív rekurzív, elkezdhetjük látni, hogy milyen gyorsan tud növekedni egy primitív rekurzív függvény. És minden olyan függvény, amelyet egy Turing -gép kiszámíthat egy primitív rekurzív függvény által korlátozott futási idő alatt, maga is primitív rekurzív. Így nehéz elképzelni a teljes μ -rekurzió gyakorlati alkalmazását, ahol a primitív rekurzió nem fog működni, különösen azért, mert az előbbit az utóbbi rendkívül hosszú futási időkig képes szimulálni.

És mindenesetre, Kurt Gödel első hiányos tétele és a leállási probléma azt jelenti, hogy vannak olyan ciklusok, amelyek mindig véget érnek, de nem bizonyíthatók; így elkerülhetetlen, hogy a felmondás formális igazolásának bármely követelménye csökkentse a programozási nyelv kifejezőerejét. Bár megmutattuk, hogy minden befejeződő ciklusnak van változata, ez nem jelenti azt, hogy a ciklus iteráció megalapozottsága bizonyítható.

Példa

Íme egy példa a C -szerű pszeudokódban egy egész variánsra, amelyet a while ciklusban fennmaradó iterációk számának valamilyen felső korlátjából számítottunk ki. A C azonban megengedi a mellékhatásokat a kifejezések értékelésében, ami elfogadhatatlan egy számítógépes program hivatalos ellenőrzése szempontjából.

/** condition-variable, which is changed in procedure S() **/
bool C;
/** function, which computes a loop iteration bound without side effects **/
inline unsigned int getBound();

/** body of loop must not alter V **/ 
inline void S(); 

int main() {
    unsigned int V = getBound(); /* set variant equal to bound */
    assert(I); /* loop invariant */
    while (C) {
        assert(V > 0); /* this assertion is the variant's raison d'être (reason of existence) */
        S(); /* call the body */
        V = min(getBound(), V - 1); /* variant must decrease by at least one */
    };
    assert(I && !C); /* invariant is still true and condition is false */

    return 0;
};

Miért érdemes egy nem egész változatot is figyelembe venni?

Miért érdemes egy nem egész vagy transzfinit változatot is figyelembe venni? Ez a kérdés azért merült fel, mert minden gyakorlati esetben, amikor be akarjuk bizonyítani, hogy egy program leáll, azt is be akarjuk bizonyítani, hogy ésszerű időn belül leáll. Legalább két lehetőség van:

A ciklus iterációinak felső korlátja feltétele lehet a lezárás bizonyítása. Kívánatos lehet külön -külön (vagy fokozatosan) bizonyítani a
- részleges helyesség,
- megszüntetés, és
- futási idő.
Általánosság: a transzfinit változatok figyelembe vétele lehetővé teszi, hogy egy bizonyos időtartamú ciklus minden lehetséges bizonyítékát egy variáns létezése szempontjából tekintsük.

Languages

In other projects

Hurok változat - Loop variant

Tartalom

Következtetési szabály a teljes helyesség érdekében

Minden befejeződő ciklusnak van egy változata

Gyakorlati szempontok

Példa

Miért érdemes egy nem egész változatot is figyelembe venni?

Lásd még

Hivatkozások