Rev 37 | Details | Compare with Previous | Last modification | View Log | RSS feed

Rev | Author | Line No. | Line |
---|---|---|---|

19 | haftmann | 1 | |

20 | haftmann | 2 | `% aims` |

3 | `% * raw material for proposal` |
||

4 | `% * properties of Isabelle relevant for project context` |
||

5 | `% * comparison to other TP systems – why Isabelle?` |
||

6 | `% * communication of Isabelle to non-TP-people` |
||

7 | |||

19 | haftmann | 8 | |

29 | neuper | 9 | \section{Mission}\label{mission} |

10 | |||

28 | neuper | 11 | `We give an overview of the interactive proof assistant Isabelle/HOL \cite{Nipkow-Paulson-Wenzel:2002}` |

26 | haftmann | 12 | `with a particular focus on properties which are relevant in our envisaged project context.` |

19 | haftmann | 13 | |

14 | `When reading this, bear in mind that the aim of this project is to` |
||

15 | `provide a running prototype environment. This requires to focus on` |
||

16 | `one particular TP system. This does not imply that the issues we want` |
||

17 | `to investigate could not be transferred to other TP systems as well – but` |
||

18 | `without any experience gained from a prototype, it is too early to` |
||

33 | haftmann | 19 | `generalise, although this could be a focus of a future successor project.` |

26 | haftmann | 20 | |

21 | `A baseline is that only \emph{interactive} proof assistants come into question.` |
||

22 | `This rules out the vast collection of automatic provers, but also bare` |
||

28 | neuper | 23 | `programming languages like Agda \cite{adga-phd-07}. Typical representatives of` |

26 | haftmann | 24 | `interactive proof assistants are the Coq system,` |

28 | neuper | 25 | `\cite{coq-team-10}, ACL2 \cite{moore:acl2-00}, Mizar\footnote{http://mizar.org/}, the HOL` |

26 | `family\footnote{This covers both HOL4 \cite{Gordon:93} and HOL Light \cite{harrison:hol-light}}, and Isabelle/HOL.` |
||

26 | haftmann | 27 | |

28 | `A realistic crosscut through relevant properties of existing TP` |
||

20 | haftmann | 29 | `systems led us to the conclusion that Isabelle/HOL (from now, just Isabelle)` |

26 | haftmann | 30 | `is the most promising one to start with.` |

19 | haftmann | 31 | |

32 | |||

33 | `\section{How Isabelle/HOL presents itself}` |
||

34 | |||

29 | neuper | 35 | `\subsection{Calculus}\label{calculus}` |

19 | haftmann | 36 | |

23 | haftmann | 37 | `The logical calculus of Isabelle is higher-order logic (HOL) of simply-typed` |

38 | `schematically polymorphic $\lambda$-terms:` |
||

19 | haftmann | 39 | |

40 | `\begin{description}` |
||

41 | |||

42 | ` \item[types $\tau$] consist of \emph{type constructors}` |
||

43 | ` $\kappa$ with a fixed arity and type variables $\alpha$:` |
||

44 | |||

45 | ` \[` |
||

46 | ` \tau ::= \kappa \ \tau_1 \cdots \tau_k \ \| \ \alpha` |
||

47 | ` \]` |
||

48 | |||

49 | ` Function space $\alpha \Rightarrow \beta$ is simply a binary type` |
||

50 | ` constructor.` |
||

51 | |||

52 | ` \item[terms $t$] include application, abstraction,` |
||

53 | ` (local) variables of a particular type, and constants (operations):` |
||

54 | |||

55 | ` \[` |
||

24 | haftmann | 56 | ` t ::= t_1 \ t_2 \ \| \ \lambda x :: \tau. \ t \ \| \ x :: \tau \ \| \ f` |

19 | haftmann | 57 | ` \]` |

58 | |||

27 | neuper | 59 | ` \item[formulae $P$] are terms of a distinguished type \emph{bool}` |

19 | haftmann | 60 | ` with the usual connectives: conjunction, disjunction, implication,` |

26 | haftmann | 61 | ` negation, universal and existential quantifiers. By convention,` |

33 | haftmann | 62 | ` chained implications at the outermost level are printed as inference rules:` |

26 | haftmann | 63 | ` $Q_1 \Longrightarrow … \Longrightarrow Q_n \Longrightarrow P$ is printed` |

64 | ` as` |
||

65 | ` \begin{simplegather}` |
||

66 | ` \infer{P}{Q_1 … Q_n}` |
||

67 | ` \end{simplegather}` |
||

19 | haftmann | 68 | |

