¿Diferencia entre$\lambda$ -$\mu$ - cálculo y teoría de tipo intuicionista + LEM para pruebas clásicas?

Question

Tengo algo de experiencia con el uso de tipo de teoría para hacer pruebas en intuitionistic lógica. Si quiero demostrar teoremas que requieren de la lógica clásica, yo simplemente plantear la ley de medio excluido (LEM) como un axioma. Como tengo entendido, intuitionistic lógica + LEM le da la lógica clásica, así que me imagino que todos los teoremas que tienen un clásico de pruebas, una prueba en intuitionistic-lógica-tipo-la teoría con la LEM, como un axioma.

Pero entonces escuché acerca de los llamados $\lambda$-$\mu$-cálculo, y que este está destinado a extender el Curry-Howard isomorfismo a la lógica clásica. No he logrado conseguir el punto de $\lambda$-$\mu$-cálculo aún, por lo tanto esta pregunta.

Cómo es $\lambda$-$\mu$-cálculo diferente de $\lambda$-cálculo + de Curry-Howard + LEM como un axioma?

Answer 1

En primer lugar, de Curry-Howard no es una cosa que "agregar" para el cálculo lambda. Es una familia de teoremas que se refiere escribió lambda cálculo y prueba de teorías.

De todos modos, digamos que usted está trabajando en Agda. Desea hacer algún clásico de razonamiento para que postulan LEM, digo como:

postulate lem : {P : Set} → isProp P → P ∨ ¬ P

donde isProp P simplemente afirma que hay más de un valor de P. Véase más abajo para una lista completa.

Ahora queremos probar un clásico teorema como la doble negación de la eliminación.

dne : {P : Set} → isProp P → ¬ (¬ P) → P
dne isProp-P ¬¬p with lem isProp-P
dne isProp-P ¬¬p | Left p = p
dne isProp-P ¬¬p | Right ¬p = absurd (¬¬p ¬p)

Este typechecks y es válida la clásica prueba, así que ¿cuál es el problema?

El problema es que esto no compute. Si intenta normalizar, Agda se atasque (como con todos los postulados) en el caso de análisis de lem. Bien, pero que en realidad se ejecuta a sus Agda programas? Agda. Agda normaliza durante el curso de validación de tipos, y si se queda atascado, se acaba de fallar a-comprobación de tipo. Independientemente, una parte clave de la de Curry-Howard correspondencia es conectar el cálculo para la prueba de reducción, y los postulados no tienen ningún cálculo de reglas asociadas con ellos.

Cuál es el $\lambda\mu$ cálculo que hace es hacer un sistema computacional que da computacional significado a los clásicos teoremas como lem. El equivalente a un uso de ladne prueba puede ser "normalizado". Básicamente lo que sucede es que la llamada a lem e inmediatamente vuelve Right ¬p donde ¬p es una continuación de la cual se pasa a ¬¬p. ¬¬p produce ⊥ sin usar ¬p, en cuyo caso estamos bien porque estamos saltar lejos de abandonar este (sub)cálculo, o se aplica ¬p algunos p que nos hace saltar de nuevo a la llamada a la lem y regresar Left p y hemos terminado. Este enfoque para el cálculo no está disponible en el tipo simple cálculo lambda que representa intuitionistic (o mínimo) de la lógica proposicional, y sigue sin estar disponible en un intuitionistic tipo de teoría, tales como Agda.

Listado completo:

data ⊥ : Set where

absurd : {A : Set} → ⊥ → A
absurd ()

¬ : Set → Set
¬ A = A → ⊥

data _≡_ {A : Set} (a : A) : A → Set where
    Refl : a ≡ a

data _∨_ (A B : Set) : Set where
    Left : A → A ∨ B
    Right : B → A ∨ B

isProp : Set → Set
isProp P = (x y : P) → x ≡ y

postulate lem : {P : Set} → isProp P → P ∨ ¬ P

dne : {P : Set} → isProp P → ¬ (¬ P) → P
dne isProp-P ¬¬p with lem isProp-P
dne isProp-P ¬¬p | Left p = p
dne isProp-P ¬¬p | Right ¬p = absurd (¬¬p ¬p)

Answer 2

Como lo que puedo decir (no soy un experto, simplemente he buscado en google) son diferentes maneras de hacer la misma cosa. $mu$ cálculo aparece para dar una continuaciones.

Voy a usar Haskell notaciones de aquí en adelante. Si esto no funciona para usted, puedo volver a escribir mi respuesta, pero estoy más familiarizado con la lógica a través de Haskell/Coq de las matemáticas, así que yo podría hacerlo mal :)

Ahora bien, si tenemos continuaciones, entonces para cualquier tipo a, podemos construir el valor equivalente cont_a :: forall r. (a -> r) -> r que es la continuación de la representación de a.

Configuración de r = Void nos da cont_a :: forall a. (a -> Void) -> Void. Este es el principio de la doble negación de la eliminación, ya que nos permiten "crear una instancia de un valor" (producir una prueba) de $\lnot\lnot a$, desde el $\lnot a$ es codificado como a -> Void en el tipo de teoría.