Formal Mathematics:
A Key to the Future

Bruno Buchberger
RISC, Austria

Talk at "Engineering and Life Sciences"
June 26-30, 2006, Avignon, France
Dedicated to the 60th Birthday of Gautam Dasgupta

Purpose

Give the flavor of a certain area in algorithmic mathematics: 
"formal math", "automated reasoning", "intellectics", "mathematical knowledge management", "computer-supported mathematical theory exploration", ...

Does this have applications for life sciences?

Application to Life Sciences

????

A recent project with "Genomica" company: imitate the process of how biologists guess the mapping between the presence of certain genes and biologic behavior.  (⟶  "Algorithm synthesis")

Processes in life sciences cannot be simulated without simulating the "evolution" of the processes. 
Example: simulation of a cell.  (  ⟶  "Self-reference" is an important issue.)

Conference Announcement:  "Algebraic Biology 2007",  July 2-4, 2007

www.risc.uni-linz.ac.at/about/conferences/ab2007/

We need biologists who present problems !

Symbolic methods tutorial week before AB 2007 !

Focus of This Talk

Formal mathematics: Why a key? Answer: Increase the efficiency of the mathematical research process.

Mathematical research process: invention and verification.

In this talk only one example: automated invention of a (non-trivial) algorithm and automated proof, namely algorithm for constructing Groebner bases.

Contents of the Talk

All Current Algorithmics (Numerics, Symbolics,...) is Available in Systems

Systems like Mathematica, Maple, Derive, Mathlab, ... FORM, Singular, Cocoa, ...

An enormous potential for science (physics, ...) and engineering.

Help!  and additional Packages

⟶ The other math talks at this conference

Remark:

There is lots of new and deep mathematics behind the (numeric, discrete, graphic, algebraic, and symbolic) algorithms of the current math systems.

In this talk only one example: Gröbner bases theory:

Why are Gröbner bases important? (Dozens of fundamental problems in pure and applied math can be reduced to Gröbner bases constructions! Examples: non-linear equation solving, diophantine equs with poly coefficients, presentations of polys as polys of polys, decomposition of varieties, canonical simplification modulo poly relations, ...)

What are Gröbner bases?

How can Gröbner bases be computed?

Example of a Groebner Basis   (BB 1965, ...)

