Isomorfismo de Curry-Howard

Question

He buscado en Internet, y no encuentro ninguna explicación de CHI que no degenere rápidamente en una conferencia sobre teoría de la lógica que está drásticamente sobre mi cabeza. (Estas personas hablan como si "cálculo intuicionista proposición" es una frase que en realidad significa algo a los seres humanos normales!)

Aproximadamente palabras, CHI dice que los tipos son teoremas, y los programas son pruebas de los teoremas. ¿Pero qué diablos eso incluso significa ??

Hasta ahora, me he dado cuenta de esto:

• Considere id :: x -> x. Su tipo dice "dado que X es verdadero, podemos concluir que X es verdadero". Parece un teorema razonable para mí.

• Considera ahora foo :: x -> y. Como cualquier programador de Haskell te dirá, esto es imposible. No puedes escribir esta función. (Bueno, sin hacer trampa de todos modos.) Leído como un teorema, dice "dado que cualquier X es verdadera, podemos concluir que cualquier Y es verdadera". Esto es obviamente una tontería. Y, por supuesto, no puedes escribir esta función.

• De manera más general, los argumentos de la función se pueden considerar "esto que se supone que son verdaderos", y el tipo de resultado se puede considerar "cosa que es verdad asumiendo todas las demás cosas". Si hay un argumento de función, digamos x -> y, podemos tomar eso como una suposición de que X es verdadero implica que Y debe ser verdadero.

• Por ejemplo, (.) :: (y -> z) -> (x -> y) -> x -> z se puede tomar como "suponiendo que Y implica Z, que X implica Y, y que X es verdadero, podemos concluir que Z es verdadero". Lo cual parece lógicamente sensato para mí.

Ahora, ¿qué demonios significa Int -> Int? o_O

La única respuesta sensata que puedo encontrar es esta: si tiene una función X -> Y -> Z, la firma de tipo dice "asumiendo que es posible construir un valor de tipo X y otro de tipo Y, entonces es posible construir un valor de tipo Z ". Y el cuerpo de la función describe exactamente cómo harías esto.

Eso parece tener sentido, pero no es muy interesante. Entonces claramente debe haber más que esto ...

Answer 1

El isomorfismo de Curry-Howard simplemente establece que los tipos corresponden a las proposiciones, y los valores corresponden a las pruebas.

Int -> Int realmente no significa mucho interesante como una propuesta lógica. Al interpretar algo como una proposición lógica, solo está interesado en saber si el tipo es habitado (tiene algún valor) o no. Por lo tanto, Int -> Int solo significa "dado un Int, puedo darle un Int", y es, por supuesto, cierto. Hay muchas pruebas diferentes de esto (que corresponden a varias funciones diferentes de ese tipo), pero cuando lo tomas como una proposición lógica, realmente no te importa.

Eso no significa que las proposiciones interesantes no pueden involucrar tales funciones; solo que ese tipo particular es bastante aburrido, como una proposición.

Para un ejemplo de un tipo de función que no es completamente polimórfico y que tiene significado lógico, considere p -> Void (para algunos p), donde Void es el tipo deshabitado: el tipo sin valores (excepto ⊥, en Haskell, pero lo abordaré más tarde). La única manera de obtener un valor de tipo Void es si puede probar una contradicción (que, por supuesto, es imposible), y dado que Void significa que ha demostrado ser una contradicción, puede obtener cualquier valor de la misma (es decir, existe una función absurd :: Void -> a). Por consiguiente, p -> Void corresponde a ¬ p: significa "p implica falsedad".

Intuitionistic logic es solo un cierto tipo de lógica que corresponde a los lenguajes funcionales comunes. Es importante destacar, que es constructiva: básicamente, una prueba de a -> b le da un algoritmo para calcular b de a, lo cual no es cierto en la lógica clásica normal (debido a la law of excluded middle, que le dirá que algo es verdadero o falso, pero no por qué).

