Algorithm Invention and Verification 
by Lazy Thinking

Bruno Buchberger
Research Institute for Symbolic Computation
Johannes Kepler University, Linz, Austria
bruno.buchberger@jku.at

Abstract

In this paper, we study algorithm invention and verification as a specific variant of systematic theory exploration and propose the "lazy thinking paradigm" for inventing and verifying algorithms automatically; i.e., for a given predicate logic specification of the problem in terms of a set of operations (functions and predicates), the method produces an algorithm that solves the problem together with a correctness proof for the algorithm. In the ideal case, the only information that has to be provided by the user consists of the formal problem specification and a complete knowledge base for the operations that occur in the problem specification. The "lazy thinking paradigm" is characterized

by using a library of algorithm schemes

and  by using the information contained in failing attempts to prove the correctness theorem for an algorithm scheme in order to invent sufficient requirements on the auxiliary functions in the algorithm scheme.

Keywords: algorithm invention, algorithm verification, program synthesis,  algorithm correctness, re-usable algorithms, algorithm schemes, learning from failure, conjecture generation, lazy thinking, functors, requirement engineering, didactics of programming, mathematical knowledge retrieval, mathematical knowledge management,  sorting, merging, merge-sort, Theorema.

Introduction

Algorithm invention (program synthesis) has a long tradition, see [Basin 2003] for a recent survey. In this paper, we consider the systematic (computer-aided, automated) invention of algorithms as a specific part of the general problem of systematic (computer-aided, automated) theory exploration. Systematic theory exploration was introduced in [Buchberger 1999] as an alternative to the isolated theorem proving paradigm that prevailed in formal, computer-supported mathematics during the past decades. In [Buchberger 2000] we proposed various approaches to systematic, computer-supported mathematical theory exploration. In particular, we introduced the "lazy thinking" paradigm for proving mathematical theorems. The main idea of this paradigm consists in using the information of failing proof attempts for conjecturing intermediate lemmata that will allow to continue with the proof. The proof of the lemmata is then, again, attempted and may lead to the invention of sub-lemmata until the "cascade" of this invention terminates successfully.

In this paper, we modify the lazy thinking paradigm for inventing correct algorithms instead of inventing theorems: For a given predicate logic specification of the problem in terms of a set of operations (functions and predicates), the method invents an algorithm that solves the problem and also, simultaneously, provides a correctness proof for the algorithm.

Roughly, the method proceeds as follows:

The method tries out, one after the other, various "algorithm schemes" (or "algorithm types") that are stored in a library of algorithm schemes  for the given mathematical domain (or "data type"). An algorithm scheme is a predicate logic formula that describes an algorithm (recursively) in terms of unspecified subalgorithms together with a proof method appropriate for (induction) proofs of properties of algorithms having this scheme.

For the chosen algorithm type, the proof method is called for proving the correctness theorem. Typically, this proof will fail because nothing is known about the unspecified subalgorithms.

>From the failing proof situation, by a conjecture generating algorithm, lemmata are generated that would enable the prover to complete the proof successfully. The lemmata will describe certain requirements on the subalgorithms. These requirements are added to the knowledge base and the proof of the correctness theorem is attempted again. Now, the proof will get over the failing situation and will either succeed or will fail again at some later proof situation.

This procedure is iterated in a recursive cascade until the proof of the correctness theorem goes through (or one gives up). After successful termination, the following will be true: Under the assumption that all ingredient subalgorithms satisfy the requirements described in the lemmata generated, the main algorithm satisfies the problem specification.

In this stage, there are two possibilities: Either, in the initial knowledge base, algorithms are available that satisfy the requirements for the subalgorithms described in the lemmata and we are done, i.e. a correct algorithm has been synthesized for the initial problem and its correctness proof has been generated. Or subalgorithms that satisfy the requirements can be synthesized by another application of the same method in a next round of the procedure.

The distinctive features of our algorithm synthesis method, as compared to other methods, are:

the use of algorithm schemes taken from a library of algorithm schemes,

the crucial role of failing proofs and conjecture generation from failing proofs,

the decomposition of theory exploration and, in particular, algorithm invention and verification into theory layers,

the naturalness of the approach, which makes it attractive both for complete or partial automation in computer-supported systems for formal mathematics and also for usage as a strategy for human algorithm invention and teaching. (In fact, the idea for the lazy thinking paradigm for theory exploration and, in particular, algorithm invention and verification came to me while I was preparing a course on mathematical proving for high-school teachers in October 2001.)

In the sequel, we will illustrate the method by a case study, namely the automated synthesis of the merge-sort algorithm. The case study will be executed in the frame of the Theorema system. In particular, all occurring predicate logic formulae will be given in the Theorema syntax, see [Buchberger et al. 1997]. The case study will allow us also to explain some of the subtle details of the method.

Acknowledgement: My PhD student Adrian Craciun implemented the case study in the frame of the Theorema system starting from my earlier versions of the induction prover, the conjecture generation algorithm, and the cascade.

The Theorem Automatically Invented by the Method

The power of the method is best understood by considering the theorem that is automatically invented (and not only proved) by the method:

Relative Correctness Theorem for Merge-Sort

Knowledge[
      is–sorted–version]
\[Implies]
(Underscript[∀ , special, merged, left–split, 
            right–split, sorted])
(Is–Merge–Sort–Algorithm[sorted, special, 
                merged, left–split, 
                right–split] 
 \[Implies] (Underscript[∀ , is–tuple[X]])is–sorted–version[X,  sorted[X]])

Here, 'Knowledge' is the conjunction of all (some of the) formulae known about the predicate 'is–sorted–version' and all its ingredient operations (functions and predicates), like 'is–sorted', 'is–permuted–version', etc. (see Appendix) and 'Is–Correct–Merge–Sort–Algorithm' is defined as follows:

(Underscript[∀ , special, merged, left–split, right–split, sorted])Is–Merge–Sort–Algorithm[special, merged, 
        left–split, right–split, sorted]

⇔

{({{(Underscript[∀ , is–tuple[X]])(sorted[X]={({{special[X], ⇐, is–trivial–tuple[X]}, {merged[sorted[left–split[X]], 
                              sorted[right–split[X]]], ⇐, otherwise}})})
}, {(Underscript[((Underscript[∀ , is–tuple[X]])), is–trivial–tuple[X]])(special[X] = X)

            }, {(Underscript[((Underscript[∀ , is–tuple[
                        X]])), ¬ is–trivial–tuple[X]]){({{left–split[X] ≺ X}, {is–tuple[left–split[X]]}, {right–split[X] < X}, {is–tuple[right–split[X]]}})
}}, {(Underscript[∀ , is–tuple[Y, Z]])is–tuple[
                merged[Y, Z]]}, {(Underscript[((Underscript[∀ , is–tuple[X, Y, 
                        Z]])), ¬ is–trivial–tuple[X]])({({{left–split[X] ≈ Y}, {right–split[X] ≈ Z}, {is–sorted[Y]}, {is–sorted[Z]}})}\[Implies]{({{merged[Y, Z] ≈ X}, {is–sorted[merged[Y, Z]]}})})}})}

Explanation

The theorem says that,

if

the predicate 'is–sorted–version' and its sub-operations satisfy the properties described in knowledge (see the appendix),

the function 'sorted' is defined recursively in the "divide-and-conquer" style from the auxiliary functions 'special', 'merged', 'left-split', and 'right-split',

