Handouts

Week 1 | Week 2 | Week 3 | Week 4 | Week 5 | Week 6 | Week 7
Week 8 | Week 9 | Week 10 | Week 11 | Week 12 | Week 13 | Week 14

Week 1

• Assignment #1 due by midnight on Monday, Feb. 7.
• Wednesday (First day of class), Feb. 2.
  • Course overview
• Friday , Feb. 4.
  • Formalizing the meaning of Arithmetic expressions and equations

Week 2

• Monday, Feb. 7.
  • Equivalence of Arithmetic expressions, I
• Wednesday, Feb. 9.
  • Implementing restart-c-eval and call/cc
  • Solution Code for Assignment #1 on the continuation evaluator: c-eval-full.scm, desugar-full.scm
• Friday, Feb. 11.
  • Equivalence of Arithmetic expressions, II. Class problem: exhibit enough axioms to simplify arithmetic expressions into polynomial form [Soln: the Commutative Ring axioms]

• Reading: Notes 1: Arithmetic Equations (pdf), (aeqn.tex)
• Assignment #2: Problems 3, 4, 6, 8 & 9 from Notes 1 on Arithmetic Equations (pdf). Submit solutions by email to 6844-probs@theory.csail.mit.edu by midnight on Wednesday, Feb. 16. (Attachments of scanned, handwritten solutions are fine.)

Week 3

• Monday, Feb. 14.
  • Understanding continuations -- the example in §3.4.1 [added 2/17/05] of the 6.001 Continuation Evaluator project, (pdf)
  • An elegant use of call/cc: callcc-example.scm
• Wednesday, Feb. 16.
  • Proof of the Substitution Lemma by structural induction on ae's. Intro to proofs: linear, tree, DAG, & straightline or "substitution" proofs for equations.
  • Arithmetic Inequalities.
    Class problem: find an arithmetic inequality valid over Integers but not over the Reals. [Soln: x ≤ x².]
• Friday, Feb. 18.
  • Substitution into arithmetic inequalities.
    
  • Terms over a signature. Class problem: what equalities are valid in all models? Prove it. [Soln: two terms are equal in all models iff they are identical. Complete proof next class.]
• Reading: Notes 3: Extended Notes on Arithmetic Equations & Inequalities (pdf), (aineq.tex)
• Assignment #3: Do Problem 1 in Substitution Proof, Problems 10 & 11 in Notes 3 (pdf), and be prepared to discuss Problem 11 in next class. Submit solutions by email to 6844-probs@theory.csail.mit.edu by midnight on Wednesday, Feb. 23.
• Assignment #3.5 (pdf), (tex) Due by midnight, Friday, 2/25. (original version html)

Week 4

• Tuesday, Feb. 22 (virtual Monday)
  • Construct a term-model to show that two terms have the same meaning in all models iff they are identical. Def. of a model of an arbitrary set of equational axioms.

• Reading:
  • Notes 4: Substitution into Arithmetic Equations (pdf), (subst.tex). These include a careful proof of the Substitution Lemma, as well as solutions to the problems about substitution in Assignment #2 & the Substitution Proof handout.
  • Notes 5: Term Models & Equational Completeness (pdf), (term-models.tex)
• Wednesday, Feb. 23
  • Equational completeness theorem:

    If an equation is semantically implied by a set of equations, then the equation is provable using standard formal rules starting with the set of equations as axioms.

    Outline of proof using a term model.
    Class problem: verify that "provably equal" is a congruence relation on a term model.
• Friday, Feb. 25.
  • Intro to the Scheme Substitution Model. Desugaring Rules for quoted lists. Patterns with ?variables that match single items and *variables that match sequences of items.
  • Assignment #4, Due Wednesday, March 2, before class.

Week 5

• Monday, Feb. 28.
  • Class Problem: the Variable Convention (pdf), solution (pdf) (tex)