69 | ` A constant (operation) with a particular relevance for formulae` |
||

23 | haftmann | 70 | ` is equality $t_1 = t_2$ of type $\alpha \Rightarrow \alpha \Rightarrow$` |

25 | haftmann | 71 | ` \emph{bool}.` |

19 | haftmann | 72 | |

73 | `\end{description}` |
||

74 | |||

20 | haftmann | 75 | `On top of this core calculus, Isabelle provides various predefined` |

19 | haftmann | 76 | `type constructors with corresponding operations that resemble concepts` |

77 | `well-known from mathematics and functional programming:` |
||

78 | |||

79 | `\begin{description}` |
||

80 | |||

24 | haftmann | 81 | ` \item[numeric types \emph{nat}, \emph{int}, \emph{rat}, \emph{real}, \emph{complex}]` |

19 | haftmann | 82 | ` modelling the natural, integer, rational, real and complex numbers` |

83 | ` with the usual arithmetic operations;` |
||

84 | |||

85 | ` \item[type of sets \emph{$\alpha$ set}] modelling sets as comprehensions` |
||

86 | ` over predicates of type \emph{$\alpha \Rightarrow$ bool} with typical` |
||

87 | ` operations like union, intersection, difference, set product, image` |
||

88 | ` of a set under a operation etc.` |
||

89 | |||

24 | haftmann | 90 | ` \item[fundamental collection types \emph{unit}, $\alpha * \beta$, \emph{$\alpha$ option}, \emph{$\alpha$ list}]` |

91 | ` representing the common unit, product, option and list types from functional programming` |
||

92 | ` with dozens of operations similar to what can be found in typical functional` |
||

93 | ` programming libraries: membership test, concatenation, reversal, sorting, etc.` |
||

19 | haftmann | 94 | |

24 | haftmann | 95 | ` \item[advanced data structures, e.g. red-black trees \emph{$(\alpha, \beta)$ rbt}]` |

19 | haftmann | 96 | ` with the typical lookup, insert and delete operations` |

97 | ` providing efficient data structures for functional programs embedded` |
||

33 | haftmann | 98 | ` in Isabelle (see \secref{code-generation}).` |

19 | haftmann | 99 | |

100 | `\end{description}` |
||

101 | |||

20 | haftmann | 102 | `Isabelle also comes with syntactic sugar for \emph{if}-, \emph{let}- and` |

23 | haftmann | 103 | `\emph{case}-expressions known from functional programming, which are` |

24 | haftmann | 104 | `internally mapped to suitable combinators.` |

19 | haftmann | 105 | |

106 | |||

39 | haftmann | 107 | `\subsection{Specification and proof language Isar}\label{Isar}` |

19 | haftmann | 108 | |

20 | haftmann | 109 | `To conduct formal developments, Isabelle uses the specification` |

110 | `and proof language \emph{Isar}. An Isar text is` |
||

111 | `structured as a series of Isar commands, each consisting of a` |
||

112 | `particular keyword followed by text denoting logical and non-logical` |
||

113 | `entities (types, terms, names, \ldots). Isar commands are aggregated` |
||

114 | `in theories, where one theory's content is given by the Isar commands` |
||

115 | `it contains: commands add type constructors, constants, proofs etc.` |
||

116 | `to the theory.` |
||

19 | haftmann | 117 | |

20 | haftmann | 118 | `Typical representatives of Isar commands are specification tools as follows:` |

19 | haftmann | 119 | |

20 | haftmann | 120 | `\begin{description}` |

19 | haftmann | 121 | |

20 | haftmann | 122 | ` \item[Inductive datatypes] correspond to datatype declarations` |

123 | ` in functional programming languages:` |
||

19 | haftmann | 124 | |

20 | haftmann | 125 | \isacommand{datatype}\isamarkupfalse% |

126 | \ color\ {\isacharequal}\ R\ {\isacharbar}\ B\isanewline |
||

127 | \isacommand{datatype}\isamarkupfalse% |
||

24 | haftmann | 128 | \ {\isacharparenleft}$\alpha${\isacharcomma}\ $\beta${\isacharparenright}\ rbt\ {\isacharequal}\ Empty\ {\isacharbar}\ Branch\ color\ ({\isachardoublequoteopen}{\isacharparenleft}$\alpha${\isacharcomma}\ $\beta${\isacharparenright}\ rbt{\isachardoublequoteclose})\ $\alpha$\ $\beta$\ ({\isachardoublequoteopen}{\isacharparenleft}$\alpha${\isacharcomma}\ $\beta${\isacharparenright}\ rbt{\isachardoublequoteclose})\isanewline |

