Rozumowanie na temat niedeterministycznie kończących się pętli

Oto pytanie „ścieżka B”, czy kiedykolwiek było. Podsumowanie: pierwsza rzecz, o której myślę, kiedy próbuję nadać semantykę programom niedeterministycznym, skutkuje semantyką, w której nie mogę udowodnić rzeczy o pętlach, które kończą tylko niedeterministyczność. Z pewnością ktoś wymyślił, co zrobić w tej sytuacji, lub przynajmniej wskazał, że jest to trudne, ale nie wiem, jak się go szukać (stąd tag „żądanie referencyjne”).

tło

Chcę modelować język while z niedeterminizmem. Myślę, że jest to oczywisty (lub przynajmniej naiwny) sposób modelowania takiego języka za pomocą domeny mocy Smyth, ale popraw mnie, jeśli się mylę. Zmodyfikujemy znaczenie polecenia w tym języku jako funkcji, której domeną jest zbiór stanów, a której domeną kodową jest zbiór , gdzie jest najmniejszym elementem reprezentującym nieterminację, a jest zbiorem stanów.P ( S ) ⊥ = { ⊥ } ∪ P ( S ) ⊥ P ( S $S$${\cal P}(S)_\bot = \{ \bot \} \cup {\cal P}(S)$$\bot$${\cal P}(S)$

Interpretujemy polecenia jako mapy od stanów do zdarzenia zakończenia lub do zestawów stanów które reprezentują możliwe wyniki. jest wyborem niedeterministycznym.$\sigma$$\bot$$\{ \sigma_1, \sigma_2, \ldots \}$$P \circledast Q$

• $⟦\mathbf{skip}⟧\sigma = \{ \sigma \}$
• $⟦x := E⟧\sigma = \{ \sigma[(⟦E⟧\sigma)/x] \}$
• $⟦\mathbf{abort}⟧\sigma = \bot$
• $⟦\mathbf{if}~E~\mathbf{then}~P~\mathbf{else}~Q⟧\sigma = ⟦P⟧\sigma$ jeśli $⟦E⟧\sigma = \mathit{true}$ , w przeciwnym razie $⟦Q⟧\sigma$
• $⟦P \circledast Q⟧\sigma = \bot$ jeśli $⟦P⟧\sigma = \bot$ lub $⟦Q⟧\sigma = \bot$ , w przeciwnym razie $⟦P⟧\sigma \cup ⟦Q⟧\sigma$
• $⟦P; Q⟧\sigma = \bot$ jeśli lub dla niektórych , w przeciwnym razie$⟦P⟧\sigma = \bot$$⟦Q⟧\tau = \bot$$\tau \in ⟦P⟧\sigma$$\bigcup_{\tau \in ⟦P⟧\sigma} ⟦Q⟧\tau$

Istnieje ukierunkowane pełne zamówienie częściowe , gdzie dla dowolnego i jeśli oba i są poprawnymi zestawami, a , i możemy rozszerzyć to na funkcje od do punktowo: if dla każdego i to funkcja odwzorowująca każdy stan na .$\sqsubseteq$$\bot \sqsubseteq S'$$S' \in {\cal P}(S)_\bot$$S_1 \sqsubseteq S_2$$S_1$$S_2$$S_1 \supseteq S_2$$f$$S$${\cal P}(S)_\bot$$f_1 \sqsubseteq f_2$$f_1(\sigma) \sqsubseteq f_2(\sigma)$$\sigma$$f_\bot$$\bot$

Znaczenie pętli to to najmniejsza górna granica łańcucha , gdzie if , w przeciwnym razie jeśli lub dla niektórych , w przeciwnym razie . (Ta definicja zakłada, że właśnie zdefiniowane mnie jest ciągłe Scott, ale myślę, że można to bezpiecznie pominąć.)$⟦\mathbf{while}~E~\mathbf{do}~P⟧\sigma$$f_\bot \sqsubseteq f(f_\bot) \sqsubseteq f(f(f_\bot)) \sqsubseteq \ldots$$f(g)(\sigma) = \{\sigma\}$$⟦E⟧(\sigma) = \mathit{false}$$\bot$$⟦P⟧\sigma = \bot$$g(\tau) = \bot$$\tau \in ⟦P⟧\sigma$$\bigcup_{\tau \in ⟦P⟧\sigma}g(\tau)$$f$

Pytanie

Rozważ ten program:

$x := 0;$
$b := \mathsf{true};$
$\mathbf{while}~b~\mathbf{do}$
$\qquad x := x + 2;$
$\qquad b := \mathsf{false} \circledast b := \mathsf{true}$

Intuicyjnie jest to pętla, która może zwrócić dowolną dodatnią liczbę parzystą lub jej nie zakończyć, i która odpowiada temu, co możemy udowodnić w tej pętli przy użyciu najsłabszego wstępnego warunku liberalnego (można pokazać, że jest pętlą niezmienny). Ponieważ jednak pętla może nie zostać zakończona (możemy doprecyzować niedeterministyczny wybór programu, który zawsze przyjmuje prawą gałąź), znaczenie tego programu dla dowolnego stanu początkowego to . (Mniej nieformalnie: funkcja odwzorowująca każdy stan, w którym jest fałszywy, i każdy stan, w którym jest prawdziwe dla jest stałym punktem używanym do definiowania pętli.)$\exists n. x = 2n$$\bot$$b$$b$$\bot$$f$

Oznacza to, że naiwna semantyka, którą zaproponowałem, nie odpowiada temu, w jaki sposób mogę rozumować programy. Obwiniam swoją semantykę, ale nie wiem, jak to naprawić.

W [dB80] analiza Hitchcocka i Parka dotycząca właściwości końcowych rekurencji odpowiada analizie semantycznej opartej na tak zwanej interpretacji relacji Egli-Milnera [Egl75, Plo76], która wyraża nieregularny niedeterminizm. Pojęcie to wychwytuje, że niedeterministyczny związek relacji jest poprawny, jeśli generuje co najmniej jedno obliczenie prowadzące do pożądanego rezultatu (nawet w obecności obliczenia nieterminacyjnego). To wydaje się odpowiadać temu, co próbujesz zrobić.

Następnie scharakteryzuj znaczenie instrukcji jako funkcji odwzorowującej każdy stan początkowy na jakiś niepusty zbiór stanów, prawdopodobnie zawierający , tak że jest ścisły w tym sensie, że . Niedeterministyczny wybór między instrukcjami i jest opisany przez funkcję odwzorowującą każdy stan początkowy na połączenie poszczególnych wyników . Tak więc, ilekroć lub$S$$f_S$$\sigma$$\bot$$f_S$$f_S(\bot) = \{\bot\}$$S_1$$S_2$$\sigma$$f_{S_1} (\sigma) \cup f_{S_2} (\sigma)$$S_1$$S_2$ma niedeterministyczną możliwość wywołania niepożądanego rezultatu, podobnie robi ich niedeterministyczny wybór. Jako wynikowe zestawy stanów końcowych otrzymujemy w tej analizie tak zwany zestaw stanów Egli-Milnera:

${\cal P}_{\text{E--M}}(S) = \{ ~s\subseteq S_\bot ~|~ s$ jest skończony i niepusty lub zawiera$\bot\}$

Dlaczego nieskończone podzbiory nie są uważane za możliwe zestawy stanów końcowych w tym modelu? Zakładając, że wszystkie podstawowe elementy składowe terminów relacyjnych wytwarzają tylko skończone, niepuste zbiory możliwych stanów końcowych, nieskończony zbiór możliwych stanów końcowych można wygenerować tylko wtedy, gdy możliwe jest obliczenie nieskończone. To może być rozumiane w następujący sposób. zestaw wszystkich możliwych obliczeń rozpoczynających się w danym stanie jako drzewo z rootem i stany jako węzły. Zbiór liści jest wówczas dokładnie zbiorem możliwych stanów końcowych osiągalnych z , z wyjątkiem$S$$\sigma_0$$\sigma_0$$\sigma_0$$\bot$, którego może brakować wśród liści, ale w zestawie stanów końcowych jest reprezentowany przez fakt, że w drzewie istnieje nieskończona ścieżka. Zgodnie z powyższym założeniem, a ponieważ dostępny jest tylko skończony niedeterministyczny wybór, drzewo to jest skończone. Zatem na określonej skończonej głębokości jest tylko skończona liczba liści. W konsekwencji nieskończoną liczbę możliwych stanów końcowych można wygenerować tylko w obecności nieskończonego obliczenia (zastosowanie lematu Königa [Kön32]).

$({\cal P}_{\text{E--M}}(S),\sqsubseteq_{\text{E--M}})$ to zestaw dla zdefiniowane przez: dla ,$\sqsubseteq_{\text{E--M}}$$s,t\in{\cal P}_{\text{E--M}}(S)$

$s\sqsubseteq_{\text{E--M}} t\quad = \quad (\bot\in s \land s\setminus\{\bot\}\subseteq t) \lor (\bot\notin s \land s=t)~.$

W tym przypadku może być postrzegany jako symbol zastępczy, przez który można generować większe zbiory wstawiając więcej stanów zamiast . Dlatego jest najmniejszym elementem . Co więcej, poset posiada lub dla łańcuchów. Podobnie ścisłe funkcje od do są częściowo uporządkowane przez punktowe rozszerzenie . Co więcej, najmniejszą taką funkcją jest$\bot$$\sqsubseteq_{\text{E--M}}$$\bot$$\{\bot\}$$({\cal P}_{\text{E--M}}(S),\sqsubseteq_{\text{E--M}})$$({\cal P}_{\text{E--M}}(S),\sqsubseteq_{\text{E--M}})$$\omega$$S\cup\{\bot\}$${\cal P}_{\text{E--M}}(S)$$\sqsubseteq_{\text{E--M}}$$\lambda\sigma.\{\bot\}$Istnieją także i lub z łańcuchów takich funkcji.$\omega$

[dB80] JW de Bakker. Matematyczna teoria poprawności programu . Prentice Hall, 1980.

[Egl75] H Egli. Model matematyczny obliczeń niedeterministycznych. Raport techniczny, ETH Zürich, 1975.

[Kön32] D König. Theorie der endlichen und unendlichen Graphen. Raport techniczny, Lipsk, 1932.

[Plo76] GD Plotkin. Konstrukcja powerdomain. SIAM Journal on Computation , 5 (3): 452–487, 1976.

Zastrzeżenie: zostało to zaczerpnięte niemal dosłownie z książki, którą kiedyś współautorem:

WP de Roever i K Engelhardt. Udoskonalenie danych: metody dowodowe zorientowane na model i ich porównanie . Cambridge University Press, 1998.