The Curry-Howard Isomorphism, a Tiny Appetizer

Enjoy these two facts.

Amazing fact 1: Any combinator (i.e. lambda-definable term) can be written using only the two combinators S (lambda (x) (lambda (y) (lambda (z) ((x z) (y z))) and K (lambda (x) (lambda (y) x). For a cute exploitation of this fact, see Iota and Jot: the simplest languages?.

Amazing fact 2 (The Curry-Howard Isomorphism): The types of combinators correspond to tautologies of propositional logic. For example, the type of K is A -> B -> (B -> A). Read A, B, C as variables and -> as implication. Try S: A -> B -> C -> ((A -> C) -> (B -> C). Even more, any tautology can be derived from S and K using modus ponens. Why? The rules (for abstraction and application) in typed lambda-calculus correspond to the rules (for introduction and elimination of implication) in a natural deduction system. For a whirlwind tour of lambda-calculus which mentions the Curry-Howard isomorphism, see the paper Church's Thesis and Functional Programming (PDF). For an exposition of a natural deduction system, see the book Building Problem Solver, section 4.4 Natural Deduction.