19 | haftmann | 129 | |

20 | haftmann | 130 | ` \item[Recursive functions with pattern matching] correspond to function` |

131 | ` definitions in functional programming languages:` |
||

19 | haftmann | 132 | |

20 | haftmann | 133 | \isacommand{fun}\isamarkupfalse% |

24 | haftmann | 134 | \ splice\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}$\alpha$\ list\ {\isasymRightarrow}\ $\alpha$\ list\ {\isasymRightarrow}\ $\alpha$\ list{\isachardoublequoteclose}\ \isakeyword{where}\isanewline |

135 | ` \ {\isachardoublequoteopen}splice\ {\isacharbrackleft}{\isacharbrackright}\ ys\ {\isacharequal}\ ys{\isachardoublequoteclose}\ {\isacharbar}\isanewline` |
||

136 | ` \ {\isachardoublequoteopen}splice\ xs\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs{\isachardoublequoteclose}\ {\isacharbar}\isanewline` |
||

137 | \ {\isachardoublequoteopen}splice\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}\ {\isacharequal}\ x\ {\isacharhash}\ y\ {\isacharhash}\ splice\ xs\ ys{\isachardoublequoteclose}% |
||

19 | haftmann | 138 | |

20 | haftmann | 139 | TP experts may note that recursive function definitions within |

140 | a formal calculus require a complex machinery to construct termination |
||

141 | proofs and similar. The good news is that end-users need only seldom |
||

142 | to care about that: Isabelle's function package does the job |
||

22 | haftmann | 143 | for a huge class of practically occurring functions |

20 | haftmann | 144 | \cite{nipkow-krauss:07-find-lex-orders,Krauss:07-size-terminat}. |

19 | haftmann | 145 | |

20 | haftmann | 146 | `\end{description}` |

19 | haftmann | 147 | |

23 | haftmann | 148 | `Note that Isabelle's calculus as presented here resembles an ML-like` |

24 | haftmann | 149 | `programming language enriched with logical concepts like sets and quantifiers:` |

150 | `datatype and function definitions enable a user to extend the calculus with new notions` |
||

20 | haftmann | 151 | `in the manner of a functional programming language, and state properties` |

23 | haftmann | 152 | `about those newly introduced concepts. In other words, Isabelle's can be` |

24 | haftmann | 153 | `seen as a carrier for a shallowly embedded functional programming language;` |

23 | haftmann | 154 | `this observation, condensed into the slogan »HOL = functional programming +` |

24 | haftmann | 155 | `logic«, has a couple of consequences:` |

19 | haftmann | 156 | |

20 | haftmann | 157 | `\begin{itemize}` |

19 | haftmann | 158 | |

24 | haftmann | 159 | ` \item People with a (functional) programming language background get acquainted` |

33 | haftmann | 160 | ` with Isabelle comparably fast, and most existing introductions to Isabelle` |

20 | haftmann | 161 | ` follow that track \cite{nipkow-prog-prove}.` |

19 | haftmann | 162 | |

20 | haftmann | 163 | ` \item Algorithmic issues can be expressed directly in a functional style` |

164 | ` in Isabelle, which eases transfer of algorithms from CA to Isabelle.` |
||

19 | haftmann | 165 | |

20 | haftmann | 166 | ` \item Formulations in the embedded functional programming language` |

23 | haftmann | 167 | ` can be translated to code for common functional programming language` |

39 | haftmann | 168 | ` systems using code generation \secref{code-generation}.` |

19 | haftmann | 169 | |

20 | haftmann | 170 | `\end{itemize}` |

171 | |||

172 | `\fixme[elaborate: comparison to other systems]` |
||

173 | |||

23 | haftmann | 174 | `Proofs themselves, the Holy Grail of TP systems, are conducted in a fragment` |

24 | haftmann | 175 | of the Isar language, the Isar \emph{proof} language. This is not a tutorial |

27 | neuper | 176 | `% //////////////////////` |

24 | haftmann | 177 | on how to write Isar proofs, and in our project the envisaged end users, mainly |

20 | haftmann | 178 | engineers, are not expected to come in touch with fundamental proofs at all, |

27 | neuper | 179 | `% !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!` |

29 | neuper | 180 | `% Proofs of within domain-specific knowledge might become the duty of so-called` |

181 | `% domain-engineers: they do not only provide algorithms solving particular` |
||

182 | `% domain-specific problems, rather, they start with formalizing the essential` |
||

183 | `% notions of the domain by definitions, theorem and proofs ` |
||

