Formal Semantics

Due Monday, November 3, at the start of class.

For this assignment, you may develop your answers electronically and/or write them down by hand on paper, as long as the result is readable.

1.  
   1. Perform the following substitution, ensuring that you do not suffer from variable capture:
      [x -> (y (lambda z. z y))] (x (lambda y. z x y (lambda x. z x y)))
   2. In the definition of substitution on slide 11, one rule relies on implicit alpha-renaming to establish its pre-conditions.  Rewrite that rule, or add another, so that no implicit renaming is needed, i.e., all renaming is done explicitly through substitution in some subexpression.  Hint: your answer may wish to have some condition like "z not in freeVars(e)" for some e.
2. Consider the following untyped lambda-calculus expression:
   ((lambda x. (lambda y. x)) (lambda z. (z z))) ((lambda w. (w w)) (lambda v. v))
   1. Show the sequence of beta-reductions performed to reduce this term to a normal form under small-step call-by-value evaluation, as we did in class for many untyped lambda-calculus terms, for instance Church arithmetic (slide 48 defines this reduction order formally for the simply-typed lambda-calculus).
   2. Show the full derivation tree of evaluating this term using big-step call-by-value evaluation rules (slide 54 defines these rules, albeit for the simply-typed lambda-calculus).
   3. Show the full derivation tree of evaluating this term using big-step call-by-value evaluation rules using explicit environments and closures (slide 57 defines these rules, albeit for the simply-typed lambda-calculus).
3. Show the full typing derivation tree for the following term in the simply-typed lambda calculus extended with ints, bools, and tagged unions (slides 36, 62, and 67 define the relevant typing rules):

lambda u:<m:int, n:bool>.
    case u of
        <m=i> => i+4
        <n=j> => if j then 1 else 2

4. Define typing and small-step evaluation rules for ML-style andalso and orelse operators.  Note that these operators are short-circuiting: they do not evaluate their second argument unless necessary.
5. Add a new type to the simply-typed lambda calculus: a map (a.k.a., an association list).  Here are the extensions to the syntax of types and expressions:

t ::= ...
      | map t_key t_val

• the type of maps whose keys are all of type t_key and whose values are all of type t_val

e ::= ...
      | map e_val

• create a new map that maps all keys to (the result of evaluating) e_val
• the type of the keys of the resulting map can be anything; it will be determined by how the map is later used

      | e_map[e_key -> e_val] 

• return a new map that's like (the result of evaluating) e_map except that it maps (the result of evaluating) e_key to (the result of evaluating) e_val

      | e_map[e_key] 

• return the value to which (the result of evaluating) e_key maps in (the result of evaluating) e_map

Here is an example program using this feature (plus a few other simple things like top-level val bindings and strings):

val m:map int string = map "default";   // all keys in m map to "default", by default
print(m[7]);    // prints "default"
val m2 = m[7 -> "seven"];
val m3 = m2[8 -> "eight"];
val m4 = m3[7 -> "second seven"];
print(m4[7]);  // prints "second seven"
print(m4[8]);  // prints "eight"
print(m3[7]);  // prints "seven"
print(m2[7]);  // prints "seven"
print(m[7]);    // prints "default"

1. Extend the syntax of values to represent map values.
2. Specify the big-step call-by-value evaluation rules for this extension.
3. Specify the typing rules for this extension.