%\vfill\eject
\section{Formal semantics}
\label{formalsemanticssection}

\bgroup

\newcommand{\sembrack}[1]{[\![#1]\!]}
\newcommand{\fun}[1]{\hbox{\it #1}}
\newenvironment{semfun}{\begin{tabbing}$}{$\end{tabbing}}
\newcommand\LOC{{\tt{}L}}
\newcommand\NAT{{\tt{}N}}
\newcommand\TRU{{\tt{}T}}
\newcommand\SYM{{\tt{}Q}}
\newcommand\CHR{{\tt{}H}}
\newcommand\NUM{{\tt{}R}}
\newcommand\FUN{{\tt{}F}}
\newcommand\EXP{{\tt{}E}}
\newcommand\STV{{\tt{}E}}
\newcommand\STO{{\tt{}S}}
\newcommand\ENV{{\tt{}U}}
\newcommand\ANS{{\tt{}A}}
\newcommand\ERR{{\tt{}X}}
\newcommand\EC{{\tt{}K}}
\newcommand\CC{{\tt{}C}}
\newcommand\MSC{{\tt{}M}}
\newcommand\PAI{\hbox{\EXP$_{\rm p}$}}
\newcommand\VEC{\hbox{\EXP$_{\rm v}$}}
\newcommand\STR{\hbox{\EXP$_{\rm s}$}}

\newcommand\elt{\downarrow}
\newcommand\drop{\dagger}
%\newcommand\injekt{\hbox{ \rm in }}
%\newcommand\projekt{\,\vert\,}

This section provides a formal denotational semantics for the primitive
expressions of Scheme and selected built-in procedures.  The concepts
and notation used here are described in~\cite{Stoy77}; the notation is
summarized below:

\begin{tabular}{ll}
$\langle\,\ldots\,\rangle$ & sequence formation \\
$s \elt k$	           & $k$th member of the sequence $s$ (1-based) \\
$\#s$			   & length of sequence $s$ \\
$s \:\S\: t$	           & concatenation of sequences $s$ and $t$ \\
$s \drop k$                & drop the first $k$ members of sequence $s$ \\
$t \rightarrow a, b$       & McCarthy conditional ``if $t$ then $a$ else $b$'' \\
$\rho[x/i]$	           & substitution ``$\rho$ with $x$ for $i$'' \\
$x\hbox{ \rm in }{\tt{}D}$         & injection of $x$ into domain ${\tt{}D}$ \\
$x\,\vert\,{\tt{}D}$	   & projection of $x$ to domain ${\tt{}D}$
\end{tabular}

To avoid special treatment for a top-level environment, the semantics
assumes that environments assign locations to all variables.

The reason that expression continuations take sequences of values instead
of single values is to simplify the formal treatment of procedure calls
and to make it easy to add multiple return values.

The order of evaluation within a call is unspecified.  We mimic that
here by applying arbitrary permutations {\it permute} and {\it
unpermute}, which must be inverses, to the arguments in a call before
and after they are evaluated.  This still requires that the order of
evaluation be constant throughout a program (for any given number of
arguments), but it is a closer approximation to the intended semantics
than a left-to-right evaluation would be.

The storage allocator {\it new} is implementation-dependent, but it must
obey the following axiom:  if \hbox{$\fun{new}\:\sigma\:\elem\:\LOC$}, then
$\sigma\:(\fun{new}\:\sigma\:\vert\:\LOC)\elt 2 = {\it false}$.


The semantics in this section was translated by machine from an
executable version of the semantics written in Scheme itself.


\subsection{Abstract syntax}

\def\K{\hbox{\rm K}}
\def\I{\hbox{\rm I}}
\def\E{\hbox{\rm E}}
\def\C{\hbox{$\Gamma$}}
\def\Con{\hbox{\rm Con}}
\def\Ide{\hbox{\rm Ide}}
\def\Exp{\hbox{\rm Exp}}
\def\Com{\hbox{\rm Com}}
\def\|{$\vert$}

\begin{tabular}{r@{ }c@{ }l@{\qquad}l}
\K & \elem & \Con & constants, including quotations \\
\I & \elem & \Ide & identifiers (variables) \\
\E & \elem & \Exp & expressions\\
\C & \elem & \Com{} $=$ \Exp & commands
\end{tabular}

\setbox0=\hbox{\tt\Exp{} \goesto{}}  %\tt for spacing
\setbox1=\hbox to 1\wd0{\hfil \|}
\begin{grammar}
\Exp{} \goesto{} \K{} \| \I{} \| (\E$_0$ \arbno{\E})
 \copy1{} (lambda (\arbno{\I}) \arbno{\C} \E$_0$)
 \copy1{} (lambda (\arbno{\I} {\bf.}\ \I) \arbno{\C} \E$_0$)
 \copy1{} (lambda \I{} \arbno{\C} \E$_0$)
 \copy1{} (if \E$_0$ \E$_1$ \E$_2$) \| (if \E$_0$ \E$_1$)
 \copy1{} (set! \I{} \E)
\end{grammar}

\subsection{Domain equations}

\begin{tabular}{@{}r@{ }c@{ }l@{ }l@{ }ll}
$\alpha$   & \elem & \LOC & &          & locations \\
$\nu$      & \elem & \NAT & &          & natural numbers \\
           &       & \TRU &=& $\{$\it false, true$\}$ & booleans \\
           &       & \SYM & &          & symbols \\
           &       & \CHR & &          & characters \\
           &       & \NUM & &          & numbers \\
           &       & \PAI &=& $\LOC \times \LOC$  & pairs \\
           &       & \VEC &=& $\arbno{\LOC}$ & vectors \\
           &       & \STR &=& $\arbno{\LOC}$ & strings \\
	   &	   & \MSC &=& \makebox[0pt][l]{$\{$\it false, true, 
                                null, undefined, unspecified$\}$} \\
	   &	   &	  & &          & miscellaneous \\
$\phi$     & \elem & \FUN &=& $\LOC\times(\arbno{\EXP} \to \EC \to \CC)$
                                       & procedure values \\
$\epsilon$ & \elem & \EXP &=& \makebox[0pt][l]{$\SYM+\CHR+\NUM+\PAI+\VEC+\STR+\MSC+\FUN$}\\
	   &	   &	  & &          & expressed values \\
%          &       & \STV &=& \EXP     & stored values \\
$\sigma$   & \elem & \STO &=& $\LOC\to(\STV\times\TRU)$ & stores \\
$\rho$	   & \elem & \ENV &=& $\Ide\to\LOC$  & environments \\
$\theta$   & \elem & \CC  &=& $\STO\to\ANS$  & command continuations \\
$\kappa$   & \elem & \EC  &=& $\arbno{\EXP}\to\CC$ & expression continuations \\
	   &	   & \ANS & &		     & answers \\
	   &	   & \ERR & &		     & errors
\end{tabular}

\subsection{Semantic functions}

\def\Ksem{\hbox{$\cal K$}}
\def\Esem{\hbox{$\cal E$}}
\def\Csem{\hbox{$\cal C$}}

\begin{tabular}{@{}r@{ }l}
  $\Ksem:$ & $\Con\to\EXP$  \\
  $\Esem:$ & $\Exp\to\ENV\to\EC\to\CC$ \\
$\arbno{\Esem}:$ & $\arbno{\Exp}\to\ENV\to\EC\to\CC$ \\
  $\Csem:$ & $\arbno{\Com}\to\ENV\to\CC\to\CC$
\end{tabular}


% thin \,  medium \> [or \:]   thick \;

\renewcommand{\:}{\mskip\medmuskip}
\newcommand{\wrong}[1]{\fun{wrong }\hbox{\rm``#1''}}
\newcommand{\go}[1]{\hbox{\hspace*{#1em}}}

\bgroup\small

\vspace{1ex}

Definition of \Ksem{} deliberately omitted.

\begin{semfun}
\Esem\sembrack{\K} =
  \lambda\rho\kappa\:.\:\fun{send}\,(\Ksem\sembrack{\K})\,\kappa
\end{semfun}

\begin{semfun}
\Esem\sembrack{\I} = 
  \lambda\rho\kappa\:.\:\fun{hold}\:
    $\=$(\fun{lookup}\:\rho\:\I)$\\
     \>$(\fun{single}(\lambda\epsilon\:.\:
        $\=$\epsilon = \fun{undefined}\rightarrow$\\
     \>  \> \go{2}$\wrong{undefined variable},$\\
     \>  \>\go{1}$\fun{send}\:\epsilon\:\kappa))
\end{semfun}

\begin{semfun}
\Esem\sembrack{\hbox{\tt($\E_0$ \arbno{\E})}} =$\\
 \go{1}$\lambda\rho\kappa\:.\:\arbno{\Esem}
    $\=$(\fun{permute}(\langle\E_0\rangle\:\S\:\arbno{\E}))$\\
     \>$\rho\:$\\
     \>$(\lambda\arbno{\epsilon}\:.\:
        ($\=$(\lambda\arbno{\epsilon}\:.\:
                 \fun{applicate}\:(\arbno{\epsilon}\elt 1)
	 			\:(\arbno{\epsilon}\drop 1)
				\:\kappa)$\\
     \>   \>$(\fun{unpermute}\:\arbno{\epsilon})))
\end{semfun}

\begin{semfun}
\Esem\sembrack{\hbox{\tt(\ide{lambda} (\arbno{\I}) \arbno{\C} $\E_0$)}} =$\\
 \go{1}$\lambda\rho\kappa\:.\:\lambda\sigma\:.\:$\\
  \go{2}$\fun{new}\:\sigma\:\elem\:\LOC\rightarrow$\\
   \go{3}$\fun{send}\:
     $\=$(\langle
         $\=$\fun{new}\:\sigma\,\vert\,\LOC,$\\
      \>  \>$\lambda\arbno{\epsilon}\kappa^\prime\:.\:
	       $\=$\#\arbno{\epsilon} = \#{\arbno{\I}}\rightarrow$\\
      \>  \>    \>$\go{1}\fun{tievals}
		   $\=$(\lambda\arbno{\alpha}\:.\:
			 $\=$(\lambda\rho^\prime\:.\:\Csem\sembrack{\arbno{\C}}\rho^\prime
			      (\Esem\sembrack{\E_0}\rho^\prime\kappa^\prime))$\\
      \>  \>    \>  \>    \>$(\fun{extends}\:\rho\:{\arbno{\I}}\:\arbno{\alpha}))$\\
      \>  \>	\>  \>$\arbno{\epsilon},$\\
      \>  \>    \>\go{1}$\wrong{wrong number of arguments}\rangle$\\
      \>  \>$\hbox{ \rm in }\EXP)$\\
      \>$\kappa$\\
      \>$(\fun{update}\:(\fun{new}\:\sigma\,\vert\,\LOC)
	                   \:\fun{unspecified}
			   \:\sigma),$\\
  \go{3}$\wrong{out of memory}\:\sigma
\end{semfun}

\begin{semfun}
\Esem\sembrack{\hbox{\tt(lambda (\arbno{\I} {\bf.}\ \I) \arbno{\C} $\E_0$)}} =$\\
 \go{1}$\lambda\rho\kappa\:.\:\lambda\sigma\:.\:$\\
  \go{2}$\fun{new}\:\sigma\:\elem\:\LOC\rightarrow$\\
   \go{3}$\fun{send}\:
     $\=$(\langle
         $\=$\fun{new}\:\sigma\,\vert\,\LOC,$\\
      \>  \>$\lambda\arbno{\epsilon}\kappa^\prime\:.\:
	       $\=$\#\arbno{\epsilon} \geq \#\arbno{\I}\rightarrow$\\
      \>  \>    \>\go{1}$\fun{tievalsrest}$\\
      \>  \>	\>\go{2}\=$(\lambda\arbno{\alpha}\:.\:
			   $\=$(\lambda\rho^\prime\:.\:\Csem\sembrack{\arbno{\C}}\rho^\prime
			       (\Esem\sembrack{\E_0}\rho^\prime\kappa^\prime))$\\
      \>  \>    \>       \> \>$(\fun{extends}\:\rho
			       \:(\arbno{\I}\:\S\:\langle\I^\prime\rangle)
			       \:\arbno{\alpha}))$\\
      \>  \>	\>       \>$\arbno{\epsilon}$\\
      \>  \>	\>       \>$(\#\arbno{\I}),$\\
      \>  \>    \>\go{1}$\wrong{too few arguments}\rangle\hbox{ \rm in }\EXP)$\\
      \>$\kappa$\\
      \>$(\fun{update}\:(\fun{new}\:\sigma\,\vert\,\LOC)
	                   \:\fun{unspecified}
			   \:\sigma),$\\
  \go{3}$\wrong{out of memory}\:\sigma
\end{semfun}

\begin{semfun}
\Esem\sembrack{\hbox{\tt(lambda \I{} \arbno{\C} $\E_0$)}} =
 \Esem\sembrack{\hbox{\tt(lambda ({\bf.}\ \I) \arbno{\C} $\E_0$)}}
\end{semfun}

\begin{semfun}
\Esem\sembrack{\hbox{\tt(\ide{if} $\E_0$ $\E_1$ $\E_2$)}} =$\\
 \go{1}$\lambda\rho\kappa\:.\:
   \Esem\sembrack{\E_0}\:\rho\:(\fun{single}\:(\lambda\epsilon\:.\:
    $\=$\fun{truish}\:\epsilon\rightarrow\Esem\sembrack{\E_1}\rho\kappa,$\\
     \>\go{1}$\Esem\sembrack{\E_2}\rho\kappa))
\end{semfun}

\begin{semfun}
\Esem\sembrack{\hbox{\tt(if $\E_0$ $\E_1$)}} =$\\
 \go{1}$\lambda\rho\kappa\:.\:
   \Esem\sembrack{\E_0}\:\rho\:(\fun{single}\:(\lambda\epsilon\:.\:
    $\=$\fun{truish}\:\epsilon\rightarrow\Esem\sembrack{\E_1}\rho\kappa,$\\
     \>\go{1}$\fun{send}\:\fun{unspecified}\:\kappa))
\end{semfun}

Here and elsewhere, any expressed value other than {\it undefined} may
be used in place of {\it unspecified}.

\begin{semfun}
\Esem\sembrack{\hbox{\tt(\ide{set!} \I{} \E)}} =$\\
 \go{1}$\lambda\rho\kappa\:.\:\Esem\sembrack{\E}\:\rho\:
     (\fun{single}(\lambda\epsilon\:.\:\fun{assign}\:
       $\=$(\fun{lookup}\:\rho\:\I)$\\
	\>$\epsilon$\\
	\>$(\fun{send}\:\fun{unspecified}\:\kappa)))
\end{semfun}

\begin{semfun}
\arbno{\Esem}\sembrack{\:} =
  \lambda\rho\kappa\:.\:\kappa\langle\:\rangle
\end{semfun}

\begin{semfun}
\arbno{\Esem}\sembrack{\E_0\:\arbno{\E}} =$\\
 \go{1}$\lambda\rho\kappa\:.\:
      \Esem\sembrack{\E_0}\:\rho\:
         (\fun{single}
	    (\lambda\epsilon_0\:.\:\arbno{\Esem}\sembrack{\arbno{\E}}
		\:\rho\:(\lambda\arbno{\epsilon}\:.\:
		           \kappa\:(\langle\epsilon_0\rangle\:\S\:\arbno{\epsilon}))))
\end{semfun}

\begin{semfun}
\Csem\sembrack{\:} = \lambda\rho\theta\,.\:\theta
\end{semfun}

\begin{semfun}
\Csem\sembrack{\C_0\:\arbno{\C}} =
  \lambda\rho\theta\:.\:\Esem\sembrack{\C_0}\:\rho\:(\lambda\arbno{\epsilon}\:.\:
   \Csem\sembrack{\arbno{\C}}\rho\theta)
\end{semfun}

\egroup  % end smallish

\subsection{Auxiliary functions}

\bgroup\small

\begin{semfun}
\fun{lookup}        :  \ENV \to \Ide \to \LOC$\\$
\fun{lookup} =
 \lambda\rho\I\:.\:\rho\I
\end{semfun}

\begin{semfun}
\fun{extends}       :  \ENV \to \arbno{\Ide} \to \arbno{\LOC} \to \ENV$\\$
\fun{extends} =$\\
 \go{1}$\lambda\rho\arbno{\I}\arbno{\alpha}\:.\:
   $\=$\#\arbno{\I}=0\rightarrow\rho,$\\
    \>$\go{1}\fun{extends}\:(\rho[(\arbno{\alpha}\elt 1)/(\arbno{\I}\elt 1)])
			       \:(\arbno{\I}\drop 1)
			       \:(\arbno{\alpha}\drop 1)
\end{semfun}

\begin{semfun}
\fun{wrong}  :  \ERR \to \CC    \hbox{\qquad [implementation-dependent]}
\end{semfun}

\begin{semfun}
\fun{send}          :  \EXP \to \EC \to \CC$\\$
\fun{send} =
 \lambda\epsilon\kappa\:.\:\kappa\langle\epsilon\rangle
\end{semfun}

\begin{semfun}
\fun{single}        :  (\EXP \to \CC) \to \EC$\\$
\fun{single} =$\\
 \go{1}$\lambda\psi\arbno{\epsilon}\:.\:
   $\=$\#\arbno{\epsilon}=1\rightarrow\psi(\arbno{\epsilon}\elt 1),$\\
    \>$\go{1}\wrong{wrong number of return values}
\end{semfun}

\begin{semfun}
\fun{new}           :  \STO \to (\LOC + \{ \fun{error} \})
    \hbox{\qquad [implementation-dependent]}
\end{semfun}

\begin{semfun}
\fun{hold}          :  \LOC \to \EC \to \CC$\\$
\fun{hold} =
 \lambda\alpha\kappa\sigma\:.\:\fun{send}\,(\sigma\alpha\elt 1)\kappa\sigma
\end{semfun}

\begin{semfun}
\fun{assign}        :  \LOC \to \EXP \to \CC \to \CC$\\$
\fun{assign} =
 \lambda\alpha\epsilon\theta\sigma\:.\:\theta(\fun{update}\:\alpha\epsilon\sigma)
\end{semfun}

\begin{semfun}
\fun{update}        :  \LOC \to \EXP \to \STO \to \STO$\\$
\fun{update} =
 \lambda\alpha\epsilon\sigma\:.\:\sigma[\langle\epsilon,\fun{true}\rangle/\alpha]
\end{semfun}

\begin{semfun}
\fun{tievals}       :  (\arbno{\LOC} \to \CC) \to \arbno{\EXP} \to \CC$\\$
\fun{tievals} =$\\
 \go{1}$\lambda\psi\arbno{\epsilon}\sigma\:.\:
   $\=$\#\arbno{\epsilon}=0\rightarrow\psi\langle\:\rangle\sigma,$\\
    \>$\fun{new}\:\sigma\:\elem\:\LOC\rightarrow\fun{tievals}\,
       $\=$(\lambda\arbno{\alpha}\:.\:\psi(\langle\fun{new}\:\sigma\:\vert\:\LOC\rangle
				     \:\S\:\arbno{\alpha}))$\\
    \>  \>$(\arbno{\epsilon}\drop 1)$\\
    \>  \>$(\fun{update}(\fun{new}\:\sigma\:\vert\:\LOC)
			         (\arbno{\epsilon}\elt 1)
				 \sigma),$\\
    \>$\go{1}\wrong{out of memory}\sigma
\end{semfun}

\begin{semfun}
\fun{tievalsrest}   :  (\arbno{\LOC} \to \CC) \to \arbno{\EXP} \to \NAT \to \CC$\\$
\fun{tievalsrest} =$\\
 \go{1}$\lambda\psi\arbno{\epsilon}\nu\:.\:\fun{list}\:
   $\=$(\fun{dropfirst}\:\arbno{\epsilon}\nu)$\\
    \>$(\fun{single}(\lambda\epsilon\:.\:\fun{tievals}\:\psi\:
           ((\fun{takefirst}\:\arbno{\epsilon}\nu)\:\S\:\langle\epsilon\rangle)))
\end{semfun}

\begin{semfun}
\fun{dropfirst} =
 \lambda l n \:.\:  n=0 \rightarrow l, \fun{dropfirst}\,(l \drop 1)(n - 1)
\end{semfun}

\begin{semfun}
\fun{takefirst} =
 \lambda l n \:.\: n=0 \rightarrow \langle\:\rangle,
     \langle l \elt 1\rangle\:\S\:(\fun{takefirst}\,(l \drop 1)(n - 1))
\end{semfun}

\begin{semfun}
\fun{truish}        :  \EXP \to \TRU$\\$
\fun{truish} =
  \lambda\epsilon\:.\:
     (\epsilon = \fun{false}\vee\epsilon = \fun{null})\rightarrow
          \fun{false},
          \fun{true}
\end{semfun}

\begin{semfun}
\fun{permute}       :  \arbno{\Exp} \to \arbno{\Exp}
    \hbox{\qquad [implementation-dependent]}
\end{semfun}

\begin{semfun}
\fun{unpermute}     :  \arbno{\EXP} \to \arbno{\EXP}
    \hbox{\qquad [inverse of \fun{permute}]}
\end{semfun}

\begin{semfun}
\fun{applicate}     :  \EXP \to \arbno{\EXP} \to \EC \to \CC$\\$
\fun{applicate} =$\\
 \go{1}$\lambda\epsilon\arbno{\epsilon}\kappa\:.\:
   $\=$\epsilon\:\elem\:\FUN\rightarrow(\epsilon\:\vert\:\FUN\elt 2)\arbno{\epsilon}\kappa,
          \wrong{bad procedure}
\end{semfun}

\begin{semfun}
\fun{onearg}	  :  (\EXP \to \EC \to \CC) \to (\arbno{\EXP} \to \EC \to \CC)$\\$
\fun{onearg} =$\\
 \go{1}$\lambda\zeta\arbno{\epsilon}\kappa\:.\:
   $\=$\#\arbno{\epsilon}=1\rightarrow\zeta(\arbno{\epsilon}\elt 1)\kappa,$\\
    \>$\go{1}\wrong{wrong number of arguments}
\end{semfun}

\begin{semfun}
\fun{twoarg}	  :  (\EXP \to \EXP \to \EC \to \CC) \to (\arbno{\EXP} \to \EC \to \CC)$\\$
\fun{twoarg} =$\\
 \go{1}$\lambda\zeta\arbno{\epsilon}\kappa\:.\:
   $\=$\#\arbno{\epsilon}=2\rightarrow\zeta(\arbno{\epsilon}\elt 1)(\arbno{\epsilon}\elt 2)\kappa,$\\
    \>$\go{1}\wrong{wrong number of arguments}
\end{semfun}

\begin{semfun}
\fun{list}          :  \arbno{\EXP} \to \EC \to \CC$\\$
\fun{list} =$\\
 \go{1}$\lambda\arbno{\epsilon}\kappa\:.\:
   $\=$\#\arbno{\epsilon}=0\rightarrow\fun{send}\:\fun{null}\:\kappa,$\\
    \>$\go{1}\fun{list}\,(\arbno{\epsilon}\drop 1)
             (\fun{single}(\lambda\epsilon\:.\:
                   \fun{cons}\langle\arbno{\epsilon}\elt 1,\epsilon\rangle\kappa))
\end{semfun}

\begin{semfun}
\fun{cons}          :  \arbno{\EXP} \to \EC \to \CC$\\$
\fun{cons} =$\\
 \go{1}$\fun{twoarg}\,(\lambda\epsilon_1\epsilon_2\kappa\sigma\:.\:
   $\=$\fun{new}\:\sigma\:\elem\:\LOC\rightarrow$\\
    \> \go{1}
        \=$(\lambda\sigma^\prime\:.\:
           $\=$\fun{new}\:\sigma^\prime\:\elem\:\LOC\rightarrow$\\
    \>  \>  \>$\go{1}\fun{send}\,
	       $\=$(\langle\fun{new}\:\sigma\:\vert\:\LOC,
					    \fun{new}\:\sigma^\prime\:\vert\:\LOC\rangle
				       \hbox{ \rm in }\EXP)$\\
    \>  \>  \>  \>$\kappa$\\
    \>  \>  \>  \>$(\fun{update}(\fun{new}\:\sigma^\prime\:\vert\:\LOC)
			             \epsilon_2
				     \sigma^\prime),$\\
    \>  \>  \>$\go{1}\wrong{out of memory}\sigma^\prime)$\\
    \>  \>$(\fun{update}(\fun{new}\:\sigma\:\vert\:\LOC)\epsilon_1\sigma),$\\
    \>$\go{1}\wrong{out of memory}\sigma)
\end{semfun}

\begin{semfun}
\fun{less}          :  \arbno{\EXP} \to \EC \to \CC$\\$
\fun{less} =$\\
 \go{1}$\fun{twoarg}\,(\lambda\epsilon_1\epsilon_2\kappa\:.\:
   $\=$(\epsilon_1\:\elem\:\NUM\wedge\epsilon_2\:\elem\:\NUM)\rightarrow$\\
    \>$\go{1}\fun{send}\,
	       (\epsilon_1\:\vert\:\NUM<\epsilon_2\:\vert\:\NUM\rightarrow
	           \fun{true},
		   \fun{false})
	       \kappa,$\\
    \>$\go{1}\wrong{non-numeric argument to \ide{<}})
\end{semfun}

\begin{semfun}
\fun{add}          :  \arbno{\EXP} \to \EC \to \CC$\\$
\fun{add} =$\\
 \go{1}$\fun{twoarg}\,(\lambda\epsilon_1\epsilon_2\kappa\:.\:
   $\=$(\epsilon_1\:\elem\:\NUM\wedge\epsilon_2\:\elem\:\NUM)\rightarrow$\\
    \>$\go{1}\fun{send}\,
       $\=$((\epsilon_1\:\vert\:\NUM+\epsilon_2\:\vert\:\NUM)\hbox{ \rm in }\EXP)
           \kappa,$\\
    \>$\go{1}\wrong{non-numeric argument to \ide{+}})
\end{semfun}

\begin{semfun}
\fun{car}          :  \arbno{\EXP} \to \EC \to \CC$\\$
\fun{car} =$\\
 \go{1}$\fun{onearg}\,(\lambda\epsilon\kappa\:.\:
   $\=$\epsilon\:\elem\:\PAI\rightarrow
          \fun{hold}\, (\epsilon\:\vert\:\PAI\elt 1) \kappa,$\\
    \>$\go{1}\wrong{non-pair argument to \ide{car}})
\end{semfun}

\begin{semfun}
\fun{cdr}          :  \arbno{\EXP} \to \EC \to \CC %$\\$
\hbox{\qquad [similar to \fun{car}]}
\end{semfun}

\begin{semfun}
\fun{setcar}          :  \arbno{\EXP} \to \EC \to \CC$\\$
\fun{setcar} =$\\
 \go{1}$\fun{twoarg}\,(\lambda\epsilon_1\epsilon_2\kappa\:.\:
   $\=$\epsilon_1\:\elem\:\PAI\rightarrow
          \fun{assign}\,$\=$(\epsilon_1\:\vert\:\PAI\elt 1)$\\
    \>		              \>$\epsilon_2$\\
    \>			      \>$(\fun{send}\:\fun{unspecified}\:\kappa),$\\
    \>$\go{1}\wrong{non-pair argument to \ide{set-car!}})
\end{semfun}

\begin{semfun}
\fun{eqv}          :  \arbno{\EXP} \to \EC \to \CC$\\$
\fun{eqv} =$\\
 \go{1}$\fun{twoarg}\,(\lambda\epsilon_1\epsilon_2\kappa\:.\:
   $\=$(\epsilon_1\:\elem\:\MSC\wedge\epsilon_2\:\elem\:\MSC)\rightarrow$\\
    \>$\go{1}\fun{send}\,
       $\=$(\epsilon_1\:\vert\:\MSC = \epsilon_2\:\vert\:\MSC\rightarrow\fun{true},
            \fun{false})\kappa,$\\
    \>$(\epsilon_1\:\elem\:\SYM\wedge\epsilon_2\:\elem\:\SYM)\rightarrow$\\
    \>$\go{1}\fun{send}\,
       $\=$(\epsilon_1\:\vert\:\SYM = \epsilon_2\:\vert\:\SYM\rightarrow\fun{true},
            \fun{false})\kappa,$\\
    \>$(\epsilon_1\:\elem\:\CHR\wedge\epsilon_2\:\elem\:\CHR)\rightarrow$\\
    \>$\go{1}\fun{send}\,
       $\=$(\epsilon_1\:\vert\:\CHR = \epsilon_2\:\vert\:\CHR \rightarrow\fun{true},
            \fun{false})\kappa,$\\
    \>$(\epsilon_1\:\elem\:\NUM\wedge\epsilon_2\:\elem\:\NUM)\rightarrow$\\
    \>$\go{1}\fun{send}\,
       $\=$(\epsilon_1\:\vert\:\NUM=\epsilon_2\:\vert\:\NUM\rightarrow\fun{true},
            \fun{false})\kappa,$\\
    \>$(\epsilon_1\:\elem\:\PAI\wedge\epsilon_2\:\elem\:\PAI)\rightarrow$\\
    \>$\go{1}\fun{send}\,
       $\=$($\=$(\lambda{p_1}{p_2}\:.\:
                ($\=$({p_1}\elt 1) = ({p_2}\elt 1)\wedge$\\
    \>  \>   \>   \>$({p_1}\elt 2) = ({p_2}\elt 2))
                     \rightarrow\fun{true},$\\
    \>  \>   \>   \>$\go{1}\fun{false})$\\
    \>  \>   \>$(\epsilon_1\:\vert\:\PAI)$\\
    \>  \>   \>$(\epsilon_2\:\vert\:\PAI))$\\
    \>  \>$\kappa,$\\
    \>$(\epsilon_1\:\elem\:\VEC\wedge\epsilon_2\:\elem\:\VEC)\rightarrow
%\fun{send}\,
%       $\=$((\#(\epsilon_1\:\vert\:\VEC)=\#(\epsilon_2\:\vert\:\VEC)
%         \wedge\hbox{\rm Y}(\lambda\fun{loop}\:.\:\lambda\fun{v1}\fun{v2}\:.\:
%       $\=$\#\fun{v1}=0\rightarrow\fun{true},$\\
%    \>  \>  \>$(\fun{v1}\elt 1) = (\fun{v2}\elt 1)\rightarrow
%       \fun{loop}(\fun{v1}\drop 1)(\fun{v2}\drop 1),$\\
%    \>  \>  \>$\go{1}\fun{false})(\epsilon_1\:\vert\:\VEC)(\epsilon_2\:\vert\:\VEC))
%          \rightarrow\fun{true},$\\
%    \>  \>$\go{1}\fun{false})\kappa
\ldots,$\\
    \>$(\epsilon_1\:\elem\:\STR\wedge\epsilon_2\:\elem\:\STR)\rightarrow
%\fun{send}\,
%       $\=$((\#(\epsilon_1\:\vert\:\STR)=\#(\epsilon_2\:\vert\:\STR)\wedge
%    \hbox{\rm Y}(\lambda\fun{loop}\:.\:\lambda\fun{v1}\fun{v2}\:.\:
%       $\=$\#\fun{v1}=0\rightarrow\fun{true},$\\
%    \>  \>  \>$(\fun{v1}\elt 1) = (\fun{v2}\elt 1)\rightarrow
%     \fun{loop}(\fun{v1}\drop 1)(\fun{v2}\drop 1),$\\
%    \>  \>  \>$\go{1}\fun{false})(\epsilon_1\:\vert\:\STR)(\epsilon_2\:\vert\:\STR))
%      \rightarrow\fun{true},$\\
%    \>  \>$\go{1}\fun{false})\kappa
\ldots,$\\
    \>$(\epsilon_1\:\elem\:\FUN\wedge\epsilon_2\:\elem\:\FUN)\rightarrow$\\
    \>$\go{1}\fun{send}\,
       $\=$((\epsilon_1\:\vert\:\FUN\elt 1) = (\epsilon_2\:\vert\:\FUN\elt 1)
               \rightarrow\fun{true},
	                  \fun{false})$\\
    \>  \>$\kappa,$\\
    \>$\go{1}\fun{send}\,\:\fun{false}\:\kappa)
\end{semfun}

\begin{semfun}
\fun{apply}          :  \arbno{\EXP} \to \EC \to \CC$\\$
\fun{apply} =$\\
 \go{1}$\fun{twoarg}\,(\lambda\epsilon_1\epsilon_2\kappa\:.\:
   $\=$\epsilon_1\:\elem\:\FUN\rightarrow
         \fun{valueslist}\,\langle\epsilon_2\rangle
            (\lambda\arbno{\epsilon}\:.\:\fun{applicate}\:\epsilon_1\arbno{\epsilon}\kappa),$\\
    \>$\go{1}\wrong{bad procedure argument to \ide{apply}})
\end{semfun}

\begin{semfun}
\fun{valueslist}          :  \arbno{\EXP} \to \EC \to \CC$\\$
\fun{valueslist} =$\\
 \go{1}$\fun{onearg}\,(\lambda\epsilon\kappa\:.\:
   $\=$\epsilon\:\elem\:\PAI\rightarrow$\\
    \>$\go{1}\fun{cdr}
         $\=$\langle\epsilon\rangle$\\
    \>    \>$(\lambda\arbno{\epsilon}\:.\:
	          $\=$\fun{valueslist}\:$\\
    \>    \>       \>$\arbno{\epsilon}$\\
    \>    \>       \>$(\lambda\arbno{\epsilon}\:.\:\fun{car}\langle\epsilon\rangle
	    (\fun{single}(\lambda\epsilon\:.\:
	      \kappa(\langle\epsilon\rangle\:\S\:\arbno{\epsilon}))))),$\\
    \>$\epsilon = \fun{null}\rightarrow\kappa\langle\:\rangle,$\\
    \>$\go{1}\wrong{non-list argument to \ide{values-list}})
\end{semfun}

\begin{semfun}
\fun{cwcc}          :  \arbno{\EXP} \to \EC \to \CC
    \hbox{\qquad [\ide{call-with-current-continuation}]}$\\$
\fun{cwcc} =$\\
 \go{1}$\fun{onearg}\,(\lambda\epsilon\kappa\:.\:
   $\=$\epsilon\:\elem\:\FUN\rightarrow$\\
    \>$\go{1}(\lambda\sigma\:.\:
       $\=$\fun{new}\:\sigma\:\elem\:\LOC\rightarrow$\\
    \>  \>$\go{1}\fun{applicate}\:
	   $\=$\epsilon$\\
    \>  \>  \>$\langle\langle\fun{new}\:\sigma\:\vert\:\LOC,
			     \lambda\arbno{\epsilon}\kappa^\prime\:.\:
			     \kappa\arbno{\epsilon}\rangle
		      \hbox{ \rm in }\EXP\rangle$\\
    \>  \>  \>$\kappa$\\
    \>  \>  \>$(\fun{update}\,
	        $\=$(\fun{new}\:\sigma\:\vert\:\LOC)$\\
    \>	\>  \>	 \>$\fun{unspecified}$\\
    \>	\>  \>	 \>$\sigma),$\\
    \>  \>$\go{1}\wrong{out of memory}\,\sigma),$\\
    \>$\go{1}\wrong{bad procedure argument})
\end{semfun}

\egroup  % end smallish

\egroup
