diff options
author | Camil Staps | 2016-06-03 00:39:37 +0200 |
---|---|---|
committer | Camil Staps | 2016-06-03 00:39:37 +0200 |
commit | 6ecadcb8571712536f9d121264f67f30f7bb0147 (patch) | |
tree | 0542e10ca752f538195095713ca786ab494335b6 /paper/interp.tex | |
parent | Update example program (diff) |
First version almost finished
Diffstat (limited to 'paper/interp.tex')
-rw-r--r-- | paper/interp.tex | 127 |
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. |