Verified Algorithm Development 
by Lazy Thinking

Invited talk at 
International Mathematica Symposium
Imperial College, London
7-11 July, 2003

Bruno Buchberger

RISC
(Research Institute for Symbolic Computation)
Johannes Kepler University
A4040 Linz, Austria
bruno.buchberger@jku.at

Copyright Note:  Copyright Bruno Buchberger 2004.

Copying is granted if the following conditions are satisfied:

- the file is kept unchanged
- in particular, it must include the copyright note
- an e-mail is sent to bruno.buchberger@jku.at

If you use the material in this talk, cite it appropriately.

Summary of Talk

Can old Buchberger 2003-... automate young Buchberger 1965 ?

Problems and Algorithms

Algorithmic Mathematics and Mathematica

Mathematica (etc.)  = the accumulated algorithmic knowledge for solving mathematical problems.

Much of this knowledge was invented and developed only in the past 40 years!

Problems and Algorithmic Solutions

A problem:

Given x,
find y such that P[ x, y ].

An algorithmic solution:

An algorithm (program) S such that
for all x,  P[ x, S[ x ]].

Example

Problem

Given a system F of polynomials,
find a tuple T of numbers such that T substituted for the indeterminates of F makes all F to zero.

Algorithmic Solution "Solve"

Solve[F] substituted for the indeterminates of F makes all F to zero.

Example Computation

F = {x (y^2) - 2  (x^2) + x y + 3 == 
            0,   (x^2) + (y^2) + x + y == 0};

T = 
      Solve[{x (y^2) - 2  (x^2) + x y + 3 == 
            0,   (x^2) + (y^2) + x + y == 0}]

N[T]

T[[1]]

Simplify[x (y^2) - 2  (x^2) + x y + 3 /. T[[1]]]

Simplify[(x^2) + (y^2) + x + y /. T[[1]]]

The Algorithm:

Transform F into an equivalent Gröbner basis G.

Solve the univariate poly of G.

Backsubstitute and solve for the other variables.

F = {x (y^2) - 2  (x^2) + x y + 3,   (x^2) y + (y^2) + x + 
            y};

GroebnerBasis[F]

How Do We Invent Algorithms?

Understand the problem P!

Specify P and collect knowledge on the underlying concepts of P! 

(Ask old mathematicians, they know a lot!     Example: Gröbner 1965.)

Think!

...  
Find S.

(Young mathematicians are good at this!    Example: BB 1965.)

Verify!

Verify that S solves the prolem P, i.e. prove that, for all x, P[ x, S[ x ]].

How Do I Want to Invent Algorithms Algorithmically?

Solve the following meta-problem by an algorithm (a "system"):

Given: Any problem P.

Find:    An algorithm S that solves the problem P and proves the correctness of S.

Algorithmically unsolvable.

More and more general and powerful (interactive) systems possible.

This talk: A progress report on this meta-problem.

The current state of this research is implemented in Theorema on top of Mathematica.

Acknowledgement to my co-workers A. Craciun, F. Piroi, K. Nakagawa, W. Windsteiger, T. Jebelean who helped in the implementation.

Initialize Theorema

The Basic Idea of Algorithm Invention and Verification by "Lazy Thinking"

Let's Look Once More at Algorithm Invention

Understand the problem P!

Specify P and collect knowledge on the underlying concepts of P!

Think!

...  
Find S.

Verify!

Verify that S solves the prolem P, i.e. prove that, for all x, P[ x, S[ x]].

If we want to automate algorithm invention and verification, we have to automate mathematical thinking.

A Refinement and Approach

Understand the problem P:

Give a complete specification of the problem (in the language of predicate logic).

Collect all knowledge on the ingredient concepts (as formulae in predicate logic).

Note: Knowledge libraries for all areas of mathematics will be an indispensible part of future math software systems.

Think "lazily":

Introduce a name, say S, for the unknown algorithm.

Chose an algorithm type from a library of algorithm types, by which