184 | `% \cite{db:SW-engIII,db:dom-eng,Hansen94b,Dehbonei&94}.` |
||

185 | `% ` |
||

23 | haftmann | 186 | as this is rather the task of the system implementers; therefore we will |

24 | haftmann | 187 | not dive deeper here. Nevertheless, the ability to write human-readable and |

23 | haftmann | 188 | robust proofs in Isar is a key aspect to maintain voluminous formal |

24 | haftmann | 189 | developments in the mid-term and long-term run. \footnote{An ever-growing collection |

37 | haftmann | 190 | `of Isabelle developments is collected in the Archive of Formal Proofs\footnote{\url{http://afp.sourceforge.net/topics.shtml}};` |

191 | `adjustments because of broken` |
||

20 | haftmann | 192 | proofs due to changes in the system have become seldom over the years.} |

193 | |||

27 | neuper | 194 | `%% ^^^ relates to pt.3 in TPPL-abstract.tex in particular:` |

195 | `%% with this go into detail in \sect{Methods}` |
||

196 | |||

20 | haftmann | 197 | \fixme[elaborate: comparison to other systems] |

198 | |||

199 | |||

33 | haftmann | 200 | \subsection{A bluffer's glance at Isabelle's architecture}\label{architecture} |

20 | haftmann | 201 | |

33 | haftmann | 202 | `This short overview provides the context to understand the subsequent technical` |

203 | `details.` |
||

204 | |||

205 | `\begin{center}` |
||

206 | `\includegraphics[width=0.5\linewidth]{fig/fig-isabelle-architecture}` |
||

207 | `\end{center}` |
||

208 | |||

209 | `\begin{itemize}` |
||

210 | |||

211 | `\item Interaction with the system nowadays happens through` |
||

212 | ` an IDE (see \secref{jedit}) which is implemented` |
||

213 | ` in Scala \footnote{\url{http://www.scala-lang.org}; Scala combines an industry-proven` |
||

214 | ` runtime environment, the Java Virtual Machine (JVM), with a state-of-the-art` |
||

215 | ` type-safe general purpose programming language.}.` |
||

216 | |||

217 | `\item The interactive prover itself acts as a backend to the IDE` |
||

218 | ` and is implemented in Standard ML. The languages of the ML family are standard workhorses` |
||

219 | ` for interactive provers; Isabelle prefers PolyML which excels especially` |
||

220 | ` in parallelism (see \secref{parallel}).` |
||

221 | |||

222 | `\item External non-interactive provers can be hooked to the core prover` |
||

223 | ` (see \secref{external}).` |
||

224 | |||

225 | `\item Code generation allows to turn suitable specifications` |
||

226 | ` into programs (see \secref{code-generation}).` |
||

227 | |||

228 | `\end{itemize}` |
||

229 | |||

230 | |||

231 | `\subsection{The jEdit user interface}\label{jedit}` |
||

232 | |||

23 | haftmann | 233 | `Traditionally, TP systems have a reputation of being difficult to access.` |

234 | `Recent developments in Isabelle attempt to overcome this by providing` |
||

235 | `a state-of-the-art editor framework (jEdit) with a plugin establishing` |
||

236 | `an IDE-like feeling when editing Isabelle theories:` |
||

20 | haftmann | 237 | |

23 | haftmann | 238 | `\begin{center}` |

239 | `\includegraphics[width=0.7\linewidth]{fig/jedit}` |
||

240 | `\end{center}` |
||

20 | haftmann | 241 | |

23 | haftmann | 242 | `The key idea to make this work is continuous proof checking: the theory` |

26 | haftmann | 243 | `source text is annotated by semantic information by the proof assistant as it becomes` |

23 | haftmann | 244 | `available incrementally. This works via an asynchronous` |

26 | haftmann | 245 | `protocol that neither blocks the editor nor stops the proof assistant from` |

23 | haftmann | 246 | `exploiting parallelism on multi-core hardware` |

247 | `\cite{makarius:isa-scala-jedit,makarius-jEdit-12}.` |
||

20 | haftmann | 248 | |

23 | haftmann | 249 | `User interface support is vital to our project aims. The traditional` |

250 | `users of TP systems have mostly been scientists engaging in logic or` |
||

251 | `verification with a strong background in computer science, who would` |
||

252 | `find their individual ways to cope with the arcane TP system interfaces.` |
||

253 | `If we want to target engineers, we cannot expect them to develop` |
||

254 | `a similar hackitude, but must strive to provide a system with a user` |
||

