\documentstyle{article}
\nofiles
\input{use-full-page}
\input{math-notations}
\input{denotational-semantics}
\input{theorems}

\newcommand{\BETAR}{\BETAREDUCESTO}
\newcommand{\ALPHA}{\ALPHACONVERTSTO}
\newcommand{\ETA}{\ETAREDUCESTO}
\renewcommand{\INTEGER}{{\it Integer}}
\newcommand{\IDENTIFIER}{{\rm Identifier}}
\newcommand{\EXTENDENV}{\mbox{{\rm extend-env}}}
\newcommand{\LOOKUP}{\mbox{lookup}}

\begin{document}
\noindent
\hfill CS 541 --- Programming Languages 1
\hfill \today \\

\begin{center}
{\huge Solutions to Quiz}
\end{center}

The problem is to find the denotation of
\begin{verbatim}
(bind y 4
      (call (proc x (bind y 3 (* y x)))
      y))
\end{verbatim}
using (1) the pass-by-name semantics and (2) the pass-by-denotation semantics
of FL.\\

We use the following lemmas below.

\begin{lemma}
For all $u \in \ENVIRONMENT$,
$$\DENEXPRESSION{{\tt 4}}u = \INJECTION{\VALUE}(\INJECTION{\INTEGER}(4)),$$
and $$\DENEXPRESSION{{\tt 3}}u = \INJECTION{\VALUE}(\INJECTION{\INTEGER}(3)).$$
\end{lemma}

\PROOF
	The proof is left as an exercise for the reader. \\
\QED

\begin{lemma}
For all $u \in \ENVIRONMENT$,
for all $I \in \IDENTIFIER$,
for all $d \in \DENOTABLE$,
$$\LOOKUP (\EXTENDENV \: u \: \synbracket{I} \: d) \: \synbracket{I}
	= \INJECTION{\DENOTABLE}(d).$$
\end{lemma}

\PROOF
The left-hand side reduces to 
$\IFEXP{(\fun{same-identifier?} \: \synbracket{I} \: \synbracket{I})}{
			\INJECTION{\DENOTABLE}(d)}{
			u \: \synbracket{I}}$,
as shown in the calculation below.
This in turn is equal to the right-hand side, by the definition
of $\fun{same-identifier?}$ (assumed) and if-expressions (from Schmidt).

\begin{eqnarray*}
\lefteqn{\LOOKUP (\EXTENDENV \: u \: \synbracket{I} \: d) \: \synbracket{I}} \\
& \equiv & (\LAMBDA{u} u) (\EXTENDENV \: u \: \synbracket{I} \: d)
	 \: \synbracket{I} \\
