1.1 --- a/doc-isac/mlehnfeld/master/thesis/appendix_a.tex	Thu Jun 26 10:50:27 2014 +0200
     1.2 +++ b/doc-isac/mlehnfeld/master/thesis/appendix_a.tex	Thu Jun 26 17:19:30 2014 +0200
     1.3 @@ -0,0 +1,101 @@
     1.4 +\chapter{Code Samples and Comments}
     1.5 +\label{app:code}
     1.6 +
     1.7 +\section{Fibonacci Implementations}
     1.8 +\label{sec:fib-imp}
     1.9 +The Fibonacci numbers are an integer sequence given by
    1.10 +\begin{equation}
    1.11 +  F_n = F_{n-1} + F_{n-2}
    1.12 +\end{equation}
    1.13 +and
    1.14 +\begin{equation}
    1.15 +  F_0 = 0, F_1 = 1\;.
    1.16 +\end{equation}
    1.17 +Because this is a very simple, recursive definition, it was chosen for the demonstration of certain concepts in this thesis. However, it is very important to note that the straight forward implementation
    1.18 +\imlcode{~~\=fu\=n fib 0 = 0\\
    1.19 +\>\>| fib 1 = 1\\
    1.20 +\>\>| fib x = fib (x - 1) + fib (x - 2)\textrm{,}}
    1.21 +\noindent
    1.22 +which we presented as an example for pattern matching in \textit{Standard ML} (page \pageref{alg:patmatch}, section \ref{sec:patmatch}), is very inefficient because it has a runtime behavior of $O(F_n)$. An efficient version of the function,
    1.23 +\imlcode{~~\=fu\=n \=fi\=b' 0 = (0, 1)\\
    1.24 +\>\>| fib' n = let\\
    1.25 +\>\>\>\>val (x1, x2) = fib' (n - 1)\\
    1.26 +\>\>\>in\\
    1.27 +\>\>\>\>(x2, x1 + x2)\\
    1.28 +\>\>\>end;\\
    1.29 +\>(*gets 2nd element of touple*)\\
    1.30 +\>fun fib n = fib' (n - 1) |> snd \textrm{,}}
    1.31 +\noindent
    1.32 +shows linear runtime behavior. Annotations (section \ref{sec:annot}) were demonstrated using the Fibonacci function (page \pageref{alg:parannot}):
    1.33 +\imlcode{~~\=fu\=n fib 0 = 1\\
    1.34 +\>\>| fib 1 = 1\\
    1.35 +\>\>| fib x = fib (x - 1) + par (fib (x - 2))}
    1.36 +\noindent
    1.37 +In practice, the gain from parallelism in this example would not just be marginal, the overhead for managing parallel execution would most likely result in a performance worse than the sequential version. Note that annotations of this kind can only work in a programming language following a lazy evaluation strategy because in an eager language like \textit{Standard ML} the annotated expression would be evaluated before being passed to the hypothetical {\tt par} evaluation.
    1.38 +Futures have been discussed in detail throughout this thesis (sections \ref{sec:futurespro}, \ref{sec:actors_scala}, \ref{sec:csp}, \ref{sec:isafut}). The example on page \pageref{alg:futures} redefined {\tt fib} with a future:
    1.39 +\imlcode{\label{alg:fib-futures}
    1.40 +~~\=fu\=n \=fi\=b \=0 = 1\\
    1.41 +\>\>| fib 1 = 1\\
    1.42 +\>\>| fib x = let\\
    1.43 +\>\>\>\>\>fun fib' () = fib (x - 2)\\
    1.44 +\>\>\>\>\>val fibf = Future.fork fib'\\
    1.45 +\>\>\>\>in fib (x - 1) + (Future.join fibf) end}
    1.46 +This code does work in {\em Isabelle/ML} (section \ref{sec:isabelleml}). The performance concerns we saw with the previous example also apply here: in practice, parallelising the evaluation of the Fibonacci function in this way makes no sense.
    1.47 +
    1.48 +
    1.49 +\section{{\tt merge\_lists} implementation}
    1.50 +\label{app:merge-lists}
    1.51 +In the \texttt{Theory\_Data} implementation on page \pageref{alg:thydata-functor} (section \ref{ssec:parall-thy}) we omitted the definitions of the functions {\tt merge\_lists} and {\tt merge\_lists'} for simplicity reasons. They have been added here (program \ref{alg:merge-lists}). Please note that they require that their input lists of type {\tt int list} are already ordered. The difference is that {\tt merge\_lists} accepts the two lists in a touple and {\tt merge\_lists'} as two separate arguments.
    1.52 +\begin{program}
    1.53 +\caption{{\tt merge\_lists} implementation.}
    1.54 +\label{alg:merge-lists}
    1.55 +\begin{MLCode}
    1.56 +fun merge out [] xs = (rev out) @ xs
    1.57 +  | merge out xs [] = (rev out) @ xs
    1.58 +  | merge out (xs' as x::xs) (ys' as y::ys) =
    1.59 +      if x = y then
    1.60 +        merge (x::out) xs ys
    1.61 +      else if x < y then
    1.62 +        merge (x::out) xs ys'
    1.63 +      else
    1.64 +        merge (y::out) xs' ys;
    1.65 +val merge_lists' = merge [];
    1.66 +fun merge_lists (xs, ys) = merge_lists' xs ys;
    1.67 +\end{MLCode}
    1.68 +\end{program}
    1.69 +
    1.70 +
    1.71 +\section{Irrationality of \texorpdfstring{$\sqrt{2}$}{the square root of 2} in \textit{Isar}}
    1.72 +\label{app:sqrt2-isar}
    1.73 +
    1.74 +Program \ref{alg:isar-sqrt2} is a simple proof in \textit{Isar}, showing that the square root of 2 is an irrational number\footnote{\tt \textasciitilde\textasciitilde/src/HOL/ex/Sqrt.thy}.
    1.75 +
    1.76 +
    1.77 +\begin{program}
    1.78 +\caption{\textit{Isabelle/Isar} proof of the irrationality of $\sqrt{2}$.}
    1.79 +\label{alg:isar-sqrt2}
    1.80 +\vspace{\medskipamount}
    1.81 +\noindent
    1.82 +\colorbox{color5}{\texttt{\small
    1.83 +\begin{minipage}{.98\textwidth}
    1.84 +\setlength{\parindent}{1pc}
    1.85 +\noindent
    1.86 +{\tiny\ttfamily\color{color6} 1~}~{\bfseries\color{color1} lemma} {\color{color3} "$\exists$a b::real. a $\notin$ $\mathbb{Q}$ $\land$ b $\notin$ $\mathbb{Q}$ $\land$ a powr b $\in$ $\mathbb{Q}$"}\\
    1.87 +{\tiny\ttfamily\color{color6} 2~}~{\indent({\bfseries\color{color1} is} {\color{color3} "EX a b. ?P a b"})}\\
    1.88 +{\tiny\ttfamily\color{color6} 3~}~{\bfseries\color{color1} proof} cases\\
    1.89 +{\tiny\ttfamily\color{color6} 4~}~{\indent\bfseries\color{color1} assume} {\color{color3} "sqrt 2 powr sqrt 2 $\in$ $\mathbb{Q}$"}\\
    1.90 +{\tiny\ttfamily\color{color6} 5~}~{\indent\bfseries\color{color1} then have} {\color{color3} "?P (sqrt 2) (sqrt 2)"}\\
    1.91 +{\tiny\ttfamily\color{color6} 6~}~{\indent\indent\bfseries\color{color1} by} (metis sqrt\_2\_not\_rat)\\
    1.92 +{\tiny\ttfamily\color{color6} 7~}~{\indent\bfseries\color{color1} then show} {\color{color2} ?thesis} {\bfseries\color{color1} by} blast\\
    1.93 +{\tiny\ttfamily\color{color6} 8~}~{\bfseries\color{color1} next}\\
    1.94 +{\tiny\ttfamily\color{color6} 9~}~{\indent\bfseries\color{color1} assume} 1: {\color{color3} "sqrt 2 powr sqrt 2 $\notin$ $\mathbb{Q}$"}\\
    1.95 +{\tiny\ttfamily\color{color6} 10}~{\indent\bfseries\color{color1} have} {\color{color3} "(sqrt 2 powr sqrt 2) powr sqrt 2 = 2"}\\
    1.96 +{\tiny\ttfamily\color{color6} 11}~{\indent\indent\bfseries\color{color1} using} powr\_realpow [of \_ 2]\\
    1.97 +{\tiny\ttfamily\color{color6} 12}~{\indent\indent\bfseries\color{color1} by} (simp add: powr\_powr power2\_eq\_square [symmetric])\\
    1.98 +{\tiny\ttfamily\color{color6} 13}~{\indent\bfseries\color{color1} then have} {\color{color3} "?P (sqrt 2 powr sqrt 2) (sqrt 2)"}\\
    1.99 +{\tiny\ttfamily\color{color6} 14}~{\indent\indent{\bfseries\color{color1} by} (metis 1 Rats\_number\_of sqrt\_2\_not\_rat)}\\
   1.100 +{\tiny\ttfamily\color{color6} 15}~{\indent\bfseries\color{color1} then show} {\color{color2} ?thesis} {\bfseries\color{color1} by} blast\\
   1.101 +{\tiny\ttfamily\color{color6} 16}~{\bfseries\color{color1} qed}
   1.102 +\end{minipage}}}
   1.103 +\end{program}
   1.104 +