Curry-Howard y programas de pruebas no constructivas

Esta es una pregunta de seguimiento para

¿Cuál es la diferencia entre pruebas y programas (o entre proposiciones y tipos)?

¿Qué programa correspondería a una prueba no constructiva (clásica) de la forma ? (Suponga que es una relación decidible interesante, por ejemplo, -th TM no se detiene en pasos)T e $\forall k \ T(e,k) \lor \lnot \forall k \ T(e,k)$$T$$e$$k$

(PD: estoy publicando esta pregunta en parte porque estoy interesado en aprender más sobre lo que Neel quiere decir con " la traducción de Godel-Gentzen es una transformación de paso continuo" en su comentario ).

Esta es una pregunta interesante. Obviamente, uno no puede esperar tener un programa que decida para cada si cumple o no, ya que esto decidiría el problema de detención. Como ya se mencionó, hay varias formas de interpretar las pruebas computacionalmente: extensiones de Curry-Howard, realizabilidad, dialéctica, etc. Pero todos interpretarían computacionalmente el teorema que usted mencionó más o menos de la siguiente manera.∀ k T ( e , k $e$$\forall k T(e, k)$

Para simplificar, considere el teorema clásico equivalente

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

Esto es (constructivamente) equivalente al mencionado porque dado podemos decidir si cumple o no simplemente comprobando el valor de . Si mantiene, entonces y, por lo tanto, . Si, por otro lado, no se cumple, entonces (1) tenemos que implica .∀ k T ( e , k ) ¬ T ( e , i ) ¬ T ( e , i ) ∃ i ¬ T ( e , i ) ¬ ∀ i T ( e , i ) ¬ T ( e , i ) ∀ j ( ¬ T ( e , j ) → ⊥ $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)$$\neg T(e, i)$$\forall j (\neg T(e, j) \to \bot)$$\forall j T(e, j)$

Ahora, una vez más, no podemos calcular en (1) para cada dada porque resolveríamos nuevamente el problema de detención. Lo que todas las interpretaciones mencionadas anteriormente harían es mirar el teorema equivalente$i$$e$

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

La función se llama función Herbrand. Intenta calcular un contraejemplo para cada testigo potencial dado . Está claro que (1) y (2) son equivalentes. De izquierda a derecha esto es constructivo, simplemente tome en (2), donde es el testigo supuesto de (1). De derecha a izquierda uno tiene que razonar clásicamente. Suponga que (1) no era cierto. Luego,j i i ′ = i $f$$j$$i$$i' = i$$i$

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

Sea una función testigo de esto, es decir$f'$

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

Ahora, tome en (2) y tenemos , para algunos . Pero tomando en (4) obtenemos la negación de eso, contradicción. Por lo tanto (2) implica (1).$f = f'$$(\neg T(e, f'(i')) \to \neg T(e, i'))$$i'$$i = i'$

Entonces, tenemos que (1) y (2) son clásicamente equivalentes. Pero lo interesante es que (2) tiene ahora un testigo constructivo muy simple. Simplemente tome si no se cumple, porque entonces la conclusión de (2) es verdadera; o bien tome si cumple, porque entonces no se cumple y la premisa de (2) es falsa, lo que lo vuelve a hacer verdadero.$i' = f(0)$$T(e, f(0))$$i' = 0$$T(e, f(0))$$\neg T(e, f(0))$

Por lo tanto, la forma de interpretar computacionalmente un teorema clásico como (1) es mirar una formulación equivalente (clásica) que se pueda demostrar de manera constructiva, en nuestro caso (2).

Las diferentes interpretaciones mencionadas anteriormente solo divergen en la forma en que aparece la función . En el caso de la realizabilidad y la interpretación dialéctica, esto es explícitamente dado por la interpretación, cuando se combina con alguna forma de traducción negativa (como la de Goedel-Gentzen). En el caso de las extensiones de Curry-Howard con los operadores de call-cc y de continuación la función surge del hecho de que el programa se le permite "saber" como un valor determinado (en nuestro caso se utilizará), por lo que es la continuación del programa alrededor del punto donde se calcula .$f$$f$$i$$f$$i$

