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)

λ-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.
 Introduction to Higher Order Categorical Logic - Lambek & Scott - Relates lambda calculus to higher order logic and cartesian closed categories.

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
(a: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
(a: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

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.

 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.