\section{Interpreting}
\label{sec:interp}

The semantics of While have been specified mathematically~\citep{semantics}.
While difficult in other paradigms, translating these semantic rules to a
functional program is trivial. Consider, as an example, the composition rule:

$$
\begin{prooftree}
	\trans{S_1}{s}{s'}\quad
	\trans{S_2}{s'}{s''}
	\justifies
	\trans{\whcomp{S_1}{S_2}}{s}{s''}
	\using{\rcompns}
\end{prooftree}
$$

This derivation rule consists of two premises, above the line, and one
conclusion, beneath the line. It specifies nothing else than the intuition: if
the execution of statement $S_1$ in state $s$ yields state $s'$, and $S_2$ in
$s'$ yields $s''$, then $\whcomp{S_1}{S_2}$ in $s$ yields $s''$.

The translation of this rule in a functional program looks as follows:

\begin{lstlisting}
run (Compose s1 s2) st
	= run s1 st >>= \st` -> run s2 st`
\end{lstlisting}

Or, shorter, we can use currying:

\begin{lstlisting}
run (Compose s1 s2) st
	= run s1 st >>= run s2
\end{lstlisting}

Again, using the monadic bind, any errors in running \CI{s1} will propagate,
and \CI{s2} will not be interpreted. More importantly in this case, the monad
lets us specify execution order in a convenient and readable way.

\medskip
Another case where we can clearly see the advantages of functional programming
is in the assignment rule. Updating a state $st$ works as
follows~\citep{semantics}:

$$
	(st[v\mapsto e])w =
	\begin{cases}
		e    & \text{if $v=w$} \\
		st~v & \text{if $v\neq w$.}
	\end{cases}
$$

This gives the assignment axiom\footnote{An axiom, in this context, is nothing
else than a derivation rule with zero premises.}:

$$
\begin{prooftree}
	\axjustifies
	\trans{\whass{x}{a}}{s}{s\left[x\mapsto\mathcal A\llbracket a\rrbracket s\right]}
	\using{\rassns}
\end{prooftree}
$$

It is easy to see that assignment will never fail. The only thing we need to do
is update the state. This is done easily with a lambda expression:

\begin{lstlisting}
run (Ass v e) st
	= pure (\w -> if (w == v) (eval e st) (st w))
\end{lstlisting}

The lambda expression is the direct translation of the update function used by
\cite{semantics} as described above. This is much more intuitive than using,
for example, a lookup table to model the state. Again, functional programming
lets us stay close to the mathematical definitions.

The only possible reason we would \emph{not} want to model the state as a
function is efficiency. This approach has linear fetch complexity, as has the
lookup table from \autoref{sec:eval:lookup}. However, storing the function on
the heap will in virtually any implementation be less efficient than storing a
list of simple tuples. Furthermore, the lookup table approach can be modified
using a different data structure to give a better complexity: logarithmic, if a
binary search tree is used, or even constant if the variables can be mapped to
array indices.

\medskip
The full instance of \CI{run} for \CI{Stm} is given below. It exploits monads
for error reporting and execution order. Four of the five alternatives are
derived trivially from their corresponding semantic rules. Only the \CI{If}
alternative had to be adapted; it will be discussed in the next paragraph.

\lstinputlisting[firstline=16]{While/Simple.icl}

\subsection{Conditions}
\label{sec:interp:cond}
\cite{semantics} define two rules for the \CI{If} statement. The first
specifies that if $b$ holds in state $s$, the statement $\whif{b}{S_1}{S_2}$ in
$s$ will be equivalent to $S_1$:

$$
\begin{prooftree}
	\trans{S_1}{s}{s'}
	\justifies
	\trans{\whif{b}{S_1}{S_2}}{s}{s'}
	\using{\rifttns}
	\quad\text{if $\mathcal B\llbracket b\rrbracket s$}
\end{prooftree}
$$

This derivation rule has one premise, but can only be applied when the
condition $\mathcal B\llbracket b\rrbracket s$ holds. A similar rule exists
for $S_2$ in the case that the condition does not hold.

The problem with these rules is that they can only be applied when some
condition is met. In this case, the condition is still relatively easy. In
other cases, it may also depend on the transitions above the line: for example,
we may want to check that $b$ holds in $s'$ rather than in $s$. If we would
want to support that kind of functionality, we would need to try to satisfy the
antecedent, then verify if the condition holds and only apply the rule if it
does. In the end this is possible (although we will not show it here) --- the
\CI{Alternative} class provides a nice infrastructure for this.

In the case of the \CI{If} statement this problem can be avoided as shown
above. This is however only possible thanks to the fact that the two rules for
this construct are very similar, and because the condition depends only on
the initial state and statement.

It is outside the scope of this paper to discuss the possibilities for
implementing rules with complex conditionals.