Algorithmic Algorithm Synthesis 
Case Study Gröbner Bases

Bruno Buchberger

RISC 
(Research Institute for Symbolic Computation, U of Linz, Austria)
and
RICAM 
(Radon Institute for Computational and Applied Mathematics, Austrian Academy of Science)

Talk at the Mathematical Department of Kyushu University, Fukuoka, Japan
August 25, 2004

Copyright Bruno Buchberger 2004
Copyright Note: This file may be copied and stored under the following conditions:
      - the file is kept unchanged and the copyright note is included
      - a message is sent to buchberger@risc.uni-linz.ac.at
      - if the material is used in publications etc., this talk should be cited appropriately.

What we Have, What we Want

We Have

algorithm libraries

formula (e.g. integral) tables  and table-look-up algorithms

decision algorithms and proof generators for certain logical theories

proof checkers and proof generators for predicate logic

....

mathematical "knowledge" in paper form, LaTeX files etc.

What "We" Want

Integrated systems that support (partially automate) the entire "mathematical theory exploration" process:

Starting from some given mathematical concepts and mathematical knowledge on these concepts within a uniform logical language (predicate logic),

invent definitions (axioms) of new concepts

invent and prove / disprove propositions on these concepts

invent problems

invent and verify algorithms for problems

store the new knowledge (definitions, propositions, problems, algorithms) in structured knowledge libraries so that be used easily in the next rounds of mathematical theory exploration.

For example:

start from: +, -, *, ..<  on reals (axioms, propositions, problems, algorithms)

new concepts: definitions of "sequence" and operations +, -,  ... on sequences
explore: propositions, problems, algorithms on sequences

new concepts: "limit", "continuity"
explore: propositions, problems, algorithms on sequences

A benchmark example:

Let's write lecture notes on Groebner bases.

first concepts and exploration

next concepts and exploration

....

The Theorema Project

The Theorema project [BB et al. 1996 ...]  aims at being a frame for supporting  mathematical theory exploration in the above sense.

The Theorema language is a version of predicate logic.

A sublanguage of the Theorema language is a programming language.

The Theorema system is implemented in Mathematica. (This may change in the future.)

The Theorema group: B. B. (leader), T. Jebelean, T. Kutsia, F. Piroi, M. Rosenkranz, W. Windsteiger. PhD students.

Former group members: K. Nakagawa and others.

Mathematical Knowledge Management: A Recent International Endeavor

All this is part of a major new worldwide endeavor: "Mathematical Knowledge Management".

MKM 2001 at RISC
MKM 2003 in Bologna
MKM 2004 in Byalostok
AISC 2004 at RISC
...

MKM Networks in the EU and North America.

Numerical Mathematics

Computer Algebra

Automated Theorem Proving

Mathematical Knowledge Management  
                                  ("Symbolic Computation" in its widest sense)

An Algorithm for Algorithm Synthesis

The Algorithm Invention ("Synthesis") Problem

Given a problem specification P (in predicate logic), find an algorithm A such that

(Underscript[∀ , x]) P[x, A[x]].

Higher "order": Find an algorithm ("method") S such that

(Underscript[∀ , P])     (Underscript[∀ , x]) P[
            x,  S[P] [x]].

Examples of specifications P:

P[x, y]  ⇔  is–greater[x, y]
P[x, y]  ⇔  
      is–sorted–version[x, y]
P[x, y]  ⇔  
      has–derivative[x, y]
P[x, y]  ⇔  
      are–factors–of[x, y]
P[x, y]  ⇔  
      is–Gröbner–basis[x, 
        y]
....

A general algorithm S for "all" P cannot exist but ...

There is a rich literature on algorithm synthesis methods.

The "Lazy Thinking" Method [BB 2001]

Given a problem specification P

consider various "algorithm schemes" for A

and try to prove (automatically) (Underscript[∀ , x]) P[x, A[x]].

This proof will normally fail because nothing is known on the unspecified sub-algorithms in the algorithm scheme.

