Finishing first version paper

9 files changed, 78 insertions, 43 deletions

diff --git a/paper/ast.tex b/paper/ast.tex
index 07553bd..97feb04 100644
--- a/paper/ast.tex
+++ b/paper/ast.tex
@@ -11,9 +11,7 @@ translates almost directly to a type definition:
 Note that we have added common binary operators like \CI{Lt} that did not exist
 in the grammar of \autoref{sec:intro:while}. These operators could also be
 constructed from other boolean expressions. We have also added \CI{Div} for
-integer division. It is a useful addition in this example, as it will force us
-to implement error handling in the evaluation of arithmetic expressions when we
-divide by zero.
+integer division.
 
 As an example, the example program from \autoref{sec:intro:while} would be
 stored in the AST as follows:
diff --git a/paper/concl.tex b/paper/concl.tex
new file mode 100644
index 0000000..502a5ad
--- /dev/null
+++ b/paper/concl.tex
@@ -0,0 +1,27 @@
+\section{Conclusion}
+\label{sec:concl}
+
+Walking through the implementation of a While interpreter we have seen
+different advantages of doing this in a functional style.
+
+First of all, the syntax could be translated directly from grammar to type
+definitions. It is true that simple algebraic data types, as used in
+\autoref{sec:ast}, could be simulated with enumeration types and pointers in
+an imperative style. However, any one will agree that the functional
+definitions are better readable, making their usage less error-prone.
+
+Secondly, in \autoref{sec:eval} we saw that functional programming languages
+allow us to easily work with higher order functions: we did not need to
+implement the state as a lookup table but could simply use a function.
+
+We then discussed the use of the \CI{Either} monad for error reporting. Monadic
+binding lets us work easily with calculations that may fail. Moreover, in
+\autoref{sec:interp} we saw that monads also let us specify execution order.
+
+In general, we have seen that a functional style allows us to stay close to the
+semantic definitions of a language. This makes it very easy to verify that our
+implementation of the semantics is correct. Proofs that hold for the semantics
+(like completeness or correctness with respect to axiomatic semantics) easily
+apply to the interpreter as well, once the correctness of the interpreter has
+been established --- this is generally a trivial task. Furthermore, the final
+implementation is better readable and thus easier to maintain.
diff --git a/paper/disc.tex b/paper/disc.tex
new file mode 100644
index 0000000..0fdee9f
--- /dev/null
+++ b/paper/disc.tex
@@ -0,0 +1,16 @@
+\section{Future work}
+\label{sec:disc}
+
+As we have seen in \autoref{sec:interp:cond}, not all rules that can be
+specified in mathematical notation are trivial to translate to a functional
+program. It should be investigated under what conditions rules can or cannot be
+translated directly. What kind of functional tools can we come up with to make
+this easier?
+
+Our claim has been that semantic rules can be translated almost directly to an
+implementation in a functional language. We can then ask ourselves: is it
+possible to store rules in a data structure and write a universal interpreter,
+say \CI{run :: [Rule stm state] stm state -> Either Error state} (note the parametrization of
+\CI{stm} and \CI{state})? Under what conditions is it possible for such a
+universal interpreter to choose those rules that allow for the most efficient
+interpretation?
diff --git a/paper/ftypes.tex b/paper/ftypes.tex
index 29407a1..803182f 100644
--- a/paper/ftypes.tex
+++ b/paper/ftypes.tex
@@ -5,4 +5,4 @@ The following functions are considered known. If not, looking them up is easy
 using Cloogle~\citep{cloogle}.
 
 \lstinputlisting[firstline=5,lastline=23,xleftmargin=0pt]{While/Common.dcl}
-\lstinputlisting[firstline=34,xleftmargin=0pt]{While/Common.dcl}
+\lstinputlisting[firstline=34,lastline=34,xleftmargin=0pt]{While/Common.dcl}
diff --git a/paper/interp.tex b/paper/interp.tex
index 0f73b2d..5b8db03 100644
--- a/paper/interp.tex
+++ b/paper/interp.tex
@@ -15,9 +15,9 @@ $$
 \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.
+This 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:
 
diff --git a/paper/intro-org.tex b/paper/intro-org.tex
index ee2a38d..70c5099 100644
--- a/paper/intro-org.tex
+++ b/paper/intro-org.tex
@@ -11,7 +11,7 @@ abstract syntax tree (AST). This AST is described in \autoref{sec:ast}. In
 \autoref{sec:eval} we will discuss different possibilities of evaluating
 mathematical expressions. Finally, in \autoref{sec:interp} we will propose a
 While interpreter. We finish by articulating the advantages of functional
