Algorithmic Algorithm Synthesis 
Case Study Gröbner Bases

Talk at
International Algebraic Conference 
Moscow State University, May 26 - June 2, 2004

Bruno Buchberger

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

Copyright Bruno Buchberger 2004.

Copyright Note: This file can be printed, stored and distributed under the following conditions:

- the file is kept unchanged
- this copyright note is included
- a message is sent to Bruno.Buchberger@RISC.Uni-Linz.ac.at

If you use the material, please, cite this  talk appropriately.

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.
There is a rich literature on synthesis algorithms (methods) for special instances of the problem,
including methods in software technology, e.g. "component-based programming".

The Theorema Project

The Theorema project [BB et al. 1996 ...]  aims at computer-support of all phases of mathematical activity:

invention of notions

invention and proof of propositions

invention of problems

invention and proof of algorithms (the subject of this talk)

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.

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 "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 auxiliary functions in the algorithm scheme.

From the temporary assumptions and goals in the failing proof situation (automatically) generate specifications for the auxiliary functions that would make the proof possible.

Now, apply the method recursively to the auxiliary functions.

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

Problem: Synthesize A such that

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

Example of algorithm scheme: "divide and conquer"

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

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

(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: All these algorithms are formulae in (Theorema) predicate logic and are executable within the same logic!

Acknowledgement: My PhD students A. Craciun, W. Windsteiger, et al.

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\&_⟩)\)}}) )

Automation of the Method

Automated induction proving: Is available in Theorema.

Automated analysis of failing proofs and automated generation of "lemmata" ( = specifications for the subalgorithms):

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

and produces lemma ( = specification )

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

Details: see papers [BB 2003].

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.

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.

Can my algorithm synthesis algorithm synthesize my own Gröbner bases algorithm (and similar algorithms)?

Main invention of Gröbner bases theory:  The "S-polynomials"  ("critical pairs").

Can we invent the notion of S-polynomials and the corresponding theorem (with proof) automatically?

Algorithmic Synthesis of My 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)\)\)\)

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

Details cannot be presented in one talk.

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

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

The algorithmization of mathematics goes higher and higher becoming more and more "symbolic" ....

More algorithmization of mathematics can only be based on more mathematics.

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.