255 | `interface similar to what one can expect today from computer tools.` |
||

20 | haftmann | 256 | |

23 | haftmann | 257 | `Since Isabelle's jEdit interface is JVM-based, existing visualisation` |

258 | `tools in Java, e.g. for drawing function graphs, could be incorporated` |
||

259 | `if this turns out to be necessary.` |
||

20 | haftmann | 260 | |

23 | haftmann | 261 | `The continuous proof checking approach with all its consequences` |

262 | `currently is unique to Isabelle, setting it apart in this respect.` |
||

263 | |||

264 | |||

19 | haftmann | 265 | `\section{System architecture}` |

266 | |||

24 | haftmann | 267 | `\subsection{Reconciling trustability and extensibility – the LCF approach}` |

19 | haftmann | 268 | |

26 | haftmann | 269 | `Isabelle is a proof assistant in the LCF tradition: each proof or theorem` |

270 | `is internally represented by a value of an abstract type \verb!thm! in` |
||

33 | haftmann | 271 | `the underlying (type-safe!) implementation language which can only be` |

26 | haftmann | 272 | `manipulated by a few trusted primitive operations, the so-called` |

37 | haftmann | 273 | `inference kernel \cite{meta-ML-79}. Therefore any construction of proofs` |

26 | haftmann | 274 | `in the run-time system boils down to operations from the inference kernel.` |

275 | `This results in high trustability. What makes this rigorous approach scale` |
||

37 | haftmann | 276 | `is that there is no fundamental distinction between operations or theorems` |

277 | `which are built-in in the sense of the inference kernel, and derived ones. This` |
||

26 | haftmann | 278 | `allows to derive operations and corresponding proof rules in terms of existing ones` |

279 | `but to ignore their construction later on. E.g. existential quantification` |
||

280 | `$\exists$\footnote{Existential quantification itself is indeed no built-in but a derived concept}` |
||

281 | `comes with two natural-deduction-style \citeme inference rules` |
||

19 | haftmann | 282 | |

26 | haftmann | 283 | `\begin{simplegather}` |

284 | ` \infer[{ex}_{intro}]{\exists x. P \: x}{P \: t} \quad` |
||

285 | ` \infer[{ex}_{elim}]{R}{\exists x. P \: x && (\forall x. P \: x \Longrightarrow R)}` |
||

286 | `\end{simplegather}` |
||

19 | haftmann | 287 | |

26 | haftmann | 288 | `Defining divisibility on the natural numbers using multiplication on natural numbers` |

289 | |||

290 | `\begin{simplegather}` |
||

291 | ` m \| n = (\exists q. n = q * m)` |
||

292 | `\end{simplegather}` |
||

293 | |||

294 | `the following natural-deduction-style inference rules for divisibility can be derived` |
||

295 | |||

296 | `\begin{simplegather}` |
||

297 | ` \infer[{divides}_{intro}]{m \| n}{n = q * m} \quad` |
||

298 | ` \infer[{divides}_{elim}]{R}{m \| n && (\forall q. n = q * m \Longrightarrow R)}` |
||

299 | `\end{simplegather}` |
||

300 | |||

301 | `Reasoning on divisibility then may continue using these two rules, regardless` |
||

302 | `how the original definition of divisibility and the proofs of the corresponding` |
||

303 | `inference rules have been accomplished.` |
||

304 | |||

305 | `\fixme[evaluate and compare to other systems]` |
||

306 | |||

307 | |||

22 | haftmann | 308 | `\subsection{Programmatic extensibility}` |

19 | haftmann | 309 | |

26 | haftmann | 310 | `Since theorems are values in the underlying ML implementation language, they` |

311 | `can be manipulated by arbitrary programmatic means. This allows to automate` |
||

312 | `complex specification and proof steps.` |
||

313 | `Prominent examples are the function package` |
||

314 | `mentioned above \refme, or Isabelle's simplifier which enables the user` |
||

315 | `to perform equational reasoning automatically.` |
||

19 | haftmann | 316 | |

26 | haftmann | 317 | `An instance in our project context could be to provide trusted` |

37 | haftmann | 318 | `computation machineries, e.g.~accompany Isabelle's Kurzweil-Henstock` |

28 | neuper | 319 | `Gauge Integration \cite{kurzweil-henstock:integral-00} in many dimensions with tools to actually` |

26 | haftmann | 320 | `compute integrals.` |

19 | haftmann | 321 | |

26 | haftmann | 322 | `\fixme[compare to other systems]` |

19 | haftmann | 323 | |

26 | haftmann | 324 | |

