Algorithm Invention and Verification 
by Lazy Thinking

Bruno Buchberger
RISC, Johannes Kepler University
RICAM, Austrian Academy of Science
Linz, Austria

Talk at Computer Science Department
Lamar University, Beaumont, Texas, USA
Nov 19, 2003

Copyright Bruno Buchberger 2003.

Copyrigh Note: This file may be copied and stored under the following conditions:

- the file is kept unchanged including the copyright note
- a message is sent to buchberger@risc.uni-linz.ac.at
- if the material is used, please, cite the talk appropriately.

Acknowledgement: Sponsored by RICAM (Radon Institute for Computational and Applied Mathematics, Austrian Academy of Science, Linz, Austria) and by SFB Project 1322 of the FWF (Austrian Science Foundation). Thanks to my PhD student A. Craciun who implemented part of the prover used in the synthesis example.

Introduction

The Problem of Algorithm Verification

Given:

P .. a problem specification ("what"),

A .. an algorithm ("how").

Find:

V .. a proof that A satisfies P ("why", "the correctness theorem").

The Problem of Algorithm Invention (Algorithm Synthesis)

Given:

P .. a problem specification.

Find:

A .. an algorithm that satisfies P (together with a proof of correctness).

Literature

Literature on algorithm verification is vast.

Literature on algorithm invention is limited, see recent survey

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.

One of the main approaches to algorithm invention:

Prove (automatically) that, for all inputs x, there exists a y such that P[ x, y].

From a successful proof, extract an algorithm A for P.

My Approach: "Lazy Thinking"

The Two Main Ideas

Use algorithm schemes for guessing possible algorithms.

For each algorithm scheme A, (automatically) attempt a proof that A satisfies P. From the failing proof, derive (automatically) specifications for the subalgorithms.

Find appropriate subalgorithms in an algorithm library or repeat lazy thinking for inventing the subalgorithms.

Earlier Papers

This is the natural application of the "lazy thinking" approach for theory exploration, see

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

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.

More Details

Try out "algorithm schemes" 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, requirements on the subalgorithms are generated that would enable the prover to complete the proof successfully.

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).

Upon Termination

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.

We will illustrate the method in a case study: Merge-Sort.

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.

Case Study: Merge Sort

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]


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

⟹

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

'Knowledge': The better you understand a problem, the better you can solve it

(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]))}})

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

(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)}})

'Is–Correct–Merge–Sort–Algorithm': The result of the invention

(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]])∧{({{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]])), is–trivial–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]]}})})}})}

Invention learned from the algorithm scheme including type requirements.

Invention learned from "failure". The invented requirements are "natural" !

Inventing the Algorithm by Lazy Thinking: First Round

We start from the following knowledge  base:

specification of the binary predicate 'is–sorted–version'.

algorithm scheme "divide and conquer".

and the following corresponding induction principle:

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]\)\(.\)\)\)

We now start attempting to prove the correctness theorem:

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

Will get stuck soon. (Why?)

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.

Proof Attempt Begin   (is automatic in Theorema!)

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

Requirement Generation

Now we analyze the failing proof situation and conjecture the requirement (can be done completely automatically in Theorema!):

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

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

Inventing the Algorithm by Lazy Thinking: Second Round

With this requirement on special we get over the failing proof situation and continue with:

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

Requirement Generation

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, first of all, is a good heuristic guide for human invention and verification and also for teaching algorithm design.

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

to have good algorithm scheme libaries

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.

We have all this in Theorema (to a certain extent and we are working on more).

Also note that 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.)

Case Study: Sorting by Insertion

Remark

Of course, sorting by insertion can be viewed as a degenerate case of sorting by merging.

The interest of this lies in the investigation of what happens if we start with the same algorithm specification

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

but throw in a different algorithm scheme.

Algorithm Scheme

This time we use the following algorithm scheme

sorted[⟨⟩] = c

(Underscript[∀ , x])(sorted[⟨x⟩] = 
          d[x])

\(∀ \+\(x, y, z\&_\)\((sorted[⟨x, y, 
              z\&_⟩] = 
          i[x, sorted[⟨y, 
                z\&_⟩]])\)\)

with the following natural type requirements on the auxiliary functions

({{is–tupe[c]

          }, {(Underscript[∀ , x]) is–tuple[d[x]]

          }, {(Underscript[∀ , x, is–tuple[Y]])is–tuple[
                i[x, Y]].}})

The corresponding inductive proof technique is:

For proving (Underscript[∀ , it[X]])A[X] do the following:

1. Prove  A[⟨⟩].

2. Take (Subscript[x, o]) arbitrary but fixed and prove    A[⟨(Subscript[x, 0])⟩].