Otro punto importante es que desea que el pasaje de (1) a (2) sea "modular", es decir, si (1) se usa para probar (1 '), entonces su interpretación (2) debe usarse de manera similar para probar la interpretación de (1 '), diga (2'). Todas las interpretaciones mencionadas anteriormente lo hacen, incluida la traducción negativa de Goedel-Gentzen.

Es bastante conocido que la aritmética clásica e intuicionista es equiconsistente.

Una forma de mostrar esto es a través de las "incorporaciones negativas" de la lógica clásica en la lógica intuicionista. Entonces, supongamos que son fórmulas de aritmética clásica de primer orden. Ahora, podemos definir una fórmula de lógica intuicionista de la siguiente manera:$\phi$

$$\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}$$

Tenga en cuenta que es básicamente un homomorfismo que se adhiere a los no-no adicionales en todas partes, excepto que en disyunciones y existenciales, utiliza la dualidad de Morgan para convertirlos en conjunciones y universales. (Estoy bastante seguro de que esta no es la traducción exacta de Godel-Gentzen, ya que lo preparé para esta respuesta; básicamente, cualquier cosa que escriba usando doble negación + dualidad de Morgan funcionará. Esta variedad en realidad resulta ser importante para interpretaciones computacionales de la lógica clásica; ver más abajo).$G(\phi)$

Primero: es obvio que esta traducción conserva la verdad clásica, de modo que es verdadera si y solo si es, en términos clásicos.$G(\phi)$$\phi$

Segundo: es menos obvio, pero sigue siendo el caso, que para las fórmulas en fragment, la probabilidad en la lógica intuitiva y clásica coincide. La forma de demostrar esto es mirar primero las fórmulas extraídas de esta gramática:$\forall, \implies, \land, \lnot$

$$\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}$$

