Homework # 12
due Tuesday, November 25

Reading

Please read Chapter 22 in your textbook.

Problems

Please do the following problems (with some variation, as noted):

• Exercise 22.2.3
• Exercise 22.3.3
• Exercise 22.3.9
  Instead of using the approach given here, please have the $F$ and $F'$ being passed around be integers, where you assume the existence of an infinite (coutable) set of variables You may use the solution to the assignment if you get stuck, but remember that the solution deals with lists, not integers.

  Write a proof in the style of the book (natural language). Doing something like this in SASyLF requires a whole lot of definitions for set operations lemmas on them. It gets very messy--trust me. For the proof, omit all but the VAR, APP and ABS rules. The proof is very short if you define equivalence correctly.

• Exercises 22.4.3
  Check your answers against the solution in the book; do not turn them in.

• Exercise 22.5.2

Proofs

Prove that constraint type checking is sound and complete using the SASyLF definitions and skeleton provided.

Discussion

• The definition of constraint typing in the SASyLF file ignores all the conditions about freshness and non-overlapping uses of variables. The proofs of soundness and completeness are still possible. Did the author of the textbook make a mistake in having all those conditions? Explain!
• The SASyLF theorems and proofs look somewhat different that the textbook's. In particular, where is $\sigma$ ? Explain!

About this document