Maths - Types - Curry-Howard

Curry-Howard Correspondence

There is a relationship between computer programs and mathematical proofs, this is known as the Curry-Howard correspondence.

A type in λ-calculus has the same mathematical structure as a proposition in intuitionistic logic.

A constructor for that type corresponds to a proof of the proposition. The following table has some specific types with their corresponding propositions:

Proposition Type
true formula unit type
false formula empty type
implication function type
conjunction product type
disjunction sum type
universal quantification generalised product type (Π type)
existential quantification generalised sum type (Σ type)

For more information about the Curry-Howard correspondence see the page here.

λ-calculus Structure

There is more information about λ-calculus on page here but here we are interested in its basic type structure.

We can start with some predefined type. T
A function type goes from one type to another T->S
We can have higher order function types which go from a function to another function. (T->S)->(P->Q)
  ... and so on.

Intuitionistic Logic Structure

There is more information about Intuitionistic Logic on page here but here we are interested in its basic structure.

We can start with a simple proposition. A
Predicate calculus allows us to have conditional predicates. if A then B
Again we han have higher order versions of this to any level. if (if A then B) then (if C then D)
  ... and so on.

Curry–Howard–Lambek Correspondence

We can extend this correspondence to include cartesian closed categories (CCC) in category theory.
flag flag flag flag flag flag Introduction to Higher Order Categorical Logic - Lambek & Scott - Relates lambda calculus to higher order logic and cartesian closed categories.

More information about:

Cartesian Closed Category λ-calculus intuitionistic logic
objects

types
p:P

proposition
p = proposition
P = proof of p
Operator Types
 

function type
b(a):A->B

implication
A implies B
  product type
<a,b>:A/\B
conjunction
if A is proof of 'a'
and B is proof of 'b'
then A/\B is proof of <a,b>
  sum type
a+b:A\/B
disjunction
if A is proof of 'a'
and B is proof of 'b'
then A\/B is proof of a+b
Dependant Types
  dependent product type
The type of the result B(a) depends on the value a .
universal quantification
(for alla:A).B(a)
 

dependent sum type
a of type A meets the specification B(a) as proved by b:B(a)
Can be used to represent abstract data types.

existential quantification
(there existsa:A).B(a)
 
  unit type true formula
T
  bottom type false formula
_|_
Inductive Types
  recursive function inductive proof
 
morphisms terms proof
  variable axiom
  constructor introduction rule
  destructor elimination rule
  normal form normal deduction
  weak normalisation normalisation of deductions
  type inhabitation problem provability
  inhabited type intuitionistic tautology
  function application  
  substitution  
     

See Wiki


metadata block
see also:

Correspondence about this page

Book Shop - Further reading.

Where I can, I have put links to Amazon for books that are relevant to the subject, click on the appropriate country flag to get more details of the book or to buy it from them.

flag flag flag flag flag flag Computation and Reasoning - This book is about type theory. Although it is very technical it is aimed at computer scientists, so it has more discussion than a book aimed at pure mathematicians. It is especially useful for the coverage of dependant types.

 

Terminology and Notation

Specific to this page here:

 

This site may have errors. Don't use for critical systems.

Copyright (c) 1998-2023 Martin John Baker - All rights reserved - privacy policy.