Y luego podemos demostrar como un lema (por inducción en ) que es derivable intuitivamente. Entonces, ahora podemos mostrar la equiderivabilidad de las fórmulas negativas haciendo una inducción sobre la estructura de la prueba (en, por ejemplo, el cálculo posterior) y usar el lema anterior para simular la ley del medio excluido.G ( A $A$$G(A) \implies A$

Entonces, ¿cómo deberías pensar en esto intuitivamente?

• Primero, la vista de la prueba teórica. Si observa las reglas del cálculo posterior, puede ver que el único lugar en el que la lógica clásica e intuitiva difiere seriamente es en las reglas de disyunción y existenciales. Entonces, estamos usando este hecho para mostrar que las pruebas en una lógica de estas fórmulas pueden traducirse en pruebas en la otra. Esto muestra cómo pensar en la lógica constructiva como una extensión de la lógica clásica con los dos nuevos conectivos y . Lo que llamamos "existencia clásica" y "disyunción clásica" no eran más que abreviaturas que implicaban , conjunción y negación, y por eso, para hablar sobre la existencia real, necesitábamos introducir nuevas conectivas.∨ $\exists$$\vee$$\forall$

• En segundo lugar, hay una vista topológica. Ahora, el modelo de una lógica clásica (como una familia de conjuntos) es un álgebra booleana (es decir, una familia de subconjuntos cerrados bajo uniones arbitrarias, intersecciones y complementos). Resulta que el modelo de lógica intuitiva es como un espacio topológico , con las proposiciones interpretadas como conjuntos abiertos. La interpretación de la negación es el interior del complemento, y luego es fácil demostrar que , lo que significa que la doble negación nos envía al clopen más pequeño que cubre cada abierto --- y los clopens forman un álgebra booleana.$\lnot\lnot\lnot P = \lnot P$

Ahora, gracias a Curry-Howard, sabemos cómo interpretar las pruebas en lógica intuicionista como programas funcionales. Entonces, una posible respuesta (pero no la única) a la pregunta de "¿cuál es el contenido constructivo de una prueba clásica?" es el siguiente:

El contenido computacional de una prueba clásica es cualquiera que sea el contenido computacional de la traducción de su prueba (de acuerdo con la traducción negativa).

Entonces, veamos la traducción de . Entonces esto dice que el contenido constructivo del medio excluido es lo mismo que decir que no es el caso que y mantengan, es decir, no contradicción. Entonces, en este sentido, en realidad no hay mucho contenido computacional en la ley del medio excluido.$G(A \vee \lnot A) = \lnot(\lnot G(A) \land \lnot\lnot G(A))$$\lnot P$$\lnot\lnot P$

Para ver qué es concretamente, recuerde que constructivamente, la negación se define como . Entonces, esta fórmula es . El siguiente bit de código Ocaml ilustrará:$\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 

Es decir, si obtiene no-A y no-no-A, puede pasar la primera negación a la segunda para obtener la contradicción que desea.

Ahora, ¿qué es una continuación de las transformaciones de estilo de paso?

• Una continuación de tipo es algo que toma un valor de tipo y calcula una respuesta final a partir de él.$\tau$$\tau$
• Las continuaciones se utilizan para modelar los contextos del programa. Es decir, podríamos tener un término evaluando como parte de un programa mucho más grande . Todas esas cosas a su alrededor tomarán el resultado de calcular y calcularán la respuesta final.$3+5$$C[3+5]$$3 + 5$
• Entonces, puede pensar en una continuación de tipo como una función , donde es el tipo de respuesta que sea.τ → α $\tau$$\tau \to \alpha$$\alpha$
• Entonces, si tiene un programa de tipo , podemos "convertirlo a CPS" encontrando un término de tipo , que terminará pasando lo que haya calculado Su continuación. (Básicamente, esto solo hace que el flujo de control sea explícito).τ ( τ → α ) → α $e$$\tau$$(\tau \to \alpha) \to \alpha$$e$
• Pero tenemos que hacer esto de forma hereditaria, para que cada subterráneo del programa haya hecho explícita su continuación.

Ahora,

• La traducción negativa básicamente envía hereditariamente a .¬ ¬ $\phi$$\lnot\lnot\phi$
• Sin embargo, aunque nuestra traducción utiliza la negación, en realidad nunca elimina la proposición falsa, por lo que la traducción funciona paramétricamente en esa proposición.
• En particular, podemos reemplazar con cualquier tipo de respuesta .$\bot$$\alpha$
• Así que reemplazamos hereditariamente con .( ϕ → α ) → $\phi$$(\phi \to \alpha) \to \alpha$
• Esta es una transformación de CPS.

Vi "una" transformación de CPS, ya que como mencioné anteriormente, hay muchas traducciones negativas que le permiten probar este teorema, y ​​cada una corresponde a una transformación de CPS diferente. En términos operativos, cada transformación corresponde a un orden de evaluación diferente . Por lo tanto, no existe una interpretación computacional única de la lógica clásica, ya que tiene que tomar decisiones y las opciones de diferencia tienen características operativas muy diferentes.

Hay conferencias completas sobre el tema de las pruebas no constructivas como programas , y no soy un experto en el tema. Arriba, Neel Krishnaswami aludió a una respuesta más larga que está preparando, que, a juzgar por su trabajo aquí, será excelente. Esto es solo una muestra de una respuesta.

Resulta que el tipo de llamada con continuación actual corresponde a la proposición conocida como la ley de Peirce , que puede usarse para probar la Ley del Medio Excluido ( ). Se puede escribir un programa LEM usando callcc. En Coq:$\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.

da el 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)))

La introducción más clara a esto que he visto está en la "Noción de control de fórmulas como tipos" de Tim Griffin .