the unknown algorithm is decribed in terms of unknown subalgorithms.

Note: There are millions of algorithms but there are only a few algorithm types!

Note: Algorithm type libraries for the various data types will be an indispensable part of future math software systems.

Note: The algorithmic know-how of mathematics can be captured in algorithm types.

Verify "lazily":

Try to prove that S solves the problem P, i.e. that, for all x, P[ x, S[ x]].             (Correctness Theorem)

Typically, this proof will fail (because nothing is known on the subalgorithms).

From the failing proof, conjecture requirements on the subalgorithms that would make the proof work.

Repeat trying to prove the correctness theorem until requirements for all subalgorithms are found that are strong enough for proving the correctness theorem.

The key idea: Try to verify before you invent!

Note: In case this procedure stops one has a verified algorithm S for the problem P that works with all subalgorithms that satisfy the requirements generated. 

The invention and verification of the subalgorithm can then be done by the same procedure until one arrives at requirements that are already satisfied by existing algorithms!

Note: This procedure can be automated, if proving and conjecture generating can be automated.  Hence, all research attention has to go to automating proving and conjecture generating.

Note: Even in contexts where proving and conjecture generating can not be completely automated, the above procedure is a worthwhile heuristic and didactic approach for human algorithm invention and verification.

Example: The Problem of Sorting

Problem Specification

The Sorting Predicate

Given: X satisfying

is–tuple[X]

Find:   Y such that

is–sorted–version[X, Y]

Details

Definition["is sorted version",any[is–tuple[X],  Y],
is–sorted–version[X, Y]  ⇔(∧{({{is–tuple[Y] }, {X≈Y  }, {is–sorted[Y]}})} )]

Note: From here on, we use the Theorema syntax for predicate logic formulae.

X≈Y     ...      X and Y contain the same elements (X and Y are permuted versions of each other).

"Complete" Knowledge on the Ingredient Concepts (Functions and Predicates)

Definition["is sorted",\(any[x, y, z\&_]\),
({{is–sorted[⟨⟩] }, {is–sorted[⟨x⟩]}, {\(is–sorted[⟨x, y, 
                    z\&_⟩]\)   ⇔
(∧{({{x ≥ y}, {\(is–sorted[⟨y, 
                                z\&_⟩]\)}})} )}})]

Definition["is permuted version",\(any[x, x\&_, y, y\&_]\),
({{⟨⟩≈⟨⟩ }, {\(⟨⟩ ≉ ⟨y, y\&_⟩\)}, {\(⟨x, 
                    x\&_⟩ ≈ ⟨y\&_⟩\  ⇔ \((x ∈ ⟨y\&_⟩ ∧ ⟨x\&_⟩ ≈ 
                      delete[x, \ ⟨y\&_⟩])\)\)}})]

....

Proposition[\("only empty tuple equivalent to empty tuple", 
      any[is–tuple[
          X]], 
\((X ≈ ⟨⟩)\) \[Implies] \((X = ⟨⟩)\)\)]

...

Dozens of formulae constitute the "complete" knowledge on these concepts. (All these formulae can be proved automatically by Theorema and similar systems. In fact, many of these formulae can also be invented by the lazy thinking paradigm.)

Collect (Relevant) Knowledge in a "Theory"

Theory["knowledge: is sorted version",
({{Definition["is sorted"]}, {Definition["is permuted version"]}, {Definition["is sorted version"]}, {...}, {Proposition["only empty tuple equivalent to empty \
tuple"]}, {Proposition["reflexivity of permuted version"]}, {...}})]

The Correctness Theorem for the Unknown Sorting Algorithm "Sorted"

