Isomorfismo de Curry-Howard

Quizás la mejor manera de entender lo que significa es comenzar (o intentar) usando tipos como proposiciones y programas como pruebas. Es mejor aprender un lenguaje con tipos dependientes, como Agda (está escrito en Haskell y similar a Haskell). Hay varios artículos y cursos sobre ese idioma. Aprender que un Agda está incompleto, pero es tratar de simplificar las cosas, al igual que LYAHFGG libro.

Aquí hay un ejemplo de un simple prueba:

{-# 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 prueba como función. Hay técnicas más avanzadas para tales pruebas (por ejemplo, razonamiento de preorden, combinadores en Agda es como tácticas en Coq).

Qué más se puede probar:

• head ∘ init ≡ head para vectores, aquí .

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

• Cualquier otra cosa que se pueda probar 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 puede extenderse a física y topología y a topología algebraica .

La única respuesta sensata que se me ocurre es esta: Si tienes una función X -> Y -> Z, entonces la firma de tipo dice "suponiendo 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. Así que claramente tiene que haber algo más que esto...

Bueno, sí, hay bastante más aún, porque tiene muchas implicaciones y abre muchas preguntas.

En primer lugar, su discusión del CHI se enmarca exclusivamente en términos de tipos de implicación/función (->). Usted no habla de esto, pero probablemente ha visto también cómo la conjunción y la disyunción corresponden a los tipos de producto y suma respectivamente. Pero, ¿qué pasa 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 ¿involucrarlos en programas? Resulta que es más o menos así:

• La negación corresponde a continuaciones de primera clase. No me pidas que te 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
• La cuantificación existencial sobre 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 lenguajes de programación. Por ejemplo, el la decidibilidad de la lógica proposicional intuicionista implica la terminación de todos los programas en el cálculo lambda de tipo simple.

Ahora, ¿qué demonios 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 tanto funciones como constantes como" programas", o alternativamente una prueba. La semántica del lenguaje debe proporcionar f como 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 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.