Aunque funciones como Int -> Int no significan mucho como proposiciones, podemos hacer afirmaciones sobre ellas con otras proposiciones. Por ejemplo, se puede declarar el tipo de igualdad de dos tipos (usando una GADT):

data Equal a b where 
    Refl :: Equal a a 

Si tenemos un valor de tipo Equal a b, entonces a es el mismo tipo de b: Equal a b corresponde a la proposición a = b. El problema es que solo podemos hablar de igualdad de tipos de esta manera. Pero si tuviéramos dependent types, nos podría generalizar esta definición para trabajar con cualquier valor , y así Equal a b correspondería a la proposición de que los valores de un y b son idénticos. Así, por ejemplo, podríamos escribir:

type IsBijection (f :: a -> b) (g :: b -> a) = 
    forall x. Equal (f (g x)) (g (f x)) 

Aquí, f y g son funciones regulares, por lo f fácilmente podría tener un tipo Int -> Int. Nuevamente, Haskell no puede hacer esto; necesitas tipos dependientes para hacer cosas como esta.

lenguajes funcionales típicos no son realmente muy adecuado para escribir demostraciones, no sólo porque carecen de tipos dependientes, sino también debido a ⊥, que, teniendo tipo a para todos a, actúa como una prueba de cualquier proposición. Pero total idiomas como Coq y Agda explotan la correspondencia para actuar como sistemas de prueba, así como los idiomas de programación de tipo dependiente.

Answer 2

Tal vez la mejor manera de entender lo que significa es comenzar (o intento) utilizando tipos como proposiciones y programas como pruebas.Es mejor aprender un idioma con tipos dependientes, como Agda (está escrito en Haskell y es similar a Haskell). Hay varios articles and courses en ese idioma. Learn you an Agda está incompleto, pero trata de simplificar las cosas, al igual que el libro LYAHFGG.

Aquí es un ejemplo de una prueba sencilla:

