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