Curry-Howard: Encyclopedia II - Curry-Howard - Programs are proofs

Curry-Howard - Programs are proofs

A second aspect of the Curry-Howard isomorphism is that a program whose type corresponds to a logical formula is itself analogous to a proof of that formula.

Consider the two following functions of λ-calculus:

It can be shown that any function can be created by suitable applications of K and S to each other. (See the combinatory logic article for a proof.) For example, the function B defined above is equivalent to (S (K S) K). If a function, such as B, can be expressed as a composition of S and K, the expression can be converted directly into a proof that the type of B, interpreted as a logical formula, is a theorem of intuitionistic logic. Essentially, appearances of K correspond to uses of the first axiom schema, appearances of S correspond to uses of the second axiom schema, and function applications correspond to uses of the modus ponens deduction rule.

The first axiom schema is α → β → α, and this is precisely the type of the K function; similarly the second axiom schema, (α → β → γ) → (α → β) → α → γ, is the type of the S function. Modus ponens says that if we have two expressions, one of type α → β (that is, a function that takes a value of type α and returns a value of type β) and the other of type α (that is, a value of type α) then we should be able to find a value of type β; clearly, we can do this by applying the function to the value; the result will have type β.

Curry-Howard - Proof of α → α

As a simple example, we will construct a proof of the theorem α → α. This is the type of the identity function I = λx.x. The function ((S K) K) is also equivalent to the identity function. As a description of a proof, this says that we need to first apply S to K. We do this as follows:

If we let γ = α in S, we get:

Since the antecedent of this formula (α → β → α) is a known theorem, and is in fact precisely K, we can apply modus ponens and deduce the consequent:

This is the type of the function (S K). Now we need to apply this function to K. Again, we manipulate the formula so that the antecedent looks like K, this time by substituting (β → α) for β:

Once again we can use modus ponens to detach the consequent:

and we are done.

In general, the procedure is that whenever the program contains an application of the form (P Q), we should first prove theorems corresponding to the types of P and Q. Since P is being applied to Q, the type of P must have the form α → β and the type of Q must have the form α for some α and β. We can then detach the conclusion, β, via the modus ponens rule.

Curry-Howard - Proof of β → α → γ → β → γ → α

As a more complicated example, let's look at the theorem that corresponds to the B function. The type of B is (β → α) → (γ → β) → γ → α. B is equivalent to (S (K S) K). This is our roadmap for the proof of the theorem (β → α) → (γ → β) → γ → α.

First we need to construct (K S). We make the antecedent of the K axiom look like the S axiom by setting α equal to (α → β → γ) → (α → β) → α → γ, and β equal to δ:

Since the antecedent here is just S, we can detach the consequent:

This is the theorem that corresponds to the type of (K S). We now apply S to this expression. Taking S

we put α = δ, β = (α → β → γ), and γ = ((α → β) → α → γ), yielding

and we then detach the consequent:

This is the formula for the type of (S (K S)). A special case of this theorem has δ = (β → γ):

We need to apply this last formula to K. Again, we specialize K, this time by replacing α with (β → γ) and β with α:

This is the same as the antecedent of the prior formula, so we detach the consequent:

Switching the names of the variables α and γ gives us

which was what we had to prove.

Adapted from the Wikipedia article "Programs are proofs", under the G.N U Free Docmentation License. Please also see http://en.wikipedia.org/wiki