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.

Subscribe to:
Posts (Atom)

## My Webabouts

## My Blog List

## Blog Archive

## Labels

- code (5)
- programming-languages (5)
- fsharp (4)
- logic (2)
- monads (2)
- probability (2)
- programming (2)
- scala (2)
- types (2)
- ai (1)
- cs (1)
- game (1)
- haskell (1)
- lambda-calculus (1)
- python (1)
- tips (1)