\section{Abstract Syntax}
\begin{spec}\tabset Declaration &=&
\item[\needs] \ide{Lexical Syntax} .
\item[\closed] \ide{Abstract Syntax} . %\ \ \except \ide{Literals} .
\item[\grammar]
\item \tab Program &=& 
	Declaration \| \=
	Declaration Program .
\item \tab Declaration &=&
	\verb%val% Identifier \verb%=% Expression \| \=
	\verb%val rec% Identifier \verb%=% \verb+fn+ Identifier \verb%=>% Expression .
\item \tab Expression &=&
        \verb%true% \| \=
        \verb%false% \| \=
        Numeral \| \=
        Identifier \| \=
        \verb+fn+ Identifier \verb+=>+ Expression \| \=
	Expression \verb+(+ Expression \verb+)+ \| \= 
        \verb%if% Expression \verb%then% Expression \verb%else% Expression
\| \=
        Expression Operator Expression \| \=
        Operator Expression .

\item \tab Operator &=& \verb+not+ \|
                     \verb+and+ \|
                     \verb+or+ \|
		     \verb+~+ \|
                     \verb%+% \|
                     \verb+-+ \|
                     \verb+*+ \|
                     \verb+/+ \| 
		     \verb+=+ .
\end{spec}
%
\section{Semantic Entities}
\begin{spec}
\item[\needs] \ide{Action Notation} , \ide{Data Notation} .
\end{spec}
%
\subsection{Data}
\begin{spec}
\item[\introduces] value , operand , operation-result .
\item[\needs] \ide{Abstractions} .
\item value = truth-value \| integer \| function .
\item operand = truth-value \| integer .
\item operation-result = truth-value \| integer .
\end{spec}
%
\subsection{Bindings}
\begin{spec}
\item[\needs] \ide{Data} , \ide{Abstractions} .
\item token \sub string .
\item bindable(~t:token) = value .
\end{spec}
%
\subsection{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}
%
\section{Semantic Functions}
\begin{spec}
\item[\needs] \ide{Abstract Syntax} , \ide{Semantic Entities} .
\end{spec}
%
\subsection{Programs}
\begin{spec}
\item[\introduces] run \[ \_ \] .
\item[\needs] \ide{Declarations} .
\item[\ $\bullet$] run \[ \_ \] :: Program \into act .
\item run \[ ~D \] = elaborate \[ ~D \] .
\item run \[ ~D ~P \] = elaborate \[ ~D \] before run \[ ~P \] .
\end{spec}
%
\subsection{Declarations}
\begin{spec}
\item[\introduces] elaborate \[ \_ \] .
\item[\needs] \ide{Expressions} .
\item[\ $\bullet$] elaborate \[ \_ \] :: Declaration \into act .
\item   elaborate \[ \verb+val+ ~I \verb+=+ ~E \] = 
	evaluate \[ ~E \] then bind token of \[ ~I \] to it .
\item   elaborate \[ \verb+val rec+ ~I_1 \verb+= fn+ ~I_2 \verb+=>+ ~E \] = \=
        \(
        recursively bind token of \[ ~I_1 \] to closure abstraction \=
	   \< \< rebind moreover bind token of \[ ~I_2 \] to the argument \> \\
              hence \\
	      \< evaluate \[ ~E \] . \> \> 
        \) 
%	recursively (evaluate \[ ~E \] then bind token of \[ ~I \] to it) .
\end{spec}
%
\subsection{Expressions}
\begin{spec}
\item[\introduces] evaluate \[ \_ \] , evaluate operator \[ \_ \] .
%\item[\needs] \ide{Literals} .
\end{spec}
%
\subsubsection{Evaluating Expressions}
\begin{spec}
\item[\ $\bullet$] evaluate \[ \_ \] :: Expression \into act .
\item   evaluate \[ \verb%true% \] = give true .
\item   evaluate \[ \verb%false% \] = give false .
\item   evaluate \[ ~N \] = give valuation \[ ~N \] .
\item   evaluate \[ ~I \] = give the value bound to token of \[ ~I \] .
\item   evaluate \[ \verb+fn+ ~I \verb+=>+ ~E \] = \=
        \(
        give closure abstraction \=
	   \< \< rebind moreover bind token of \[ ~I \] to the argument \> \\
              hence \\
	      \< evaluate \[ ~E \] . \> \> 
        \)
