In this lecture we make more precise the ideas we sketched last time. We define the concept of an environment and a closure, and then we write a semantic function, eval, which characterizes an eager semantics equivalent to the eager substitution semantics (call-by-value rewrite or natural semantics).
Definition
These are mutually recursive types. We could define them
precisely using pairs of types defined inductively. That is, we
define and form
where
Exercise: Write the induction principle for this type and give rules for creating elements.
Recall the list operations.
Definition
We write to construct a new list from
and
. Note
gives the first element of
and
the rest.
Definition
Now we define an evaluation relation that uses the environment.
Definition eval is a partial function from
into Closures defined recursively by cases on
.
Example
Here is the example from the last lecture done carefully. Notice that we start with a closed lambda term and the empty environment.
Key Line, matches informal explanation
let
Key
Line