The relation of this paper to “Theorem-Proving (TP) components for educational software” deserves explanation: TP technology is designed for mechanised justification of formalised facts - so educational software gains a prerequisite for being a “transparent system” [12] which explains itself. Computer Algebra (CA), however, is not designed for justification (and thus leaves full responsibility for interpreting results with the user, which over-strains students frequently), and CA is not designed for “transparency”1. So integration of CA into TP promises to improve justification and “transparency” of CA, provides requisites for step-wise “Lucas-Interpretation” [11], another advantage for interactive educational software.
but in Isabelle/HOL. The first challenge was to identify, which SML integers represent coefficients of polynomials, and which represent primes. The latter were represented by HOL’s nat — an instructive exercise in precise programming.
The translation took care to use the simplest Isabelle tool possible: definition for non-recursive functions (which well might comprise fold or map), primrec for primitive recursion and fun otherwise. The latter resolves all proof obligations automatically and creates a suite of theorems: customized induction rules *.induct and case rules *.cases required later for proofs in x4 and x5. The simplification rules *.simps, generated as well, allow immediate testing of functions by value — most important for programmers’ approaches.
Only if implementation by fun does not succeed immediately, one expands the definition to function and resolves the proof obligations explicitly calling by pat completeness auto and postpones the termination proof by termination sorry. Table.1 gives a survey on all functions implemented so far: Isabelle’s tool definition primrec fun function total of function definitions tool’s features no recursion primitive recursion automated proofs interactive proof number of occurrences 21
1 10
9 41
Defining functions in the FP is almost trivial but not in all cases of 41 above, which seem typical for CA. The first function which really challenged the programmer was the following one, which decides divisibility (dvd) for univariate polynomials (up, actually lists of integers, i.e. of exponents). The identifier for the function is declared as infix with priority 70 in line 01, the function is implemented by two patterns in line 02 and in line 03: 01 function (sequential) dvd up :: ”unipoly ) unipoly ) bool” (infixl ”%j%” 70) where List.length rest ^ ds % % rest)) j : 09 in 10 rest = [] _ (quot 6= 0 ^ List.length ds 12 by pat completeness auto 13 termination sorry 3
For the working programmer automated code generation for relevant target languages is a major
motivation. And indeed motivating, following the tutorial [
Further investigations on the efficiency of the generated code are planned, in particular with respect to the indefinite precision integers and naturals in comparison with the original SML code. 4
Admittedly, generating code from Isabelle definitions with termination sorry (as done in x2 and x3 above) is a bad practice in terms of software verification in HOL: On termination, even when stated with sorry, i.e. omitting a proof, the theorems mentioned in x2 are created and seduce to inappropriate use. However, as already mentioned, this case study started from a programmers perspective which considers automated generation of code a major success — while the generated code is not less trustworthy than the original SML code.
The obligation to prove termination, as imposed by the FP, marks the transition from naive programming to software engineering. Isabelle’s FP supports this transition with much automation: Table.1 shows that from 41 functions only 9 require an explicit termination proof:
Termination proof not necessary (definition, primrec) done automatically by FP (fun) by lexicographic order by relation measure by size change did not yet succeed total of function definitions number of occurrences 22 10 1 2 0 6 41
2The final paper will show some examples.
The ration between automated proof and interactive proof of termination seems typical for CA: recursion is not structural with respect to some datatype, rather depends on specific mathematical knowledge. In this case study the crucial function for proving termination is
function next prime not dvd :: ”nat ) nat ) nat” which determines a prime with a certain property greater than a given number. Isabelle2013 lacks respective knowledge, however, the Isabelle development already started to fill this gap3. So we look forward to have completed all termination proofs at the end of the case study. 5
This task has not begun at the time of writing this extended abstract. For sake of efficiency in development and of coherence of Isabelle’s knowledge the first step of this task will be to adopt Isabelle’s multivariate Polynomials4 — from the side of Isabelle development respective tools are already under construction5 for supporting this task.
Transferring the gcd algorithm completely to Isabelle’s FP and verifying it seems essential: there seems no way to produce a certificate for the property of being the greatest common divisor. Thus, in order to get a computable gcd into the Isabelle distribution, verification of some algorithm seems necessary. 6
Lucas-Interpretation [
While the benefits for education seem evident, the benefits for implementing CA are not. On completion the case study is expected to produce detailed requirements for debugging (with inspection of environment and context) and experiences, how Lucas-Interpretation might support verification of the underlying CA algorithm. 7
The steps already done in this case study suggest, that Isabelle’s function package is ready for
implementation of comprehensive algorithms in Computer Algebra. Furthermore, the experiences with
“programming in Isabelle” are promising such, that integrative support for “Domain Engineering” (as an offspring
of Formal Methods) [
About advantages of Lucas-Interpretation for the implementation of CA nothing can be said at the time of writing this extended abstract; results are expected on completion of the case study for the final publication in autumn 2013.
3See the development branch at http://isabelle.in.tum.de/reports/Isabelle/rev/7f864f2219a9. 4http://isabelle.in.tum.de/dist/library/HOL/HOL-Library/Polynomial.html 5See the development branch at http://isabelle.in.tum.de/reports/Isabelle/rev/3cc46b8cca5e.