\item   evaluate \[ ~E_1 \verb+(+ ~E_2 \verb+)+ \] = \=
        \(
        \< \< evaluate \[ ~E_1 \] then give the abstraction label \#1 \> \\
           and \\
           \< evaluate \[ ~E_2 \] then give the argument label \#2 \> \> \\
        then \\
        \< enact the abstraction\#1 with the argument\#2 . \> 
        \)

\item   evaluate \[ \verb+if+ ~E_1 \verb+then+ ~E_2 \verb+else+ ~E_3 \] = \=
        \(
        \< evaluate \[ ~E_1 \] then give the truth-value \> \\
        then \\
        \< \< check (it is true) and then evaluate \[ ~E_2 \] \> \\
           or \\
           \< check (it is false) and then evaluate \[ ~E_3 \] . \>
 \>
        \)
\item   evaluate \[ ~E\on1 ~O ~E\on2 \] = \=
        \(
        \< \< evaluate \[ ~E\on1 \] then give the operand label \#1 \> \\
           and \\
           \< evaluate \[ ~E\on2 \] then give the operand label \#2 \> \> \\
        then \\
        \< evaluate operator \[ ~O \] . \>
        \)
\item   evaluate \[ ~O ~E \] = \=
        \(
        \< evaluate \[ ~E \] then give the operand \> \\
        then \\
        \< evaluate operator \[ ~O \] . \>
        \)
\end{spec}
\subsubsection{Evaluating Operators}
\begin{spec}
\item[\ $\bullet$] evaluate operator \[ \_ \]  :: Operator \into act .
\end{spec}
\begin{spec}
\item evaluate operator \[ \verb%not% \] = 
	give not (the truth-value) .
\item evaluate operator \[ \verb%and% \] =
        give conjunction (the truth-value\#1, the truth-value\#2) .
\item evaluate operator \[ \verb%or% \] =
        give disjunction (the truth-value\#1, the truth-value\#2) .
\item evaluate operator \[ \verb%~% \] = 
	give negation (the integer) .
\item evaluate operator \[ \verb%+% \] = 
	give sum (the integer\#1, the integer\#2) .
\item evaluate operator \[ \verb%-% \] = 
	give difference (the integer\#1, the integer\#2) .
\item evaluate operator \[ \verb%*% \] = 
	give product (the integer\#1, the integer\#2) .
\item evaluate operator \[ \verb%/% \] = 
	give quotient (the integer\#1, the integer\#2) .
\item evaluate operator \[ \verb%=% \] = 
	give (the operand\#1 is the operand\#2) .
\end{spec}
%
\section{Lexical Syntax}
\begin{spec}\tabset Identifier &=&
\item[\introduces] token of \[ \_ \] , valuation  \[ \_ \] .
\item[\grammar]
\item \tab Identifier &=&  letter \| \=
                        Identifier letter \| \=
                        Identifier digit .
\item \tab Numeral &=& digit \| \=
                    Numeral digit .
\item \tab digit   &=& \verb+0+ \| \verb+1+ \| \dots \| \verb+9+ .
\item \tab letter  &=& \verb+A+ \| \verb+B+ \| \dots \| \verb+Z+ \| \verb+a+ \| 
\dots \| \verb+z+ .
\end{spec}
%
\subsection{Identifiers}
\begin{spec}
\item[\ $\bullet$] token of \[ \_ \] :: Identifier \into token .
\item token of \[ ~I \] = ~I .
\end{spec}
%
\subsection{Numerals}
\begin{spec}
\item[\ $\bullet$] valuation \[ \_ \] :: Numeral \into integer .
\end{spec}
\begin{spec} \tabset valuation \[ ~N ~D \] &=&
\item \tab valuation \[ \verb+0+ \] &=& 0 .
\item \tab valuation \[ \verb+1+ \] &=& 1 .
\item[] \dots
\setcounter{enumi}{9}
%\item \tab valuation \[ \verb+2+ \] &=& 2 .
%\item \tab valuation \[ \verb+3+ \] &=& 3 .
%\item \tab valuation \[ \verb+4+ \] &=& 4 .
%\item \tab valuation \[ \verb+5+ \] &=& 5 .
%\item \tab valuation \[ \verb+6+ \] &=& 6 .
%\item \tab valuation \[ \verb+7+ \] &=& 7 .
%\item \tab valuation \[ \verb+8+ \] &=& 8 .
\item \tab valuation \[ \verb+9+ \] &&= 9 .
\item \tab valuation \[ ~N ~D \] &=& 
	sum (product (valuation \[ ~N \], 10), valuation \[ ~D \]) .
\end{spec}
%
