Homework #3 Questions

Using the fulluntype checker

NB: I have fixed the fulluntyped checker to work with weise.

NB: Many people are having difficulty defining the ~>*.

1. First, recall the definition of ->* from Homework #2.
2. Write something similar. In particular, if you find yourself writing rules that have special cases for applications as opposed to lamba abstractions, you are doing something wrong. Recall that ->* didn't do anything special for if's.
3. Your multi-step relation ~>* should use single-step Gamma |- t ~> t'.
4. Rather than accept any Gamma it should only use the empty context *.
5. Now you are ready to consider what the Homework recommended: using a right-recursive solution rather thjan a binary recursive solution. The "binary recursive" solution is analogous to the following grammar for seqeuences of a's. (Remember CS 417?)

   S ::= epsilon
       | a
       | S S
   

   For this Homework, you will find it easier to write the required proof if you define the multi-step relation analogous instead to the following right recursive grammar:

   S ::= epsilon
       | a S
   

   Notice that there are only TWO cases here. proving that the relation is transitive is harder (but still fairly easy.) (But, no, for this homework, you don't need to prove that the relation is transitive. On the other hand, if your relation isn't transitive, you haven't defined multi-step evaluation correctly.)