2 Apr 2015

winterkoninkje: shadowcrane (clean) (Default)

The past couple weeks I've been teaching about recursive types and their encodings in B522. Here's a short annotated bibliography for followup reading:

  • For a basic intro to recursive types, and for the set-theoretic metatheory: see section IV, chapters 20 and 21.
    • Benjamin C. Pierce (2002) Types and Programming Languages. MIT Press.
  • The proof of logical inconsistency and non-termination is "well-known". For every type τ we can define a fixed-point combinator and use that to exhibit an inhabitant of the type:
    • fixτ = λf:(τ→τ). let e = λx:(μα.α→τ). f (x (unroll x)) in e (roll(μα.α→τ) e)
    • τ = fixτ (λx:τ. x)
  • A category-theoretic proof that having fixed-points causes inconsistency
  • The proof of Turing-completeness is "well-known". Here's a translation from the untyped λ-calculus to STLC with fixed-points:
    • (x)* = x
    • (λx. e)* = roll(μα.α→α) (λx:(μα.α→α). e*)
    • (f e)* = unroll (f*) (e*)
  • Knaster–Tarski (1955): For any monotone function, f, (a) the least fixed-point of f is the intersection of all f-closed sets, and (b) the greatest fixed-point of f is the union of all f-consistent sets.
  • For a quick introduction to category theory, a good place to start is:
    • Benjamin C. Pierce (1991) Basic Category Theory for Computer Scientists. MIT Press.
  • For a more thorough introduction to category theory, consider:
  • The Boehm–Berarducci encoding
  • Under βη-equivalence, Church/Boehm–Berarducci encodings are only weakly initial (hence, can define functions by recursion but can't prove properties by induction)
  • However, using contextual equivalence, Church/Boehm–Berarducci encodings are (strongly) initial
  • Surjective pairing cannot be encoded in STLC (i.e., the implicational fragment of intuitionistic propositional logic): see p.155
    • Morten H. Sørensen and Paweł Urzyczyn (2006) Lectures on the Curry–Howard isomorphism. Studies in Logic and the Foundations of Mathematics, v.149.
  • However, adding it is a conservative extension
  • Boehm–Berarducci encoded pairs is not surjective pairing: the η-rule for Boehm–Berarducci encoding of pairs cannot be derived in System F. (The instances for closed terms can be, just not the general rule.)
  • Compiling data types with Scott encodings
  • For more on the difference between Scott and Mogensten–Scott encodings:
  • Parigot encodings
    • M. Parigot (1988) Programming with proofs: A second-order type theory. ESOP, LNCS 300, pp.145–159. Springer.
  • Parigot encoding of natural numbers is not canonical (i.e., there exist terms of the correct type which do not represent numbers); though both Church/Boehm–Berarducci and Scott encoded natural numbers are.
  • For more on catamorphisms, anamorphisms, paramorphisms, and apomorphisms
  • build/foldr list fusion
    • Andy Gill, John Launchbury, and Simon Peyton Jones (1993) A short cut to deforestation. In Proc. Functional Programming Languages and Computer Architecture, pp.223–232.
    • Many more links at the bottom of this page
  • For another general introduction along the lines of what we covered in class
  • "Iterators" vs "recursors" in Heyting arithmetic and Gödel's System T: see ch.10:
    • Morten H. Sørensen and Paweł Urzyczyn (2006) Lectures on the Curry–Howard isomorphism Studies in Logic and the Foundations of Mathematics, v.149.
  • There are a great many more papers by Tarmo Uustalu, Varmo Vene, Ralf Hinze, and Jeremy Gibbons on all this stuff; just google for it.

June 2017

18192021 222324


Page generated 29 Jun 2017 05:36 am
Powered by Dreamwidth Studios