{-# OPTIONS --without-K #-} -- we are consistent 

module Equality where 

-- Peano arithmetic. 
-- 
-- ℕ-formation:  ℕ is set. 
-- 
-- ℕ-introduction: o ∈ ℕ, 
--     a ∈ ℕ | (1 + a) ∈ ℕ. 
-- 
data ℕ : Set where 
    o : ℕ 
    1+ : ℕ → ℕ 

-- Axiom for _+_. 
-- 
-- Form of ℕ-elimination. 
-- 
infixl 6 _+_ 
_+_ : ℕ → ℕ → ℕ 
o + m = m 
1+ n + m = 1+ (n + m) 

-- The identity type for ℕ. 
-- 
infix 4 _≡_ 
data _≡_ (m : ℕ) : ℕ → Set where 
    refl : m ≡ m 

-- Usefull property. 
-- 
cong : {m n : ℕ} → m ≡ n → 1+ m ≡ 1+ n 
cong refl = refl 

-- Proof _of_ mathematical induction: 
-- 
-- P 0, ∀ x. P x → P (1 + x) | ∀ x. P x. 
-- 
ind : (P : ℕ → Set) → P o → (∀ n → P n → P (1+ n)) → ∀ n → P n 
ind P P₀ _ o = P₀ 
ind P P₀ next (1+ n) = next n (ind P P₀ next n) 

-- Associativity of addition using mathematical induction. 
-- 
+-associative : (m n p : ℕ) → (m + n) + p ≡ m + (n + p) 
+-associative m n p = ind P P₀ is m 
    where 
    P : ℕ → Set 
    P i = (i + n) + p ≡ i + (n + p) 
    P₀ : P o 
    P₀ = refl 
    is : ∀ i → P i → P (1+ i) 
    is i Pi = cong Pi 

-- Associativity of addition using (dependent) pattern matching. 
-- 
+-associative′ : (m n p : ℕ) → (m + n) + p ≡ m + (n + p) 
+-associative′ o _ _ = refl 
+-associative′ (1+ m) n p = cong (+-associative′ m n p) 

Allí se puede ver (m + n) + p ≡ m + (n + p) proposición como tipo y su demostración como la función. Existen técnicas más avanzadas para tales pruebas (por ejemplo, preorder reasoning, los combinadores en Agda son como tácticas en Coq).

¿Qué más se puede probar:

• head ∘ init ≡ head de vectores, here.

• Su compilador produce un programa cuya ejecución da el mismo valor que el valor obtenido en la interpretación del mismo programa (host), here, para Coq. This book es también una buena lectura sobre el tema de modelado de lenguaje y verificación de programa.

• Cualquier otra cosa que pueda demostrarse en las matemáticas constructivas, ya que la teoría de tipos de Martin-Löf en su poder expresivo es equivalente a ZFC. De hecho, el isomorfismo de Curry-Howard se puede extender a physics and topology y a algebraic topology.

Answer 3

La única respuesta sensata que puedo llegar a decir esto: Si usted tiene una función X -> Y -> Z, entonces el tipo de firma dice "asumiendo que es posible la construcción de un valor de tipo X y otro de tipo Y, entonces es posible construir un valor de tipo Z ". Y el cuerpo de la función describe exactamente cómo harías esto. Eso parece tener sentido, pero no es muy interesante. Entonces claramente debe haber más que esto ...

Bueno, sí, hay mucho más, porque tiene muchas implicaciones y abre muchas preguntas.

En primer lugar, su discusión de la CHI se enmarca exclusivamente en términos de tipos de implicación/función (->). No habla de esto, pero probablemente también haya visto cómo la conjunción y la disyunción corresponden a los tipos de producto y suma, respectivamente. Pero, ¿qué ocurre con otros operadores lógicos como la negación, la cuantificación universal y la cuantificación existencial? ¿Cómo traducimos las pruebas lógicas que involucran estos a los programas? Resulta que es más o menos así:

• negación corresponde a continuaciones de primera clase. No me pidas que explique esto.
• La cuantificación universal sobre variables proposicionales (no individuales) corresponde a polimorfismo paramétrico. Así, por ejemplo, la función polimórfica id realmente tiene el tipo forall a. a -> a
• cuantificación existencial sobre las variables proposicionales corresponde a un puñado de cosas que tienen que ver con los datos o escondite aplicación: tipos de datos abstractos, sistemas de módulos y dinámico despacho.Los tipos existenciales de GHC están relacionados con esto.
• La cuantificación universal y existencial sobre variables individuales lleva a sistemas de tipo dependiente.

Aparte de eso, también significa que todo tipo de pruebas sobre lógicas se traducen instantáneamente en pruebas sobre los lenguajes de programación. Por ejemplo, la decidabilidad de la lógica proposicional intuicionista implica la terminación de todos los programas en cálculo lambda simplemente tipado.

Ahora, ¿qué diablos significa Int -> Int? o_O

Es un tipo, o como alternativa, una proposición. En f :: Int -> Int, (+1) nombra un "programa" (en un sentido específico que admite tanto funciones y constantes como "programas", como alternativamente una prueba. La semántica del lenguaje debe proporcionar f como una regla de inferencia primitiva, o demostrar cómo f es una prueba que se puede construir a partir de tales reglas y premisas.

Estas reglas a menudo se especifican en términos de axiomas ecuacionales que definen los miembros base de un tipo y reglas que le permiten probar qué otros programas habitan ese tipo. Por ejemplo, cambiando de Int a Nat (números naturales desde 0 hacia adelante), podríamos tener estas reglas:

• axioma: 0 :: Nat (0 es una prueba primitiva de Nat)
• Regla: x :: Nat ==> Succ x :: Nat
• Regla: x :: Nat, y :: Nat ==> x + y :: Nat
• Regla: x + Zero :: Nat ==> x :: Nat
• Regla: Succ x + y ==> Succ (x + y)

Estas reglas son suficientes para probar muchos teoremas sobre la adición de números naturales. Estas pruebas también serán programas.