Maths - Curry-Howard - Martin Baker

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.

Introduction to Higher Order Categorical Logic - Lambek & Scott - Relates lambda calculus to higher order logic and cartesian closed categories.

More information about:

Cartesian Closed Categories (CCC) on page here.
λ-calculus on page here.
Intuitionistic Logic on page here.

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

Composition of Maps and Nested Types

First look at how we might approximate reversing a map and then extend this to reversing a composition of maps.

We can't reverse a surjective map exactly but instead of mapping back to invividual elements we can map back to sets. This generates equivalence classes or fibre bundles (or, in type theory, dependent types).

Here we try to reverse two functions t and s composed together.

Now we get nested equivalence classes or (or, in type theory, nested dependent types).

More about maps on this page.

Computation, Logic and Geometry

Venn diagrams show us a deep connection between sets , logic and geometry.

If we swap from sets to types and and from Boolean logic to constructive logic we get similar mathematical structure that has this 3-way correspondence.

	Type Theory	Logic	Geometry
	computation	proofs	category theory spaces
types	programs constructions	proposition	spaces objects
terms	algorithmns recipies constants, variables & functions.	a term is a proof of the proposition.	generalised elements points in a space.
non-dependant types	empty	false	initial object
	unit T	true	terminal object
	sum	or	coproduct
	pair	and	product
	function	implication	internal hom
dependant types	type family	predicate	bundle
	substitution	substitution	pullback of a bundle
	Σ type	exists	total space of a bundle
	Π type	for all	space of sections of bundles

See Wiki

Maths - Types - Curry-Howard

Curry-Howard Correspondence

λ-calculus Structure

Intuitionistic Logic Structure

Curry–Howard–Lambek Correspondence

Composition of Maps and Nested Types

Computation, Logic and Geometry

EuclideanSpace

Sets, Logic and Topology

Venn diagrams

Logic Lattices