• Wednesday, March 2
  • Review solutions to Assignments 3.5 & 4
  • Solution to Assignment #3.5 (pdf), (tex)
  • Assignment 4A (resubmission of Assignment #4) due before class Wednesday, Mar. 9
• Friday, March 4
  • Quiz 1 (pdf), (tex) covering through Monday, Feb. 28,
    Solutions (pdf)
  • Appendix for Quiz 1 (pdf), (tex)

Week 6

• Monday, March 7
  • Quiz 1 debriefing
• Wednesday, March 9
  • Pattern-match based procedure proof-match.scm for converting a sequence-of-equations proof into a tree proof.
  • Simple pattern-match rewrite rules: "Doctor" program using unnested matching eliza.scm
• Friday, March 11
  • : canonical expressions for Scheme values.

Week 7

• Monday, March 14
  • Context patterns to control where to rewrite.
  • Intro to Scheme Model rewrite rules
  • Reading: Notes 6: Substitution Model, I: Rewrite Rules (pdf), (submodel1.tex).
• Wednesday, March 16
  • Class Problem: Substitution Model example evaluation (pdf)
• Friday, March 18
  • Substitution rules for letrec; the Variable convention implies that error letrec's cannot rewrite.

Week 8

• Monday, March 28
  • Reading: Notes 7: Substitution Model (full definition) (pdf) (submodel.tex)
  • Garbage collection; uniqueness of final form (to be proved)
• Wednesday, March 30
  • Class Problem: Which Submodel Rules do not preserve the Variable Convention? Examples.
  • Assignment 5 due before class Friday, April 8:
    Notes 7 (pdf), Problems 2, 3, 7, 8, 9
• Friday, April 1
  • Diamond property (Strong confluence) implies Confluence; Submodel with Garbage-collect Rules has this property;
    Weak confluence + Termination implies confluence.
  • Intro to Observational Equivalence.
  • Notes 7 edited 4/5/05 (pdf)

Week 9

• Monday, April 4
  • Class problem: prove that Observational Equivalence is the same whether observing all printable values, some particular printable value (like 17), or only termination (successful return of some value)
  • Def. of Control-context Independence
• Wednesday, April 6
  • Reading: Notes 8 : Scheme Equations (pdf), (tex)
  • Control-context Independence: holds for the non-call/cc Submodel Rules; not for the (call/cc) rules. Sketch of modified (call/cc) rules that are control-context independent.
  • Intro to Context Rewriting.
• Friday, April 8
  • Quiz 2 (pdf), (tex) covering Notes 7 (pdf) and class problem of Monday, April 4
  • Quiz2 solutions (pdf), (tex)
  • Term project suggestions

Week 10

• Monday, April 11
  • Review of Abelson & Sussman: compiling Scheme to register machines; def of register machines.
• Wednesday, April 13
  • Class problem: simulating a register machine with a memory array by one without.
• Friday, April 15
  • Simulating Scheme with 2-Counter Machines.
  • Notes 9: Compiling Scheme to "Micro²" computers (pdf), (tex)

Week 11

• Monday, April 18, holiday
• Wednesday, April 20
  • The Twin Prime conjecture reduces to the Totality Problem for 2-CM's
• Friday, April 22
  • Scheme computability on S-expressions & many-one reducibility, ≤_m
  • Notes 10: The Semigroup Word Problem (pdf), (tex)

Week 12

• Monday, April 25
  • 2-CM Halting in ≤_m Semigroup Word Problem
• Wednesday, April 27
  • Scheme Equations (pdf), (tex): context rewriting & operational extensionality
• Friday, April 29
  • Undecidability of the Scheme Halting Problem
  • Notes 11: Scheme Computability (pdf), (tex) revised 5/3

Week 13

• Monday, May 2:
  • Unrecognizability of the complement of the Halting Problem
  • Productivity of the complement of the Self-Halting Problem; productivity inherits up many-one reducibility (≦_m).
• Wednesday, May 4
  
  • Recognizability of the provable assertions in any proof system.
  • Incompleteness theorem for Scheme observational equivalences.
• Friday, May 6 -- NO CLASS

Week 14

• Monday, May 9
  • Notes 12: Scheme Computability, II (pdf), (tex)
  • Inconsistent Sets of Scheme equations; recongizability of inconsistency; statement of the Second Incompleteness Theorem for Scheme equations.
• Wednesday, May 4
• Friday, May 6 -- NO CLASS

Scheme information

• 6.001 Scheme available at 6.001 SchemeImplementations
• The online Scheme repository is http://www.schemers.org. In particular, the latest official Scheme specification is in the Revised^5 Report on the Algorithmic Language Scheme, also available in pdf.

• Introductory Scheme Texts

• Sample edwin customization file:
  • Unix .edwin
  • Windows edwin.ini

Latex macros

• course.sty
• course.dat

This document last modified