B.B. An Algorithmic Criterion for the Solvability of Systems of Algebraic Equations, aequationes mathematicae, 1970. (English translation in: B.B., F.Winkler. Gröbner Bases: Theory and Applications. Cambridge University Press, 1998, pp. 540-560.

A system of polynomials (not a Groebner basis):

(Subscript[f, 1])=x y-2  y z - z;
(Subscript[f, 2]) = (y^2) - (x^2) z  +  x z;
(Subscript[f, 3])=(z^2)-(y^2) x + x;

F  =  {(Subscript[f, 1]), (Subscript[f, 2]), (Subscript[f, 3])};

A ("the") corresponding Groebner basis:

G = GroebnerBasis[F]

What important property of Groebner bases can we observe here?

zsol = NSolve[G[[1]] == 0, z]

Gsubnum = G  /.  zsol[[1]]

ysol = NSolve[ Gsubnum[[2]] == 0, y]

Theorem (Roider, Kalkbrener et al. 1990): It suffices to consider the poly in y with lowest degree.

xsol = NSolve[ Gsubnum[[4]] == 0, x]

F /. zsol[[1]] /. ysol[[1]] /. xsol[[1]]

Another Example of Application of Groebner Bases: Invariant Theory

A Question:  Can

h = ((Subscript[x, 1])^7) (Subscript[x, 2]) - (Subscript[x, 1]) ((Subscript[x, 2])^7)

be expressed as a polynomial in

F = {((Subscript[x, 1])^2) + ((Subscript[x, 2])^2), ((Subscript[x, 1])^2) ((Subscript[x, 2])^2), ((Subscript[x, 1])^3) (Subscript[x, 2]) - 
          (Subscript[x, 1]) ((Subscript[x, 2])^3)}

?

Note: These polynomials are fundamental invariants for the group (Subscript[ℤ, 4]).

Reduction to Groebner Bases Computation

{time, GB} = 
      GroebnerBasis[{-(Subscript[i, 1]) + ((Subscript[x, 1])^2) + 
              ((Subscript[x, 2])^2), -(Subscript[i, 2]) + ((Subscript[x, 1])^2) 
                ((Subscript[x, 2])^2), -(Subscript[i, 3]) + ((Subscript[x, 1])^3) (Subscript[x, 2]) - 
              (Subscript[x, 1]) ((Subscript[x, 2])^3)}, {(Subscript[x, 2]), (Subscript[x, 1]), (Subscript[i, 3]), (Subscript[i, 2]), (Subscript[i, 1])}] // 
        Timing

PolynomialReduce[((Subscript[x, 1])^7) (Subscript[x, 2]) - (Subscript[x, 1]) ((Subscript[x, 2])^7), 
      GB, {(Subscript[x, 2]), (Subscript[x, 1]), (Subscript[i, 3]), (Subscript[i, 2]), (Subscript[i, 1])}, 
      MonomialOrder -> Lexicographic]

(Subscript[i, 1]^2) (Subscript[i, 3]) - (Subscript[i, 2]) (Subscript[i, 3])

Theorem (Sweedler, Sturmfels et al. 1988): h can be represented in terms of I iff remainder of h w.r.t. "Groebner basis of I with slack variables" is a polynomial in the slack variables (which gives the representation).

(Subscript[i, 1]^2) (Subscript[i, 3]) - (Subscript[i, 2]) (Subscript[i, 3]) /. {(Subscript[i, 1]) -> ((Subscript[x, 1])^2) + ((Subscript[x, 2])^2), 
          (Subscript[i, 2]) -> ((Subscript[x, 1])^2) ((Subscript[x, 2])^2), 
          (Subscript[i, 3]) -> ((Subscript[x, 1])^3) (Subscript[x, 2]) - (Subscript[x, 1]) ((Subscript[x, 2])^3)}  // 
      Expand

R = 
      PolynomialReduce[((Subscript[x, 1])^6) (Subscript[x, 2]) - (Subscript[x, 1]) ((Subscript[x, 2])^6), 
        GB, {(Subscript[x, 2]), (Subscript[x, 1]), (Subscript[i, 3]), (Subscript[i, 2]), (Subscript[i, 1])}, 
        MonomialOrder -> Lexicographic]

-(Subscript[i, 1]^3) (Subscript[x, 1]) + 2 (Subscript[i, 1]) (Subscript[i, 2]) (Subscript[x, 1]) + (1/2) (Subscript[i, 1]) (Subscript[i, 3]) (Subscript[x, 1]) + 
      (Subscript[i, 1]^2) (Subscript[x, 1]^3) - (Subscript[i, 2]) (Subscript[x, 1]^3) + (1/2) (Subscript[i, 3]) (Subscript[x, 1]^3) + 
      (1/2) (Subscript[i, 1]) (Subscript[i, 2]) (Subscript[x, 2])

((Subscript[x, 1])^6) (Subscript[x, 2]) - (Subscript[x, 1]) ((Subscript[x, 2])^6) can not be expressed by the fundamental invariants in I.

Another Example of the Application of Groebner Bases: Computation on Differential Operators

See talk by M. Rosenkranz.

More Applications

> 1000 papers and > 10 textbooks on Groebner bases.

Applications in: Algebraic Geometry, Cryptography, Coding Theory, Integer Optimization, Algebraic Combinatorics, Combinatorial and Special Function Identities, Symbolic Summation, Symbolic Analysis (in particular, Differential Equations), Geometry Theorema Proving, Control Theory, etc.

Gröbner Bases 2006 Special Semester at RICAM and RISC (Feb - June 2006): 10 Proceedings volumes will be issued.

The Problem of Constructing Gröbner Bases

Definition: F is a Gröbner basis iff

polynomial reduction ("division") w.r.t. F is unique.

Problem: Given F,  find G   such that G is a Gröbner basis 
                                            and F and G generate the same set of linear combinations.

Why is this problem fundamental?

Many problems that are difficult for general F are easy for Gröbner bases G.

Hence, many difficult problems can be solved by (easy) reductions to the problem of constructing Gröbner bases, for wich these problems are easy.

The "Main Theorem" of Gröbner Bases Theory (BB 1965):

F is a Gröbner basis  ⟺   (Underscript[∀ , (Subscript[f, 1]), (Subscript[f, 2]) ∈ F])  reduction[ F, S–polynomial[(Subscript[f, 1]), (Subscript[f, 2])]] = 0.

S–polynomial[-2 y+x y,-(x^2)+(y^2)]=y  (-2 y+x y)-x  (-(x^2)+(y^2))

Main intuition: least common multiple of the leading power products play the important role.

Proof: Nontrivial. Combinatorial.

The power of the Gröbner bases method is contained in the invention of the notion of S-polynomial and the theorem,  and the proof of this theorem.

An Algorithm for Constructing Gröbner Bases (BB 1965)

Recall the main theorem:

F is a Gröbner basis   ⟺    (Underscript[∀ , (Subscript[f, 1]), (Subscript[f, 2]) ∈ F])  reduction[ F, S–polynomial[(Subscript[f, 1]), (Subscript[f, 2])]] = 0.

Based on the main theorem, the problem can be solved by the following algorithm:

Start with G:= F. 
For any pair of polynomials (Subscript[f, 1]), (Subscript[f, 2]) ∈ G:

      h := remainder[ G, S–polynomial[(Subscript[f, 1]), (Subscript[f, 2])]] 
      
      If h = 0, consider the next pair.
      
      If h ≠ 0, add h to G and iterate.

Termination of the Algorithm

Termination: by Dickson's Lemma (Dickson 1913, BB 1970).

Example: Pappus Theorem

What does the theorem say geometrically?

Textbook formulation:

Let A, B,  C and A1, B1,  C1 be on two lines and P = A B1 ⋂ A1 B, Q = A C1 ⋂ A1 C, S = B C1 ⋂ B1 C. Then P, Q, and S are collinear.

Input to the system:

Proposition["Pappus",  any[A, B, A1, B1, C, C1, P, Q, S], 
      point[A, B, A1, B1] ∧ pon[C, line[A, B]] ∧ 
          pon[C1, line[A1, B1]] ∧ 
          inter[P, line[A, B1], line[A1, B]] ∧ 
          inter[Q, line[A, C1], line[A1, C]] ∧ 
          inter[S, line[B, C1], line[B1, C]] \[Implies] 
        collinear[P, Q, S]]

Input to the system:

Prove[Proposition["Pappus"], by -> GeometryProver, 
      ProverOptions -> {Method -> "GroebnerProver", 
          Refutation -> True}]

Notebook generated automatically by the proving algorithm based on Groebner basis algorithm:

Predicate Logic Proving: Automated Proofs of Theorems in Analysis (The "PCS" Prover: BB 2001)

Initialize Theorema

Needs["Theorema`"];

Needs["Theorema`Provers`UserProvers`PCS`"]

Needs["Theorema`Provers`UserProvers`VariousPC`"]

SetGlobals[TraceLevel -> 0, DebugLevel -> 0, 
      SearchDepth -> 100, Prover -> PCS, 
      FormatMetas -> "Subscripted"]

SetOptions[Prove, transformBy -> ProofSimplifier, 
        TransformerOptions -> {branches -> Proved}];

$RecursionLimit = 1024;

$TmaSolveLevel = 3;

$NDDebug = False;

Off[General::spell]

Off[General::spell1]

SetGlobals[LabelStyle -> "Numeric", 
        Prover -> NNEqIndProver];
Needs["Theorema`Provers`Cascade`Cascade`"]; 
    Needs["Theorema`Provers`Cascade`ConjectureGenerator`"]

\(Needs["Theorema`Provers`UserProvers`GroebnerBasesProver`"]; $TmaProofPresentation\  = \ 100;\)

Theorema`Provers`PCS`Solver`Private`$TmaSolveLevel=3

SetOptions[Prove, transformBy -> ProofSimplifier, 
        TransformerOptions -> {branches -> 
              Proved}] ;

    $RecursionLimit = 1024;  Off[General::spell]; 
    Off[General::spell1]; $TmaQRTarget = {"kb", "goal"};

Example

Definition[\("limit:", any[f, a], 
	
      limit[f, a]⟺\ \(\(∀ \+ϵ\)\+\(ϵ > 0\)\(∃ \+N\(\(∀ \+n\)\+\(n ≥ N\)\[LeftBracketingBar]f[n] - 
                    a\[RightBracketingBar] < ϵ\)\)\)\)]

Proposition[\("limit of sum", 
      any[f, a, g, 
        b], 
	\((limit[f, a] ∧ 
            limit[g, b])\)\ \ \ \ \  \[Implies] \ \ \ \ \ limit[f + g, 
          a + b]\)]

Definition[\("+:", 
      any[f, g, x], 
	\((f + g)\)[x] = f[x] + g[x]\)]

Lemma[\("|+|", 
      any[x, y, a, 
        b, δ, ϵ], 
	\((\[LeftBracketingBar]\((x + 
                    y)\) - \((a + 
                    b)\)\[RightBracketingBar] < \((δ + ϵ)\))\)\ \ \ \ ⟸\ \ \ \((\[LeftBracketingBar]x - a\[RightBracketingBar] < δ ∧ \[LeftBracketingBar]y - 
                  b\[RightBracketingBar] < ϵ)\)\)]

Lemma[\("max", any[m, M1, M2], 
	
      m ≥ 
          max[M1, M2]\ \ \ \ \  \[Implies] \ \ \ \ \ \((m ≥ 
              M1 ∧ m ≥ M2)\)\)]

Theory["limit",
	({{Definition["limit:"]}, {Definition["+:"]}, {Lemma["|+|"]}, {Lemma["max"]}})]

Prove[Proposition["limit of sum"], 
      using -> Theory["limit"], by -> PCS]

Proof contains interesting algorithmic and didactic information!

Induction Prover

Example: Inductive Proofs about Behavior of Turing Machines (in a Project with J. Hertel 2001)

\(Show–Raster[
      Compute[TM⋱[TM0, 
          ic, 
\(\(\(\(\(\(0\^+\)\^+\)\^+\)\^+\)\^+\)\^+\)*\((\(\(\(\(\(\(0\^+\)\^+\)\^+\)\^+\)\^+\)\^+\)*\(\(\(\(\(\(0\^+\)\^+\)\^+\)\^+\)\^+\)\^+\))\)], 
using -> ⟨Definition["TM0:"], 
            Theory["⊢TM:"]⟩], 1, 33, 
      50]\)

Prove:

under the assumptions:

As there are several methods which can be applied, we have different choices to proceed with the proof.

Alternative proof 1: failed

The proof of (Proposition (TM0 left run))fails.(The Simplifier was unable to transform the proof situation.)

Alternative proof 2: proved

We prove (Proposition (TM0 left run)) by  induction on k.

Induction Base:

As there are several methods which can be applied, we have different choices to proceed with the proof.

Alternative proof 1: proved

We take in (1) all variables arbitrary but fixed and prove:

A proof by simplification of (4) works.

Simplification of the lhs term:

TM↵[TM0,⟨2,⟨□[(OverBar[(Subscript[l, 1])])],1,■[◻[1,(Subscript[n, 1])+0]]⟩⟩,0] =by (Proposition (nu⊢): 1)

TM↵[TM0,⟨2,⟨□[(OverBar[(Subscript[l, 1])])],1,■[◻[1,(Subscript[n, 1])]]⟩⟩,0] =by (Definition (TM↵:): 2)

⟨2,⟨□[(OverBar[(Subscript[l, 1])])],1,■[◻[1,(Subscript[n, 1])]]⟩⟩⌋

Simplification of the rhs term:

⟨2,⟨□[(OverBar[(Subscript[l, 1])]),◻[0, 0]],1,■[◻[1,(Subscript[n, 1])]]⟩⟩ =by (Definition (ta⊢): 5)

⟨2,⟨□[(OverBar[(Subscript[l, 1])])],1,■[◻[1,(Subscript[n, 1])]]⟩⟩⌋

Alternative proof 2: pending

Pending proof of (1).

Induction Step:

Induction Hypothesis:

Induction Conclusion:

As there are several methods which can be applied, we have different choices to proceed with the proof.

Alternative proof 1: proved

We take in (3) all variables arbitrary but fixed and prove:

A proof by simplification of (5) works.

Simplification of the lhs term:

TM↵[TM0,⟨2,⟨□[(OverBar[(Subscript[l, 2])])],1,■[◻[1,(Subscript[n, 2])+(SuperPlus[(Subscript[k, 1])])]]⟩⟩,(SuperPlus[(Subscript[k, 1])])] =by (Proposition (nu⊢): 2)

TM↵[TM0,⟨2,⟨□[(OverBar[(Subscript[l, 2])])],1,■[◻[1,(SuperPlus[(Subscript[n, 2])])+(Subscript[k, 1])]]⟩⟩,(SuperPlus[(Subscript[k, 1])])] =by (Definition (TM↵:): 3)

TM↵[TM0,TM↵[TM0,⟨2,⟨□[(OverBar[(Subscript[l, 2])])],1,■[◻[1,(SuperPlus[(Subscript[n, 2])])+(Subscript[k, 1])]]⟩⟩,(Subscript[k, 1])]] =by (2)

TM↵[TM0,⟨2,⟨□[(OverBar[(Subscript[l, 2])]),◻[0,(Subscript[k, 1])]],1,■[◻[1,(SuperPlus[(Subscript[n, 2])])]]⟩⟩] =by (Definition (TM↵:): 1)

r↵[rc[TM0,⟨2,⟨□[(OverBar[(Subscript[l, 2])]),◻[0,(Subscript[k, 1])]],1,■[◻[1,(SuperPlus[(Subscript[n, 2])])]]⟩⟩],⟨2,⟨□[(OverBar[(Subscript[l, 2])]),◻[0,(Subscript[k, 1])]],1,■[◻[1,(SuperPlus[(Subscript[n, 2])])]]⟩⟩] =by (Definition (TM0:): 4)

r↵[⟨0, R, 2⟩,⟨2,⟨□[(OverBar[(Subscript[l, 2])]),◻[0,(Subscript[k, 1])]],1,■[◻[1,(SuperPlus[(Subscript[n, 2])])]]⟩⟩] =by (Definition (r↵:): 3)

⟨2,⟨□[(OverBar[(Subscript[l, 2])]),◻[0,(Subscript[k, 1])],\(◻[0, \(0\^+\)]\)],1,■[◻[1,(Subscript[n, 2])]]⟩⟩ =by (Definition (ta⊢): 3)

⟨2,⟨□[(OverBar[(Subscript[l, 2])]),◻[0,(Subscript[k, 1])+\(0\^+\)]],1,■[◻[1,(Subscript[n, 2])]]⟩⟩ =by (Proposition (nu⊢): 2)

⟨2,⟨□[(OverBar[(Subscript[l, 2])]),◻[0,(SuperPlus[(Subscript[k, 1])])+0]],1,■[◻[1,(Subscript[n, 2])]]⟩⟩ =by (Proposition (nu⊢): 1)

⟨2,⟨□[(OverBar[(Subscript[l, 2])]),◻[0,(SuperPlus[(Subscript[k, 1])])]],1,■[◻[1,(Subscript[n, 2])]]⟩⟩⌋

Simplification of the rhs term:

⟨2,⟨□[(OverBar[(Subscript[l, 2])]),◻[0,(SuperPlus[(Subscript[k, 1])])]],1,■[◻[1,(Subscript[n, 2])]]⟩⟩⌋

Alternative proof 2: pending

Pending proof of (3).

Automated Synthesis of the Gröbner Bases Algorithm by the "Lazy Thinking Method" (BB 2002 ...)

Starting from a formal (predicate logic) specification of the problem,

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

and a list of possible "algorithm schemes", e.g.

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

by this new algorithm synthesis method, the key idea of the main theorem (the notion of S-polynomial) is automatically generated and verified:

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

df[h1, h2]=h1-h2.

The Algorithm Synthesis Method ("Lazy Thinking") is Based on

the use of "formula schemes" (re-use high-level mathematical knowledge),

automated theorem proving,

learning from failing proofs.

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 produce 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 (and other provers), the proof attempt could be done automatically. (Ongoing PhD thesis of A. Craciun.)

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], 
is–Gröbner–basis[
      G],  
      i . e .  
      is–Church–Rosser[ (Subscript[-> , G])] .

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

Using Available Knowledge

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

The (Automated) Proof Attempt

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

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

Now Use a Specification Generation Algorithm

Specification generation rule (rough sketch; the intelligence is in the details of this rule!):  Collect the temporary assumptions and temporary goals, write a "⟹" in between and generalize from constant terms to variables.   (The details are a little tricky.)

In the case of the proof at hand, 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.

Summarize the (Automatically Generated) Specifications of the Subalgorithm lc

(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

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

wich is a consequence of

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

Summarize Again

For synthesizing an algorithm for the Gröbner bases problem it suffices to find an lc satisfying

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

and

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

This problem can be solved by any high-school student (or university professor)! No knowledge on Gröbner bases theory necessary!

A Suitable lc

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

is a suitable function that satisfies the above requirements.

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

Case h1≠h2

In this case, df[h1,h2]∈G:

In this part of the proof (wich is much easier) we are basically stuck right at the beginning. By the requirement generation algorithm we obtain the following requirement for df:

({{(Underscript[∀ , h1, h2])(h1 (SuperStar[(Subscript[↓, {df[h1, h2]}])])h2), (df requirement).  }})

Looking to the Knowledge Base for a Suitable df

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

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

We illustrated the automated synthesis of a non-trivial algorithm.

Non trivial: ~ 1960 a conjecture was made that (Groebner bases) related problems are algorithmically unsolvable.

An algorithm was found 1965 by human (young BB) mathematical exploration.

A human (old BB) systematic algorithm invention method was able to synthesize, 2005, an algorithm automatically.

Implications for increase in efficiency of the mathematical exploration process (with implications on all sciences).

Possible implications on life sciences:

synthesizing "algorithms" between structure and behavior.

understanding the phenomenon of self-reference in evolution.

...

How Difficult is the Construction of Gröbner Bases?

Very Easy

The structure of the algorithm is easy. The operations needed in the algorithm are elementary. "Every high-school student can execute the algorithm." (See palm-top TI-98.)

Very Difficult

The inherent complexity of the problems that can be solved by the GB method (e.g. graph colorings) is "exponential". Hence, the worst-case complexity of the GB algorithm must be high.

Sometimes Easy

Mathematically interesting examples often have a lot of "structure" and, in concrete examples, GB computations can be reasonably, even surprisingly, fast.

Enormous Potential for Improvement

More mathematical theorems can lead to drastic speed-up:

The use of "criteria" for eliminating the consideration of certain S-polynomials.

p-adic approaches and floating point approaches.

The "Gröbner Walk" approach.

The "linear algebra" approach. (Generalized Sylvester matrices.)

The "numerics" approach.

Tuning of the algorithm:

Heuristics, strategies for choosing orderings, selecting S-polynomials etc.

Good implementation techniques.

A huge literature.

Why "Gröbner" Bases?

Professor  Wolfgang Gröbner (1899-1980) was my PhD thesis supervisor.

He gave me the problem of finding "the uncovered points if the black points are given".

In my thesis (1965) and journal publication  (1970) I introduced:

* the concept of Gröbner bases and reduced Gröbner bases
* the S-polynomials
* the main theorem with proof
* the algorithm with termination and correctness proof
* the uniqueness of Gröbner bases
* first applications (computing in residue rings, Hilbert function, algebraic systems)
* the technique of base-change w.r.t. to different orderings
* a complete computer implementation 
* first complexity considerations.

However, in the thesis, I did not use the name "Gröbner bases". I introduced this name only in 1976, for honoring Gröbner, when people started to become interested in my work.

My later contributions:

* the technique of criteria for eliminating unnecessary reductions
* an abstract characterization of "Gröbner bases rings".

Gröbner Bases on Your Desk and in Your Palm

GB implementations are contained in all the current math software systems like Mathematica (see demo), Maple, Magma, Macsyma, Axiom, Derive, Reduce, Mupad, ...

Software systems specialized on Gröbner bases: RISA-ASIR (M. Noro, K. Yokoyama), CoCoA, Macaulay, Singular, ...

Gröbner bases are now availabe on the TI-98 (implemented in Derive).

Textbooks on Gröbner Bases

T. Kreuzer, L. Robbiano: Algorithmic Commutative Algebra I. Springer, Heidelber, 2000: Contains a list of all other, approx. 10, textbooks on GB.

W.W.Adams, P. Loustenau. Introduction to Gröbner Bases. Graduate Studies in Mathematics: Amer. Math. Soc., Providence, R.I., 1994.

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

D.Cox, J.Little, D.O'Shea. Ideals, Varieties, and Algorithms: An Introduction to Computational Algebraic Geometry and Commutative Algebra. Springer, New York, 1992.

....

M. Maruyama. Gröbner Bases and Applications. 2002.

M. Noro, K. Yokoyama. Computational Fundamentals of Gröbner Bases. University of Tokyo Press, 2003.

Gröbner Bases on the Web

Search. E.g. in the Research Index you obtain ~ 3000 citations.

Original Publications on Gröbner Bases

Approximately 600 papers appeared meanwhile on Gröbner bases.

J of Symbolic Computation, in particular, special issues.

ISSAC Conferences.

Mega Conferences.

ACA Conferences.

...

The essential  additional original ideas in the literature:

Gröbner bases can be constructed w.r.t. arbitrary "admissible" orderings (W. Trinks 1978)

Gröbner bases w.r.t. to "lexical" orderings have the elimination property (W. Trinks 1978)

Gröbner bases can be used for computing syzygies and the S-polys generate the module of syzygies (G. Zacharias 1978)

A given F, w.r.t. the infinitely many admissible orderings, has only finitely many Gröbner bases and, hence, we can construct a "universal" Gröbner bases for F (L. Robbiano, V. Weispfenning, T. Schwarz 1988)

Starting from a Gröbner bases for F for ordering (Subscript[O, 1]) one can "walk", by changing the basis only slightly, to a basis for a "nearby" ordering (Subscript[O, 2])  and so on ... until one arrives at a Gröbner bases for a desired ordering (Subscript[O, k]) (Kalkbrener, Mall 1995, Nam 2000).

Use arbitrary linear algebra algorithms for the reduction (remaindering) process: (Faugère 1997).

... numerours applications,

Research Topics

the inner structure of Groebner bases: generalized Sylvester matrices

the numerics of GB computations

axiomatic characterization of Groebner rings

generalizations (e.g. non-commutative poly-rings)

speeding up the computation

Groebner bases for particular classes of ideals (avoid computation)

the study of admissible orderings

applications (problem reductions, e.g. functional analysis, BV problems, Rosenkranz 2003)

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.

A.Asperti, G.Bancerek, A.Trybulec (eds.).
Proceedings of the Third International Conference on Mathematical Knowledge Management, MKM 2004,
Bialowieza, Poland, September 19-21, 2004,  Lecture Notes in Computer Science, Vol. 3119, Springer, Berlin-Heidelberg-NewYork, 2004

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, 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), Vol. 98/1, to appear, 10 pages.