19 | haftmann | 325 | `\subsection{Syntax variability}` |

326 | |||

26 | haftmann | 327 | `Isabelle's syntax in large parts is not hard-wired to the system. This` |

328 | `allows to customise the appearance of commands, terms etc. with high degrees` |
||

329 | `of freedom. In the context of computer science, this is not really an issue:` |
||

330 | `computer scientists are used to switch between different notational conventions` |
||

331 | `as needed. However, we want to approach engineers with a different attitude` |
||

332 | `and approximate notation found in engineering literature as close as possible and appropriate.` |
||

19 | haftmann | 333 | |

26 | haftmann | 334 | `\fixme[example: example from engineering book, example in Isabelle »as it is«, possible variant of Isabelle syntax]` |

335 | |||

336 | `\fixme[compare to other systems]` |
||

337 | |||

338 | |||

19 | haftmann | 339 | `\section{Speedful computation}` |

340 | |||

26 | haftmann | 341 | `Proof assistants are designed for proofs, but often do not perform` |

37 | haftmann | 342 | `very well on computations \footnote{This goes back to the first edition` |

343 | `of Russell's \emph{Principia}, where the proof of $1 + 1 = 2$ appears` |
||

344 | `only on page 379.}` |
||

345 | `The deeper reason is that by their very nature proof assistants carry out` |
||

26 | haftmann | 346 | `computations \emph{symbolically} which is quite heavyweight.` |

347 | `In this section we discuss some devices to make computations in Isabelle` |
||

348 | `feasible in practice.` |
||

349 | |||

350 | |||

33 | haftmann | 351 | `\subsection{Parallel computation}\label{parallel}` |

19 | haftmann | 352 | |

26 | haftmann | 353 | `Recent releases of Isabelle exploit parallelism on multicore machines` |

28 | neuper | 354 | `\cite{makarius:isa-scala-jedit}. Beside the speedup itself, this is also a device to keep` |

26 | haftmann | 355 | `up reactivity of the system while background threads are engaged` |

37 | haftmann | 356 | `in massive computations \secref{jedit}. On suitable hardware, speedups` |

357 | `by factor of 4 to 5 have been achieved \cite{parallel-ML}. Recent versions of` |
||

358 | `PolyML (Isabelle's run-time system) featuring parallel garbage` |
||

26 | haftmann | 359 | `collection have shown further boost.` |

19 | haftmann | 360 | |

37 | haftmann | 361 | `Both the parallelism facilities of the underlying run-time system as` |

362 | `well as the consideration and exploitation of parallelism in the` |
||

363 | `overall system architecture in combination currently set Isabelle` |
||

364 | `apart from similar systems in that respect.` |
||

19 | haftmann | 365 | |

26 | haftmann | 366 | |

33 | haftmann | 367 | `\subsection{Code generation and datatype refinement}\label{code-generation}` |

19 | haftmann | 368 | |

39 | haftmann | 369 | `To avoid the overhead of computations \emph{within} the proof assistant,` |

370 | `it is possible to generate code from specifications and run that code` |
||

371 | `in its target language environment. Isabelle implements code generation` |
||

372 | `by turning a suitable set of equational theorems into a program` |
||

373 | `with the \emph{same equational semantics} in a specific language; currently,` |
||

374 | `Standard ML, OCaml, Haskell and Scala are supported` |
||

375 | `\cite{haftm-nipkow-code-gen-HRS-10}. Typical applications of code generation` |
||

376 | `are:` |
||

19 | haftmann | 377 | |

39 | haftmann | 378 | `\begin{itemize}` |

19 | haftmann | 379 | |

39 | haftmann | 380 | ` \item Turning a specification into a executable program which` |

381 | ` by construction obeys the original specification.` |
||

19 | haftmann | 382 | |

39 | haftmann | 383 | ` \item Using generated code as a fast evaluator. This is` |

384 | ` particularly suitable for decision procedures, i.e.~` |
||

385 | ` procedures that solve a class of problems programmatically` |
||

386 | ` but by construction of a suitable proofs, which often involves` |
||

387 | ` heavy equational rewriting \cite{Chaieb-PhD}.` |
||

19 | haftmann | 388 | |

39 | haftmann | 389 | `\end{itemize}` |

19 | haftmann | 390 | |

39 | haftmann | 391 | `A particularity of Isabelle's code generator is that it comes` |

392 | `with support for algorithm and datatype refinement, which allows` |
||

393 | `it e.g. to implement (finite) sets by balanced trees in a trustable way (see` |
||

394 | `\cite{isa-codegen}) – and thus more performant code.` |
||