-interpretation in \autoref{sec:conclusions}.
+interpretation in \autoref{sec:concl}.
 
 \autoref{sec:ftypes} lists the functions and types that the reader is supposed
 to know.
diff --git a/paper/intro.tex b/paper/intro.tex
index 49fbeed..2d44b4a 100644
--- a/paper/intro.tex
+++ b/paper/intro.tex
@@ -4,27 +4,32 @@ Compilers and interpreters are among the most complex pieces of software
 written to date. Due to the rapid technological development of the last
 decades, programming languages have become increasingly complex, semantically
 speaking. It has become impossible for a programmer to keep in mind the impact
-of their changes on the generated machine code. This led to the
-\emph{assumption problem}: developers constantly rely on assumptions about how
+of their changes on the generated machine code. Developers now constantly rely on assumptions about how
 the language that they write in works. Intuitive semantics may change over
 time, however, and proper definitions are required now that our world relies so
 principally on software.
 
 Nowadays, programming languages have semantical specifications as the main link
-between programmers and compiler designers. This solves the assumption problem
-on the programmer's side. However, now that programming languages become
-increasingly complex, the same problem occurs on the compiler designer's side:
-the specification has become too complex to efficiently translate it into
-imperative code, and writing a correct compiler or interpreter has become no
+between programmers and compiler designers. This solves the problem on the
+programmer's side. However, now that programming languages become increasingly
+complex, another problem occurs on the compiler designer's side: the
+specification has become too complex to efficiently translate it into
+imperative code, and writing a correct compiler or interpreter is no longer a
 trivial task.
 
 Functional programming languages offer writers of code processing systems tools
-to efficiently work with semantical specifications. Using a high level of
-abstraction, the gap between specification and implementation is closed,
-allowing for quicker correctness checks and better maintainable code. The
-connections between functional languages and mathematics let us \emph{prove}
-properties about code processing systems (for example, their correctness with
-respect to a specification).
+to efficiently work with semantical specifications --- indeed, functional
+programs can be used as the very specification themselves~\citep{fpasspec}.
+However, we will not go this far. While functional programs are indeed better
+suitable for semantic specifications than natural language, mathematical
+notation gives even more freedom. We therefore suggest tools for the
+implementation of these mathematical definitions in a functional style.
+
+Using a high level of abstraction, the gap between specification and
+implementation is closed, allowing for quicker correctness checks and better
+maintainable code.  The connections between functional languages and
+mathematics let us \emph{prove} properties about code processing systems (for
+example, their correctness with respect to a specification).
 
 \input{intro-org}
 \input{intro-while}
diff --git a/paper/paper.bib b/paper/paper.bib
index f43c91e..a0a462f 100644
--- a/paper/paper.bib
+++ b/paper/paper.bib
@@ -20,25 +20,12 @@
 	year = {1995}
 }
 
-@article{algol,
- author = {Backus, J. W. and Bauer, F. L. and Green, J. and Katz, C. and McCarthy, J. and Perlis, A. J. and Rutishauser, H. and Samelson, K. and Vauquois, B. and Wegstein, J. H. and van Wijngaarden, A. and Woodger, M.},
- editor = {Naur, Peter},
- title = {Report on the Algorithmic Language ALGOL 60},
- journal = {Commun. ACM},
- issue_date = {May 1960},
- volume = {3},
- number = {5},
- month = may,
- year = {1960},
- issn = {0001-0782},
- pages = {299--314},
- numpages = {16},
- url = {http://doi.acm.org/10.1145/367236.367262},
- doi = {10.1145/367236.367262},
- acmid = {367262},
- publisher = {ACM},
- address = {New York, NY, USA},
-} 
+@book{fpasspec,
+	author = {Koopman, P.},
+	title = {Functional Programs as Executable Specifications},
+	year = {1990},
+	publisher = {Krips Repro Meppel}
+}
 
 @article{yard,
 	author = {Jager, P.T.},
diff --git a/paper/paper.tex b/paper/paper.tex
index 7d63d8c..724dfc7 100644
--- a/paper/paper.tex
+++ b/paper/paper.tex
@@ -51,12 +51,14 @@
 	\input{ast}
 	\input{eval}
 	\input{interp}
-
-	\appendix
-	\input{ftypes}
+	\input{concl}
+	\input{disc}
 
 	\bibliographystyle{jfp}
 	\bibliography{paper}
+
+	\appendix
+	\input{ftypes}
 \end{multicols}
 
 \end{document}