Course Projects

The final project is due at the beginning of lecture on the last day of class, Wednesday, May 12. Suggested projects include:
  1. Modify the submodel code in sm.scm to implement the the revised continuation form rules in Notes 8.

  2. Modify the submodel code in sm.scm to do context rewriting. Do it so that the partial information available about the hole contents may be specified by a user in a more general way than just the choosing among the four kinds nonval, proc, constant, struc mentioned in Notes 8.

  3. Notes 8, Problems 5 & 6: carefully prove that with the revised call/cc rules, rewriting is Control-context Independent.

  4. Notes 8, Work out a careful proof of The Standard Context Lemma 3.5

  5. Notes 8, Problem 9: carefully prove that rewriting preserves observational equivalence.

  6. Carefully work out a solution to Notes 8, Problem 10 – watch out, the claimed result may be buggy.

  7. Modify the submodel code in sm.scm to be a "normal form" evaluator. Use this as the basis of a Scheme equation theorem-prover.

  8. Find an explicit arithmetic inequality that can't be proved using the final proof system for inequalities in Notes 3 on Arithmetic Equations & Inequalities, and explain why it can't be proved.

  9. Develop a pset or project based on the submodel code suitable for 6.001 students in the first weeks of the course. Ongoing consultation about this with the Lecturer is advised.

  10. Given expressions, F,G, respectively computing functions, f,g, on S-expressions, and a fresh variable, s, Lemma 3.4 in Scheme Compuability Notes 11 observes that the expression
    (lambda (s) (F (G s)))
    computes f o g, the composition of f and g. The proof in the Notes of this claim is not very satisfactory because it rests on a variety of reasoning principles that were not fully spelled out or justified, for example, rules like

    M ↓ (letrec (B) V),      (letrec (B) (V N)) ↓ W
    -----------------------------------------------------------------
    (M N) ↓ W.

    Use properties of the Substitution Model to verify this rule and any similar rules needed to develop a thorough proof of Lemma 3.4.

    Then go on and try to develop a complete proof system for assertions of the form "M ↓ F" where M is an expression and F is a final value.

  11. Computability, Part I (Notes 11), Prob.22: generalize Scott's Rice's 2nd Theorem.

  12. Identify some other poorly written or inadequately explained portion of the course Notes or Scheme Code, and improve it. Prior approval by the Lecturer is required.

This document last modified