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 -> A). Read A, B as variables and -> as implication. Try S: (A -> (B -> C)) -> ((A -> B) -> (A -> 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.
5 years ago
Posts
