Solutions

• Lexical version of Define-Datatype

  • Michel
  • Roshan
  
  

• Irrationality of sqrt(2)

  You can place your proofs in /l/www/classes/b621/proofs.
  • Pythagoras' (Michel)
  • Matt
  • Joe
  • Trinary (Michael)
  
  
• Matt: I put some interesting things about the X combinator (with respect to its definition and also expressing it interms of itself).
  
  
• Kyle: I've uploaded some code for assorted assignments on a page on my web-site here.
  
  
• Roshan: Uploaded an interpreter for the pure lambda calculus. This interpreter uses lexical addressing for variables.
  • lsh.scm - this is a repl for simple lambda terms
  • fact.scm - shows using the interpreter for write a factorial solution.
  • A description of a number and list encoding using the pure lambda calculus. This is different from Church numerals.
  
  

• Same Fringe

  • Roshan: Solution using Yield implementation in Scheme
  • Roshan: Solution using MSR's Comega.