Homework # 12
due Tuesday, November 25
Please read Chapter 22 in your textbook.
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
and
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
Prove that constraint type checking is sound and complete using the
SASyLF definitions and skeleton provided.
- 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
? Explain!
About this document
John Tang Boyland
2008-11-23