From the temporary assumptions and goals in the failing proof situation (automatically) generate such specifications for the unspecified sub-algorithms that would make the proof possible.

Now, apply the method recursively to the auxiliary functions.

"Lazy" because

we use the condensed algorithmic experience of others (in the schemes)

we start (routine) proving before we have an algorithm

we just wait until we fail in order to get an idea from the failure

Example: Synthesis of Merge-Sort [BB et al. 2003]

Problem

Synthesize A such that

(Underscript[∀ , x]) is–sorted–version[x, 
          A[x]].

Knowledge on Problem

(Underscript[∀ , x, y])(is–sorted–version[x, y]⇔({{is–sorted[y]}, {is–permuted–version[x, y]}}))

(Underscript[∀ , x, y])(is–sorted⇔({{is–sorted[y]}, {is–permuted–version[x, y]}}))

is–sorted[⟨⟩]

(Underscript[∀ , x]) 
        is–sorted[⟨x⟩]

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

etc.

An Algorithm Scheme

(Underscript[∀ , x])(A[x]={({{s[x], ⇐, is–trivial–tuple[x]}, {m[A[l[x]],A[r[x]]], ⇐, otherwise}})})

("divide and conquer")

The Result of Applying Lazy Thinking

Lazy Thinking, automatically (in approx. 2 minutes on a laptop using the Theorema system), finds the following specifications for the sub-algorithms that provenly guarantee the correctness of the above algorithm (scheme):

(Underscript[∀ , x])(s[x]=x)

(Underscript[∀ , y, z])(({{is–sorted[y]}, {is–sorted[z]}}) \[Implies]({{is–sorted[m[y, z]]}, {m[y, z] ≈ (y ≍ z)}}) )

(Underscript[∀ , x])(l[x]≍r[x] ≈  x)

Note: Definitions, theorems, algorithms are all just formulae in (Theorema) predicate logic.

For the intermediate and final notebooks automatically generated by the implementation of the lazy thinking method within the Theorema system see the enclosed notebooks Cascade-for-Merge-Sort-1-Polished.nb,  ...,  ....-4-Polished.nb.

What Do We Have Now?

Case A: We find algorithms S, M, L, R in our knowledge base for which the properties specified above are already contained in the knowledge base.
In this case, we are done, i.e. we have synthesized a sorting algorithm.

Case B: We find algorithms S, M, L, R in our knowledge base for which the properties specified above can be (automatically) proved.
In this case, we done, i.e. we have synthesized a sorting algorithm.

Case C: We do not find algorithms S, M, L, R in our knowledge base for which the properties specified can be proved.
In this case, we apply Lazy Thinking again in order to synthesize appropriate S, M, L, R,

until we arrive at sub-sub-...-algorithms in our knowledge base (e.g. the basic operations of tuple theory like append, prepend etc.)

Cases B and C can be avoided, if we proceed systematically bottom-up ("complete theory exploration" in layers).

Cases B and C are typical if one prefers a top-down exploration style.

How Can we Teach (= Automate) the Method

Compile a library of your algorithm design experience (= algorithm schemes).

Teach (automate) proving.

Teach (automate) generation of useful specifications of sub-algorithms from failing correctness proofs:

A simple (but amazingly powerful) rule:

Collects temporary assumptions  T[ x0, ... A [  ],  ...  ]
and temporary goals G[ x0, ...m  [  A [  ]  ]  ]

and produces specification

(Underscript[∀ , X,   ... ,  Y,   ... ])  (T[X,...Y,...]    ⟹   G[Y,...m  [Y] ] ).

Details: see papers [BB 2003] and example.

Research topic: other rules.

Parameters for Lazy Thinking

Lazy Thinking

Example: Synthesis of Insertion-Sort

Problem: Synthesize A such that

(Underscript[∀ , x]) is–sorted–version[x, 
          A[x]].

Example of algorithm scheme: "simple recursion"

A[⟨⟩]=c

