Raciocínio sobre loops de terminação não determinísticos

Aqui está uma pergunta da "faixa B", se é que alguma vez houve. Resumo: a primeira coisa que penso quando tento dar uma semântica a programas não determinísticos resulta em uma semântica em que não posso provar coisas sobre loops que terminam apenas de forma não determinística. Certamente alguém descobriu o que fazer nessa situação, ou pelo menos apontou que é difícil, mas não sei como procurá-la (daí a tag "solicitação de referência").

fundo

Eu quero modelar uma linguagem while com não-determinismo. Acho que essa é a maneira óbvia (ou pelo menos ingênua) de modelar essa linguagem com um domínio de poder Smyth, mas me corrija se eu estiver errado. Modelaremos o significado de um comando nessa linguagem como uma função cujo domínio é o conjunto de estados e cujo código-fonte é o conjunto , em que é o elemento menos representativo da não terminação e é o conjunto de estados dos estados.P ( S ) ⊥ = { ⊥ } ∪ P ( S ) ⊥ P ( S $S$${\cal P}(S)_\bot = \{ \bot \} \cup {\cal P}(S)$$\bot$${\cal P}(S)$

Interpretamos comandos como mapas de states para o evento sem término ou para conjuntos de estados que representam possíveis resultados. é uma escolha não determinística.$\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$ se $⟦E⟧\sigma = \mathit{true}$ , caso contrário $⟦Q⟧\sigma$
• $⟦P \circledast Q⟧\sigma = \bot$ se $⟦P⟧\sigma = \bot$ ou $⟦Q⟧\sigma = \bot$ , caso contrário, $⟦P⟧\sigma \cup ⟦Q⟧\sigma$
• $⟦P; Q⟧\sigma = \bot$ se ou para alguns , caso contrário$⟦P⟧\sigma = \bot$$⟦Q⟧\tau = \bot$$\tau \in ⟦P⟧\sigma$$\bigcup_{\tau \in ⟦P⟧\sigma} ⟦Q⟧\tau$

Existe uma ordem parcial completa direcionada , em que para qualquer e se e forem conjuntos adequados e , e podemos estender isso para funções de para pointwise: se para cada , e é a função que mapeia todos os estados para .$\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$

O significado de um loop é é o limite superior mínimo da cadeia , onde se , caso contrário se ou para alguns , caso contrário . (Esta definição pressupõe que o I acabou de definir é Scott contínua, mas eu acho que é seguro para deixar isso de lado.)$⟦\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$

Questão

Considere este programa:

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

Intuitivamente, este é um loop que pode retornar qualquer número par positivo ou não terminar, e que corresponde ao que podemos provar sobre esse loop usando a pré-condição liberal mais fraca (é possível mostrar que é um loop invariante). No entanto, como o loop tem a capacidade de não terminar (podemos refinar a escolha não determinística pelo programa que sempre assume o ramo direito), o significado desse programa, dado qualquer estado inicial, é . (Menos informalmente: a função que mapeia qualquer estado em que é falso para si mesmo e qualquer estado em que é verdadeiro para é um ponto fixo de usado para definir o loop.)$\exists n. x = 2n$$\bot$$b$$b$$\bot$$f$

Isso significa que a semântica ingênua que propus não corresponde da maneira que espero ser capaz de raciocinar sobre os programas. Eu culpo minha semântica, mas não como corrigi-las.

[DB80] A análise de Hitchcock e Park das propriedades de terminação da recursão corresponde a uma análise semântica baseada na chamada interpretação das relações de Egli-Milner [Egl75, Plo76], que expressa um incondicionalismo errático . Essa noção captura que uma união não determinística de relações é correta se gerar pelo menos um cálculo que conduz ao resultado desejado (mesmo na presença de um cálculo não-determinante). Isso parece corresponder ao que você está tentando fazer.

Em seguida, caracterize o significado de uma instrução como uma função mapeando cada estado inicial para algum conjunto de estados não vazio, possivelmente contendo , de modo que seja rigoroso no sentido de que . A escolha não determinística entre as afirmações e é descrita pela função que mapeia cada estado inicial até a união dos resultados individuais . Assim, sempre que ouf S σ ⊥ f S f S ( ⊥ ) = { ⊥ } S 1 S 2 σ f S 1 ( σ ) ∪ f S 2 ( σ ) S 1 S $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$tem a possibilidade não-determinística de produzir um resultado indesejável, o mesmo acontece com a sua escolha não-determinística. Como os conjuntos resultantes de estados finais, obtém-se nesta análise o chamado conjunto de estados Egli-Milner:

⊥${\cal P}_{\text{E--M}}(S) = \{ ~s\subseteq S_\bot ~|~ s$ é finito e não vazio, ou contém$\bot\}$

Por que subconjuntos infinitos de não são considerados conjuntos possíveis de estados finais neste modelo? Sob a suposição de que todos os blocos de construção básicos de termos relacionais produzem apenas conjuntos finitos e não vazios de possíveis estados finais, um conjunto infinito de possíveis estados finais só pode ser gerado quando uma computação infinita é possível. Poderá ser visto da seguinte forma. Estruture o conjunto de todos os cálculos possíveis, começando em um determinado estado como uma árvore com raiz e estados como nós. O conjunto de folhas é então exatamente o conjunto de possíveis estados finais alcançáveis ​​a partir de , excetoσ 0 σ 0 σ 0$S$$\sigma_0$$\sigma_0$$\sigma_0$$\bot$, que pode estar ausente entre as folhas, mas é representado no conjunto de estados finais pelo fato de haver um caminho infinito na árvore. Pela suposição acima, e como somente a escolha finita e não determinística está disponível, essa árvore está se ramificando finitamente. Assim, existe apenas um número finito de folhas em qualquer profundidade finita. Consequentemente, um número infinito de possíveis estados finais só pode ser gerado na presença de uma computação infinita (uma aplicação do lema de König [Kön32]).

$({\cal P}_{\text{E--M}}(S),\sqsubseteq_{\text{E--M}})$ é um poset para definido por: para , s , t ∈ P E - M ( S $\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)~.$

Aqui, pode ser visto como um espaço reservado por meio do qual - conjuntos maiores podem ser gerados inserindo mais estados no lugar de . Portanto, é o menor elemento de . Além disso, o poset possui lubrificantes para cadeias . Da mesma forma, as funções estritas de a são parcialmente ordenadas pela extensão pontual de . Além disso, pelo menos essa função é⊑ E - H ⊥ { ⊥ } ( P E - H ( S ) , ⊑ E - H ) ( P E - H ( S ) , ⊑ E - H ) ω S ∪ { ⊥ } P E --M ( S ) ⊑ E - M λ σ . { ⊥ } $\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\}$ e cadeias lub de tais funções também existem.$\omega$

JB de Bakker. Teoria matemática da correção do programa . Prentice Hall, 1980.

[Egl75] H Egli. Um modelo matemático para cálculos não determinísticos. Relatório técnico, ETH Zürich, 1975.

[Kön32] D König. Theorie der endlichen und unlichlichen Graphen. Relatório técnico, Leipzig, 1932.

[Plo76] GD Plotkin. Uma construção de domínio de poder. SIAM Journal on Computation , 5 (3): 452-487, 1976.

Isenção de responsabilidade: isso é tirado quase literalmente de um livro que eu co-autoria:

WP de Roever e K. Engelhardt. Refinamento de dados: métodos de prova orientados a modelos e sua comparação . Cambridge University Press, 1998.