Curry-Howard correspondence

https://en.wikipedia.org/wiki/Curry-Howard_correspondence

Summary

Logic

PLs

natural deduction

λ-calculus

proposition

type

proof

program

Second-order quantification

Generics and modules

Classical logic

Control flow effects, call/cc

Types

Logic

type

proposition

term

proof

program

proof

product type

conjunction

product, A × B

conjunction, A ∧ B

pair, (a, b)

conjunction, A ∧ B

sum type

disjunction

A + B

A ∨ B

Either type

disjunction

function type

implication

A -> B

A => B

b(x):B(x)

conditional proof

a -> Bool

predicate, B(x)

⊥

true

⊤

Σ x:A. B(x)

∃x:A. B(x)

Π x:A. B(x)

∃x:A. B(x)

equality, ~

unit type, ()

theorem, true, ⊤

type

non-theorem, false, ⊥

Void

non-theorem, false, ⊥

Haskell specific

Types

Logic

type

proposition

term

proof

program

proof

type var, a

proposition, a

lambda introduction

natural deduction

CH introduction

In programming language theory and proof theory, the Curry-Howard correspondence(CH), also referred to as isomorphism or equivalence, is the relation between mathematical proofs and computer programs.
The Curry-Howard correspondence is the interpretation of mathematical proofs-as-programs and logical propositions-as-types in a programming language.
It is the link between logic and computation, a generalization of the syntactic analogy between systems of formal logic and computational calculi.
It is usually attributed to by Haskell Curry and W. A. Howard, although the idea is related to the operational interpretation of intuitionistic logic given in various formulations by L.E.J. Brouwer, Arend Heyting and Andrey Kolmogorov, viz. BHK interpretation, and S. Kleene, viz. Realizability.
The CH relation has been extended to include category theory as the three-way Curry-Howard-Lambek correspondence (CHL).

CH references

The idea starting in 1934 with Haskell Curry and it was finalized in 1969 with William Alvin Howard. It connects the "computational component" of many type theories to the derivations in logics.

Howard showed that the typed lambda calculus corresponded to intuitionistic natural deduction (natural deduction without LEM).

The connection between types and logic lead to a lot of subsequent research to find new type theories for existing logics and new logics for existing type theories.

Comparing points of view on type-theoretic operations

Types

Logic

Sets

Homotopy

Proposition

Set

Space

a:A

proof

element

point

B(x)

predicate

family of sets

fibration

b(x):B(x)

conditional proof

family of elems

section

0,1

⊥ ⊤

∅, {∅}

∅,*

A + B

$A\lor B$

disjoint union

coproduct

A × B

$A\land B$

set of pairs

product space

A → B

$A\to B$

set of functions

function space

$\sum_{x:A}B(x)$

$\exists_{x:A}B(x)$

disjoint sum

total space

$\prod_{x:A}B(x)$

$\forall{x:A}B(x)$

product

space of sections

Idₐ

equality =

{x : x·x ∈ A}

path space Aⁱ

Practical Curry-Howard Isomorphism

(from the paper "Curry-Howard Isomorphism Down-to-Earth" by Jannis Grimm, 2015)

theorem, true, ⊤, () unit type
non-theorem, false, ⊥, Void type
implication, →, -> function type
conjunction ∧, product types
disjunction ∨, sum types

In its most basic form, the Curry-Howard Isomorphism states that given a type in the world of programming languages, there is a term with this type if and only if the type corresponds to a theorem in the world of intuitionistic logic.

In other words, if a proposition in the world of intutionistic logic holds true, there is a way in the world of programming languages to write a term with the type corresponding to this proposition, and there is no such way if the proposition is false in intutionistic logic.

We examine writing basic propositions from intuitionistic logic in Haskell. Since Haskell performs type checking at compile-time, the snippets don't even have to be executed - if the code compiles, then the corresponding theorems are true.

1. Theorem

1.1. Basic Theorem in Intuitionistic Logic

In intuitionistic logic, propositional formulae are true (⊤) if and only if we have evidence for the proposition, thus a proof. This makes the proposition a theorem.

1.2. Basic Theorem in Programming Languages

Given a type, this means that if we can write down a value of this type, then this type has a proof, i.e. it is said that the type is inhabited; it is also said that we have produced a witness - the witness is a value of this type which is paramount in a constructive logic such as intuitionistic logic. Knowing that something is true is relatively useless unless we can construct at least one representative bearing witness to the proof. By finding a term of a type we have proven that the type corresponds to a theorem in intuitionistic logic.

For example, consider the Integer type in Haskell:

proofForInteger :: Integer
proofForInteger = 42

We have come up with a term of the Integer type, which means Integer is inhabited. Since this program compiles, we know that Integer correspondends to a theorem - the propositional formula called proofForInteger in the listing is ⊤ (true).

It is not important which type we use for ⊤, because every inhabited value depicts ⊤. By convention, the unit type is used.

Logic: ⊤ (true)
Types: () (unit type)

2. Nontheorem

2.1 Nontheorem in Intuitionistic Logic

Propositional formulae are ⊥ (false) if we do not have a proof for the proposition. This doesn't mean that a proof doesn't exist, only that we don't have it). Every proposition that is not a theorem is ⊥, hence a nontheorem.

