Upgrade to Pro — share decks privately, control downloads, hide ads and more …

Papers We Love NYC: "Propositions As Types" By ...

Michael Bernstein
August 20, 2015
1.6k

Papers We Love NYC: "Propositions As Types" By Philip Wadler

Michael Bernstein

August 20, 2015
Tweet

Transcript

  1. “Like busses: you wait two thousand years for a definition

    of ‘effectively calculable,’ and then three come along at once.”
  2. “There may, indeed, be other applications of the system than

    its use as a logic.” - Alonzo Church, on the Lambda Calculus
  3. Conjunction A ∧ B corresponds to cartesian product A x

    B, Disjunction A ∨ B corresponds to a disjoint sum A + B Implication A ⊃ B corresponds to function space A → B. A proof of the proposition A ⊃ B consists of a procedure that given a proof of A yields a proof of B.
  4. Conjunction A ∧ B corresponds to cartesian product A x

    B, Disjunction A ∨ B corresponds to a disjoint sum A + B Implication A ⊃ B corresponds to function space A → B. A proof of the proposition A ⊃ B consists of a procedure that given a proof of A yields a proof of B.
  5. Conjunction A ∧ B corresponds to cartesian product A x

    B, Disjunction A ∨ B corresponds to a disjoint sum A + B Implication A ⊃ B corresponds to function space A → B. A proof of the proposition A ⊃ B consists of a procedure that given a proof of A yields a proof of B.
  6. Conjunction A ∧ B corresponds to cartesian product A x

    B, Disjunction A ∨ B corresponds to a disjoint sum A + B Implication A ⊃ B corresponds to function space A → B. A proof of the proposition A ⊃ B consists of a procedure that given a proof of A yields a proof of B.
  7. (dethm if-true (x y) (equal (if 't x y) x))

    (dethm if-false (x y) (equal (if 'nil x y) y)) (dethm if-same (x y) (equal (if x y y) y))
  8. * Replace a function application with its body * Replace

    expressions according to axioms * Prove that a function is total * Leverage homoiconic language for maximum theorem proving fun
  9. (defun dethm.first-of-pair () (J-Bob/define (defun.second-of) '(((dethm first-of-pair (a b) (equal

    (first-of (pair a b)) a)) nil ((1 1) (pair a b)) ((1) (first-of (cons a (cons b '())))) ((1) (car/cons a (cons b '()))) (() (equal-same a))))))