Curry-Howard e programas de provas não construtivas

Esta é uma pergunta de acompanhamento para

Qual é a diferença entre provas e programas (ou entre proposições e tipos)?

O programa que corresponderia a uma prova não-construtiva (clássica) do formulário $\forall k \ T(e,k) \lor \lnot \forall k \ T(e,k)$ ? (Assume-se que $T$ alguma relação decidíveis interessante por exemplo, $e$ não -ésimo TM não parar em $k$ passos).

(ps: estou postando esta pergunta em parte porque estou interessado em aprender mais sobre o que Neel quer dizer com " a tradução de Godel-Gentzen é uma transformação de passagem contínua" em seu comentário .)

lo.logic pl.programming-languages proof-theory Kaveh
fonte

Resposta parcial na página 2 destas notas de aula . É um pouco enigmático; Vou tentar descobrir algo mais completo.

Dave Clarke

Estou demorando um pouco mais do que o planejado para escrever minha resposta, desde que cometi o erro de decidir provar as coisas que sabia, em vez de apenas afirmá-las. :)

Neel Krishnaswami /

A JSL mais recente teve este artigo . A essência é que o conteúdo computacional das provas clássicas pode depender fortemente de como você escolheu extraí-las. Ainda não o tenho digerido, mas pensei em jogá-lo lá fora.

Re: Reitblatt #

Mas você especificou que T é uma relação decidível ; portanto, há provas construtivas de sua proposição. A lógica clássica é um subconjunto da lógica intuicionista e você especificou que T pertence a esse subconjunto, chamando-o de decidível.

Wren romano

wren, foi o que eu pensei no começo também! Mas a proposição P no exemplo P \ / ~ P da pergunta se realmente é quantificada em todo k, e essa quantificação de T não é necessariamente decidível.

Jbapple #

Respostas:

Esta é uma pergunta interessante. Obviamente, não se pode esperar para ter um programa que decide para cada se possui ou não, pois isso iria decidir a suspensão problema. Como já mencionado, existem várias maneiras de interpretar provas computacionalmente: extensões de Curry-Howard, capacidade de realização, dialética e assim por diante. Mas todos interpretariam computacionalmente o teorema que você mencionou mais ou menos da seguinte maneira. $e$ $\forall k T(e, k)$

Para simplificar, considere o teorema clássico equivalente

(1) $\exists i \forall j (\neg T(e, j) \to \neg T(e, i))$

Este é (construtivamente), equivalente ao mencionado porque dada podemos decidir se possui ou não, basta verificar o valor do . Se mantém então e, portanto, . Se por outro lado $i$ $\forall k T(e, k)$ $\neg T(e, i)$ $\neg T(e, i)$ $\exists i \neg T(e, i)$ $\neg \forall i T(e, i)$ não se sustenta então por (1) temos que implica . $\neg T(e, i)$ $\forall j (\neg T(e, j) \to \bot)$ $\forall j T(e, j)$

Agora, novamente, não podemos computar em (1) para cada dado, porque resolveríamos novamente o Problema da Parada. O que todas as interpretações mencionadas acima fariam é olhar para o teorema equivalente $i$ $e$