19 | haftmann | 395 | |

39 | haftmann | 396 | `Note that specifications restricting themselves to the shallowly` |

397 | `embedded programming language of Isabelle identified in \secref{Isar}` |
||

398 | `can (almost) always be turned into programs by code generation` |
||

399 | `without further ado, which enables engineers etc. developing` |
||

400 | `algorithms in them are able to see their algorithms work on` |
||

401 | `other platforms, too.` |
||

19 | haftmann | 402 | |

39 | haftmann | 403 | `For specifications which go beyond that language, there is still` |

404 | `a high chance that reasonable subsets can be turned executable` |
||

405 | `by providing reasonable models for the involved types. E.g.~although` |
||

406 | `rational numbers in Isabelle are constructed abstractly using` |
||

407 | `quotients, they are executable by default since at the same` |
||

408 | `time an implementation by pairs of integer numbers is provided.` |
||

409 | |||

410 | |||

33 | haftmann | 411 | `\subsection{Integration of external tools}\label{external}` |

19 | haftmann | 412 | |

26 | haftmann | 413 | `Over the years, various external tools have been hooked to the Isabelle` |

28 | neuper | 414 | `system, e.g. first-order provers for the sledgehammer proof searcher \cite{sledgehammer-10},` |

37 | haftmann | 415 | `SAT solvers for the nitpick counterexample searcher \cite{nitpick-10}, etc.` |

19 | haftmann | 416 | |

26 | haftmann | 417 | `These external tools are generally useful on their own; even` |

418 | `more relevant is the shared generic infrastructure to connect Isabelle` |
||

419 | `to external tools, which turns Isabelle into a system hub for gluing together` |
||

28 | neuper | 420 | `various kinds of systems for proving, computing, evaluating, etc. This` |

26 | haftmann | 421 | `enables us to integrate specific CA tools into the whole machinery` |

28 | neuper | 422 | `where necessary.` |

19 | haftmann | 423 | |

26 | haftmann | 424 | `\fixme[comparison to other systems]` |

425 | |||

426 | |||

29 | neuper | 427 | `\section{Isabelle's knowledge for application in engineering}` |

428 | `Isabelle's features described so far establish a system appealing for` |
||

429 | `computer scientists, mathematicians and logicians to mechanise their` |
||

430 | `respective knowledge due to individual interests and in projects of` |
||

37 | haftmann | 431 | `various size. The Isabelle developer has been continuously integrating` |

432 | `the many contributions to a coherent and manageable system of mechanised` |
||

433 | `knowledge, providing a base for further development.` |
||

19 | haftmann | 434 | |

37 | haftmann | 435 | |

29 | neuper | 436 | `\subsection{Preexisting formalisations}` |

28 | neuper | 437 | |

37 | haftmann | 438 | `In addition to the datatypes mentioned in \secref{calculus}, the` |

439 | `Isabelle distribution~\footnote{http://isabelle.in.tum.de/dist/library/HOL}` |
||

440 | `and the accompanying Archive of Formal Proofs~\footnote{\url{http://afp.sourceforge.net/topics.shtml}}` |
||

441 | `contain various already formalised knowledge which can be built on,` |
||

442 | `to name some promising candidates:` |
||

443 | |||

28 | neuper | 444 | `\begin{description}\label{isa-know-survey}` |

445 | |||

446 | `\item[Algebra] is developed from groups, rings, fields up to the` |
||

447 | `fundamental theorem of algebra in the univariate case and Groebner` |
||

448 | `bases in the multivariate case.` |
||

449 | |||

450 | `\item[Linear algebra] with executable operations on matrices of` |
||

451 | `arbitrary dimensions over ordered semirings, elementary linear algebra` |
||

452 | `on Euclidean spaces, convexity in real vector spaces up to` |
||

453 | `Gauss-Jordan Elimination for Matrices.` |
||

454 | |||

455 | `\item[Analysis] includes semicontinuous and continuous functions,` |
||

456 | `Cauchy's Mean Theorem and the Cauchy-Schwarz Inequality, MacLaurin and` |
||

457 | `Taylor series, nth roots and the transcendental functions.` |
||

458 | |||

459 | `\item[Multivariate analysis] concerning Frechet Derivative, Inner` |
||

460 | `Product Spaces and the Gradient Derivative, Finite-Dimensional Inner` |
||

461 | `Product Spaces, Multivariate calculus in Euclidean space,` |
||

462 | `Kurzweil-Henstock Gauge Integration in many dimensions, up to initial` |
||

463 | `value problems of Ordinary Differential` |
||

