First version almost finished

1 files changed, 127 insertions, 0 deletions

diff --git a/paper/interp.tex b/paper/interp.tex
new file mode 100644
index 0000000..0f73b2d
--- /dev/null
+++ b/paper/interp.tex
@@ -0,0 +1,127 @@
+\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 specifies nothing else than the intuition: the composition
+$\whcomp{S_1}{S_2}$ executed in state $s$ will yield a state $s''$ which we get
+by executing $S_1$ and $S_2$ in $s$, consecutively.
+
+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 rule:
+
+$$
+\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}
+$$
+
+A similar rule exists for $S_2$ in the case that $\mathcal B\llbracket
+b\rrbracket s$ 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.