Curry-Howard

Juan Pablo Yamamoto
jpyamamoto[at]ciencias.unam.mx
Lógica Computacional II. Semestre 2025-1.

Requisitos Previos

{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE LiberalTypeSynonyms #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE MultiParamTypeClasses #-}

data Prueba (term :: k) = QED deriving Show

axioma :: Prueba p
axioma = QED

data Verdadero
data Falso

data Conjuncion p q
data Disyuncion p q
data Implicacion p q

type No p = Implicacion p Falso
type Equivalencia p q = Conjuncion (Implicacion p q) (Implicacion q p)

data Existe x p
data ParaTodo x p

type p ∧ q = Conjuncion p q
type p ∨ q = Disyuncion p q
type p → q = Implicacion p q
type p ↔ q = Equivalencia p q

infixl 5 ∨
infixl 5 ∧
infixr 4 →
infixr 3 ↔

type p ⊢ q = p -> q
infixr 2 ⊢

type p ∴ q = p -> q
infixr 1 ∴

trivial :: Prueba Verdadero
trivial = axioma

exfalso :: Prueba Falso ∴ Prueba a
exfalso _ = axioma

constructor :: (Prueba a, Prueba b) ∴ Prueba (a ∧ b)
constructor _ = axioma

first :: Prueba (a ∧ b) ∴ Prueba a
first _ = axioma

second :: Prueba (a ∧ b) ∴ Prueba b
second _ = axioma

left :: Prueba a ∴ Prueba (a ∨ b)
left _ = axioma

right :: Prueba b ∴ Prueba (a ∨ b)
right _ = axioma

cases :: (Prueba (a ∨ b), Prueba a ⊢ Prueba c, Prueba b ⊢ Prueba c) ∴ Prueba c
cases (_, _, _) = axioma

intro :: (Prueba a ⊢ Prueba b) ∴ Prueba (a → b)
intro _ = axioma

apply :: (Prueba (a → b), Prueba a) ∴ Prueba b
apply (_, _) = axioma

generalize :: (forall c. Prueba (p c)) ∴ Prueba (ParaTodo x (p x))
generalize _ = axioma

specialize :: Prueba (ParaTodo x (p x)) ∴ Prueba (p c)
specialize _ = axioma

use :: Prueba (p c) ∴ Prueba (Existe x (p x))
use _ = axioma

destruct :: (Prueba (Existe x (p x)), (forall c. Prueba (p c)) ⊢ Prueba q) ∴ Prueba q
destruct _ = axioma

class Clasicamente

absurd :: Clasicamente => (Prueba (No a) ⊢ Prueba Falso) ∴ Prueba a
absurd _ = axioma

¿Qué computan las pruebas?

ejemplo1 :: (Prueba a, Prueba ((b → a) → c)) ⊢ Prueba (d → c)
ejemplo1 (a, bac) = intro (\d -> apply (bac, intro (\b -> a)))

Use const

Found:

\ b -> a

Why Not:

const a

ejemplo2 :: Clasicamente => Prueba ((No (p → q)) → p)
ejemplo2 = intro (\nopq -> absurd (\nop -> apply (nopq, intro (\p -> exfalso (apply (nop, p))))))

Redundant bracket

Found:

(No (p -> q)) -> p

Why Not:

No (p -> q) -> p

ejemplo1 (QED, QED)

QED

¿Cómo podemos darle contenido computacional a las pruebas?

Nota: Reiniciar kernel de Jupyter en este punto.

Requisitos Previos

{-# LANGUAGE TypeOperators #-}

Definiciones

data Falso
data Verdadero = QED

type No a = a -> Falso

type a ∧ b = (a, b)
type a ∨ b = Either a b

:i Either

type Either :: * -> * -> * data Either a b = Left a | Right b -- Defined in ‘Data.Either’ instance Semigroup (Either a b) -- Defined in ‘Data.Either’ instance Foldable (Either a) -- Defined in ‘Data.Foldable’ instance Traversable (Either a) -- Defined in ‘Data.Traversable’ instance (Read a, Read b) => Read (Either a b) -- Defined in ‘Data.Either’ instance Applicative (Either e) -- Defined in ‘Data.Either’ instance Functor (Either a) -- Defined in ‘Data.Either’ instance Monad (Either e) -- Defined in ‘Data.Either’ instance (Eq a, Eq b) => Eq (Either a b) -- Defined in ‘Data.Either’ instance (Ord a, Ord b) => Ord (Either a b) -- Defined in ‘Data.Either’ instance (Show a, Show b) => Show (Either a b) -- Defined in ‘Data.Either’

type a ↔ b = (a -> b) ∧ (b -> a)

Teoremas

ejemplo1 :: a -> ((b -> a) -> c) -> (d -> c)
ejemplo1 a bac = \d -> bac (\b -> a)

Redundant lambda

Found:

ejemplo1 a bac = \ d -> bac (\ b -> a)

Why Not:

ejemplo1 a bac d = bac (\ b -> a)

Use const

Found:

\ b -> a

Why Not:

const a

$$ A \rightarrow B \rightarrow C, A \rightarrow B \vdash A \rightarrow C $$

sCombinator :: (a -> b -> c) -> (a -> b) -> a -> c
sCombinator abc ab a = abc a (ab a)

$$ A \rightarrow B, \lnot B \vdash \lnot A $$

contrapositiva :: (a -> b) -> No b -> No a
contrapositiva ab noB a = noB (ab a)

$$ \lnot A \land \lnot B \vdash \lnot (A \lor B) $$

deMorgan1 :: No a ∧ No b -> No (a ∨ b)
deMorgan1 (noA, noB) ab = case ab of
    Left a -> noA a
    Right b -> noB b

dobleNegacion :: a -> No (No a)
dobleNegacion a noA = noA a

¿Algo de esto es útil?

$$ A \vdash A $$

hipotesis :: a -> a
hipotesis a = a

:i id

id :: a -> a -- Defined in ‘GHC.Base’

$$ A \rightarrow B, A \vdash B $$

modusPonens :: (a -> b) -> a -> b
modusPonens ab a = ab a

Eta reduce

Found:

modusPonens ab a = ab a

Why Not:

modusPonens ab = ab

:i ($)

($) :: (a -> b) -> a -> b -- Defined in ‘GHC.Base’ infixr 0 $

$$ B \rightarrow C, A \rightarrow B \vdash A \rightarrow C $$

silogismoHipotetico :: (b -> c) -> (a -> b) -> a -> c
silogismoHipotetico bc ab a = bc (ab a)

:i (.)

(.) :: (b -> c) -> (a -> b) -> a -> c -- Defined in ‘GHC.Base’ infixr 9 .

$$ A \land B \rightarrow C \vdash A \rightarrow B \rightarrow C $$

currificacion :: ((a, b) -> c) -> a -> b -> c
currificacion abc a b = abc (a, b)

:i curry

curry :: ((a, b) -> c) -> a -> b -> c -- Defined in ‘Data.Tuple’

$$ A \rightarrow B \rightarrow C \vdash A \land B \rightarrow C $$

descurrificacion :: (a -> b -> c) -> (a, b) -> c
descurrificacion abc (a, b) = abc a b

:i uncurry

uncurry :: (a -> b -> c) -> (a, b) -> c -- Defined in ‘Data.Tuple’