Subversion Repositories TPPL

Rev

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''.]