Wariant pętli

W informatyce wariant pętli jest funkcją matematyczną zdefiniowaną w przestrzeni stanów programu komputerowego, której wartość jest monotonicznie zmniejszana w odniesieniu do (ścisłej) dobrze uzasadnionej relacji przez iterację pętli while w pewnych niezmiennych warunkach , zapewniając w ten sposób jego zakończenie . Wariant pętli, którego zakres jest ograniczony do nieujemnych liczb całkowitych, jest również znany jako funkcja związana , ponieważ w tym przypadku zapewnia trywialną górną granicę liczby iteracji pętli przed jej zakończeniem. Jednak wariant pętli może być pozaskończony , a zatem niekoniecznie jest ograniczony do wartości całkowitych.

Dobrze ugruntowana relacja charakteryzuje się istnieniem minimalnego elementu każdego niepustego podzbioru jej dziedziny. Istnienie wariantu dowodzi zakończenia pętli while w programie komputerowym przez dobrze uzasadnione zejście . Podstawową właściwością dobrze ugruntowanej relacji jest to, że nie ma ona nieskończonych zstępujących łańcuchów . Dlatego pętla posiadająca wariant zakończy się po skończonej liczbie iteracji, o ile jej ciało kończy się za każdym razem.

że pętla while lub, bardziej ogólnie, program komputerowy, który może zawierać pętle while, jest całkowicie poprawny , jeśli jest częściowo poprawny i kończy się.

Reguła wnioskowania dla całkowitej poprawności

Aby formalnie określić regułę wnioskowania dla zakończenia pętli while, którą pokazaliśmy powyżej, przypomnijmy sobie, że w logice Floyda-Hoare'a reguła wyrażania częściowej poprawności pętli while brzmi:

; \ { ja\}}{\{ja\}\;{\mathtt {while}}\;c\;{\mathtt {do}}\;s\;\{ja\land \lnot C\}}},}

gdzie $I$ jest niezmiennikiem , C jest warunkiem , a S jest treścią pętli. Aby wyrazić całkowitą poprawność, piszemy zamiast tego:

{\ Displaystyle {\ Frac {<{\ tekst {jest uzasadniony}}, \; [I \ ziemia C \ ziemia V = z] \; S \; [I \ ziemia V <z]} {[ja] \;{\mathtt {while}}\;C\;{\mathtt {do}}\;S\;[I\land \lnot C]}},}

gdzie dodatkowo V jest wariantem , a zgodnie z konwencją przyjmuje się, że niezwiązany symbol z jest uniwersalnie skwantyfikowany .

Każda pętla, która się kończy, ma wariant

Istnienie wariantu oznacza, że pętla while się kończy. Może się to wydawać zaskakujące, ale sytuacja odwrotna jest również prawdziwa, o ile przyjmiemy aksjomat wyboru : każda pętla while, która się kończy (biorąc pod uwagę jej niezmiennik), ma wariant. Aby to udowodnić, załóżmy, że pętla

{\ Displaystyle {\ mathtt {podczas}} \; C \; {\ mathtt {robić}} \; S

kończy się, biorąc pod uwagę niezmiennik $I$ , gdzie mamy całkowitą poprawność twierdzenia

{\ Displaystyle [I \ ziemia C] \; S \; [ja].}

Rozważmy relację „następnika” na przestrzeni stanów $Σ$ indukowaną przez wykonanie instrukcji S ze stanu spełniającego zarówno niezmiennik $I$ , jak i warunek C . To znaczy, mówimy, że stan $σ'$ jest „następcą” $σ$ wtedy i tylko wtedy, gdy

$I$ i C są prawdziwe w stanie $σ$ i
$σ'$ to stan, który wynika z wykonania instrukcji S w stanie $σ$ .

Zauważmy, że $nie$ zakończyłaby się

Następnie rozważ zwrotne, przechodnie zamknięcie relacji „następca”. $skończony$ tę iterację : $że$ stan $'$ jest iteracją σ jeśli albo istnieje $σ$ takie, że ${\ Displaystyle \ sigma _ {0} = \ sigma,}$ ${\ Displaystyle \ sigma _ {n} = \ sigma '}$ i ${\ Displaystyle \ sigma _ {i + 1}}$ jest „następcą” ${\ Displaystyle \ sigma _ {i};}$ dla wszystkich $ja$ , ${\ Displaystyle 0 \ równoważnik i <n.}$

Zauważmy, że jeśli $σ$ i $σ'$ są dwoma odrębnymi stanami, a $σ'$ jest iteracją $σ$ , to $σ$ nie może być iteracją $σ',$ bo inaczej pętla nie zostałaby zakończona. Innymi słowy, iteracja jest antysymetryczna, a zatem częściowym porządkiem .

Teraz, ponieważ pętla while kończy się po skończonej liczbie kroków przy danym niezmienniku $I$ , a żaden stan nie ma następnika, chyba że $I$ jest prawdziwy w tym stanie, dochodzimy do wniosku, że każdy stan ma tylko skończenie wiele iteracji, każdy malejący łańcuch względem iteracji ma tylko skończenie wiele różnych wartości, a zatem nie ma nieskończonego łańcucha zstępującego , tzn. iteracja pętli spełnia warunek łańcucha zstępującego .

