1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
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.
|
