The purpose of this lab is to verify that we understand the necessity of closures for the implementation of the lexical scoping in the environment model. The following is a restatement of the \lambda-calculus^+, as seen in lecture.
\begin{align*}
e &::= x \ | \ \lambda x. e \ | \ e e \ | \ \texttt{let} \ x \ \texttt{=} \ e \ \texttt{in} \ e \\
x &::= \texttt{a} \ | \ \texttt{b} \ | \ \dots \ | \ \texttt{y} \ | \ \texttt{z}
\end{align*}
\begin{align*}
\frac
{(x, v) \in \mathcal E}
{
\langle \ \mathcal E \ , \ x \ \rangle \Downarrow \mathcal E(x)
}
\text{ (varEval)}
\qquad
\frac
{}
{\langle \ \mathcal E \ , \ \lambda x . e \ \rangle \Downarrow (\mathcal E, \lambda x . e) }
\text{ (funEval)}
\end{align*}
\begin{align*}
\frac
{
\langle \mathcal E \ , \ e_1 \ \rangle \Downarrow (\mathcal E', \lambda x . e) \qquad
\langle \mathcal E \ , \ e_2 \ \rangle \Downarrow v_2 \qquad
\langle \mathcal E'[x \mapsto v_2] \ , \ e \rangle \Downarrow v
}
{\langle \mathcal E \ , \ e_1 e_2 \ \rangle \Downarrow v}
\text{ (appEval)}
\end{align*}
You'll notice that we didn't include the semantic rule for let-expressions. Write down the \text{letEval} rule based on your understanding of how let-expressions work.
Describe how to represent an expression in the \lambda-calculus^+ (with let-expressions) as an expression in the \lambda-calculus proper, i.e., with no let-expressions. The resulting expression should be equivalent with respect to the semantics. This means it must evaluate to the same value as it would have had we included the \text{letEval} rule and evaluated it directly.
Suppose we changed the \text{appEval} rule so that it doesn't use the environment contained in the closure:
\begin{align*}
\frac
{
\langle \mathcal E \ , \ e_1 \ \rangle \Downarrow (\mathcal E', \lambda x . e) \qquad
\langle \mathcal E \ , \ e_2 \ \rangle \Downarrow v_2 \qquad
\langle \textcolor{red}{\mathcal E}[x \mapsto v_2] \ , \ e \rangle \Downarrow v
}
{\langle \mathcal E \ , \ e_1 e_2 \ \rangle \Downarrow v}
\text{ (appEval*)}
\end{align*}
We've seen many examples of expressions which do not evaluate─or evaluate to the wrong value─if we use the \text{appEval*} rule. But all of these examples have depended on shadowing, i.e., the ability to reuse a name in a variable binding.
Give an example of a closed expression in the \lambda-calculus^+ that:
\text{appEval} rule;\text{appEval*} rule;Give an example of an expression in the \lambda-calculus^+ that:
\text{appEval} rule;\text{appEval*} rule;