Dlatego — zakładając aksjomat wyboru — relacja „następca”, którą pierwotnie zdefiniowaliśmy dla pętli, jest dobrze ugruntowana w przestrzeni stanów $Σ$ , ponieważ jest ścisła (niezwrotna) i zawarta w relacji „iteracyjnej”. Zatem funkcja tożsamości w tej przestrzeni stanów jest wariantem pętli while, ponieważ pokazaliśmy, że stan musi ściśle się zmniejszać - jako „następca” i „iteracja” - za każdym razem, gdy ciało S jest wykonywane, biorąc pod uwagę niezmiennik $I$ i warunek C. _

Co więcej, możemy wykazać za pomocą argumentu liczącego, że istnienie dowolnego wariantu implikuje istnienie wariantu w ω ₁ , pierwszej nieprzeliczalnej liczbie porządkowej , tj.

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

Dzieje się tak, ponieważ zbiór wszystkich stanów osiągalnych przez skończony program komputerowy w skończonej liczbie kroków ze skończonego wejścia jest policzalnie nieskończony, a ω ₁ jest wyliczeniem wszystkich dobrze uporządkowanych typów na przeliczalnych zbiorach.

Względy praktyczne

W praktyce warianty pętli są często traktowane jako nieujemne liczby całkowite lub nawet wymagane, aby tak było, ale wymóg, aby każda pętla miała wariant całkowity, usuwa ekspresyjną moc nieograniczonej iteracji z języka programowania. O ile taki (formalnie zweryfikowany) język nie pozwala na pozaskończony dowód zakończenia dla innej równie potężnej konstrukcji, takiej jak rekurencyjne wywołanie funkcji , nie jest już zdolny do pełnej μ-rekurencji , a jedynie do prymitywnej rekurencji . Funkcja Ackermanna jest kanonicznym przykładem funkcji rekurencyjnej, której nie można obliczyć w pętli z wariantem całkowitym .

pod względem złożoności obliczeniowej funkcje, które nie są prymitywnie rekurencyjne, leżą daleko poza sferą tego, co zwykle uważa się za wykonalne . Biorąc pod uwagę nawet prosty przypadek potęgowania jako prymitywnej funkcji rekurencyjnej i że składanie prymitywnych funkcji rekurencyjnych jest prymitywnie rekurencyjne, można zacząć dostrzegać, jak szybko może rosnąć prymitywna funkcja rekurencyjna. A każda funkcja, którą może obliczyć maszyna Turinga w czasie działania ograniczonym przez prymitywną funkcję rekurencyjną, sama jest prymitywną rekurencyjną. Trudno więc wyobrazić sobie pełne praktyczne zastosowanie μ - rekurencja, gdzie prymitywna rekurencja nie wystarczy, zwłaszcza że ta pierwsza może być symulowana przez drugą aż do niezwykle długich czasów działania.

W każdym razie pierwsze twierdzenie Kurta Gödla o niezupełności i problem zatrzymania implikują, że istnieją pętle while, które zawsze się kończą, ale nie można tego udowodnić; w związku z tym nieuniknione jest, że wszelkie wymagania dotyczące formalnego dowodu zakończenia muszą zmniejszać siłę wyrazu języka programowania. Chociaż pokazaliśmy, że każda pętla, która się kończy, ma wariant, nie oznacza to, że można udowodnić zasadność iteracji pętli.

Przykład

Oto przykład, w pseudokodzie podobnym do C , wariantu liczb całkowitych obliczonego z pewnej górnej granicy liczby iteracji pozostałych w pętli while. C dopuszcza jednak skutki uboczne w ocenie wyrażeń, co jest niedopuszczalne z punktu widzenia formalnej weryfikacji programu komputerowego.


 

   

 
   

  
         
      /** zmienna-warunkowa, która jest zmieniana w procedurze S() **/  bool  C  ;  /** funkcja, która oblicza iterację pętli związaną bez skutków ubocznych **/  inline  unsigned  int  getBound  ();  /** treść pętli nie może zmieniać V **/  inline  void  S  ();  int  main  ()  {  unsigned  int  V  =  getBound  ();  /* ustaw wariant równy powiązaniu */  assert  (  I  );  /* niezmiennik pętli */ 
      
          0 
         
              
    
       

     podczas gdy  (  C  )  {  potwierdzić  (  V  >  );  /* to twierdzenie jest raison d'être wariantu (raison d'être) */  S  ();  /* wywołanie ciała */  V  =  min  (  getBound  (),  V  -  1  );  /* wariant musi zmniejszyć się o co najmniej jeden */  };  potwierdzić  (  I  &&  !  C  );  /* niezmiennik to nadal prawda, a warunek to fałsz */  return  0
 ;  };

Po co w ogóle rozważać wariant niecałkowity?

Po co w ogóle rozważać wariant niecałkowity lub nieskończony? To pytanie zostało postawione, ponieważ we wszystkich praktycznych przypadkach, w których chcemy udowodnić, że program kończy się, chcemy również udowodnić, że kończy się on w rozsądnym czasie. Istnieją co najmniej dwie możliwości:

Górna granica liczby iteracji pętli może być uzależniona przede wszystkim od udowodnienia zakończenia. Pożądane może być oddzielne (lub stopniowe) udowodnienie trzech właściwości
- częściowa poprawność,
- wypowiedzenie i
- czas pracy.
Ogólność: rozważanie wariantów pozaskończonych pozwala na postrzeganie wszystkich możliwych dowodów zakończenia pętli while w kategoriach istnienia wariantu.

Zobacz też