the functions 'merged', 'left-split', and 'right-split' preserve the data type 'is–tuple',

the functions 'left-split' and 'right-split', on non-trivial arguments, reduce the length,

the function 'special', on trivial arguments, is the identity,

the function 'merged', on sorted arguments, yields sorted tuples, and

the function 'merged', on arguments Y and Z that contain the same elements as left–split[X] and right-split[X], respectively, yields a tuple that contains the same elements as X,

then

the function 'sorted' solves the problem of sorting, i.e. the problem specified by the binary predicate 'is-sorted-version'.

The most important and most interesting parts of this theorem are the two requirements stating that the function 'merged' preserves sortedness and elements. These two requirements are exactly what people would naturally consider as the characteristic properties of merging. The amazing phenomenon is that exactly these two requirements are invented completely automatically, without any prior intuition or semantic understanding, by our "lazy thinking" method. In fact, the exact formulation of the requirements invented by our method, are slightly more general than the requirements one would expect naturally. This is, of course, good because, the weaker the requirements, the more functions 'merged', 'left–split', and 'right–split' satisfy the requirements!

The Knowledge on the Problem

When attempting to solve a problem by an algorithm, we assume, of course, that the problem is "completely understood". In fact, it is a heuristic rule that "the better you understand the problem the closer you are to finding a solution". Generally speaking, the problem of sorting is an instance of a "problem scheme" (or "problem type") which we call "explicit problems". An explicit problem is given by a (binary) predicate P (called "problem specification") and the solution of the problem consists in finding a function f (called the "solution function" or "solution algorithm" in case f is an algorithmic function) such that

(Underscript[∀ , is–object[X]])P[X, f[X]].

Here, 'is–object' is a unary predicate that characterizes the objects in the data domain considered.

(Of course, explicit problems can also be defined for more than one input argument.)

In our case study, the problem specification is given by the binary predicate 'is–sorted–version' which is defined as follows

(Underscript[∀ , is–tuple[X]])(is–sorted–version[X, Y]  ⇔{({{is–tuple[Y] }, {X≈Y  }, {is–sorted[Y]}})})

Note that the input X is restricted to tuples, i.e. in our case, the input domain is the domain of tuples. Also note that the requirement that the output Y is a tuple is part of the problem specification. This is appropriate because, since the predicate is used for formulating the correctness theorem

(Underscript[∀ , is–tuple[X]])is–sorted–version[X, 
        sorted[X]]

the domain requirement on the input need not (and should not) be mentioned in the problem specification whereas the domain requirement on the output is an essential part of the problem specification.

The predicate 'is–sorted–version' is defined in  terms of the two auxiliary predicates '≈' and 'is–sorted'. (For 'X≈Y' read 'Y is a permuted version of X' or 'X and Y contain the same elements equally often'):

({{is–sorted[⟨⟩] }, {(Underscript[∀ , x]) 
              is–sorted[⟨x⟩]}, {\(∀ \+\(x, y, \(z\&-\)\)\)(\(is–sorted[⟨x, y, 
                    z\&_⟩]\)   ⇔{({{x ≥ y}, {\(is–sorted[⟨y, 
                            z\&_⟩]\)}})    })}})

and

({{⟨⟩≈⟨⟩ }, {\(∀ \+\(y, y\&_\)⟨⟩ ≉ ⟨y, y\&_⟩\)}, {\(∀ \+\(x, x\&_, y\&_\)\(\((⟨x, 
                      x\&_⟩ ≈ ⟨y\&_⟩\  ⇔ \((x ∈ ⟨y\&_⟩ ∧ ⟨x\&_⟩ ≈ 
                        dfo[x, \ ⟨y\&_⟩])\))\)\(.\)\)\)}})

(For the "sequence variables" notation '\(x\&_\)' etc., see the papers on Theorema, e.g. [Buchberger et al. 1997]. Sequence variables can be replaced by arbitrarily many terms. We use angle brackets as constructors for tuples: for example, ⟨2,2,3,1,4⟩ is the tuple consisting of the elements 2, 2, 3, 1, 4.)

The definitions of 'is–sorted' and '≈', again, contain auxiliary operations like '∈' (read: 'is–element') and 'dfo' (read: 'delete first occurence') that must be defined in terms of other auxilary functions until we arrive at the basic operations on tuples. The definitions of all these auxiliary operations and also the formulae describing various properties of these auxiliary operations are supposed to be contained in the knowledge base 'Knowledge[sorted–version–of]', see appendix.

(Later in the paper, we will discuss the question of how to determine which properties of the operations between the problem specifying predicate 'is–sorted-version' and the basic operations on tuples should be included into the knowledge base.)

Algorithm Schemes

An "algorithm scheme" (or "algorithm type") for a given data type, in our view,

is a recursive definition of an unspecified "main" operation in terms of other unspecified "auxiliary" operations and the basic operations of the data type

together with a proof method that corresponds to the recursive definition in a natural way.

In our example of a problem on the data type of tuples, a possible recursive definition of the solution function is the well-know "divide-and-conquer" scheme (in a version, which appropriate to the data type of tuples) is as follows:

(Underscript[∀ , is–tuple[X]])(sorted[X]={({{special[X], ⇐, is–trivial–tuple[X]}, {merged[sorted[left–split[X]], 
                    sorted[right–split[X]]], ⇐, otherwise}})})

where you should think about the "main functions" 'sorted' and the "auxiliary functions" 'special', 'merged', 'left-split', and 'right-split' as completely unspecified (except that 'sorted' is related to the auxiliary functions as described in the scheme). In fact, at this moment, nothing is known about these functions that would justify to give them names like 'sorted', 'special', 'merged' etc. Hence, for didactic considerations, it might be better to just give them names like 's', 'sp' 'm', 'l', and 'r'. However, the "semantic" function names above have the didactic advantage of suggesting where we are ultimately driving at.

Note also, that in contrast to the operations 'sorted' etc., the predicate 'is–trivial–tuple' is not  unspecified but, rather, is defined by a formula in the knowledge base, see the appendix.

Also, we include the following "type requirement" on the auxiliary functions as a part of the algorithm scheme:

({{(Underscript[((Underscript[∀ , is–tuple[
                      X]])), ¬ is–trivial–tuple[X]]){({{is–tuple[left–split[X]]}, {is–tuple[right–split[X]]}})
}}, {(Underscript[∀ , is–tuple[Y, Z]])is–tuple[
              merged[Y, Z]]}})

The type requirements will be important for being able to prove that the function 'sorted', for tuple arguments, yields tuples as results.

Finally, we also consider the following requirement

(Underscript[((Underscript[∀ , is–tuple[
                X]])), ¬ is–trivial–tuple[X]])∧{({{left–split[X] ≺ X}, {right–split[X] ≺ X}})}

as a part of the recursive definition, which guarantees termination of the algorithm. (For '≺' read 'has shorter length', see the definition in the appendix.)

Second, we include the following special induction method into the algorithm scheme:

In order to prove, for an arbitrary property A,

(Underscript[∀ , is–tuple[X]])A[X]

