\documentstyle[headerfooter,a4wide,notation]{marticle}
\pagestyle{headings}
\pageheaderlinetrue
\pageheader{\sl\rightmark}{\bf\today}{\thepage}
\pagefooter{}{}{}
%
\title{\huge Action Semantics of {\it MicroML}}
%
\begin{document}
%
\section{The Action Semantics of {\sc nanoML}}
\label{nanoML}
%
\footnotesize

\subsection{Abstract Syntax}
\begin{spec}\seteq Declaration =
\item[\needs] \ide{Lexical Syntax} .
\item[\protects] \ide{Abstract Syntax} . %\ \ \except \ide{Literals} .
\item[\grammar]
\item \eq Declaration =
	\verb%val% Identifier \verb%=% Expression \| \=
	Declaration \verb%;% Declaration .

\item \eq Expression =
  Identifier \| \=
  \verb+fn+ Identifier \verb+=>+ Expression \| \=
  Identifier \verb+(+ Expression \verb+)+ \| \= 
  \verb%if% Expression \verb%then% Expression \verb%else% Expression \| \=
  Expression \verb-*- Expression .

\end{spec}
%
\subsection{Semantic Entities}
\begin{spec}
\item[\needs] \ide{Action Notation} , \ide{Data Notation} .
\end{spec}
%
\subsubsection{Data}
\begin{spec}
\item[\introduces] value , operand .
\item[\needs] \ide{Abstractions} .
\item value = integer \| function .
\end{spec}
%
\subsubsection{Bindings}
\begin{spec}
\item[\needs] \ide{Data} , \ide{Abstractions} .
\item token \sub string .
\item bindable(~t:token) = value .
\end{spec}
%
\subsubsection{Abstractions}
\begin{spec}
\item[\introduces] function , argument , function-result .
\item[\needs] \ide{Data} .
\item function = abstraction .
\item argument = value .
\item function-result = value .
\end{spec}
%
\subsection{Semantic Functions}
\begin{spec}
\item[\needs] \ide{Abstract Syntax} , \ide{Semantic Entities} .
\end{spec}
%
\subsubsection{Declarations}
\begin{spec}
\item[\introduces] elaborate \[ \_ \] .
\item[\needs] \ide{Expressions} .
\item[] elaborate \[ \_ \] :: Declaration \into act .
\item   elaborate \[ \verb+val+ ~I \verb+=+ ~E \] = 
	evaluate ~E then bind token of ~I to it .
\item   elaborate \[ ~D_1 \verb+;+ ~D_1  \] = \=
        \(
	\< furthermore elaborate ~D_1 \> \\
	hence \\
	\< elaborate ~D_2 \> .
        \) 
\end{spec}
\subsubsection{Expressions}
\begin{spec}
\item[\introduces] evaluate \[ \_ \] .
%\item[\needs] \ide{Literals} .
\end{spec}
%
\subsubsubsection{Evaluating Expressions}
\begin{spec}
\item[] evaluate \[ \_ \] :: Expression \into act .
\item   evaluate \[ ~I \] = give the value bound to token of ~I .
\item   evaluate \[ \verb+fn+ ~I \verb+=>+ ~E \] = \=
        \(
        give closure abstraction \=
	   \< \< furthermore bind token of ~I to the argument \> \\
              hence \\
	      \< evaluate ~E . \> \> 
        \)
\item   evaluate \[ ~I \verb+(+ ~E \verb+)+ \] = \=
        \(
        \< evaluate ~E \> \\
        then \\
        \< enact (the abstraction bound to the token of ~I
	   with the argument) . \> 
        \)

\item   evaluate \[ \verb+if+ ~E_1 \verb+then+ ~E_2 \verb+else+ ~E_3 \] = \=
        \(
        \< evaluate ~E_1 then give the value \> \\
        then \\
        \< \< check (it is 1) and then evaluate ~E_2 \> \\
           or \\
           \< check (it is 0) and then evaluate ~E_3 . \>
 \>
        \)

\item   evaluate \[ ~E_1 \verb-*- ~E_2 \] = \=
	\(
	\< \< evaluate ~E_1 then give the integer label \#1 \> \\
	   and \\
	   \< evaluate ~E_2 then give the integer label \#2 \> \\
	\> \\
	then \\
	\< give product(the integer\#1, the integer\#2) . \>
	\)

\end{spec}
\end{document}