Döngü varyantı - Loop variant

Olarak bilgisayar biliminin , bir döngü varyantı a, matematiksel fonksiyon tanımlanan durum alanı değeri monoton bir şekilde bir (katı) ile ilgili olarak daha düşük olan bir bilgisayar programı iyi kurulmuş ilişki bir yineleme ile ise döngü bazı altında değişmeyen koşullar , bu şekilde sağlanması onun sona ermesi . Menzili negatif olmayan tamsayılarla sınırlı olan bir döngü varyantı, aynı zamanda bir sınır işlevi olarak da bilinir , çünkü bu durumda, bir döngünün sonlanmadan önce yineleme sayısı üzerinde önemsiz bir üst sınır sağlar. Bununla birlikte, bir döngü varyantı transfinite olabilir ve bu nedenle tamsayı değerleriyle sınırlandırılması zorunlu değildir.

Sağlam temelli bir ilişki, etki alanının boş olmayan her alt kümesinin minimal bir öğesinin varlığı ile karakterize edilir. Bir varyantın varlığı, bir bilgisayar programında bir while döngüsünün sağlam temelli bir inişle sonlandırıldığını kanıtlar . Sağlam temelli bir ilişkinin temel özelliği, sonsuz azalan zincirlere sahip olmamasıdır . Bu nedenle, bir değişkene sahip bir döngü, gövdesi her seferinde sona erdiği sürece, sınırlı sayıda yinelemeden sonra sona erecektir.

Bir while döngüsü veya daha genel olarak, while döngüleri içerebilen bir bilgisayar programı , kısmen doğruysa ve sona ererse tamamen doğru olduğu söylenir .

Toplam doğruluk için çıkarım kuralı

Yukarıda gösterdiğimiz bir while döngüsünün sonlandırılması için çıkarım kuralını resmi olarak belirtmek için Floyd-Hoare mantığında bir while döngüsünün kısmi doğruluğunu ifade etme kuralının şöyle olduğunu hatırlayın :

${\displaystyle {\frac {\{I\land C\}\;S\;\{I\}}{\{I\}\;{\mathtt {while}}\;C\;{\mathtt { do}}\;S\;\{I\land \lnot C\}}},}$

burada I olan değişmez , Cı olduğu durumu ve S olan vücut döngü. Tam doğruluğu ifade etmek için bunun yerine şunu yazıyoruz:

${\displaystyle {\frac {<{\text{ sağlam bir temele sahiptir}},\;[I\land C\land V=z]\;S\;[I\land V<z]}{[I] \;{\mattt {while}}\;C\;{\mathtt {do}}\;S\;[I\land \lnot C]}},}$

burada, ek olarak, V olan varyant , ve geleneksel olarak bağlanmamış sembol z için alınır evrensel miktarı .

Sonlandırılan her döngünün bir varyantı vardır

Bir değişkenin varlığı, bir while döngüsünün sona erdiği anlamına gelir. Şaşırtıcı görünebilir, ancak seçim aksiyomunu varsaydığımız sürece tersi de doğrudur : sona eren her while döngüsünün (değişmezi verildiğinde) bir varyantı vardır. Bunu kanıtlamak için, döngünün

${\ Displaystyle {\ Mathtt {Süre}}\;C\;{\Mathtt {do}}\;S}$

toplam doğruluk iddiasına sahip olduğumuz değişmez I verildiğinde sona erer

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

Hem I değişmezini hem de C koşulunu sağlayan bir durumdan S ifadesinin yürütülmesiyle indüklenen durum uzayı Σ üzerindeki "ardıl" ilişkisini düşünün . Yani, biz bir devlet demek olduğunu σ ' bir "halef" dir σ ancak ve ancak

• I ve C her ikisi de σ durumunda doğrudur ve
• σ ' ifadesinin yürütülmesi sonuçları durumudur S durum içinde σ .