3. Take (Subscript[x, o]), (Subscript[y, 0]), and \(TraditionalForm\`\(z\_0\)\&_\) arbitrary but fixed, assume \(A[⟨y\_0, \(z\_0\)\&_⟩]\) and prove \(\(\(\ \)\(\(A[⟨x\_0, 
            y\_0, \(z\_0\)\&_⟩]\)\(.\)\)\)\)

Algorithm Synthesis

We start with an attempt to prove

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

We do not show the proof attempts for the two base cases. Analyzing the failing situations in these two attempts readily leads to the two requirements

c = ⟨⟩

and

d[x] = ⟨x⟩.

Now we do the induction step. For this, we take (Subscript[x, o]), (Subscript[y, 0]), and \(TraditionalForm\`\(z\_0\)\&_\) arbitrary but fixed and assume

\(\(\(is–sorted–version[⟨y\_0, \(z\_0\)\&_⟩, \ 
      sorted[⟨y\_0, \(z\_0\)\&_⟩]]\)\(,\)\(\ \)\)\)

i.e.

({{\(is–tuple[
            sorted[⟨y\_0, \(z\_0\)\&_⟩]]\), (A1)

          }, {\(⟨y\_0, \(z\_0\)\&_⟩ ≈ 
            sorted[⟨y\_0, \(z\_0\)\&_⟩]\), (A2)

          }, {\(is–sorted[
            sorted[⟨y\_0, \(z\_0\)\&_⟩]]\), (A3)}})

and prove

\(\(\(is–sorted–version[⟨x\_0, 
        y\_0, \(z\_0\)\&_⟩, \ 
      sorted[⟨x\_0, 
          y\_0, \(z\_0\)\&_⟩]]\)\(,\)\(\ \)\)\)

i.e.

\(\(\(is–sorted–version[⟨x\_0, 
        y\_0, \(z\_0\)\&_⟩, \ 
      i[x\_0, sorted[⟨y\_0, \(z\_0\)\&_⟩]]]\)\(,\)\(\ \)\)\)

which we expand to

({{\(is–tuple[
            i[x\_0, sorted[⟨y\_0, \(z\_0\)\&_⟩]]]\), (G1)

          }, {\(⟨x\_0, 
              y\_0, \(z\_0\)\&_⟩ ≈ 
            i[x\_0, sorted[⟨y\_0, \(z\_0\)\&_⟩]]\), (G2)

          }, {\(is–sorted[
            i[x\_0, sorted[⟨y\_0, \(z\_0\)\&_⟩]]]\), (G3).}})

Now, (G1) follows from the type requirement on i and (A1).

The proof of (G2) and (G3) fails. However, the following requirements for i can be readily (i.e. automatically) generated from the temporary assumptions and goals:

\(∀ \+\(x, y, z\&_, is–tuple[Y]\)\)({({{\(⟨y, 
                        z\&_⟩ ≈ Y\)}, {is–sorted[Y]}})} \[Implies]{({{\(⟨x, y, 
                        z\&_⟩ ≈ i[x, Y]\)}, {is–sorted[i[x, Y]]}})}).

With these requirements, the proof can be completed.

In fact, together with the type requirement on i, these requirements characterize the natural properties of "insertion algorithms".

Case Study: Merging by Comparison

Problem Specification

Now we want to synthesize algorithms 'L', 'R', 'M' that satisfy the specification

(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, Y, 
                Z]])), ¬ is–trivial–tuple[X]])({({{L[X] ≈ Y}, {R[X] ≈ Z}, {is–sorted[Y]}, {is–sorted[Z]}})}\[Implies]{({{M[Y, Z] ≈ X}, {is–sorted[M[Y, Z]]}})})

Algorithm Scheme

We use the following algorithm scheme, which we again suppose to be available in our "algorithm schemes library":

({{c[⟨⟩, ⟨⟩] = cee}, {\(∀ \+\(y, \ y\&_\)c[⟨⟩, ⟨y, \ 
                  y\&_⟩] = ceg[y, \ y\&_]\)}, {\(∀ \+\(x, \ x\&_\)c[⟨x, \ 
                  x\&_⟩, ⟨⟩] = cge[x, \ x\&_]\)}, {\(∀ \+\(x, \ x\&_, y, \ y\&_\)c[⟨x, \ 
                  x\&_⟩, ⟨y, \ 
                  y\&_⟩]\) ={({{\(cgg1[x, 
                        c[⟨x\&_⟩, ⟨y, \ y\&_⟩]] ⇐ \ 
                      p[x, y]\)}, {\(cgg2[y, 
                        c[⟨x, \ 
                            x\&_⟩, ⟨y\&_⟩]] ⇐ \(¬ p[x, y]\)\)}})}}})

with the type requirements

({{is–tuple[cee]}, {\(∀ \+\(x, \ x\&_\)is–tuple[ceg[x, \ x\&_]]\)}, {\(∀ \+\(x, \ x\&_\)is–tuple[cge[x, \ x\&_]]\)}, {(Underscript[∀ , x, is–tuple[X]]){({{is–tuple[cgg1[x, X]]}, {is–tuple[cgg2[x, X]]}})}}})

where cee, ceg, cge, cgg1, cgg2, and p are the unknown subalgorithms.

The corresponding inductive proof technique is:

For proving (Underscript[∀ , it[X]])A[X] do the following:

1. Prove A[⟨⟩].

2. Take (Subscript[x, o])and \(TraditionalForm\`\(x\_0\)\&_\) arbitrary but fixed, assume \(A[⟨\(x\_0\)\&_⟩]\) and prove \(\(\(A[⟨x\_0, \(x\_0\)\&_⟩]\)\(.\)\)\)

This proof technique can be expanded to the following proof technique for conditioned formulae:

For proving (Underscript[((Underscript[∀ , it[X]])), C[X]])B[X] do the following:

1. Assume C[⟨⟩] and show B[⟨⟩].

2. Take (Subscript[x, o])and \(TraditionalForm\`\(x\_0\)\&_\) arbitrary but fixed. Assume \(\(\(\ \)\(¬ C[⟨\(x\_0\)\&_⟩]\)\)\) and \(C[⟨x\_0, \(x\_0\)\&_⟩]\) and prove \(\(\(B[⟨x\_0, \(x\_0\)\&_⟩]\)\(.\)\)\)

3. Now assume \(C[⟨\(x\_0\)\&_⟩]\), \(B[⟨\(x\_0\)\&_⟩]\), and \(C[⟨x\_0, \(x\_0\)\&_⟩]\) and prove \(\(\(B[⟨x\_0, \(x\_0\)\&_⟩]\)\(.\)\)\)

Summary of the Requirements Automatically Synthesized for the Subalgorithms

cee = ⟨⟩

(Underscript[∀ , z])(z ∈ 
            ceg[z] ∧ (dfo[z, 
                ceg[z]] = ⟨⟩))

(Underscript[∀ , z])(is–sorted[ceg[z]])

\(∀ \+\(z0, z1, z\&_\)\((z0 ∈ 
            ceg[z0, z1, z\&_] ∧ \((ceg[z1, z\&_] ≈ 
              dfo[z0, ceg[z0, z1, z\&_]])\))\)\)

\(∀ \+\(z0, z1, z\&_\)\)({({{\(is–sorted[ceg[z1, z\&_]]\)}, {z0 ≥ z1}})} \[Implies]\(is–sorted[ceg[z0, z1, z\&_]]\))

\(∀ \+\(y, y\&_\)\((is–sorted[⟨y, 
              y\&_⟩] \[Implies] 
          is–sorted[cge[y, y\&_]])\)\)

\(∀ \+\(y, y\&_\)\((is–sorted[⟨y, 
              y\&_⟩] \[Implies] ⟨y, 
              y\&_⟩ ≈ 
            cge[y, y\&_])\)\)

(Underscript[∀ , x, it[Y, Z]])(Y ≈ Z \[Implies] 
          cgg1[x, Y] ≈ cgg1[x, Z])

\(∀ \+\(y, y\&_, z, z\&_\)⟨y, y\&_, z, 
          z\&_⟩ ≈ 
        cgg1[y, ⟨y\&_, z, 
            z\&_⟩]\)

\(∀ \+\(y, y\&_, z, z\&_, it[Y]\)\)(∧{({{is–sorted[Y]}, {\(Y ≈ ⟨y\&_, z, 
                        z\&_⟩\)}, {\(is–sorted[⟨y, 
                        y\&_⟩]\)}, {\(is–sorted[⟨z, 
                        z\&_⟩]\)}, {p[y, z]}})}\[Implies]is–sorted[cgg1[y, Y]])

(Underscript[∀ , x, it[Y, Z]])(Y ≈ Z \[Implies] 
          cgg2[x, Y] ≈ cgg2[x, Z])

\(∀ \+\(y, y\&_, z, z\&_\)⟨y, y\&_, z, 
          z\&_⟩ ≈ 
        cgg2[z, ⟨y, y\&_, 
            z\&_⟩]\)

\(∀ \+\(y, y\&_, z, z\&_, it[Y]\)\)(∧{({{is–sorted[Y]}, {\(Y ≈ ⟨y, y\&_, 
                          z\&_⟩\)}, {\(is–sorted[⟨y, 
                          y\&_⟩]\)}, {\(is–sorted[⟨z, 
                          z\&_⟩]\)}, {¬ p[y, z]}})}\[Implies]is–sorted[cgg2[z, Y]]).

It is clear that the most natural definitions of algorithms satisfying these requirements are the following:

cee = ⟨⟩

\(∀ \+\(x\&_\)\((ceg[
            x\&_] = ⟨x\&_⟩)\)\)

\(∀ \+\(y\&_\)\((cge[
            y\&_] = ⟨y\&_⟩)\)\)

(Underscript[∀ , x, it[Z]])(cgg1[x, Z] = x⌣Z)

(Underscript[∀ , y, it[Z]])(cgg2[y, Z] = x⌣Z).

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

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 seen as a contribution to the problem of generating re-usable algorithms

can also be seen under the perspective of Mathematical Knowledge Management (MKM).

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.