(2) $\forall f \exists i' (\neg T(e, f(i')) \to \neg T(e, i'))$

A função é chamada de função Herbrand. Ele tenta calcular um contra-exemplo para cada testemunha em potencial . É claro que (1) e (2) são equivalentes. Da esquerda para a direita, isso é construtivo, basta considerar em (2), onde é a testemunha assumida de (1). Da direita para a esquerda, é preciso raciocinar classicamente. Suponha que (1) não fosse verdade. Então, $f$ $j$ $i$ $i' = i$ $i$

(3) $\forall i \exists j \neg (\neg T(e, j) \to \neg T(e, i))$

Seja uma função testemunhando isso, ie $f'$

(4) $\forall i \neg (\neg T(e, f'(i)) \to \neg T(e, i))$

Agora, pegue em (2) e temos , para alguns . Mas, tomando em (4), obtemos a negação disso, contradição. Portanto (2) implica (1). $f = f'$ $(\neg T(e, f'(i')) \to \neg T(e, i'))$ $i'$ $i = i'$

Portanto, temos que (1) e (2) são classicamente equivalentes. Mas o interessante é que (2) agora tem uma testemunha construtiva muito simples. Simplesmente tome se não se mantiver, porque a conclusão de (2) é verdadeira; ou então tome se mantém, porque então $i' = f(0)$ $T(e, f(0))$ $i' = 0$ $T(e, f(0))$ não se mantém e a premissa de (2) é falsa, tornando-a novamente verdadeira. $\neg T(e, f(0))$

Portanto, a maneira de interpretar computacionalmente um teorema clássico como (1) é olhar para uma formulação (classicamente) equivalente que pode ser comprovada construtivamente, no nosso caso (2).

As diferentes interpretações mencionadas acima divergem apenas na maneira como a função exibida. No caso da realização e da interpretação dialética, isso é explicitamente dado pela interpretação, quando combinada com alguma forma de tradução negativa (como a de Goedel-Gentzen). No caso de extensões Curry-Howard com operadores call-cc e continuation, a função decorre do fato de o programa poder "saber" como um determinado valor (no nosso caso ) será usado, então é a continuação do programa em torno do ponto em que é computado. $f$ $f$ $i$ $f$ $i$

Outro ponto importante é que você deseja que a passagem de (1) para (2) seja "modular", ou seja, se (1) for usado para provar (1 '), sua interpretação (2) deverá ser usada de maneira semelhante para provar a interpretação de (1 '), digamos (2'). Todas as interpretações mencionadas acima fazer isso, incluindo a tradução Gödel-Gentzen negativo.

Paulo
fonte

Bem vinda! É ótimo ver um teórico de provas especializadas aqui.

Neel Krishnaswami

Obrigado Paulo, sua resposta esclareceu uma parte da imagem em um problema relacionado no qual estou trabalhando.

Kaveh

É bem sabido que a aritmética clássica e intuicionista são equiconsistentes.

Uma maneira de mostrar isso é através dos "embates negativos" da lógica clássica na lógica intuicionista. Então, suponha que são fórmulas da aritmética clássica de primeira ordem. Agora, podemos definir uma fórmula da lógica intuicionista da seguinte maneira: $\phi$

\begin{array}{lcl} G (⊤) & = & \neg \neg ⊤ \\ G (ϕ \land ψ) & = & \neg \neg (G (ϕ) \land G (ψ)) \\ G (⊥) & = & \neg ⊤ \\ G (\neg ϕ) & = & \neg G (ϕ) \\ G (ϕ \lor ψ) & = & \neg (\neg G (ϕ) \land \neg G (ψ)) \\ G (\forall x . ϕ) & = & \forall x . \neg \neg G (ϕ) \\ G (\exists x . ϕ) & = & \neg \forall x . \neg (G (ϕ)) \\ G (P) & = & \neg \neg P \end{array}

$\begin{array}{lcl} G(\top) & = & \lnot\lnot\top \\ G(\phi \land \psi) & = & \lnot\lnot(G(\phi) \land G(\psi)) \\ G(\bot) & = & \lnot\top \\ G(\lnot\phi) & = & \lnot G(\phi) \\ G(\phi \vee \psi) & = & \lnot(\lnot G(\phi) \land \lnot G(\psi)) \\ G(\forall x.\;\phi) & = & \forall x.\; \lnot\lnot G(\phi) \\ G(\exists x.\;\phi) & = & \lnot \forall x.\; \lnot(G(\phi)) \\ G(P) & = & \lnot\lnot P \\ \end{array}$

$G(\phi)$

$G(\phi)$ $\phi$

$\forall, \implies, \land, \lnot$

\begin{array}{lcl} A, B & ::= & \forall x . A (x) | A ⟹ B | A \land B | \neg A | \neg \neg P \end{array}

$\newcommand{\bnfalt}{\;\;|\;\;} \begin{array}{lcl} A,B & ::= & \forall x.\;A(x) \bnfalt A \implies B \bnfalt A \land B \bnfalt \lnot A \bnfalt \lnot\lnot P \end{array}$

$A$ $G(A) \implies A$

Então, como você deve pensar sobre isso intuitivamente?

$\exists$ $\vee$ $\forall$
$\lnot\lnot\lnot P = \lnot P$

Agora, graças a Curry-Howard, sabemos como interpretar provas na lógica intuicionista como programas funcionais. Portanto, uma resposta possível (mas não a única) à pergunta "qual é o conteúdo construtivo de uma prova clássica?" é o seguinte:

O conteúdo computacional de uma prova clássica é qualquer que seja o conteúdo computacional da tradução de sua prova (de acordo com a tradução negativa).

$G(A \vee \lnot A) = \lnot(\lnot G(A) \land \lnot\lnot G(A))$ $\lnot P$ $\lnot\lnot P$

$\lnot A == A \implies \bot$ $((G(A) \implies \bot) \land ((G(A) \implies \bot) \implies \bot)) \implies \bot$

type bot = Void of bot
type 'a not = 'a -> bot

let excluded_middle : ('a not * 'a not not) not = fun (u, k) -> k u

Ou seja, se você obtém não-A e não-A, pode passar a primeira negação para a segunda para derivar a contradição que deseja.

Agora, o que são transformações no estilo de passagem de continuação?

$\tau$ $\tau$
$3+5$ $C[3+5]$ $3 + 5$
$\tau$ $\tau \to \alpha$ $\alpha$
$e$ $\tau$ $(\tau \to \alpha) \to \alpha$ $e$
Mas temos que fazer isso hereditariamente, para que todos os subtermos do programa tornem explícita sua continuação.

Agora,

$\phi$ $\lnot\lnot\phi$
No entanto, embora nossa tradução use negação, ela nunca elimina a proposição falsa - portanto, a tradução funciona parametricamente nessa proposição.
$\bot$ $\alpha$
$\phi$ $(\phi \to \alpha) \to \alpha$
Esta é uma transformação do CPS.

Eu vi "uma" transformação do CPS, pois, como mencionei anteriormente, existem muitas traduções negativas que permitem provar esse teorema, e cada uma corresponde a uma transformação diferente do CPS. Em termos operacionais, cada transformação corresponde a uma ordem de avaliação diferente . Portanto, não há uma interpretação computacional única da lógica clássica, pois você tem opções a fazer e as diferenças têm características operacionais muito diferentes.

Neel Krishnaswami
fonte

Esta é uma ótima resposta. Isso me lembrou o artigo de Wadler "Chamada por valor é duplo para chamar por nome": homepages.inf.ed.ac.uk/wadler/topics/call-by-need.html , que inclui uma anedota muito memorável na seção 4 para explicar a relação entre callCC e o meio excluído.

Sclv 03/03

Existem conferências inteiras sobre o tema de provas não construtivas como programas , e eu não sou especialista no assunto. Acima, Neel Krishnaswami aludiu a uma resposta mais longa que ele está preparando, o que, a julgar pelo seu trabalho aqui, será excelente. Esta é apenas uma amostra de uma resposta.

$\forall P, P \lor \lnot P$

Set Implicit Arguments.

Axiom callcc : forall (A B : Set), ((A -> B) -> A) -> A.

Lemma lem : forall (A B:Set), sum A (A -> B).
Proof.
  intros.
  eapply callcc.
  intros H.
  right.
  intros.
  apply H.
  left.
  assumption.
Defined.

Recursive Extraction lem.

fornece o código O'Caml:

type ('a, 'b) sum =
  | Inl of 'a
  | Inr of 'b

(** val callcc : (('a1 -> 'a2) -> 'a1) -> 'a1 **)

let callcc =
  failwith "AXIOM TO BE REALIZED"

(** val lem : ('a1, 'a1 -> no) sum **)

let lem =
    callcc (fun h -> Inr (fun h0 -> h (Inl h0)))

A introdução mais clara a isso que eu vi está na "noção de controle de fórmulas como tipos de Tim " .

jbapple
fonte

Você deve tentar extrair para o Scheme e informar que o procedimento de extração deve extrair o seu callccpara o Scheme callcc. Então você pode realmente experimentar as coisas.

precisa