(Underscript[∀ , x]) A[⟨x⟩]=s[⟨x⟩]

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

Lazy Thinking, automatically (in approx. 2 minutes on a laptop using the Theorema system), finds the following specifications for the auxiliary functions

c=⟨⟩

(Underscript[∀ , x])(s[⟨x⟩]=⟨x⟩)

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

Details of an Automated Synthesis

See the notebooks automatically produced by Theorema for the merge-sort example.

How far can we go with this method?

Can we automatically synthesize algorithms for non-trivial problems?

Example of a non-trivial problem: construction of Gröbner bases.

What is "non-trivial"?

Non-trivial: dozens of fundamental problems in algebraic geometry and related fields can be reduced to the construction of Gröbner bases, see the vast literature on Gröbner bases.

Non-trivial: for some of these problems no algorithm was known or was even conjectured not to exist (see [Loos 1974]).

Hence, question: Can Lazy Thinking automatically synthesize a Gröbner bases algorithm?

Main algorithmic idea of Gröbner bases theory:  The "S-polynomials"  ("critical pairs") together with the S-polynomial theorem.

Hence, question: Can Lazy Thinking automatically invent the notion of S-polynomial and automatically deliver the S-polynomial theorem.

Algorithmic Synthesis of a Gröbner Bases Algorithm

The Problem of Constructing Gröbner Bases

Find algorithm Gb such that

(Underscript[∀ , F])    (({{is–finite[ Gb[F] ]}, {is–Gröbner–basis[ Gb[F]]}, {ideal[F]=ideal[ Gb[F]].}}))

Definitions [BB 1965, 1970]:

is–Gröbner–basis[G]⇔is–confluent[ (Subscript[-> , G])].

Confluence of Division  (Subscript[-> , G])

(h1 (Subscript[-> , G])h2)⇔ (Underscript[∃ , g ∈ G])({({{lp[g] | lp[h1]}, {h2 = h1 - (lm[h1]/lm[g]) g}})} ),

is–confluent[->] :\(\(⇔\)\(∀ \+\(f1, f2\)\((f1\( ↔ \^*\)f2 \[Implies] 
              f1\(↓\^*\)f2)\)\)\)

Knowledge on the Concepts Involved

h1 (Subscript[-> , G])h2   \[Implies]  
          p  .  h1 (Subscript[-> , G])p . h2

etc.

Algorithm Scheme "Critical Pair / Completion"

({{A[F] =A[F, pairs[F]]}, {A[F, ⟨⟩]=F
}, {A[\(F, ⟨⟨g1, 
                  g2⟩, p\&_⟩\)]=
where[f=lc[g1, g2],h1 = trd[rd[f, g1], F],h2 = trd[rd[f, g2], F],
{({{A[\(F, ⟨p\&_⟩\)], ⇐, h1 = h2}, {A[F⌢df[h1, 
                                h2],\(⟨p\&_⟩\)≍⟨⟨(Subscript[F, k]),df[h1, h2]⟩ (Underscript[\[VerticalSeparator] , k = 
                                        1, …, \[LeftBracketingBar]F\[RightBracketingBar]])⟩], ⇐, otherwise}})} ]}})

This scheme can be tried in any domain, in which we have a reduction operation rd that depends on sets F of objects and a Noetherian relation ≻ which interacts with rd in the following natural way:

(Underscript[∀ , f, g])(f ⪰ 
            rd[f, g]).

The Essential Problem

The problem of synthesizing a Gröbner bases algorithm can now be also stated by asking whether starting with the proof of

(Underscript[∀ , F])    (({{is–finite[ A[F] ]}, {is–Gröbner–basis[ A[F]]}, {ideal[F]=ideal[ A[F]].}}))

we can automatically arrive at the idea that

lc[g1, g2]=lcm[lp[g1], lp[g2]]

and

df[h1, h2]=h1-h2

and prove that the idea is correct.

Now Start the (Automated) Correctness Proof