Theorem[\("correctness of sort", 

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

Now Press the Button and a Sorting Algorithm (Various Sorting Algorithms) Will be Invented and Verified Automatically

We can now call the lazy thinking procedure by the following call in Theorema:

\(\(\(Prove\)\([\)\(Theorem["correctness of sort"], 
using -> 
        Theory["knowledge: is sorted version", 
by -> \ Cascade\  ... ]\)\)\)

The generation and verification of the algorithm will take approximately 12 minutes.

Meanwhile we continue with the talk.

Algorithm Type: Divide and Conquer for Tuples

The Main Structure of the Algorithm Type

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

The functions 'special', 'left–split', 'right-split', 'merged' are unknown.

The predicate 'is–trivial–tuple' is known: tuples with length ≤ 1. (Definition is part of the knowledge base.)

Auxiliary Ingredients of the Algorithm Type

Lemma["splits are shorter",any[is–tuple[X]],with[¬ is–trivial–tuple[X]],
({{X ≻ left–split[X]}, {X ≻ right–split[X]}})  ]

Lemma["closure of special",  any[X],  
      with[is–tuple[X] ∧ 
          is–trivial–tuple[
            X]],  
is–tuple[special[X]]]

Lemma["splits are tuples",any[X],with[
          is–tuple[X] ∧ ¬ is–trivial–tuple[X]],
({{is–tuple[left–split[X]]}, {is–tuple[right–split[X]]}})  ]

Lemma["closure of merge",  
      any[is–tuple[X,  Y]],  
is–tuple[
        merged[X,  Y]]]

Theory["algorithm type knowledge", 
({{Lemma["closure of special"]}, {Lemma["splits are tuples"]}, {Lemma["splits are shorter"]}, {Lemma["closure of merge"]}})
]

The Proof Method Attached to the Algorithm Type

For proving

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

it suffices to do the following:

Take \(TraditionalForm\`\(x\_0\)\&_\) arbirtrary but fixed and assume

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

and

\(∀ \+\(is–tuple[X]\)\(\((X ≺ ⟨\(x\_0\)\&_⟩ \[Implies] A[X])\)\(.\)\)\)

Prove

\(\(\(A[⟨\(x\_0\)\&_⟩]\)\(.\)\)\)

Here, '≺' is the ordering of tuples by length. (Its definition is part of the knowledge base.)

Lazy Thinking: First Round

Proof Attempt (by Automated Prover)

We now attempt to prove

the correctness theorem for the unknown algorithm 'sorted'

using

the knowledge on the concepts in the problem specification

the knowledge on the chosen algorithm type

by

the above inductive proof method.

(Automated) Conjecture Generation from Failing Proof

The proof fails (because nothing is known on 'special', 'left–split', 'right–split', 'merged'.

By considering the algorithm type, the proof naturally splits into two cases:

\(is–trivial–tuple[⟨\(x\_0\)\&_⟩]\)

\(¬ is–trivial–tuple[⟨\(x\_0\)\&_⟩]\)

In fact, the proof already fails in the case  'is–trivial–tuple[\(⟨\(x\_0\)\&_⟩\)]'.

However, amazingly, from the failing proof the following requirement on 'special' can be generated (automatically):

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

Note: This requirement on 'special' is not some strange condition but is simple and natural.

Return to (the Beginning of) the Main Proof

Lazy Thinking: Second Round

Proof Attempt (by Automated Prover)

We now attempt, again, to prove

the correctness theorem for the unknown algorithm 'sorted'

using

the knowledge on the concepts in the problem specification

the knowledge on the chosen algorithm type

the requirement generated in the first round:

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

by

the above inductive proof method.

(Automated) Conjecture Generation from Failing Proof

The proof fails again (because nothing is known on 'left–split', 'right–split', 'merged'.

This time, the proof fails in one of the branches in the case  '¬is–trivial–tuple[\(⟨\(x\_0\)\&_⟩\)]'.

However, amazingly, from the failing proof the following requirement on 'special' can be generated (automatically):

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

Note: This requirement on 'left–split', 'right–split', 'merged' is not some strange condition but is simple and natural.

Return to (the Beginning of) the Main Proof

Lazy Thinking: Third Round

Proof Attempt (by Automated Prover)

We now attempt, again, to prove

the correctness theorem for the unknown algorithm 'sorted'

using

the knowledge on the concepts in the problem specification

the knowledge on the chosen algorithm type

the requirements generated in the first and second round:

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

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

by

the above inductive proof method.

(Automated) Conjecture Generation from Failing Proof

The proof fails again (because too little is known on 'left–split', 'right–split', 'merged'.

This time, the proof fails in the last branch in the case  '¬is–trivial–tuple[\(⟨\(x\_0\)\&_⟩\)]'.

However, amazingly, from the failing proof the following requirement on 'special' can be generated (automatically):

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

Note: This requirement on 'merged' is not some strange condition but is simple and natural.

Return to (the Beginning of) the Main Proof

Lazy Thinking: Last Round

Proof Attempt (by Automated Prover)

We now attempt, again, to prove

the correctness theorem for the unknown algorithm 'sorted'

using

the knowledge on the concepts in the problem specification

the knowledge on the chosen algorithm type

the requirement generated in the first and second round:

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

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

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

by

the above inductive proof method.

This Time the Proof Goes Through Successfully

What Do We Know Now?

We know now that the algorithm

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

is a correct sorting algorithm, i.e. satisfies the correctness theorem

is–sorted–version[X, sorted[X]]

if we take, as subalgorithms, any algorithms 'special', 'left–split', 'right–split', 'merged' that satisfy the following "requirement" (i.e. problem specification):

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

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

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

(and respect types).

How Can We Proceed?

The subalgorithm 'special' is fully described by the requirement.

We can now look in our knowledge base for algorithms 'left–split', 'right–split', 'merged' that satisfy the above requirements.

Note: Future mathematical software systems must be mathematical knowledge bases, not only algorithm bases!

If we find such algorithms then we are done.

If we do not yet have such algorithms 'left–split', 'right–split', 'merged' in our knowledge base then we can apply the lazy thinking method again for inventing and verifying such algorithms.

The Whole Cycle Could be Repeated Now With Other Algorithm Types

Then we would get various different sorting algorithms.

Let's Look to the Output of the Automated Lazy Thinking Procedure

Note that all proofs and conjectures in the following notebook are generated, completely automatically, by our lazy thinking procedure, which is part of the Theorema system.

Theorema is programmed in the Mathematica language and, also, uses many features of the Mathematica front-end.

The automated prover used in this example is a combination of well-founded induction and general predicate logic "natural deduction".

The details of the conjecture generation algorithm will be explained when looking to the failing proofs generated by the lazy thinking procedure.

Summary of Talk

The Challenge

Can old Buchberger 2003-... automate young Buchberger 1965 ?

It may be possible.

Algorithm Invention and Verification

A  procedure for automated algorithm invention and verification.

The proposed procedure

is natural

uses algorithm types as condensed algorithmic knowledge

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

is able to generate conjectures 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 (not shown in this talk).

Theorem Invention and Verification

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.

Knowledge types have to be used instead of algorithm types.

Challenge Beyond

The challenge beyond

Can old Buchberger 2003-... automate old Gröbner 1965 ?

is:

Can we automate problem  invention?

Challenge Beyond

Can we automate concept invention? E.g. concept of Gröbner basis.

Future Math Systems

All this is part of the new field of "Mathematical Knowledge Management" (MKM), see "MKM 2001" at RISC, "MKM 2003" at U of Bologna, "MKM 2004" at U of Birmingham, etc.

Current mathematical systems handle only a small sector of MKM: Algorithm libraries.

Future mathematical systems will have to support all aspects of MKM:

algorithm libraries and computational engine for these libraries

knowledge libraries

problem type, data type, algorithm type, knowledge type libraries

automated reasoners (provers, solvers, simplifiers) and conjecture generators

tools for organizing large web-accessible knowledge and algorithm bases in a structured way.

Appendix: The Four Notebooks Automatically Generated During the Synthesis of Merge-Sort

First Notebook

Pending proof of (13.4).

Pending proof of (8).

Second Notebook

Pending proof of (41.4).

Third Notebook

Fourth Notebook