haskell types logic curry-howard

haskell - Isomorfismo de Curry-Howard



types logic (3)

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 el "cálculo de proposición intuicionista" es una frase que realmente significa algo para los humanos normales!)

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

Hasta ahora, me he dado cuenta de esto:

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

  • Ahora considere 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 es verdadero", y el tipo de resultado se puede considerar "cosa que es verdadera asumiendo que todas las demás cosas son". 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 verdadera, podemos concluir que Z es verdadero ". Lo cual parece lógicamente sensato para mí.

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

La única respuesta sensata que se me ocurre es la siguiente: si tienes una función X -> Y -> Z, la firma de tipo dice "suponiendo que es posible construir un valor de tipo X y otro de tipo Y, luego 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 ...

La única respuesta sensata que se me ocurre es la siguiente: si tienes una función X -> Y -> Z, la firma de tipo dice "suponiendo que es posible construir un valor de tipo X y otro de tipo Y, luego 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 sobre el 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í:

  • La negación corresponde a las continuaciones de primera clase . No me pidas que explique esto.
  • La cuantificación universal sobre las variables proposicionales (no individuales) corresponde al polimorfismo paramétrico . Entonces, por ejemplo, la función polimórfica id realmente tiene el tipo para todo forall a. a -> a forall a. a -> a
  • La cuantificación existencial sobre las variables proposicionales corresponde a un puñado de cosas que tienen que ver con la ocultación de datos o implementación: tipos de datos abstractos , sistemas de módulos y despacho dinámico . Los tipos existenciales de GHC están relacionados con esto.
  • La cuantificación universal y existencial sobre variables individuales conduce 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 alternativamente una proposición. En f :: Int -> Int , (+1) nombra un "programa" (en un sentido específico que admite funciones y constantes como "programas", o como alternativa una prueba. La semántica del lenguaje debe proporcionar f una regla primitiva de inferencia, o demostrar cómo f es una prueba que puede construirse a partir de tales reglas y premisas.

Estas reglas a menudo se especifican en términos de axiomas ecuacionales que definen los miembros básicos de un tipo y reglas que le permiten probar qué otros programas habitan ese tipo. Por ejemplo, al cambiar de Int a Nat (números naturales de 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.

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 proposición lógica. Al interpretar algo como una proposición lógica, solo está interesado en si el tipo está habitado (tiene algún valor) o no. Entonces, Int -> Int solo significa "dado un Int , puedo darte 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 una instancia de un tipo de función que no es completamente polimórfica y que tiene un significado lógico, considere p -> Void (para algunos p ), donde Void es el tipo deshabitado: el tipo sin valores (excepto ⊥, en Haskell, pero Voy a llegar a eso más tarde). La única forma de obtener un valor de tipo Void es si puede probar una contradicción (que es, por supuesto, imposible), y como Void significa que ha demostrado ser una contradicción, puede obtener cualquier valor (es decir, existe una función absurd :: Void -> a ). En consecuencia, p -> Void corresponde a ¬ p : significa " p implica falsedad".

La lógica intuitiva es solo un cierto tipo de lógica a la que corresponden los lenguajes funcionales comunes. Es importante destacar que es constructivo : básicamente, una prueba de a -> b le da un algoritmo para calcular b partir de a , lo cual no es cierto en la lógica clásica regular (debido a la ley del medio excluido , 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, podemos declarar el tipo de igualdad de dos tipos (usando un GADT ):

data Equal a b where Refl :: Equal a a

Si tenemos un valor de tipo Equal ab , entonces a es el mismo tipo de b : Equal ab corresponde a la proposición a = b . El problema es que solo podemos hablar sobre igualdad de tipos de esta manera. Pero si tuviéramos tipos dependientes , podríamos generalizar fácilmente esta definición para trabajar con cualquier valor, y así Equal ab correspondería a la proposición de que los valores a y b son idénticos. Entonces, 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 que f podría tener fácilmente un tipo Int -> Int . Nuevamente, Haskell no puede hacer esto; necesitas tipos dependientes para hacer cosas como esta.

Los lenguajes funcionales típicos no son muy adecuados para escribir pruebas, no solo porque carecen de tipos dependientes, sino también por ⊥, que, al tener a tipo a para todo a , actúa como una prueba de cualquier proposición. Pero los lenguajes total como Coq y Agda explotan la correspondencia para actuar como sistemas de prueba, así como también como lenguajes de programación de tipos dependientes.

Quizás la mejor manera de entender lo que significa es comenzar (o intentar) usar 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 artículos y cursos en ese idioma. Aprende que un Agda está incompleto, pero trata de simplificar las cosas, al igual que el libro de LYAHFGG.

Aquí hay un ejemplo de una prueba simple:

{-# 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í puede ver (m + n) + p ≡ m + (n + p) proposición como tipo y su prueba como función. Existen técnicas más avanzadas para tales pruebas (por ej., Razonamiento preordenador , combinadores en Agda son como tácticas en Coq).

Qué más se puede probar:

  • head ∘ init ≡ head para 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. Este libro también es una buena lectura sobre el tema del modelado del lenguaje y la verificación de programas.

  • Cualquier otra cosa que pueda ser probada en 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 la física y la topología y a la topología algebraica .