& \BETAR & (\EXTENDENV \: u \: \synbracket{I} \: d) \: \synbracket{I} \\
& \equiv & ((\LAMBDA{u} \LAMBDA{I} \LAMBDA{d} \LAMBDA{I'}
		\IFEXP{(\fun{same-identifier?} \: I \: I')}{
			\INJECTION{\DENOTABLE}(d)}{
			u \: I'})
	     \: u \: \synbracket{I} \: d) \: \synbracket{I} \\
& \BETAR & ((\LAMBDA{I} \LAMBDA{d} \LAMBDA{I'}
		\IFEXP{(\fun{same-identifier?} \: I \: I')}{
			\INJECTION{\DENOTABLE}(d)}{
			u \: I'})
	     \: \synbracket{I} \: d) \: \synbracket{I} \\
& \BETAR & ((\LAMBDA{d} \LAMBDA{I'}
		\IFEXP{(\fun{same-identifier?} \: \synbracket{I} \: I')}{
			\INJECTION{\DENOTABLE}(d)}{
			u \: I'})
	      \: d) \: \synbracket{I} \\
& \BETAR & (\LAMBDA{I'}
		\IFEXP{(\fun{same-identifier?} \: \synbracket{I} \: I')}{
			\INJECTION{\DENOTABLE}(d)}{
			u \: I'})
	       \: \synbracket{I} \\
& \BETAR & \IFEXP{(\fun{same-identifier?} \: \synbracket{I} \: \synbracket{I})}{
			\INJECTION{\DENOTABLE}(d)}{
			u \: \synbracket{I}}  \\
& = & \IFEXP{\TT}{\INJECTION{\DENOTABLE}(d)}{u \: \synbracket{I}}  \\
& = & \INJECTION{\DENOTABLE}(d)
\end{eqnarray*}
\QED

A consideration that may bug you about the above is the following.
If $M \BETAR N$ do $M$ and $N$ denote the same function?
That is, how do we get from $M \BETAR N = N'$ to $M = N'$?
Such a step is justified by the the fact that our function definitions
(valuation clauses) only {\em represent\/} functions.
If $M$ and $N$ are convertible, then by definition they represent the
same function
(see Schmidt, page 28).

\newpage

Now, we calculate the denotation of the expression for each parameter-passing
mechanism.
\section{Call-by-name}

First, we have the following lemma for the procedure denotation.
\begin{lemma}
For all $u \in \ENVIRONMENT$, let
$$T = (\LAMBDA{d} \DENEXPRESSION{\mbox{\tt (* y x)}}
		(\EXTENDENV (\EXTENDENV \: u \: \synbracket{{\tt x}} d)
		\synbracket{{\tt y}} \: 
		(\INJECTION{\VALUE}(\INJECTION{\INTEGER}(3))))),$$
so that,
$$\DENEXPRESSION{\mbox{\tt (proc x (bind y 3 (* y x)))}}u =
 		(\INJECTION{\VALUE}(\INJECTION{\PROCEDURE}(T))).$$
\end{lemma}

\PROOF
To start, calculate as follows.
\begin{eqnarray*}
\lefteqn{\DENEXPRESSION{\mbox{\tt (proc x (bind y 3 (* y x)))}}u} \\
& \DEF & (\LAMBDA{u} \INJECTION{\VALUE}(\INJECTION{\PROCEDURE}(
		\LAMBDA{d} \DENEXPRESSION{\mbox{\tt (bind y 3 (* y x))}}
			(\EXTENDENV \: u \synbracket{{\tt x}} \: d)))) u \\
& \BETAR & \INJECTION{\VALUE}(\INJECTION{\PROCEDURE}(
		\LAMBDA{d} \DENEXPRESSION{\mbox{\tt (bind y 3 (* y x))}}
			(\EXTENDENV \: u \synbracket{{\tt x}} \: d))) \\
\end{eqnarray*}
Now compute the denotation of {\tt (bind y 3 (* y x))}.
\begin{tabbing}
mm \= mm \= mm \= mm \= mm \= mm \= \kill
$\DENEXPRESSION{\mbox{\tt (bind y 3 (* y x))}}$ \\
$\DEF$ \> $\LAMBDA{u} \LETHEAD{e_1}{\DENEXPRESSION{{\tt 3}}u}$ \\
\>	\> $\CASEHEAD{e_1}$ \\
\>	\>	\> $\CASE{\ISTEST{\ERROR}()}{\INJECTION{\ERROR}()}$ \\
\>	\>	\> $\CASEELSE \DENEXPRESSION{\mbox{\tt (* y x)}}
			(\EXTENDENV \: u \synbracket{{\tt y}} \: e_1)$ \\
\>	\> $\CASEEND$ \\
$=$ \> $\LAMBDA{u} \LETHEAD{e_1}{(\INJECTION{\VALUE}(\INJECTION{\INTEGER}(3)))}$ \\
\>	\> $\CASEHEAD{e_1}$ \\
\>	\>	\> $\CASE{\ISTEST{\ERROR}()}{\INJECTION{\ERROR}()}$ \\
\>	\>	\> $\CASEELSE \DENEXPRESSION{\mbox{\tt (* y x)}}
			(\EXTENDENV \: u \synbracket{{\tt y}} \: e_1)$ \\
\>	\> $\CASEEND$ \\
$=$ \> $\LAMBDA{u} \DENEXPRESSION{\mbox{\tt (* y x)}}
		(\EXTENDENV \: u \synbracket{{\tt y}} \:
		 (\INJECTION{\VALUE}(\INJECTION{\INTEGER}(3))))$ \\
\end{tabbing}
Therefore, we have,
\begin{eqnarray*}
\lefteqn{\DENEXPRESSION{\mbox{\tt (proc x (bind y 3 (* y x)))}}u} \\
& = & (\INJECTION{\VALUE}(\INJECTION{\PROCEDURE}(
		\LAMBDA{d} (\LAMBDA{u} \DENEXPRESSION{\mbox{\tt (* y x)}}
		(\EXTENDENV \: u \synbracket{{\tt y}} \: 
		(\INJECTION{\VALUE}(\INJECTION{\INTEGER}(3)))))
		(\EXTENDENV \: u \: \synbracket{{\tt x}} d)))) \\
& \BETAR & (\INJECTION{\VALUE}(\INJECTION{\PROCEDURE}(
		\LAMBDA{d} \DENEXPRESSION{\mbox{\tt (* y x)}}
		(\EXTENDENV (\EXTENDENV \: u \: \synbracket{{\tt x}} d)
		\synbracket{{\tt y}} \: 
		(\INJECTION{\VALUE}(\INJECTION{\INTEGER}(3))))))) \\
\end{eqnarray*}
\QED

We know proceed with the calculation of the {\tt call} subexpression, with
$T$ as in the above lemma.

\begin{tabbing}
mm \= mm \= mm \= mm \= mm \= mm \= \kill
$\DENEXPRESSION{\mbox{\tt (call (proc x (bind y 3 (* y x))) y)}}$ \\
$\DEF$ \> $\LAMBDA{u} \CASEHEAD{\DENEXPRESSION{\mbox
		{\tt (proc x (bind y 3 (* y x)))}}u}$ \\
\>	\>	\> $\CASE{\ISTEST{\VALUE}(v_1)}{\CASEHEAD{v_1}}$ \\
\>	\>	\>	\> $\CASE{\ISTEST{\PROCEDURE}(p)}{(p \: (\DENEXPRESSION{
					{\tt y}}u))}$ \\
\>	\>	\>	\> $\CASEELSE \INJECTION{\ERROR}()$ \\
\>	\>	\>	\> $\CASEEND$ \\
\>	\>	\> $\CASESEP \CASE{\ISTEST{\ERROR}()}{\INJECTION{\ERROR}()}$ \\
\>	\>	\> $\CASEEND$ \\
$=$ 	\> $\LAMBDA{u} \CASEHEAD{
		(\INJECTION{\VALUE}(\INJECTION{\PROCEDURE}(T)))}$ \\
\>	\>	\> $\CASE{\ISTEST{\VALUE}(v_1)}{\CASEHEAD{v_1}}$ \\
\>	\>	\>	\> $\CASE{\ISTEST{\PROCEDURE}(p)}{(p \: (\DENEXPRESSION{
					{\tt y}}u))}$ \\
\>	\>	\>	\> $\CASEELSE \INJECTION{\ERROR}()$ \\
\>	\>	\>	\> $\CASEEND$ \\
\>	\>	\> $\CASESEP \CASE{\ISTEST{\ERROR}()}{\INJECTION{\ERROR}()}$ \\
\>	\>	\> $\CASEEND$ \\
$=$ 	\> $\LAMBDA{u} {\CASEHEAD{(\INJECTION{\PROCEDURE}(T))}}$ \\
\>	\>	\> $\CASE{\ISTEST{\PROCEDURE}(p)}{(p \: (\DENEXPRESSION{
					{\tt y}}u))}$ \\
\>	\>	\> $\CASEELSE \INJECTION{\ERROR}()$ \\
\>	\>	\> $\CASEEND$ \\
$=$	\> $\LAMBDA{u} (T \: (\DENEXPRESSION{{\tt y}}u))$ \\
\end{tabbing}
Finally,
\begin{tabbing}
mm \= mm \= mm \= mm \= mm \= mm \= \kill
$\DENEXPRESSION{\mbox{\tt (bind y 4 (call (proc x (bind y 3 (* y x))) y))}}$ \\
$\DEF$ \> $\LAMBDA{u} \LETHEAD{e_1}{\DENEXPRESSION{{\tt 4}}u}$ \\
\>	\> $\CASEHEAD{e_1}$ \\
\>	\>	\> $\CASE{\ISTEST{\ERROR}()}{\INJECTION{\ERROR}()}$ \\
\>	\>	\> $\CASEELSE \DENEXPRESSION{\mbox{
			{\tt (call (proc x (bind y 3 (* y x))) y)}}}
			(\EXTENDENV \: u \synbracket{{\tt y}} \: e_1)$ \\
\>	\> $\CASEEND$ \\
$\ALPHA$ \> $\LAMBDA{u'} \LETHEAD{e_1}{\DENEXPRESSION{{\tt 4}}u'}$ \\
\>	\> $\CASEHEAD{e_1}$ \\
\>	\>	\> $\CASE{\ISTEST{\ERROR}()}{\INJECTION{\ERROR}()}$ \\
\>	\>	\> $\CASEELSE \DENEXPRESSION{\mbox{
			{\tt (call (proc x (bind y 3 (* y x))) y)}}}
			(\EXTENDENV \: u' \synbracket{{\tt y}} \: e_1)$ \\
\>	\> $\CASEEND$ \\
$=$ \> $\LAMBDA{u'} \LETHEAD{e_1}{(\INJECTION{\VALUE}(\INJECTION{\INTEGER}(4)))}$\\
\>	\> $\CASEHEAD{e_1}$ \\
\>	\>	\> $\CASE{\ISTEST{\ERROR}()}{\INJECTION{\ERROR}()}$ \\
\>	\>	\> $\CASEELSE (\LAMBDA{u} (T \: (\DENEXPRESSION{{\tt y}}u)))
			(\EXTENDENV \: u' \synbracket{{\tt y}} \: e_1)$ \\
\>	\> $\CASEEND$ \\
$=$ \> $\LAMBDA{u'} (\LAMBDA{u} (T \: (\DENEXPRESSION{{\tt y}}u)))
		(\EXTENDENV \: u' \synbracket{{\tt y}} \:
		 (\INJECTION{\VALUE}(\INJECTION{\INTEGER}(4))))$ \\
$\BETAR$ \> $\LAMBDA{u'} (T \: (\DENEXPRESSION{{\tt y}}
		 (\EXTENDENV \: u' \synbracket{{\tt y}} \:
		 (\INJECTION{\VALUE}(\INJECTION{\INTEGER}(4))))))$ \\
\end{tabbing}

To get the value of {\tt y} out of the environment, we use the following lemma.

\begin{lemma}
For all $u' \in \ENVIRONMENT$, and for all $n \in \INTEGER$,
$$(\DENEXPRESSION{{\tt y}}) (\EXTENDENV \: u'
\synbracket{{\tt y}} \: (\INJECTION{\VALUE}(\INJECTION{\INTEGER}(n))))
= (\INJECTION{\VALUE}(\INJECTION{\INTEGER}(n)))$$
\end{lemma}

\PROOF
	The proof is left as an exercise for the reader.\\
\QED \\

Putting all of the above together, we obtain,
\begin{tabbing}
mm \= mm \= mm \= mm \= mm \= mm \= \kill
$\DENEXPRESSION{\mbox{\tt (bind y 4 (call (proc x (bind y 3 (* y x))) y))}}$ \\
$=$ \> $\LAMBDA{u'} (T \: (\INJECTION{\VALUE}(\INJECTION{\INTEGER}(4))))$ \\
$=$ \> $\LAMBDA{u'} ((\LAMBDA{d} \DENEXPRESSION{\mbox{\tt (* y x)}}
		(\EXTENDENV (\EXTENDENV \: u \: \synbracket{{\tt x}} d)
		\synbracket{{\tt y}} \: 
		(\INJECTION{\VALUE}(\INJECTION{\INTEGER}(3))))) \:
		(\INJECTION{\VALUE}(\INJECTION{\INTEGER}(4)))) $ \\
$\BETAR$ \> $\LAMBDA{u'} (\DENEXPRESSION{\mbox{\tt (* y x)}}
		(\EXTENDENV (\EXTENDENV \: u \: \synbracket{{\tt x}}
		(\INJECTION{\VALUE}(\INJECTION{\INTEGER}(4))))
		\synbracket{{\tt y}} \: 
		(\INJECTION{\VALUE}(\INJECTION{\INTEGER}(3))))) $ \\
$\Rightarrow^*$ \> $(\INJECTION{\VALUE}(\INJECTION{\INTEGER}(7))) $ \\
\>	\>	\>	\>	\> 
	(Using the lemma above, the definition of
		$\DENEXPRESSION{({\rm A} \: {\rm E}_1 \: {\rm E}_2)}$, and
		${\cal A}\synbracket{+}$) \\
\end{tabbing}
\newpage

\section{Call-by-denotation}

{\em Note:\/}~~ For call-by-denotation, there should be another change made to
	the original semantics of FL.  The denotation of {\tt bind} needs to
	be changed too!  The revised clause for {\tt bind} is as follows.
	Do you see why (hint:~ check the types)?
\begin{tabbing}
mm \= mm \= mm \= mm \= mm \= mm \= mm \= \kill
$\DENEXPRESSION{({\tt bind} \: {\rm I} \: {\rm E}_1 \: {\rm E}_2)} = 
	\LAMBDA{u} \LETHEAD{e_1}{\DENEXPRESSION{{\rm E}_1}u}$ \\
\>	\>	\>	\>	\>	\> $\CASEHEAD{e_1}$ \\
\>	\>	\>	\>	\>	\>	\> $\CASE{\ISTEST{\ERROR}()}
					{\INJECTION{\ERROR}()}$ \\
\>	\>	\>	\>	\>	\>	\> $\CASEELSE \DENEXPRESSION{{\rm E}_1}
					(\EXTENDENV \: u \synbracket{{\rm I}} \:
					(\LAMBDA{u} e_1))$ \\
\>	\>	\>	\>	\>	\> $\CASEEND$ \\
\end{tabbing}

As above, we first calculate the denotation of the procedure.

\begin{lemma}
For all $u \in \ENVIRONMENT$, let
$$T = (\LAMBDA{d} \DENEXPRESSION{\mbox{\tt (* y x)}}
		(\EXTENDENV (\EXTENDENV \: u \: \synbracket{{\tt x}} d)
		\synbracket{{\tt y}} \: 
		(\LAMBDA{u} 
		(\INJECTION{\VALUE}(\INJECTION{\INTEGER}(3)))))),$$
so that,
$$\DENEXPRESSION{\mbox{\tt (proc x (bind y 3 (* y x)))}}u =
 		(\INJECTION{\VALUE}(\INJECTION{\PROCEDURE}(T))).$$
\end{lemma}

\PROOF
To start, calculate as follows.
\begin{eqnarray*}
\lefteqn{\DENEXPRESSION{\mbox{\tt (proc x (bind y 3 (* y x)))}}u} \\
& \DEF & (\LAMBDA{u} \INJECTION{\VALUE}(\INJECTION{\PROCEDURE}(
		\LAMBDA{d} \DENEXPRESSION{\mbox{\tt (bind y 3 (* y x))}}
			(\EXTENDENV \: u \synbracket{{\tt x}} \: d)))) u \\
& \BETAR & \INJECTION{\VALUE}(\INJECTION{\PROCEDURE}(
		\LAMBDA{d} \DENEXPRESSION{\mbox{\tt (bind y 3 (* y x))}}
			(\EXTENDENV \: u \synbracket{{\tt x}} \: d))) \\
\end{eqnarray*}
Now compute the denotation of {\tt (bind y 3 (* y x))}.
\begin{tabbing}
mm \= mm \= mm \= mm \= mm \= mm \= \kill
$\DENEXPRESSION{\mbox{\tt (bind y 3 (* y x))}}$ \\
$\DEF$ \> $\LAMBDA{u} \LETHEAD{e_1}{\DENEXPRESSION{{\tt 3}}u}$ \\
\>	\> $\CASEHEAD{e_1}$ \\
\>	\>	\> $\CASE{\ISTEST{\ERROR}()}{\INJECTION{\ERROR}()}$ \\
\>	\>	\> $\CASEELSE \DENEXPRESSION{\mbox{\tt (* y x)}}
			(\EXTENDENV \: u \synbracket{{\tt y}} \: 
				(\LAMBDA{u} e_1))$ \\
\>	\> $\CASEEND$ \\
$=$ \> $\LAMBDA{u} \LETHEAD{e_1}{(\INJECTION{\VALUE}(\INJECTION{\INTEGER}(3)))}$ \\
\>	\> $\CASEHEAD{e_1}$ \\
\>	\>	\> $\CASE{\ISTEST{\ERROR}()}{\INJECTION{\ERROR}()}$ \\
\>	\>	\> $\CASEELSE \DENEXPRESSION{\mbox{\tt (* y x)}}
			(\EXTENDENV \: u \synbracket{{\tt y}} \:
				(\LAMBDA{u} e_1))$ \\
\>	\> $\CASEEND$ \\
$=$ \> $\LAMBDA{u} \DENEXPRESSION{\mbox{\tt (* y x)}}
		(\EXTENDENV \: u \synbracket{{\tt y}} \:
		 (\LAMBDA{u} (\INJECTION{\VALUE}(\INJECTION{\INTEGER}(3)))))$\\
\end{tabbing}
Therefore, we have,
\begin{eqnarray*}
\lefteqn{\DENEXPRESSION{\mbox{\tt (proc x (bind y 3 (* y x)))}}u} \\
& = & (\INJECTION{\VALUE}(\INJECTION{\PROCEDURE}(
		\LAMBDA{d} (\LAMBDA{u} \DENEXPRESSION{\mbox{\tt (* y x)}}
		(\EXTENDENV \: u \synbracket{{\tt y}} \: 
		(\LAMBDA{u} (\INJECTION{\VALUE}(\INJECTION{\INTEGER}(3))))))
		(\EXTENDENV \: u \: \synbracket{{\tt x}} d)))) \\
& \BETAR & (\INJECTION{\VALUE}(\INJECTION{\PROCEDURE}(
		\LAMBDA{d} \DENEXPRESSION{\mbox{\tt (* y x)}}
		(\EXTENDENV (\EXTENDENV \: u \: \synbracket{{\tt x}} d)
		\synbracket{{\tt y}} \: 
		(\LAMBDA{u} 
			(\INJECTION{\VALUE}(\INJECTION{\INTEGER}(3)))))))) \\
\end{eqnarray*}
\QED

Again, let $T$ be as in the above lemma.  We now calculate the denotation of
the {\tt call}.

\begin{tabbing}
mm \= mm \= mm \= mm \= mm \= mm \= \kill
$\DENEXPRESSION{\mbox{\tt (call (proc x (bind y 3 (* y x))) y)}}$ \\
$\DEF$ \> $\LAMBDA{u} \CASEHEAD{\DENEXPRESSION{\mbox
		{\tt (proc x (bind y 3 (* y x)))}}u}$ \\
\>	\>	\> $\CASE{\ISTEST{\VALUE}(v_1)}{\CASEHEAD{v_1}}$ \\
\>	\>	\>	\> $\CASE{\ISTEST{\PROCEDURE}(p)}{(p \: (\DENEXPRESSION{
					{\tt y}}))}$ \\
\>	\>	\>	\> $\CASEELSE \INJECTION{\ERROR}()$ \\
\>	\>	\>	\> $\CASEEND$ \\
\>	\>	\> $\CASESEP \CASE{\ISTEST{\ERROR}()}{\INJECTION{\ERROR}()}$ \\
\>	\>	\> $\CASEEND$ \\
$=$ 	\> $\LAMBDA{u} \CASEHEAD{
		(\INJECTION{\VALUE}(\INJECTION{\PROCEDURE}(T)))}$ \\
\>	\>	\> $\CASE{\ISTEST{\VALUE}(v_1)}{\CASEHEAD{v_1}}$ \\
\>	\>	\>	\> $\CASE{\ISTEST{\PROCEDURE}(p)}{(p \: (\DENEXPRESSION{
					{\tt y}}))}$ \\
\>	\>	\>	\> $\CASEELSE \INJECTION{\ERROR}()$ \\
\>	\>	\>	\> $\CASEEND$ \\
\>	\>	\> $\CASESEP \CASE{\ISTEST{\ERROR}()}{\INJECTION{\ERROR}()}$ \\
\>	\>	\> $\CASEEND$ \\
$=$ 	\> $\LAMBDA{u} {\CASEHEAD{(\INJECTION{\PROCEDURE}(T))}}$ \\
\>	\>	\> $\CASE{\ISTEST{\PROCEDURE}(p)}{(p \: (\DENEXPRESSION{
					{\tt y}}))}$ \\
\>	\>	\> $\CASEELSE \INJECTION{\ERROR}()$ \\
\>	\>	\> $\CASEEND$ \\
$=$	\> $\LAMBDA{u} (T \: (\DENEXPRESSION{{\tt y}}))$ \\
\end{tabbing}
Finally, we calculate the denotation of the whole expression.
\begin{tabbing}
mm \= mm \= mm \= mm \= mm \= mm \= \kill
$\DENEXPRESSION{\mbox{\tt (bind y 4 (call (proc x (bind y 3 (* y x))) y))}}$ \\
$\DEF$ \> $\LAMBDA{u} \LETHEAD{e_1}{\DENEXPRESSION{{\tt 4}}u}$ \\
\>	\> $\CASEHEAD{e_1}$ \\
\>	\>	\> $\CASE{\ISTEST{\ERROR}()}{\INJECTION{\ERROR}()}$ \\
\>	\>	\> $\CASEELSE \DENEXPRESSION{\mbox{
			{\tt (call (proc x (bind y 3 (* y x))) y)}}}
			(\EXTENDENV \: u \synbracket{{\tt y}} \: 
				(\LAMBDA{u} e_1))$ \\
\>	\> $\CASEEND$ \\
$\ALPHA$ \> $\LAMBDA{u'} \LETHEAD{e_1}{\DENEXPRESSION{{\tt 4}}u'}$ \\
\>	\> $\CASEHEAD{e_1}$ \\
\>	\>	\> $\CASE{\ISTEST{\ERROR}()}{\INJECTION{\ERROR}()}$ \\
\>	\>	\> $\CASEELSE \DENEXPRESSION{\mbox{
			{\tt (call (proc x (bind y 3 (* y x))) y)}}}
			(\EXTENDENV \: u' \synbracket{{\tt y}} \:
				(\LAMBDA{u} e_1))$ \\
\>	\> $\CASEEND$ \\
$=$ \> $\LAMBDA{u'} \LETHEAD{e_1}{(\INJECTION{\VALUE}(\INJECTION{\INTEGER}(4)))}$\\
\>	\> $\CASEHEAD{e_1}$ \\
\>	\>	\> $\CASE{\ISTEST{\ERROR}()}{\INJECTION{\ERROR}()}$ \\
\>	\>	\> $\CASEELSE (\LAMBDA{u} (T \: (\DENEXPRESSION{{\tt y}})))
			(\EXTENDENV \: u' \synbracket{{\tt y}} \:
				(\LAMBDA{u} e_1))$ \\
\>	\> $\CASEEND$ \\
$=$ \> $\LAMBDA{u'} (\LAMBDA{u} (T \: (\DENEXPRESSION{{\tt y}})))
		(\EXTENDENV \: u' \synbracket{{\tt y}} \:
		 (\LAMBDA{u} (\INJECTION{\VALUE}(\INJECTION{\INTEGER}(4)))))$ \\
$\BETAR$ \> $\LAMBDA{u'} (T \: (\DENEXPRESSION{{\tt y}}))$ \\
$=$ \> $\LAMBDA{u'} ((\LAMBDA{d} \DENEXPRESSION{\mbox{\tt (* y x)}}
		(\EXTENDENV (\EXTENDENV \: u \: \synbracket{{\tt x}} d)
		\synbracket{{\tt y}} \: 
		(\LAMBDA{u} (\INJECTION{\VALUE}(\INJECTION{\INTEGER}(3)))))) \:
	(\DENEXPRESSION{{\tt y}})) $ \\
$\BETAR$ \> $\LAMBDA{u'} (\DENEXPRESSION{\mbox{\tt (* y x)}}
		(\EXTENDENV (\EXTENDENV \: u \: \synbracket{{\tt x}}
			(\DENEXPRESSION{{\tt y}}))
		\synbracket{{\tt y}} \: 
		(\LAMBDA{u} (\INJECTION{\VALUE}(\INJECTION{\INTEGER}(3))))))$ \\
$\Rightarrow^*$ \> $(\INJECTION{\VALUE}(\INJECTION{\INTEGER}(6))) $ \\
\>	\>	\>	\>	\> 
	(Using the lemmas below, the definition of
		$\DENEXPRESSION{({\rm A} \: {\rm E}_1 \: {\rm E}_2)}$, and
		${\cal A}\synbracket{+}$)
\end{tabbing}

To get the value of {\tt y} out of the environment, we use the following lemma.

\begin{lemma}
For all $u' \in \ENVIRONMENT$, for all $n \in \INTEGER$,
$$(\DENEXPRESSION{{\tt y}}) (\EXTENDENV \: u'
\synbracket{{\tt y}} \: (\INJECTION{\VALUE}(\INJECTION{\INTEGER}(n)))) =
	(\LAMBDA{u} (\INJECTION{\VALUE}(\INJECTION{\INTEGER}(n)))) $$
\end{lemma}

\PROOF
	The proof is left as an exercise for the reader.\\
\QED

Since {\tt x} is bound to the denotation of {\tt y} ($\DENEXPRESSION{{\tt y}}$)
in the above environment, 
and call-by-denotation is dynamic scoping, we have the following lemma.

\begin{lemma}
For all $u \in \ENVIRONMENT$, for all $n \in \INTEGER$,
$$(\DENEXPRESSION{{\tt x}}) (\EXTENDENV (\EXTENDENV \: u \: \synbracket{{\tt x}}
		(\DENEXPRESSION{{\tt y}})) \synbracket{{\tt y}} \: 
		(\LAMBDA{u} (\INJECTION{\VALUE}(\INJECTION{\INTEGER}(n))))) =$$
$$(\DENEXPRESSION{{\tt y}}) (\EXTENDENV (\EXTENDENV \: u \: \synbracket{{\tt x}}
		(\DENEXPRESSION{{\tt y}})) \synbracket{{\tt y}} \: 
		(\LAMBDA{u} (\INJECTION{\VALUE}(\INJECTION{\INTEGER}(n))))) =$$
$$ (\INJECTION{\VALUE}(\INJECTION{\INTEGER}(n))) $$
\end{lemma}

\PROOF
	The proof is left as an exercise for the reader.\\
\QED

\end{document}