464 | Equations~\footnote{http://afp.sourceforge.net/entries/Ordinary\_Differential\_Equations.shtml}. |
||

465 | |||

466 | \item[Probability theory] including Binomial Coefficients, |
||

467 | Permutations, Social Choice Theory (Arrow's General Possibility |
||

468 | Theorem, Sen's Liberal Paradox and May's Theorem) and also |
||

469 | Discrete-Time Markov Chains. |
||

470 | |||

471 | \item[Polynomials] in an univariate and in a multivariate version, the |
||

472 | latter addressing monotonicity on strongly normalizing (monotone) |
||

473 | orders. \item[Number theory] with primality on $\cal N$, congruence, |
||

31 | haftmann | 474 | unique factorisation, divisibility in monoids and rings, Residue |

28 | neuper | 475 | rings: Euler's theorem and Wilson's theorem, quotient rings. |

476 | |||

29 | neuper | 477 | `% \item[Numerals] and their respective arithmetic are all available,` |

478 | `% $\cal N, I, Q, R$ and $\cal C$. For $\cal R$ there are approximations` |
||

479 | `% by floating point numbers~` |
||

480 | `% \footnote{http://isabelle.in.tum.de/dist/library/HOL/Decision\_Procs/Approximation.html}.` |
||

28 | neuper | 481 | |

482 | \end{description} |
||

483 | |||

484 | `% Following the LCF paradigm all the above knowledge is derived from` |
||

485 | `% first principles, from the axioms of HOL. The axioms, definitions,` |
||

486 | `% theorems and proofs are human readable.` |
||

29 | neuper | 487 | |

488 | This knowledge covers the range of mathematics addressed by most |
||

489 | introductory university courses in engineering sciences. So there is |
||

490 | comparably easy for the envisaged TP-PL prototype to serve in |
||

491 | engineering education. However, why should student learn something |
||

492 | which is neither required in research nor in the practice of |
||

37 | haftmann | 493 | engineering in the respective domain? |

29 | neuper | 494 | |

495 | Reaching readiness for application seems difficult in both, in |
||

30 | neuper | 496 | industry as well as in research. TP-PL decided to primarily address |

497 | research as shown in the next section. |
||

29 | neuper | 498 | |

499 | \subsection{Examples for TP-services useful in research} |
||

500 | `%\subsection{Example for an application domain}` |
||

501 | A domain where TP-PL seems to be able to serve actual research is |
||

502 | Information theory -- in spite the fact, that the Isabelle theory |
||

503 | \textit{Information.thy} in the release of 2012 covers only the first |
||

504 | `50 pages of total 650 in a standard text book~\cite{info-thy-06}: the` |
||

505 | `final theorems in \textit{Information.thy} are` |
||

506 | `\textit{mutual\_information\_eq\_entropy\_conditional\_entropy,` |
||

507 | `conditional\_entropy\_less\_eq\_entropy, entropy\_chain\_rule} and` |
||

508 | `\textit{entropy\_data\_processing}.` |
||

509 | |||

510 | `There are two promising applications, the first one is` |
||

511 | ```non-Shannon-type inequalities''~\cite{non-shannon-01}. This kind of` |
||

512 | `information theoretic inequalities still need to be treated by hand` |
||

513 | `(or by a Matlab toolbox~\cite{Ru99a}) while ``Shannon-type` |
||

514 | `inequalities'' are proved automatically by special purpose` |
||

515 | `provers~\footnote{http://user-www.ie.cuhk.edu.hk/~ITIP/}. So` |
||

516 | ```non-Shannon-type'' still might rely on interactive TP.` |
||

517 | |||

518 | `Another application is an ``inverse problem'' to the following: Given` |
||

519 | `a certain measurement device composed from several hardware and` |
||

520 | `software components, the overall precision of the device can be` |
||

521 | `calculated. Of practical interest is the problem inversion: Given a` |
||

522 | `certain precision requested by customers or by standards, how can the` |
||

523 | `components be optimised in costs and responsiveness by reducing` |
||

524 | `respective precision such that the precision requested for the` |
||

525 | `over-all system is still met. This inverse problem can be tackled by a` |
||

526 | `TP-based program using Isabelle's interval` |
||

527 | arithmetic~\cite{hoelzl09realineequalities}, which, after a trial and |
||

528 | error optimisation, would lead to a proof that the ``optimised'' |
||

529 | device meets the requirements. |
||

30 | neuper | 530 | |

39 | haftmann | 531 | \fixme[Provide a detailed example for the ``inverse problem''.] |