With current theorem proving technology, in the Theorema system, the proof attempt can be done automatically.

Details

It should be clear that, if the algorithm terminates, the final result is a finite set (of polynomials) G that has the property

(Underscript[∀ , g1, g2 ∈ G])(where[f = lc[g1, g2],h1 = trd[rd[f, g1], F],h2 = trd[rd[f, g2], F],∨{({{h1 = h2}, {df[h1, h2] ∈ G}})} ]).

We now try to prove that, if G has this property, then

is–finite[G],

ideal[F] = ideal[G],

and

is–Gröbner–basis[G],  
    i . e .  is–Church–Rosser[ (Subscript[-> , G])] .

Here, we only deal with the third, most important, property.

Using Newman's lemma and some elementary properties it can be shown that it is sufficient to prove

is–Church–Rosser[ (Subscript[-> , G])]⇔ (Underscript[∀ , p])(Underscript[∀ , f1, f2])(({({{p -> f1}, {p -> f2}})} )\[Implies]\(f1\(↓\^*\)f2\)).

Let now the power product p and the polynomials f1, f2 be arbitary but fixed and assume

{({{p (Subscript[-> , G])f1}, {p (Subscript[-> , G])f2.}})}

We have to find a polyonomial g such that

({{\(\(f1\(\( -> \_G\)\^*\)g\)\(,\)\)}, {\(f2\(\( -> \_G\)\^*\)\(\(g\)\(.\)\)\)}})

>From the assumption we know that there exist polynomials g1 and g2 in G such that

({{lp[g1] | p,}, {f1 = rd[p, g1],}})

({{lp[g2] | p,}, {f2 = rd[p, g2].}})

>From the final situation in the algorithm scheme we know that for these g1 and g2

∨{({{h1 = h2}, {df[h1, h2] ∈ G,}})}

where