it suffices to prove, for an arbitrary but fixed \(TraditionalForm\`x0\&_\),

\(A[⟨x0\&_⟩]\)

under the assumptions

\(is–tuple[⟨x0\&_⟩]\)

and

\(\(∀ \+\(is–tuple[Y]\)\)\+\(Y ≺ ⟨x0\&_⟩\)\(\(A[Y]\)\(.\)\)\)

This particular induction method (w.r.t. to the particular predicate ≺, 'shorter in length', defined in the knowledge base) is based on the property that ≺ is a Noetherian relation. We do not include this property into the knowledge base. Rather, this property is implicitly used by allowing this induction method.

One might argue that, with the inclusion of an appropriate inductive proof method into the algorithm scheme, already very much of the "invention" is taken away from the automated invention system. However, in future mathematical knowledge management systems (and, in particular, verified algorithm invention systems), it would be silly to throw away the accumulated knowledge of mathematicians on problem solving "schemes". Rather, in future systems, the accumulated algorithm invention knowledge of mathematicians should be kept available in "algorithm scheme libraries" that can then be used, in the way which we demonstrate in this paper, for inventing concrete algorithms for concrete problems. (In an analogous way, future mathematical knowledge management systems, should provide "problem scheme libraries", "data scheme libraries", "knowledge scheme libraries", and "definition scheme libraries". We cannot go into more details about this more general view in this paper but will expand on this aspect in forthcoming papers.)

We believe that, actually, for a given data type there exist only a few interesting algorithm types (algorithm schemes). These algorithm schemes should be put into libraries and can serve as an important input to algorithm invention systems. Another example of an algorithm scheme for algorithms on tuples is

({{s[⟨⟩] = c}}, {\(∀ \+\(x, x\&_\)\((s[⟨x, 
                    x\&_⟩] = 
                m[x, s[⟨x\&_⟩]])\)\)}})

with the type requirement

(Underscript[∀ , x, is–tuple[Y]])is–tuple[m[x, Y]]

and the following special induction method:

In order to prove, for an arbitrary property A,

(Underscript[∀ , is–tuple[X]])A[X]

it suffices to prove

A[⟨⟩]

and to prove, for arbitrary but fixed x0, \(TraditionalForm\`x0\&_\),

\(A[⟨x0, xo\&_⟩]\)

under the assumption

\(\(\(A[⟨xo\&_⟩]\)\(.\)\)\)

Inventing the Algorithm by Lazy Thinking: First Round

We now start from the following situation:

We have a knowledge base consisting of all the definitions and essential properties of the operations and auxiliary operations (functions and predicates) occurring in the problem specification (in our case: the specification of the binary predicate 'is–sorted–version', see appendix).

We have chosen an algorithm scheme from a finite library of algorithm schemes for the domain of tuples (in our case: the "divide-and-conquer" algorithm scheme; note that we could start from any other scheme!). Remember that the scheme consists of a scheme for a induction function definition (including also type requirements for the auxilary functions) and a corresponding inductive proof method.

We now do the following:

We include the algorithm scheme for 'sorted', the type requirements for the auxiliary functions, and the  requirements on the decreasing length of 'left–split' and 'right–split' into the knowledge base.

Then we start attempting to prove the correctness theorem

(Underscript[∀ , is–tuple[X]])is–sorted–version[X,  sorted[X]].

Of course, this proof cannot succeed because basically nothing interesting is known about the auxiliary functions 'merged', 'left-split' etc. We proceed with the proof until the proof gets stuck.

When it got stuck, we analyze the current, failing, proof situation and try to conjecture requirements (properties) of the auxiliary functions that would make it possible to get over the failing proof situation.

We add the conjectured requirements to the knowledge base and repeat the whole process, i.e. we go to the next round in the algorithm invention process.

Example:

In the example, the failing proof attempt (which can be generated completely automatically by the Theorema induction prover) is as follows:

Proof Attempt Begin

For proving the correctness theorem, we use well-founded induction w.r.t. ≻ on X:

We assume

\(is–tuple[⟨xo\&_⟩]\)

and the induction hypothesis

\(\(∀ \+\(is–tuple[Y]\)\)\+\(⟨xo\&_⟩ ≻ Y\)is–sorted–version[Y, 
        sorted[Y]]\)

and we show

\(\(\(is–sorted–version[⟨xo\&_⟩, 
        sorted[⟨xo\&_⟩]]\)\(.\)\)\)

We use the algorithm scheme for 'sorted' and distinguish two cases:

CASE

\(\(\(is–trivial–tuple[⟨xo\&_⟩]\)\(:\)\)\)

In this case, we have to show

\(is–sorted–version[⟨xo\&_⟩, 
      special[⟨xo\&_⟩]]\)

i.e., by the definition of 'is–sorted–version', we have to show

\(\(\(\((G1)\)\ \ \ \ \ \ is–tuple[
        special[⟨xo\&_⟩]]\)\(,\)\)\)

\(\(\(\((G2)\)\ \ \ \ \ \ special[⟨xo\&_⟩] ≈ ⟨xo\&_⟩\)\(,\)\)\)

\(\((G2)\)\ \ \ \ \ \ \(\(is–sorted[
          special[⟨xo\&_⟩]]\)\(.\)\)\)

(G1) is true because of the type requirement for 'special'.

For (G2), by the fact that

(Underscript[∀ , is–trivial–tuple[X],  is–tuple[Y]])(X ≈ 
            Y ⇔ (X = Y)),

it suffices to prove that

\(special[⟨xo\&_⟩] = \(\(⟨xo\&_⟩\)\(.\)\)\)

Here we are stuck.

Proof Attempt End

(The  proof attempt generated  automatically by the Theorema induction prover for tuples is basically exactly like the proof attempt above including the explanatory English text, see the papers on Theorema. However, the Theorema proof refers to formulae in the knowledge base by labels, more specifically by hyperlinks, and we prefer not to use labels in the presentation of proofs in this paper for increasing readability.)

Now we analyze the failing proof situation and find:

We have the case assumption as the only temporary assumption:

\(\(\(is–trivial–tuple[⟨xo\&_⟩]\)\(.\)\)\)

We have the temporary goal:

\(special[⟨xo\&_⟩] = \(\(⟨xo\&_⟩\)\(.\)\)\)

It is near at hand to conjecture (and our current Theorema conjecture generating algorithm can do this automatically) that the following requirement on the function 'special'

(Underscript[∀ , is–trivia–tuple[X]])(special[X] = 
          X)

will make it possible to get over the failing proof situation.

We add this requirement to the knowledge base and proceed to the next invention round.

Inventing the Algorithm by Lazy Thinking: Second Round

We now do exactly the same proof attempt once more. (Alternatively, we could jump back into the proof to the situation in which the first attempt failed. Both strategies, going back to the beginning and jumping right to the failing situation, have its advantages and disadvantages: Going back to the beginning may, in some examples, ultimately yield shorter proofs and jumping right to the failing situation, of course, saves proving effort.)

Since we have added a requirement on the auxiliary function 'special'  we will be able to get now over the failing proof situation and we will be stuck at some later situation in the proof in which, again, we will try to invent a requirement on the auxiliary functions that will make it possible to proceed further.

Example:

In the example, the next proof attempt (which can be generated completely automatically by the Theorema induction prover) is as follows:

Proof Attempt Begin

For proving the correctness theorem, we use well-founded induction w.r.t. ≻ on X:

We assume

\(is–tuple[⟨xo\&_⟩]\)

.... exactly as in the first proof attempt ...

We us the algorithm scheme for 'sorted' and distinguish two cases:

CASE

\(\(\(is–trivial–tuple[⟨xo\&_⟩]\)\(:\)\)\)

In this case, by we have to show

\(is–sorted–version[⟨xo\&_⟩, 
      special[⟨xo\&_⟩]]\)

i.e., because of the definition of 'is–sorted–version', we have to show

\(\(\(\((G1)\)\ \ \ \ \ \ is–tuple[
        special[⟨xo\&_⟩]]\)\(,\)\)\)

\(\(\(\((G2)\)\ \ \ \ \ \ special[⟨xo\&_⟩] ≈ ⟨xo\&_⟩\)\(,\)\)\)

\(\((G2)\)\ \ \ \ \ \ \(\(is–sorted[
          special[⟨xo\&_⟩]]\)\(.\)\)\)

(G1) is true because of the type requirement for 'special'.  (G2) is true because of

(Underscript[∀ , is–trivial–tuple[X],  is–tuple[Y]])(X ≈ 
            Y ⇔ (X = Y)),

and the new requirement

(Underscript[∀ , is–trivia–tuple[X]])(special[X] = 
            X).

(G3) is true because of the same requirement and the following property of 'sorted'

(Underscript[∀ , is–trivia–tuple[X]])is–sorted[
          X].

CASE

\(\(\(¬ is–trivial–tuple[⟨xo\&_⟩]\)\(:\)\)\)

In this case, we have to show

\(\(\(is–sorted–version[⟨xo\&_⟩, 
        merged[sorted[
            left–split[⟨xo\&_⟩], 
            sorted[right–split[⟨xo\&_⟩]]]]]\)\(.\)\)\)

For this, by the definition of 'is–sorted–version', it suffices to show

\(\(\(\((H1)\)\ \ \ \ \ \ is–tuple[
        merged[sorted[
            left–split[⟨xo\&_⟩], 
            sorted[right–split[⟨xo\&_⟩]]]]]\)\(,\)\)\)

\(\(\(\((H2)\)\ \ \ \ \ ⟨xo\&_⟩ ≈ 
      merged[sorted[
          left–split[⟨xo\&_⟩], 
          sorted[right–split[⟨xo\&_⟩]]]]\)\(,\)\)\)

\(\((H3)\)\ \ \ \ \ \(\(is–sorted[
          merged[sorted[
              left–split[⟨xo\&_⟩], 
              sorted[right–split[⟨xo\&_⟩]]]]]\)\(.\)\)\)

>From the case assumption, by the type requirements on 'left–split' and 'right–split', the property that 'left–split' and 'right–split' produce shorter tuples, and the induction hypothesis we obtain

\(\(\(is–sorted–version[
      left–split[⟨xo\&_⟩], 
      sorted[left–split[⟨xo\&_⟩]]]\)\(,\)\)\)

\(\(\(is–sorted–version[
        right–split[⟨xo\&_⟩], 
        sorted[right–split[⟨xo\&_⟩]]]\)\(.\)\)\)

>From this, by the definition of 'is–sorted–version', we obtain

\(\(\(\((AL1)\)\ \ \ \ \ is–tuple[
        sorted[left–split[⟨xo\&_⟩]]]\)\(,\)\)\)

\(\(\(\((AL2)\)\ \ \ \ \ left–split[⟨xo\&_⟩] ≈ 
      sorted[left–split[⟨xo\&_⟩]]\)\(,\)\)\)

\(\(\(\((AL3)\)\ \ \ \ \ is–sorted[
        sorted[left–split[⟨xo\&_⟩]]]\)\(,\)\)\)

\(\(\(\((AR1)\)\ \ \ \ \ is–tuple[
        sorted[right–split[⟨xo\&_⟩]]]\)\(,\)\)\)

\(\(\(\((AR2)\)\ \ \ \ \ right–split[⟨xo\&_⟩] ≈ 
      sorted[right–split[⟨xo\&_⟩]]\)\(,\)\)\)

\(\((AR3)\)\ \ \ \ \ \(\(is–sorted[
          sorted[right–split[⟨xo\&_⟩]]]\)\(.\)\)\)

(H1) follows from (AL1) and (AR1) by the type requirement on 'merged'.

Now we are stuck.

Proof Attempt End

Now we analyze the failing proof situation and find:

We have the case assumption and the formulae (AL1), ..., (AR3) as termporary assumptions.

We have the temporary goals (H2) and (H3).

It is not so near at hand but, after some thinking, relatively easy to conjecture (and our current Theorema conjecture generating algorithm can do this automatically) that the following requirement on the functions 'left-split', 'right-split' und 'merged'

(Underscript[((Underscript[∀ , is–tuple[X, Y, 
                Z]])), ¬ is–trivial–tuple[X]])({({{left–split[X] ≈ Y}, {right–split[X] ≈ Z}, {is–sorted[Y]}, {is–sorted[Z]}})}\[Implies]{({{merged[Y, Z] ≈ X}, {is–sorted[merged[Y, Z]]}})})

will make it possible to get over the failing proof situation.

We add this requirement to the knowledge base and proceed to the next invention round.

Inventing the Algorithm by Lazy Thinking: Last Round

We now do exactly the same proof attempt once more (or we just jump to the proof situation where the previous proof attempt got stuck.)

This time, the inductive proof will succeed using the added requirement on  'left-split', 'right-split' und 'merged' for proving (H2) and (H3).

If we now collect the requirements on the functions'special','left-split','right-split',and'merged',we see that we invented and proved the "Relative Correctness Theorem for Merge-Sort" formulated at the beginning of this paper.

Automation of the Lazy Thinking Procedure

The "lazy thinking" procedure for inventing algorithms together with their correctness proofs, first of all, is meant to be a heuristic guide for human invention and verification.

However, the procedure can be made completely automatic (algorithmic) if we manage

to automate proving in the specific area and

to automate generating conjectures (requirements on auxiliary functions) from the temporary assumptions and the left-over goals in failing proof attempts.

In fact, for the case of inductive domains, there are powerful automated provers around and we have implemented various such provers in the Theorema system. Also, we already implemented a first version of a conjecture generation algorithm which, together with our automated inductive provers, is powerful enough to completely automate the "lazy thinking" algorithm invention and verification process in the case of numerous problems on tuples. Inductive provers that qualify for the use in the frame of the lazy thinking algorithm invention procedure must have a couple of properties: First, they must prove theorems in a "natural style" that proceeds from proof situations with temporary assumptions and goals to other such proof situations. Second, they must generate a proof object also in case of failing proofs. This is so because the essence of the lazy thinking method is "learning from failures".

Our current conjecture (requirements) generation algorithm implements two stratregies that can handle the two situations in the above example  but also in many other examples. Both strategies take the conjunction A of all temporary assumptions and the (conjunction of the) temporary goals G and conjecture a variant of (A=>G):

The first strategy can handle simple failing proof situations in proofs (proof branches) without induction: It replaces all "arbitrary but fixed" constants in (A=>G) by variables v,... and produces the conjecture (Underscript[∀ , v,  ... ])(A=>G). By this strategy, one can produce, for example, the conjecture (requirement)

(Underscript[∀ , is–trivia–tuple[X]])(special[X] = 
          X)

in the first round above.

The second strategy can handle failing proof situations in the induction step parts of proofs. It first, again,  replaces all "arbitrary but fixed" constants in (A=>G) by variables v,.... Then it looks for terms whose head is the function constant for the algorithm to be synthesized. (In our case, this is the function constant 'sorted'.) All these terms are then replaced by new variables w,... and then  the variant  (Underscript[∀ , v,  ... , w,  ... ])(A=>G) is taken as the new conjecture. By this strategy, one can produce, for example, the conjecture (requirement)

(Underscript[((Underscript[∀ , is–tuple[X, Y, 
                Z]])), ¬ is–trivial–tuple[X]])({({{left–split[X] ≈ Y}, {right–split[X] ≈ Z}, {is–sorted[Y]}, {is–sorted[Z]}})}\[Implies]{({{merged[Y, Z] ≈ X}, {is–sorted[merged[Y, Z]]}})})

in the second round above.

Our future research will focus on adding more and more strategies to the conjecture generation algorithm. Of course, never, one conjecture generation algorithm will be able to handle "all" failing proof situations. However, we think that the lazy thinking cascade will be a useful tool for organizing the theory exploration process and, in particular, the algorithm invention process. The cascade becomes more and more powerful the more powerful theorem provers and conjecture generation algorithms will be used as subalgorithms and the better we understand and organize libraries of algorithm schemes.

With the current Theorema induction prover and the current Theorema conjecture generator, the above synthesis process can be executed completely automatically. This means that the user has only to compile the knowledge on the predicate 'is–sorted–version' and its auxiliary notions shown in the appendix and then to call Theorema by

\(\(\(Prove\)\([\)\(Theorem["correctness of sorting"], 
\ 
      using -> Theory["sorting"], \ 
by -> 
        Cascade[SqnsEqCasePC, \ GenerateConjectures]\)\)\)

Here, Theory["sorting"] is the name of the theory consisting of the formulae in the appendix. In Theorema, this name can be assigned to the formulae by executing

Theory["sorting",
({{(Underscript[∀ , is–tuple[X]])(is–sorted–version[X, Y]  ⇔{({{is–tuple[Y] }, {X≈Y  }, {is–sorted[Y]}})})}, {is–sorted[⟨⟩]}, {(Underscript[∀ , x]) 
                  is–sorted[⟨x⟩]}, {... (all formulae in the appendix)...}})]

Similarly, Theorem["correctness of sorting"] is the name of the correctness theorem for sorting. This name can be assigned by executing

Theorem["correctness of sorting",
(Underscript[∀ , is–tuple[X]])is–sorted–version[X,  sorted[X]]]

'SqnsEquCasePC' is the name of the particular induction prover that corresponds to the "divide-and-conquer" algorithm scheme. This prover adds the formulae that constitute the algorithm scheme, i.e. the formulae

(Underscript[∀ , is–tuple[X]])(sorted[X]={({{special[X], ⇐, is–trivial–tuple[X]}, {merged[sorted[left–split[X]], 
                    sorted[right–split[X]]], ⇐, otherwise}})})

(Underscript[((Underscript[∀ , is–tuple[X]])), ¬ is–trivial–tuple[X]])is–tuple[left–split[X]]

.... etc....,

to the knowledge and organizes the main loop of the proof by the particular induction scheme.

We are now working on a generale induction prover that gets the information on the algorithm scheme (including the type requirements for the auxiliary functions and the  appropriate induction scheme) directly from the library of algorithm schemes so that, without user interaction, the prover can attempt various algorithm syntheses successively without user interaction in between.

As result of the above Theorema call 'Prove[Theorem["correctness of sorting"],...]', after approximately 5 minutes computation time (on a Compaq  Evo N610c, with Intel Pentium 4 with 1.8 GHz, the user will get

an augmented knowledge base that contains the requirements on the auxiliary functions

(Underscript[∀ , is–trivia–tuple[X]])(special[X] = 
          X)

(Underscript[((Underscript[∀ , is–tuple[X, Y, 
                Z]])), ¬ is–trivial–tuple[X]])({({{left–split[X] ≈ Y}, {right–split[X] ≈ Z}, {is–sorted[Y]}, {is–sorted[Z]}})}\[Implies]{({{merged[Y, Z] ≈ X}, {is–sorted[merged[Y, Z]]}})})

and a complete correctness proof for the divide-and-conquer algorithm that essentially looks like the proof developed in the preceding sections.

Now the user knows that the divide-and-conquer algorithm is a  correct sorting program if one uses auxiliary functions 'special', 'left–split', 'right–split', and 'merged' that satisfy the type requirements and the above, synthesized, requirements. In other words, the user does not only get one particular sorting algorithm synthesized (together with a correctness proof) but gets a whole spectrum of possible correct sorting algorithms!

We can now proceed in two ways:

Either we already have functions 'left-split', 'right-split', and 'merged' (possibly with other names) in our knowledge base that satisfy the requirements. (The proof that the functions in the knowledge base satisfy the requirement should be something current automated provers can do. See, however, next section.) Then we  can use them as auxiliary functions and we are done, i.e. we have a correct sorting algorithm, which now can be executed. In fact, in Theorema, the execution of algorithms, i.e. the application of algorithms to concrete inputs, can be done within the Theorema system itself, i.e. proving and computing can be done in the same language and logic! (In other words, part of the inference mechanism of the logic is used as the interpreter of a universal programming language.) We will show this by an example below.

Or we take the type requirements and the synthesized requirements on 'special', 'left–split', 'right–split', and 'merged' as new specifications for synthesizing appropriate functions again by the lazy thinking procedure. The requirement for 'special' is easy to fulfil: In fact, the requirement itself is a suitable function definition for 'special'. The requirements for 'left–split', 'right–split', and 'merged' are intertwined. They do not constitute an "explicit" problem specification. In principle, it is possible to apply the lazy thinking procedure also for synthesizing algorithms whose specification is not in explicit form. However, if possible, it is much better to try to decouple interwined specifications before one starts to synthesize algorithms that meet the specification.

In our case, it is in fact possible to replace the intertwined specification for 'left–split', 'right–split', and 'merged' by a decoupled one. Namely, it can be (automatically) shown  that the following decoupled specification entails the above intertwined specification:

(Underscript[((Underscript[∀ , is–tuple[X]])), ¬ is–trivial–tuple[X]])(left–split[X] ≍ 
              right–split[X]) ≈ X}

(Underscript[∀ , is–tuple[Y, Z]])({({{is–sorted[Y]}, {is–sorted[Z]}})}\[Implies]{({{merged[Y, Z] ≈ (Y ≍ Z)}, {is–sorted[merged[Y, Z]]}})})

(Here, '≍' denotes concatentation.) Using the lazy thinking procedure on this specification working with the algorithm scheme

({{merged[⟨⟩, ⟨⟩] = mee}, {\(∀ \+\(y, \ y\&_\)merged[⟨⟩, ⟨y, \ y\&_⟩] = 
            meg[y, \ y\&_]\)}, {\(∀ \+\(x, \ x\&_\)merged[⟨x, \ 
                  x\&_⟩, ⟨⟩] = mge[x, \ x\&_]\)}, {\(∀ \+\(x, \ x\&_, y, \ y\&_\)merged[⟨x, \ x\&_⟩, ⟨y, \ 
                  y\&_⟩]\) ={({{\(mgg1[x, 
                        merged[⟨x\&_⟩, ⟨y, \ y\&_⟩]] ⇐ \ 
                      p[x, y]\)}, {\(mgg2[y, 
                        merged[⟨x, \ 
                            x\&_⟩, ⟨y\&_⟩]] ⇐ \(¬ p[x, y]\)\)}})}}})

where 'mee', 'meg', 'mge', 'mgg1', 'mgg2' and 'p' are the unknown auxiliary operations, yields the usual merge algorithm

({{merged[⟨⟩, ⟨⟩] = ⟨⟩}, {\(∀ \+\(y, \ y\&_\)merged[⟨⟩, ⟨y, \ 
                  y\&_⟩] = ⟨y, \ 
              y\&_⟩\)}, {\(∀ \+\(x, \ x\&_\)merged[⟨x, \ 
                  x\&_⟩, ⟨⟩] = ⟨x, \ x\&_⟩\)}, {\(∀ \+\(x, \ x\&_, y, \ y\&_\)merged[⟨x, \ x\&_⟩, ⟨y, \ 
                  y\&_⟩]\) ={({{\(x⌣
                        merged[⟨x\&_⟩, ⟨y, \ y\&_⟩] ⇐ \ 
                      x > y\)}, {\(y⌣
                        merged[⟨x, \ 
                            x\&_⟩, ⟨y\&_⟩] ⇐ \(¬ x > y\)\)}})}}})

Similarly, concrete algorithms that satisfy the specification of 'left–split' and 'right-split' can be synthesized, for example

({{left–split[⟨⟩]  = ⟨⟩}, {(Underscript[∀ , x])(left–split[⟨x⟩]  = ⟨x⟩)}, {\(∀ \+\(x, y, z\&_\)\((left–split[⟨x, y, 
                    z\&_⟩] = 
                x⌣left–split[⟨z\&_⟩])\)\)}, {right–split[⟨⟩]  = ⟨⟩}, {(Underscript[∀ , x])(right–split[⟨x⟩]  = ⟨⟩)}, {\(∀ \+\(x, y, z\&_\)\((right–split[⟨x, y, 
                    z\&_⟩] = 
                y⌣right–split[⟨z\&_⟩])\)\)}})

Note that these algorithms 'merged', 'left–split', and 'right–split' are now "concrete" in the sense that they only need auxiliary operations that are basic operations on tuples (and the ordering predicate '>' on the objects in tuples), i.e. no more synthesis step is necessary.

Putting all these definitions into one theory by

Theory["sorting",
({{(Underscript[∀ , is–tuple[X]])(sorted[X]={({{special[X], ⇐, is–trivial–tuple[X]}, {merged[sorted[left–split[X]], 
                                sorted[right–split[X]]], ⇐, otherwise}})})
}, {merged[⟨⟩, ⟨⟩] = ⟨⟩}, {... ...}, {\(∀ \+\(x, y, z\&_\)\((right–split[⟨x, y, z\&_⟩] = 
                    y⌣right–split[⟨z\&_⟩])\)\)}})]

One can now compute within Theorema. For example, entering

Compute[
      sorted[⟨1, 233, 3, 44, 5, 66, 7, 
          8⟩]]

yields

⟨233, 66, 44, 8, 7, 5, 3, 
        1⟩.

(Also the definitions of the basic operations on tuples must be made part of Theory['sorting'] or, alternatively, one can declare these operations as "built-in" in Theorema, see the papers on Theorema.)

Mathematical Knowledge Retrieval

After generating the requirements for the sub-functions 'merged', 'left–split', and 'right–split', the question arises whether functions satisfying these requirements already exist in our knowledge base. Seemlingly, this is an easy question and, in traditional knowledge retrieval, the question is answered by looking to functions that have these names or, at least, similar names. Thus, for example, if one wants to know what is known about "Bessel functions" in some function library then, of course, one would just look for terms in the library whose outermost function symbol is "Bessel".  However, this ad-hoc solution to the knowledge retrieval problem is not appropriate for the needs arising in the frame of the above approach to algorithm synthesis (and in other areas of "mathematical knowledge management").

Rather, we are faced with the following problem:

Given a knowledge base K, operation names f, ..., and a requirement on f, ..., i.e. a formula R[f,...]

find operation names F, ... occurring in K such that R[F,...] is a logical consequences of K.

Hence, knowlede retrieval in our context is essentially a proving problem!

For example, given the knowledge base K in the appendix augmented by the following definitions

({{M[⟨⟩, ⟨⟩] = ⟨⟩}, {\(∀ \+\(y, \ y\&_\)\((M[⟨⟩, ⟨y, \ 
                    y\&_⟩] = ⟨y, \ 
                  y\&_⟩)\)\)}, {\(∀ \+\(x, \ x\&_\)\((M[⟨x, \ 
                    x\&_⟩, ⟨⟩] = ⟨x, \ 
                  x\&_⟩)\)\)}, {\(∀ \+\(x, \ x\&_, y, \ y\&_\)\)(\(M[⟨x, \ 
                    x\&_⟩, ⟨y, \ 
                    y\&_⟩]\) ={({{\(x⌣
                            M[⟨x\&_⟩, ⟨y, \ y\&_⟩] ⇐ \ 
                          x > y\)}, {\(y⌣
                            M[⟨x, \ 
                                x\&_⟩, ⟨y\&_⟩] ⇐ \(¬ x > 
                              y\)\)}})})}})

({{L[⟨⟩]  = ⟨⟩}, {(Underscript[∀ , x])(L[⟨x⟩]  = ⟨x⟩)}, {\(∀ \+\(x, y, z\&_\)\((L[⟨x, y, 
                    z\&_⟩] = 
                x⌣L[⟨z\&_⟩])\)\)}, {R[⟨⟩]  = ⟨⟩}, {(Underscript[∀ , x])(R[⟨x⟩]  = ⟨⟩)}, {\(∀ \+\(x, y, z\&_\)\((R[⟨x, y, 
                    z\&_⟩] = 
                y⌣R[⟨z\&_⟩])\)\)}})

and the following requirement R[ left–split, right–split, merged]

(Underscript[((Underscript[∀ , is–tuple[
                X]])), ¬ is–trivial–tuple[X]]){({{left–split[X] ≺ X}, {is–tuple[left–split[X]]}, {right–split[X] < X}, {is–tuple[right–split[X]]}})}

(Underscript[∀ , is–tuple[Y, Z]])is–tuple[
        merged[Y, Z]]

(Underscript[((Underscript[∀ , is–tuple[X, Y, 
                Z]])), ¬ is–trivial–tuple[X]])({({{left–split[X] ≈ Y}, {right–split[X] ≈ Z}, {is–sorted[Y]}, {is–sorted[Z]}})}\[Implies]{({{merged[Y, Z] ≈ X}, {is–sorted[merged[Y, Z]]}})})

then "finding" operations in K that satisfy the requirement consists in trying out all possible triples of functions l, r, m  that occur in K and finding out whether the requirement R[ l, r, m] can be proved from the formulae in the knowledge base. In our case, in particular, one could try L, R, M and try to prove that R[ L, R, M] holds. One sees that this task is nothing else than proving that the algorithms L, R, M are correct w.r.t. to the specification R[ L, R, M].  Of course, such proofs, may be arbitrarily complicated.

"Complete" knowledge bases are knowledge bases in which, for all the occurring operations, all the possible  "interactions" between the operations have already been studied resulting in "rewrite properties" of these operations. For example, for the operations L, R, M defined above the following interactions  with the operations '≈', ≍', and 'is–sorted'

(Underscript[((Underscript[∀ , is–tuple[
                X]])), ¬ is–trivial–tuple[X]]){({{L[X] ≺ X}, {is–tuple[L[X]]}, {R[X] < X}, {is–tuple[R[X]]}})}

(Underscript[∀ , is–tuple[Y, Z]])is–tuple[M[Y, Z]]

(Underscript[((Underscript[∀ , is–tuple[X]])), ¬ is–trivial–tuple[X]])(L[X] ≍ R[X]) ≈ X}

(Underscript[∀ , is–tuple[Y, Z]])({({{is–sorted[Y]}, {is–sorted[Z]}})}\[Implies]{({{M[Y, Z] ≈ (Y ≍ Z)}, {is–sorted[M[Y, Z]]}})})

and many other such interactions should already be available in the knowledge base (i.e. it should have been proved in a "complete exploration" phase of the knowledge base). Then the proof that als R[ L, R, M] holds is "relatively easy", namely it can be done essentially by rewriting and other simple proof techniques ("symbolic computation proof techniques", "high-school proving", i.e. proving without quantifiers).

In other words, one could define that a knowledge base is "complete" iff proving properties that are not yet in the knowledge base is possible by "basic proving" (i.e. proving esssentially without quantifiers). Mathematical knowledge bases should be complete in this sense so that "retrieving knowledge" can be done by basic proving. Of course, all this is vague terminology. However, we think that this points into the right direction and we will elaborate on this philosophy in some other paper.

A Functorial View of Program Synthesis

We have seen that, by the above "lazy thinking" approach, algorithms A involving auxiliary operations B, C, ... can be synthesized that meet their specification P under the assumption that the ingredient auxiliary operations B, C, ... meet a certain other specification Q. In other words, the synthesis procedure invents and proves a theorem of the following structure

knowledge[P]
\[Implies]
(Underscript[∀ , B, C,  ... ])({({{(Underscript[∀ , X])(A[X] = F[X, B, C,  ... ])}, {Q[B, C,  .. ]}})} \[Implies](Underscript[∀ , X]) P[X, A[X]])

where F is the scheme (the "functional") which we use in order to define A in terms of the auxiliary operations  B, C, ...

For all this,we assumed that the specification P of the algorithm to be synthesized is "completely" given, whatever this means.

We now can go one step further: After the synthesis is completed (resulting both in the specification Q and in the proof of (Underscript[∀ , X]) P[X, A[X]], we can analyze which properties of P and its auxiliary operations actually entered into the correctness proof. Doing this, often results in a much more general theorem: If K[P,p,q,...] is the knowledge on P and its ingredient operations p, q, ... that is really needed in the correctness proof, then we may state that

(Underscript[∀ , P, p, q,  ... ])(K[P, p, q,  ... ]
\[Implies]
(Underscript[∀ , B, C,  ... ])({({{(Underscript[∀ , X])(A[X] = F[X, B, C])}, {Q[B, C,  .. ]}})} \[Implies](Underscript[∀ , X]) P[X, A[X]]))

Carrying out this analysis in the above example, yields the following theorem:

Is–Sorting–Problem[
      is–sorted–version, ≈,is–sorted]
\[Implies]
(Underscript[∀ , special, merged, left–split, 
            right–split, sorted])
( 
            Is–Merge–Sort–Algorithm[special, merged, 
                left–split, right–split, 
                sorted]
 \[Implies] (Underscript[∀ , is–tuple[X]])is–sorted–version[X,  sorted[X]])

where 'Is–Merge–Sort–Algorithm' is defined as in the section on the correctness of merge-sort and 'Is–Sorting–Problem' is defined as follows:

(Underscript[∀ , is–sorted–version, ≈,is–sorted])Is–Sorting–Problem[
        is–sorted–version, ≈,is–sorted]

⇔

{({{(Underscript[∀ , is–tuple[X]])(is–sorted–version[X, Y]  ⇔{({{is–tuple[Y] }, {X≈Y  }, {is–sorted[Y]}})})
}, {(Underscript[∀ , is–trivia–tuple[X]])is–sorted[
                X]

            }, {(Underscript[∀ , is–trivial–tuple[X], is–tuple[Y]])(X ≈ 
                    Y ⇔ (X = 
                      Y))

            }, {is–noetherian[ ≻ ]}})}

Note that the main omission in this knowledge base is the concrete definition of 'is–sorted' and '≈' in terms of more elementary operations. Hence, we can read the theorem which we invented by the lazy thininking procedure also in the following way:

Consider the "functor"

(Underscript[∀ , is–tuple[X]])(is–sorted–version[X, Y]  ⇔{({{is–tuple[Y] }, {X≈Y  }, {is–sorted[Y]}})})

(Underscript[∀ , is–tuple[X]])(sorted[X]={({{special[X], ⇐, is–trivial–tuple[X]}, {merged[sorted[left–split[X]], 
                    sorted[right–split[X]]], ⇐, otherwise}})})

that expands a domain containing the operations '≻', '≈', 'is–sorted',  'special', 'merged', 'left–split', and 'right–split' by the new operations 'is–sorted' and  'sorted'. Then we can be sure that the function 'sorted' is a correct algorithm for the explicit problem 'is–sorted–version'  as long as the operations ' '≻' etc. satisfy the properties given in the definitions of 'Is–Sorting–Problem' and 'Is–Merge–Sort–Algorithm'.

The power of this theorem can best be appreciated if you replace the semantic names 'is–sorted' etc. by some arbitrary constants like 'p', etc.

Similar ideas, maybe less explicit, have been expressed in [Farmer 2003] and [Schwarzweller 2003].

One also may view algorithm synthesis as higher-order solving. For example, in the problem of sorting we want to find a function 'sorted' that satisfies the specification

(Underscript[∀ , is–tuple[X]])is–sorted–version[X,  
        sorted[X]]

in the theory of 'is–sorted–version', i.e. in the theory compiled in the appendix or a sub-theory thereof. Now, in our setting, we do not specify 'sorted' by a higher-order term but, rather, by the algorithm synthesis procedure we gradually expand the theory by suitable definitions of 'sorted' and its auxiliary operations. Of course, formally, the result could be re-written by a higher-order term. However, we think that our setting is more natural and the result is more readable.

Conclusion

We presented a  procedure for automated algorithm invention and verification. The proposed procedure

is natural

can also be used as a heuristic and didactic guide for the development of correct algorithms and their correctness proofs

uses algorithm schemes as condensed algorithmic knowledge

exploits the information gained from failing proof attempts of the correctness theorem

is able to generate conjectures (requirements on the sub-algorithms) from failing proofs

invents verified algorithms that can be used with an infinite spectrum of possible subalgorithms (all those that satisfy the requirements)

emphasizes a layered approach in repeated, small extensions of theories

can also be used for extracting minimal requirements for the concepts in the problem specification and

can also be seen under the general perspective as viewing algorithm schemes and problem specifications as functors that transport requirements on the ingredient auxiliary operations into correctness theorems (stating that the algorithm defined by the scheme satisfies the problem specification)

and can, thereby, also seen as a contribution to the problem of generating re-usable algorithms.

Algorithms and theorems are only two sides of the same coin. Hence, algorithm and theorem invention and verification can be handled by the same approaches, e.g.  the lazy thinking approach. In the case of theorem invention, knowledge schemes take over the role of algorithm schemes. Also, it should be clear that the invention of interesting notions and interesting problems for these notions is another important part of "mathematical knowledge management". The general role of algorithm schemes, knowledge schemes, problem schemes, definition schemes, and data schemes for mathematical knowledge management will be studied in another paper.

The general subject of "mathematical knowledge management" has first been taken up in the "1st International Workshop on Mathematical Knowledge Management",   September 14-16, 2001, organized by this author at RISC, see also the special issue [Buchberger et al. 2003], which contains some of the papers of this conference.  Meanwhile mathematical knowledge management has seen increasing interest by the international research community. In our view, computer-supported mathematical theory exploration will be the key technology for future mathematical knowledge management.

References

[Basin 2003] D. Basin, Y. Deville, P. Flener, A. Hamfelt, J. Fischer Nilsson. Synthesis of Programs in Computational Logic. In: M. Bruynooghe and K. K. Lau, Program Development in Computational Logic, Springer-Verlag, to appear.

[Buchberger 1999] B. Buchberger. Theorem Proving Versus Theory Exploration. Invited talk at  the Calculemus Workshop, Univ. of Trento, July 11, 1999, Italy.

[Buchberger 2000] B. Buchberger. Theory Exploration with Theorema. Analele Universitatii Din Timisoara, Ser. Matematica-Informatica, Vol. XXXVIII, Fasc.2, 2000, (Proceedings of SYNASC 2000, 2nd International Workshop on Symbolic and Numeric Algorithms in Scientific Computing, Oct. 4-6, 2000, Timisoara, Rumania, T. Jebelean, V. Negru, A. Popovici eds.), pp. 9-32.

[Buchberger et al. 1997] B. Buchberger, T. Jebelean, F. Kriftner, M. Marin, D. Vasaru, An Overview on the Theorema Project, In: W. Kuechlin (ed.), Proceedings of ISSAC'97 (International Symposium on Symbolic and Algebraic Computation, Maui, Hawaii, July 21-23, 1997),  ACM Press 1997, pp. 384--391.

[Buchberger et al. 2003] B.Buchberger, G.Gonnet, M.Hazewinkel (eds.), Mathematical Knowledgement Management, special issue of the Journal Annals of Mathematics and Artificial Intelligence, Vol. 38, Nos. 1-3, Kluwer Academic Publishers, 2003.

[Farmer 2003] W. Farmer.  A Formal Framework for Managing Mathematics. In [Buchberger et al. 2003].

[Schwarzweller 2003] C. Schwarzweller. Towards Formal Support for Generic Programming. Habilitation Thesis, University of Tübingen, Computer Science Department, 2003.

Appendix: Knowledge Base for the Sorting Problem

Definitions

(Underscript[∀ , is–tuple[X]])(is–sorted–version[X, Y]  ⇔{({{is–tuple[Y] }, {X≈Y  }, {is–sorted[Y]}})})

({{is–sorted[⟨⟩] }, {(Underscript[∀ , x]) 
                is–sorted[⟨x⟩]}, {\(∀ \+\(x, y, \(z\&-\)\)\)(\(is–sorted[⟨x, y, 
                      z\&_⟩]\)   ⇔{({{x ≥ y}, {\(is–sorted[⟨y, 
                              z\&_⟩]\)}})    })}})

({{⟨⟩≈⟨⟩ }, {\(∀ \+\(y, y\&_\)⟨⟩ ≉ ⟨y, y\&_⟩\)}, {\(\(∀ \+\(x, x\&_, y\&_\)\((⟨x, 
                    x\&_⟩ ≈ ⟨y\&_⟩\  ⇔ \((x ∈ ⟨y\&_⟩ ∧ ⟨x\&_⟩ ≈ 
                      dfo[x, \ ⟨y\&_⟩])\))\)\)\(
\)
          \)}})

({{(Underscript[∀ , x]) 
                x ∉ ⟨⟩}, {\(∀ \+\(x, y, y\&_\)\((x ∈ ⟨y, 
                      y\&_⟩)\)\ \  ⇔ \((\((x = y)\) ∨ 
                    x ∈ ⟨y\&_⟩)\)\)}})

({{(Underscript[∀ , a]) dfo[
                  a,  ⟨⟩] = ⟨⟩}, {\(∀ \+\(a, x, x\&_\)dfo[
                  a, \ ⟨x, x\&_⟩\ ]\) ={({{\(⟨x\&_⟩\), ⇐, x = a}, {\(x⌣
                        dfo[a, \ ⟨x\&_⟩]\), ⇐, otherwise}})} }})

({{\(∀ \+\(y\&_\)\(¬ ⟨⟩ ≻ ⟨y\&_⟩\)\)}, {\(∀ \+\(x, x\&_\)⟨x, 
                  x\&_⟩ ≻ ⟨⟩\)}, {\(∀ \+\(x, x\&_, y, y\&_\)⟨x, 
                    x\&_⟩ ≻ ⟨y, 
                    y\&_⟩\  ⇔ ⟨x\&_⟩ ≻ ⟨y\&_⟩\)}})

\(∀ \+\(x, y\&_\)\((x⌣⟨y\&_⟩ = ⟨x, 
            y\&_⟩)\)\)

\(\(\(∀ \+\(x, y\&_\)\((⟨y\&_⟩⌢x = ⟨y\&_, 
            x⟩)\)\)\(
\)
    \)\)

\(∀ \+X\((is–tuple[
            X]\  ⇔ \ \(∃ \+\(x\&_\)\((X = ⟨x\&_⟩)\)\))\)\)
({{(Underscript[∀ , X])(is–empty–tuple[
                  X]  ⇔ (X = ⟨⟩))}, {(Underscript[∀ , X])(is–singleton–tuple[
                  X]  ⇔ (Underscript[∃ , x])(X = ⟨x⟩))}, {(Underscript[∀ , X])(is–trivial–tuple[
                  X] ⇔ (is–empty–tuple[
                      X] ∨ is–singleton–tuple[X]))}})

Axioms

({{\(∀ \+\(x, x\&_, y, y\&_\)\((⟨x, 
                    x\&_⟩\  = ⟨y, 
                    y\&_⟩)\) ⇔ \((\((x = 
                      y)\) ∧ \((⟨x\&_⟩ = ⟨y\&_⟩)\))\)\)}, {\(∀ \+\(x, x\&_\)⟨x, 
                x\&_⟩ ≠ ⟨⟩\)}})

Properties

(Underscript[∀ , is–trivia–tuple[X]])is–sorted[
        X]

(Underscript[∀ , is–trivial–tuple[X],  is–tuple[Y]])(X ≈ 
            Y ⇔ (X = Y))

({{(Underscript[∀ , is–tuple[X]])X ≈ X}, {(Underscript[∀ , is–tuple[X, Y]])(X ≈ 
                  Y \[Implies] Y ≈ X)}, {(Underscript[∀ , is–tuple[X, Y, Z]])((X ≈ 
                      Y ∧ Y ≈ Z) \[Implies] 
                X ≈ Z)

          }})

({{(Underscript[∀ , is–tuple[X, Y]])(X ≻ 
                  Y \[Implies] (Y ⊁ X))}, {(Underscript[∀ , is–tuple[X, Y, Z]])((X ≻ 
                      Y ∧ Y ≻ Z) \[Implies] 
                X ≻ Z)}})