Aksi takdirde döngünün sonlandırılamayacağını not ediyoruz . ${\displaystyle \sigma '\neq \sigma ,}$

Ardından, "halef" ilişkisinin dönüşlü, geçişli kapanışını düşünün. Bu Çağrı yineleme : Biz bir devlet olduğunu söylemek σ ' bir olan yinelerler ait σ ya eğer ya da orada sonlu zinciridir şekilde ve bir "halef" dir herkes için 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.}$

Biz eğer dikkat σ ve σ ' iki ayrı devletler vardır ve σ' bir yinelerler olan σ ardından σ bir yinelerler olamaz , 'σ aksi döngü sona erdirmek başarısız olur, tekrar için. Başka bir deyişle, yineleme antisimetriktir ve dolayısıyla kısmi bir düzendir .

Şimdi, while döngüsü , I değişmezi verilen sonlu sayıda adımdan sonra sona erdiğinden ve I bu durumda doğru olmadıkça hiçbir durumun halefi olmadığından , her durumun yinelemeye göre yalnızca sonlu sayıda yinelemeye, her azalan zincire sahip olduğu sonucuna varırız. yalnızca sonlu sayıda farklı değere sahiptir ve bu nedenle sonsuz azalan zincir yoktur , yani döngü yinelemesi azalan zincir koşulunu karşılar .

Bu nedenle - seçim aksiyomunu varsayarak - döngü için başlangıçta tanımladığımız "ardıl" ilişkisi , katı (dönüşümsüz) olduğundan ve "yineleme" ilişkisinde yer aldığından , durum uzayı Σ üzerinde iyi temellendirilmiştir. Gösterdiğimiz gibi Böylece, bu durum alanı kimlik fonksiyonu ise döngü için bir varyant durumu kesin olarak azaltmak-olarak gereken bir "halefi" ve "" döngü -Her zaman gövde, S verilen yürütülür değişmez I ve durum Cı .

Herhangi bir varyantı varlığı bir varyantın varlığını ima Ayrıca, bir sayma bağımsız değişken ile gösterilebilir w ₁ , ilk sayılamaz sıra , diğer bir deyişle

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

Bunun nedeni, sonlu bir bilgisayar programı tarafından sonlu bir girdiden sonlu sayıda adımda ulaşılabilen tüm durumların toplamının sayılabilir sonsuz olması ve ω _1'in sayılabilir kümelerdeki tüm iyi sıralı tiplerin numaralandırılmasıdır.

pratik düşünceler

Pratikte, döngü değişkenleri genellikle negatif olmayan tamsayılar olarak kabul edilir , hatta öyle olmaları gerekir, ancak her döngünün bir tamsayı değişkenine sahip olması gerekliliği , bir programlama dilinden sınırsız yinelemenin ifade gücünü ortadan kaldırır . Böyle (resmi olarak doğrulanmış) bir dil, özyinelemeli işlev çağrısı gibi eşit derecede güçlü başka bir yapı için sonlu ötesi bir sonlandırma kanıtına izin vermedikçe , artık tam μ özyineleme yeteneğine sahip değildir, yalnızca ilkel özyineleme yapabilir . Ackermann'ın işlevi , tamsayı değişkenli bir döngüde hesaplanamayan özyinelemeli bir işlevin kurallı örneğidir .

Bununla birlikte, hesaplama karmaşıklıkları açısından, ilkel özyinelemeli olmayan işlevler, genellikle izlenebilir olarak kabul edilen alanın çok ötesindedir . İlkel özyinelemeli bir işlev olarak basit üs alma durumu bile ve ilkel özyinelemeli işlevlerin bileşiminin ilkel özyinelemeli olduğu düşünüldüğünde, bir ilkel özyinelemeli işlevin ne kadar hızlı büyüyebileceğini görmeye başlayabilir. Ve bir Turing makinesi tarafından ilkel bir özyinelemeli işlevle sınırlanmış bir çalışma süresinde hesaplanabilen herhangi bir işlevin kendisi ilkel özyinelemelidir. Bu nedenle, ilkel özyinelemenin yapmayacağı tam μ - özyineleme için pratik bir kullanım hayal etmek zordur , özellikle birincisi son derece uzun çalışma sürelerine kadar ikincisi tarafından simüle edilebildiğinden.

Ve her halükarda, Kurt Gödel'in ilk eksiklik teoremi ve durma problemi , her zaman sona eren ancak bunu kanıtlayamayan while döngülerinin olduğunu ima eder; bu nedenle, resmi bir sonlandırma kanıtı gereksiniminin bir programlama dilinin ifade gücünü azaltması kaçınılmazdır. Sonlandırılan her döngünün bir varyantı olduğunu göstermiş olsak da, bu, döngü yinelemesinin sağlam temellerinin kanıtlanabileceği anlamına gelmez.

Örnek

İşte, bir while döngüsünde kalan yineleme sayısı üzerindeki bir üst sınırdan hesaplanan bir tamsayı değişkeninin C benzeri sözde kodunda bir örneği . Bununla birlikte, C , bir bilgisayar programının resmi olarak doğrulanması açısından kabul edilemez olan ifadelerin değerlendirilmesinde yan etkilere izin verir.

/** 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;
};

Neden tamsayı olmayan bir değişkeni düşünelim?

Neden tamsayı olmayan veya sonlu olmayan bir değişkeni düşünelim? Bu soru, bir programın sona erdiğini kanıtlamak istediğimiz tüm pratik durumlarda, makul bir süre içinde sona erdiğini de kanıtlamak istediğimiz için gündeme gelmiştir. En az iki olasılık vardır:

• Bir döngünün yineleme sayısına ilişkin bir üst sınır, ilk etapta sonlandırmanın kanıtlanmasına bağlı olabilir. Üç özelliğin ayrı ayrı (veya aşamalı olarak) kanıtlanması istenebilir.
  • kısmi doğruluk,
  • sonlandırma ve
  • koşu zamanı.
• Genellik: Sınır ötesi değişkenleri göz önünde bulundurmak, bir süre döngüsü için tüm olası sonlandırma kanıtlarının bir değişkenin varlığı açısından görülmesine izin verir.

Ayrıca bakınız

• Döngü sırasında
• Döngü değişmezi
• Sınır ötesi indüksiyon
• Azalan zincir durumu
• Büyük sayılabilir sıra
• Doğruluk (bilgisayar bilimi)
• while döngüsünün en zayıf önkoşulları

Referanslar