s1210629013@55466
|
1 |
\chapter{Code Samples and Comments}
|
s1210629013@55466
|
2 |
\label{app:code}
|
s1210629013@55466
|
3 |
|
s1210629013@55466
|
4 |
\section{Fibonacci Implementations}
|
s1210629013@55466
|
5 |
\label{sec:fib-imp}
|
s1210629013@55466
|
6 |
The Fibonacci numbers are an integer sequence given by
|
s1210629013@55466
|
7 |
\begin{equation}
|
s1210629013@55466
|
8 |
F_n = F_{n-1} + F_{n-2}
|
s1210629013@55466
|
9 |
\end{equation}
|
s1210629013@55466
|
10 |
and
|
s1210629013@55466
|
11 |
\begin{equation}
|
s1210629013@55466
|
12 |
F_0 = 0, F_1 = 1\;.
|
s1210629013@55466
|
13 |
\end{equation}
|
s1210629013@55466
|
14 |
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
|
s1210629013@55466
|
15 |
\imlcode{~~\=fu\=n fib 0 = 0\\
|
s1210629013@55466
|
16 |
\>\>| fib 1 = 1\\
|
s1210629013@55466
|
17 |
\>\>| fib x = fib (x - 1) + fib (x - 2)\textrm{,}}
|
s1210629013@55466
|
18 |
\noindent
|
s1210629013@55466
|
19 |
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,
|
s1210629013@55466
|
20 |
\imlcode{~~\=fu\=n \=fi\=b' 0 = (0, 1)\\
|
s1210629013@55466
|
21 |
\>\>| fib' n = let\\
|
s1210629013@55466
|
22 |
\>\>\>\>val (x1, x2) = fib' (n - 1)\\
|
s1210629013@55466
|
23 |
\>\>\>in\\
|
s1210629013@55466
|
24 |
\>\>\>\>(x2, x1 + x2)\\
|
s1210629013@55466
|
25 |
\>\>\>end;\\
|
s1210629013@55466
|
26 |
\>(*gets 2nd element of touple*)\\
|
s1210629013@55466
|
27 |
\>fun fib n = fib' (n - 1) |> snd \textrm{,}}
|
s1210629013@55466
|
28 |
\noindent
|
s1210629013@55466
|
29 |
shows linear runtime behavior. Annotations (section \ref{sec:annot}) were demonstrated using the Fibonacci function (page \pageref{alg:parannot}):
|
s1210629013@55466
|
30 |
\imlcode{~~\=fu\=n fib 0 = 1\\
|
s1210629013@55466
|
31 |
\>\>| fib 1 = 1\\
|
s1210629013@55466
|
32 |
\>\>| fib x = fib (x - 1) + par (fib (x - 2))}
|
s1210629013@55466
|
33 |
\noindent
|
s1210629013@55466
|
34 |
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.
|
s1210629013@55466
|
35 |
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:
|
s1210629013@55466
|
36 |
\imlcode{\label{alg:fib-futures}
|
s1210629013@55466
|
37 |
~~\=fu\=n \=fi\=b \=0 = 1\\
|
s1210629013@55466
|
38 |
\>\>| fib 1 = 1\\
|
s1210629013@55466
|
39 |
\>\>| fib x = let\\
|
s1210629013@55466
|
40 |
\>\>\>\>\>fun fib' () = fib (x - 2)\\
|
s1210629013@55466
|
41 |
\>\>\>\>\>val fibf = Future.fork fib'\\
|
s1210629013@55466
|
42 |
\>\>\>\>in fib (x - 1) + (Future.join fibf) end}
|
s1210629013@55466
|
43 |
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.
|
s1210629013@55466
|
44 |
|
s1210629013@55466
|
45 |
|
s1210629013@55466
|
46 |
\section{{\tt merge\_lists} implementation}
|
s1210629013@55466
|
47 |
\label{app:merge-lists}
|
s1210629013@55466
|
48 |
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.
|
s1210629013@55466
|
49 |
\begin{program}
|
s1210629013@55466
|
50 |
\caption{{\tt merge\_lists} implementation.}
|
s1210629013@55466
|
51 |
\label{alg:merge-lists}
|
s1210629013@55466
|
52 |
\begin{MLCode}
|
s1210629013@55466
|
53 |
fun merge out [] xs = (rev out) @ xs
|
s1210629013@55466
|
54 |
| merge out xs [] = (rev out) @ xs
|
s1210629013@55466
|
55 |
| merge out (xs' as x::xs) (ys' as y::ys) =
|
s1210629013@55466
|
56 |
if x = y then
|
s1210629013@55466
|
57 |
merge (x::out) xs ys
|
s1210629013@55466
|
58 |
else if x < y then
|
s1210629013@55466
|
59 |
merge (x::out) xs ys'
|
s1210629013@55466
|
60 |
else
|
s1210629013@55466
|
61 |
merge (y::out) xs' ys;
|
s1210629013@55466
|
62 |
val merge_lists' = merge [];
|
s1210629013@55466
|
63 |
fun merge_lists (xs, ys) = merge_lists' xs ys;
|
s1210629013@55466
|
64 |
\end{MLCode}
|
s1210629013@55466
|
65 |
\end{program}
|
s1210629013@55466
|
66 |
|
s1210629013@55466
|
67 |
|
s1210629013@55466
|
68 |
\section{Irrationality of \texorpdfstring{$\sqrt{2}$}{the square root of 2} in \textit{Isar}}
|
s1210629013@55466
|
69 |
\label{app:sqrt2-isar}
|
s1210629013@55466
|
70 |
|
s1210629013@55466
|
71 |
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}.
|
s1210629013@55466
|
72 |
|
s1210629013@55466
|
73 |
|
s1210629013@55466
|
74 |
\begin{program}
|
s1210629013@55466
|
75 |
\caption{\textit{Isabelle/Isar} proof of the irrationality of $\sqrt{2}$.}
|
s1210629013@55466
|
76 |
\label{alg:isar-sqrt2}
|
s1210629013@55466
|
77 |
\vspace{\medskipamount}
|
s1210629013@55466
|
78 |
\noindent
|
s1210629013@55466
|
79 |
\colorbox{color5}{\texttt{\small
|
s1210629013@55466
|
80 |
\begin{minipage}{.98\textwidth}
|
s1210629013@55466
|
81 |
\setlength{\parindent}{1pc}
|
s1210629013@55466
|
82 |
\noindent
|
s1210629013@55466
|
83 |
{\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}$"}\\
|
s1210629013@55466
|
84 |
{\tiny\ttfamily\color{color6} 2~}~{\indent({\bfseries\color{color1} is} {\color{color3} "EX a b. ?P a b"})}\\
|
s1210629013@55466
|
85 |
{\tiny\ttfamily\color{color6} 3~}~{\bfseries\color{color1} proof} cases\\
|
s1210629013@55466
|
86 |
{\tiny\ttfamily\color{color6} 4~}~{\indent\bfseries\color{color1} assume} {\color{color3} "sqrt 2 powr sqrt 2 $\in$ $\mathbb{Q}$"}\\
|
s1210629013@55466
|
87 |
{\tiny\ttfamily\color{color6} 5~}~{\indent\bfseries\color{color1} then have} {\color{color3} "?P (sqrt 2) (sqrt 2)"}\\
|
s1210629013@55466
|
88 |
{\tiny\ttfamily\color{color6} 6~}~{\indent\indent\bfseries\color{color1} by} (metis sqrt\_2\_not\_rat)\\
|
s1210629013@55466
|
89 |
{\tiny\ttfamily\color{color6} 7~}~{\indent\bfseries\color{color1} then show} {\color{color2} ?thesis} {\bfseries\color{color1} by} blast\\
|
s1210629013@55466
|
90 |
{\tiny\ttfamily\color{color6} 8~}~{\bfseries\color{color1} next}\\
|
s1210629013@55466
|
91 |
{\tiny\ttfamily\color{color6} 9~}~{\indent\bfseries\color{color1} assume} 1: {\color{color3} "sqrt 2 powr sqrt 2 $\notin$ $\mathbb{Q}$"}\\
|
s1210629013@55466
|
92 |
{\tiny\ttfamily\color{color6} 10}~{\indent\bfseries\color{color1} have} {\color{color3} "(sqrt 2 powr sqrt 2) powr sqrt 2 = 2"}\\
|
s1210629013@55466
|
93 |
{\tiny\ttfamily\color{color6} 11}~{\indent\indent\bfseries\color{color1} using} powr\_realpow [of \_ 2]\\
|
s1210629013@55466
|
94 |
{\tiny\ttfamily\color{color6} 12}~{\indent\indent\bfseries\color{color1} by} (simp add: powr\_powr power2\_eq\_square [symmetric])\\
|
s1210629013@55466
|
95 |
{\tiny\ttfamily\color{color6} 13}~{\indent\bfseries\color{color1} then have} {\color{color3} "?P (sqrt 2 powr sqrt 2) (sqrt 2)"}\\
|
s1210629013@55466
|
96 |
{\tiny\ttfamily\color{color6} 14}~{\indent\indent{\bfseries\color{color1} by} (metis 1 Rats\_number\_of sqrt\_2\_not\_rat)}\\
|
s1210629013@55466
|
97 |
{\tiny\ttfamily\color{color6} 15}~{\indent\bfseries\color{color1} then show} {\color{color2} ?thesis} {\bfseries\color{color1} by} blast\\
|
s1210629013@55466
|
98 |
{\tiny\ttfamily\color{color6} 16}~{\bfseries\color{color1} qed}
|
s1210629013@55466
|
99 |
\end{minipage}}}
|
s1210629013@55466
|
100 |
\end{program}
|
s1210629013@55466
|
101 |
|