2.2 Nontheorem in Programming Languages

In programming languages, the type with no values (like a set without elements, the empty set) is called the bottom type and denoted by ⊥.

Normally, Haskell doesn't support declaring nullary types, i.e. types without data constructors, but a GHC extension EmptyDataDecls allows us to define an empty data type, which we might call Void. It has no constructors, so it is impossible to come up with a witness, i.e. a value of this type, and because of that we say that this is an uninhabited type.

data Void

notProvable :: Void
-- error: signature lacks an accompanying binding

If we try to use this type in a program, we'll get a complain that the type signature lacks an accompanying binding, but we cannot produce its definition because there are no values of this type, it's empty. This wouldn't compile, so the proposition that corresponds to the Void (bottom) type is a nontheorem.

3. Implication

3.1 Implication in Intuitionistic Logic

Symbolically, a → b means that if there is a proof for a, then it's possible to transform it into a proof for b.

In other words:

if a is a theorem, b is also a theorem
or, if a then b
or just, a implies b

ASIDE: The difference between the symbols → and ⇒

a → b only states "if a then b"
a ⇒ b implies the logical connection "from a follows b"

3.2 Implication in Programming Languages

This definition tells us how we can write an implication in Haskell: (?)

Given an inhabited type a we need to construct a proof for type b to prove the implication a → b.

Remember that a → b is a proposition too: it corresponds to a type in Haskell and if we can prove this proposition, we know it is a theorem. If we cannot prove it, it is a nontheorem.

The type corresponding to implications is a function type: given a value of type a (i.e. a proof for a) it allows us to construct a value of type b (i.e. a proof for b). Hence a → b is written as the type a -> b in Haskell.

Implication Introduction Rule

Implication Introduction Rule in Intuitionistic Logic

Inference rule for introduction of implication is given by

  b
-----
a → b

and it means, if we know that b is a theorem, then we can infer that a → b is also a theorem.

The condition "if a then b" is fulfilled regarless of a:

if a is a theorem, then it's fulfilled because "if T then T" is true
if a is a nontheorem, then "if a then T" is not violated - this is called the principle of explosion, or, originally, ex nihil quodlibet (falsehood entails anything; everything may transpire with falsehood).

p → q

notes

⊤

⊤ → ⊤, straight-forward truth

⊤

⊥

⊤ → ⊥, the only false case, false statement

⊥

⊤

⊥ → ⊤, vacuously true, ex nihil quodlibet

⊥

⊤

⊥ → ⊥, contraposition: ¬q → ¬p

Examples __*"No man, no problem"*__ ``` No man → no problem p → q -------------------------------- if p p = "there is no man" then q q = "there is no problem" -------------------------------- ``` __*"Stop making sense"*__ ```txt The shaman said: "You must stop making sense to understand it." p = Stop making sense q = to understand it 1. You really did stop making sense and you understood it ✔ - this is the straight-forward case - `⊤ → ⊤`, true implies true (is true) - the statement was true: what was stated, actually transpired; the "promise" was delivered, the proposition was correct. the shaman knew his shit. 2. You really did stop making sense but you didn't understand it ✘ - also a straight-forward case, it just means that the statement was true. The person who claimed this was a liar! i.e. the shaman was a endorsing falsehood. the shaman didn't know shit from shaft. 3. You didn't stop and you understood it ✔ - this case is quite alright: stopping to make sense was sort of a sure shot, but apparently there are other ways to reach the truth. nice pull :) Ex falso quodlibet, after all. 4. You didn't stop and you didn't understad it ✔ - well, what did you expect? alt way to enlightement? Ex falso quodlibet, after all, including falso, fucko. ```

Implication Introduction Rule in Programming Languages

Summary

Theorems

Logic: ⊤ true
Types: () (unit type, or any inhabited)

Nontheorems

Logic: ⊥ false
Types: Void (bottom type)

Implication

Logic: → implies, if-then
Types: -> function type

Conjunction

Logic: ∧ and
Types: product types

Disjunction

Logic: ∨ or
Types: sum types

The Curry-Howard isomorphism: Latex table

Types

Logic

Sets

Homotopy

$A$

Proposition

Set

Space

$a:A$

proof

element

point

$B(x)$

predicate

family of sets

fibration

$b(x):B(x)$

conditional proof

family of elements

section

$0,1$

$\bot\ \top$

$\varnothing, \{\varnothing\}$

$\varnothing, \ast$

$A + B$

$A\lor B$

disjoint union

coproduct

$A\times B$

$A\land B$

set of pairs

product space

$A\to B$

set of functions

function space

$\sum_{x:A}B(x)$

$\exists_{x:A}B(x)$

disjoint sum

total space

$\prod_{x:A}B(x)$

$\forall{x:A}B(x)$

product

space of sections

$Id_A$

equality $=$

$\{x:x\mid x \in A\}$

path space $A^I$

References

https://en.wikipedia.org/wiki/Principle_of_explosion https://rationalwiki.org/wiki/Principle_of_explosion

PreviousCurry-Howard correspondence NextCurry-Howard correspondence

Last updated 3 years ago

Was this helpful?