({{h1 := trd[f1', G], f1' := rd[lc[g1, g2], g1], }, {h2 := trd[f2', G], f2' := rd[lc[g1, g2], g2].}})

Case h1=h2: In this case

\(lc[g1, 
          g2]\( -> \_g1\)\(rd[lc[g1, g2], g1]\(\( -> \_G\)\^*\)trd[
            rd[lc[g1, g2], g1], G]\) = 
trd[
          rd[lc[g1, g2], g2], G]\(\( ← \_G\)\^*\)rd[lc[g1, g2], 
          g2]\( ← \_g2\)\(\(lc[g1, g2]\)\(.\)\)\)

(Note that here we used the requirements rd[lc[g1,g2],g1]≺lc[g1,g2] and rd[lc[g1,g2],g2]≺lc[g1,g2].)

Hence, by elementary properties of polynomial reduction,

\(∀ \+\(a, q\)\(\((\ 
          a\ q\ lc[g1, 
                  g2]\( -> \_g1\)\(a\ q\ rd[lc[g1, g2], 
                    g1]\(\( -> \_G\)\^*\)a\ q\ trd[rd[lc[g1, g2], g1], 
                    G]\) = 
a\ q\ trd[rd[lc[g1, g2], g2], 
                  G]\(\( ← \_G\)\^*\)a\ q\ rd[lc[g1, g2], 
                  g2]\( ← \_g2\)\ 
              a\ q\ lc[g1, g2]\ )\)\(.\)\)\)

Now we are stuck in the proof.

However, using the above specification generation rule, we see that we could proceed successfully with the proof if lc[g1,g2] satisfied the following requirement

({{(Underscript[∀ , p, g1, g2])(({({{lp[g1] | p}, {lp[g2] | p}})} )\[Implies]((Underscript[∃ , a, q])(p = a q lc[g1, g2] ))), , (lc requirement)}})

With such an lc, we then would have

\(p\( -> \_g1\)rd[p, 
            g1] = \(a\ q\ rd[lc[g1, g2], g1]\(\( -> \_G\)\^*\)a\ q\ trd[
                rd[lc[g1, g2], g1], 
                G] = \(a\ q\ trd[rd[lc[g1, g2], g2], 
                  G]\(\( ← \_G\)\^*\)a\ q\ rd[lc[g1, g2], g2] = 
            rd[p, g2]\( ← \_g2\)p\)\)\)}

and, hence,

\(\(\(f1\(\( -> \_G\)\^*\)a\ q\ trd[rd[lc[g1, g2], g1], 
          G]\)\(,\)\)\)

\(\(\(f2\(\( -> \_G\)\^*\)a\ q\ trd[rd[lc[g1, g2], g1], 
          G]\)\(,\)\)\)

i.e. we would have found a suitable g.

Of course, it is now easy to find an lc that satifies (lc requirement), which also could be written in the form

(Underscript[∀ , p, g1, g2])(({({{lp[g1] | p}, {lp[g2] | p}})} )\[Implies](lc[g1, g2] | p)) ,

and the requirements

rd[lc[g1, g2], g1] ≺ lc[g1, g2],

rd[lc[g1, g2], g2] ≺ lc[g1, g2],

which, in the case of the domain of polynomials, are equivalent to

({{lp[g1] | lc[g1, g2],}, {lp[g2] | lc[g1, g2].}})

Namely,

lcp[g1, g2] = lcm[lp[g1], lp[g2]]

is a suitable function that satisfies the above requirements.

Heureka! The crucial function lc (the "critical pair" function) in the critical pair / completion algorithm scheme has been "automatically" synthesized!

Case h1≠h2 and, hence, df[h1,h2]∈G:

In this part of the proof we are basically stuck right at the beginning.

As a new requirement generation technique (which we did not yet consider above), we can try to reduce this case to the first case, which would generate the following requirement

({{\(∀ \+\(h1, h2\)\((h1\ \(\(↓\_{df[h1, 
                            h2]}\)\^*\)h2)\)\), (df requirement).  }})

(Looking to the knowledge base of elementary properties of polynomial reduction, it is now easy to find a function df  that satifies (df requirement), namely

df[h1, h2] = h1 - h2,

because, in fact,

\(∀ \+\(f, g\)\(\((f\ \(\(↓\_{f - 
                        g}\)\^*\)g)\)\(.\)\)\)

Heureka! The function df (the "completion" function) in the critical pair / completion algorithm scheme has been "automatically" synthesized!)

Summary of the Synthesizing Proof Attempt

The proof, of course, fails at the point where it would need knowledge about the unknown subalgorithms lc and df.

Beginning of the proof:

Let G be A[ F]. We have to prove that

is–finite[G],

ideal[F] = ideal[G],

and

is–Gröbner–basis[G],  
    i . e .  is–confluent[ (Subscript[-> , G])] .

We only deal with the third, most important, property. For this, we assume

{({{p (Subscript[-> , G])f1}, {p (Subscript[-> , G])f2.}})}

and have to find a polynomial g such that

({{\(\(f1\(\( -> \_G\)\^*\)g\)\(,\)\)}, {\(f2\(\( -> \_G\)\^*\)\(\(g\)\(.\)\)\)}})

Generation of the Specification of lc

In the failing proof situation, by the (automated) analysis algorithm sketched above, we detect that the proof could be completed if the unknown lc satisfied the following property:

({{lp[g1]|lc[g1, g2],}, {lp[g2]|lc[g1, g2],}})

(Underscript[∀ , p, g1, g2])(({({{lp[g1] | p}, {lp[g2] | p}})} )\[Implies](lc[g1, g2]|p)) .

Heureka! It is clear that this specification is (only) met by

lc[g1, g2]=lcm[lp[g1], lp[g2]].

Similarly, it can be (automatically) detected that

df[h1, h2]=h1-h2.

Conclusion

Research Topics

Libraries of algorithm schemes.

More generally, libraries of definition, theorem, problem, and algorithm schemes.

Case studies of problem (schemes), knowledge, algorithm schemes and how they produce algorithms.

"Functor" knowledge: each algorithm is a "functor"

If s, m, l, r is a merge structure                                                then             A is a sort structure.
and A results from s, m, l, r by divide and conquer

References

On Gröbner Bases

[Buchberger 1970]
B. Buchberger. Ein algorithmisches Kriterium für die Lösbarkeit eines algebraischen Gleichungssystems (An Algorithmical Criterion for the Solvability of Algebraic Systems of Equations). Aequationes mathematicae 4/3, 1970, pp. 374-383. (English translation in: [Buchberger, Winkler 1998],  pp. 535 -545.) Published version of the PhD Thesis of B. Buchberger, University of Innsbruck, Austria, 1965.

[Buchberger 1998]
B. Buchberger. Introduction to Gröbner Bases. In: [Buchberger, Winkler 1998], pp.3-31.

[Buchberger, Winkler, 1998]
B. Buchberger, F. Winkler (eds.). Gröbner Bases and Applications, Proceedings of the International Conference "33 Years of Gröbner Bases", 1998, RISC, Austria, London Mathematical Society Lecture Note Series, Vol. 251, Cambridge University Press, 1998.

[Becker, Weispfenning 1993]
T. Becker, V. Weispfenning. Gröbner Bases: A Computational Approach to Commutative Algebra, Springer, New York, 1993.

On Mathematical Knowledge Management

B. Buchberger, G. Gonnet, M. Hazewinkel (eds.)
Mathematical Knowledge Management.
Special Issue of Annals of Mathematics and Artificial Intelligence, Vol. 38, No. 1-3, May 2003, Kluwer Academic Publisher, 232 pages.

A.Asperti, B. Buchberger,J.H.Davenport (eds.)
Mathematical Knowledge Management.
Proceedings of the Second International Conference on Mathematical Knowledge Management (MKM 2003), Bertinoro, Italy, Feb.16-18, 2003, Lecture Notes in Computer Science, Vol.2594, Springer, Berlin-Heidelberg-NewYork, 2003, 223 pages.

On Theorema

[Buchberger et al. 2000]
B. Buchberger, C. Dupre, T. Jebelean, F. Kriftner, K. Nakagawa, D. Vasaru, W. Windsteiger. The Theorema Project: A Progress Report. In: M. Kerber and M. Kohlhase (eds.), Symbolic Computation and Automated Reasoning (Proceedings of CALCULEMUS 2000, Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, August 6-7, 2000, St. Andrews, Scotland),  A.K. Peters, Natick, Massachusetts, ISBN 1-56881-145-4, pp. 98-113.

On Theory Exploration and Algorithm Synthesis

[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.), ISSN 1124-970X, pp. 9-32.

[Buchberger 2003] 
B. Buchberger. Algorithm Invention and Verification by Lazy Thinking.
In: D. Petcu, V. Negru, D. Zaharie, T. Jebelean (eds), Proceedings of SYNASC 2003 (Symbolic and Numeric Algorithms for Scientific Computing, Timisoara, Romania, October 1–4, 2003), Mirton Publishing, ISBN 973–661–104–3, pp. 2–26.

[Buchberger 2004]
B. Buchberger. The Four Parallel Threads of Formal Theory Exploration. Technical Report of the SFB (Special Research Area) Scientific Computing, Johannes Kepler University, Linz, in preparation.

[Buchberger, Craciun 2003]
B. Buchberger, A. Craciun. Algorithm Synthesis by Lazy Thinking: Examples and Implementation in Theorema. in: Fairouz Kamareddine (ed.),  Proc. of the Mathematical Knowledge Management Workshop, Edinburgh, Nov. 25, 2003, Electronic Notes on Theoretical Computer Science,  volume dedicated to the MKM 03 Symposium, Elsevier, ISBN 044451290X, to appear.

[Buchberger 2004]
B. Buchberger. 
Towards the Automated Synthesis of a Gröbner Bases Algorithm.
RACSAM (Review of the Royal Spanish Academy of Science), to appear, 10 pages.