Symbolic Computation:
Self-application of Algorithmic Mathematics

Bruno Buchberger
RISC (Research Institute for Symbolic Computation)
Johannes Kepler University, Linz, Austria

Invited Talk at MAP 2006 (Mathematics, Algorithms, Proofs) 
Castro-Urdiales, Spain

Copyright Bruno Buchberger 2006.
Copyright Note: This file may be copied and distributed under the following conditions
- the file is kept unchanged including this copyright note,
- a message is sent to bruno.buchberger@jku.at
- if material of this talk is used in publications, the talk should be cited appropriately.

The Simple Message

We are entering a new era of mathematics:

"doing" mathematics by applying algorithmic mathematics on the meta-level

Self-application of (Algorithmic) Mathematics

Can / will / should revolutionize the way we do mathematics in 21st century

Mathematics:

globally accessible formal (logic / computer based) knowledge bases

expanded and verified by algorithmic (verified) reasoners

self-expansion and expansion under guidance

multiple "views"

Kind of "(anti-) bourbakism" of the 21st century.

Not a Bourbakism of content but a Bourbakism of methodology.

Not a Bourbakism that excludes "the computer" (i.e. algorithms) but a Bourbakism that puts the computer into the center of mathematics (both on the object level and the meta level).

Not a Bourbakism that builds up one view of mathematics  but gives us the tools for easily generating many views of mathematics.

The Time in History for Achieving this Aspiration

The ingredients are here

new algorithms based on new and deep mathematical results (cad, PZ...theory, ...)

deep understanding of logic

marvelous software technology

drastic improvement in hardware

the web

the mathematics and logic software systems (Mathematica, ...,  Coq, ...)

Main Obstacle

Our systems are not yet good (practical, comprehensive, uniform ...) enough for making them attractive for "working mathematicians".

Editorial of the J of Symbolic Computation, B. B. 1985

Symbolic Computation  =   "Computer Algebra"  +  "Computer Logic"

                                              "object" level               "meta" level

"object", "meta":  relative notions!

Since then,

some progress has been made in the unification of the CA and CL communities.

However, not sufficiently much. In particular, not on the (logic and software) systems level!

Even some reverse tendencies.

Some positive signals: Calculemus Network,  MKM Network,  MAP.

Future Symbolic Systems

Include general and special, interactive and fully automated, reasoners.

Include hierarchically structured formal mathematical knowledge libraries. *)

Have one language for mathematical knowledge and algorithms.

Have the algorithms formally specified and verified.

Have the algorithmic reasoners formally specified and verified.

Include tools for managing large mathematical knowledge (and algorithm) libraries. (Store knowledge, retrieve knowledge, re-use knowledge, decide about originality of knowledge, re-organize knowledge, design "views" about mathematical areas, ...)

*) See the NIST project on Special Functions. However, mathematical knowledge is more than identities (inequalities, ...).

The Theorema Project

The Theorema project aims at prototyping such a system. There are a couple of other groups with the same aim (e.g. MIZAR, ...), see Calculemus and MKM network.

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

Some Reasoners in Theorema:

- Predicate logic: natural deduction, S-decomposition
- Elementary analysis: PCS (alternating quantifiers)
- Set theory
- Induction on natural numbers, on tuples
- Equality, sequence variables
- Combinatorial identities
- Geometry (based on algebraic methods like Gröbner bases)
- Algorithms for symbolic functional analysis (boundary value problems)
- "Lazy Thinking" method for lemma and algorithm invention
- Tools for structuring knowledge bases: functors, schemes, and others

The Point:

(Predicate) logic as both a logic language and a programming language.

Proving (algorithms) and computing (with these algorithms) in the same system.

Computing as a special case of proving.

Proving

Definition["addition",any[m, n],
	({{m + 0 = m, " +0:"}, {\(m + \(n\^+\) = \(\((m + n)\)\^+\)\), " + .:"}})]

Proposition["left zero",any[m, n],
	({{0 + n = n, "0+"}})]

Prove[Proposition["left zero"],
	\(using -> ⟨Definition["addition"]⟩\),
	by -> NNEqIndProver,

	ProverOptions -> {TermOrder -> LeftToRight},transformBy -> ProofSimplifier,TransformerOptions -> {branches -> {Proved}}];

Computing in the Same System

\(Compute[\(\(0\^+\)\^+\) + \(\(\(0\^+\)\^+\)\^+\), 
      using -> ⟨Definition["addition"]⟩]\)

Another Example

Similarly, using our set theory prover, we could prove that

any[is–set[A]]∶
	({{𝔓[A] = {{}} ⇐ (A = {})}, {\(𝔓[A] = 
              where[a = an–element[A], 
                P = 𝔓[A⊖{a}], \ 
	
                P ⋃ {\(({a} ⋃ 
                          B)\)\( | \+\(B ∈ P\)\)}]\)}})

Then we could use this knowledge and compute:

𝔓[{}]

𝔓[{3}]

𝔓[{1, 3}]

𝔓[{1, 3, 4, 8}]

The Point

Practical reasoning systems should have special reasoners for special theories.

Special reasoners often reduce proving in the special theory to "solving" in some algebraic domains.

In other words, reduction (by some simple logic steps) of algorithmic reasoning to (sophisticated) algorithmic algebra.

The PCS Method for Analysis Proving (BB 2001)

This method reduces proving in elementary analysis (formulae with "alternating quantifiers" on functions) systematically to the solution of inequalities over the real numbers.

Produces "natural" proofs that also contain algorithmic information.

A Proof Generated by PCS

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]

The following proof is generated fully automatically by the PCS prover:

The Point

(Some part of) invention in mathematics may be mimicked by the application (instantiation) of "schemes".

In other words,  schemes are an abstract formulation of accumulated "mathematical experience".

Schemes can be used for inventing definitions, propositions, problems, and methods (algorithms).

Trivial example

A "typical" formula:

(Underscript[∀ , a, b, f, g])(P[f, a] ∧ 
            P[g, b])      \[Implies]      P[F[f, g], 
        G[a, b]]

Can be used as a "scheme":

(Underscript[∀ , P, F, G])  (Monotony[P, F, G]⟺
(Underscript[∀ , a, b, f, g])(P[f, a]∧P[g, b])     \[Implies]     P[F[f, g],G[a, b]])

Given a knowledge base in which 'Limit', '+', and '+' occurs, we can apply the above scheme for "inventing" (proposing, conjecturing) a proposition:

Monotony[Limit, +,+]

i.e.

(Underscript[∀ , a, b, f, g])(Limit[f, a] ∧ 
            Limit[g, b])      \[Implies]      Limit[f + g, 
        a + b]

'Monotony' is a "relator" or (the description of) a "category".

Another Example

A formula (in the special theory of tuples):

(Underscript[∀ , x])(N[x]={({{S[x], ⇐, is–trivial–tuple[x]}, {M[sorted[L[x]],sorted[R[x]]], ⇐, otherwise}})})

A scheme:

(Underscript[∀ , N, S, M, L, R])Divide–and–Conquer[N,S,M,L,R]⇔
(Underscript[∀ , x])(N[x]={({{S[x], ⇐, is–trivial–tuple[
                        x]}, {M[sorted[L[x]],sorted[R[x]]], ⇐, otherwise}})})

Given a knowledge base in which 'identity', 'merge', 'left' and 'right' occurs, we can apply the above scheme for "inventing" (proposing, conjecturing) a sorting algorithm. It could also be applied, in a different context, for defining a new notion N in terms of known notions S, M, L, R.

'Divide–and–Conquer' is a "relator" with some functional flavor. It is a "functor".  (In Theorema, a special notation is available for functors.)

This functor captures an essential mathematical idea for invention notions and solutions to problems.

Another Example

A formula:

({{(Underscript[∀ , F])A[F] =A[F, pairs[F]]}, {(Underscript[∀ , F])A[F, ⟨⟩]=F
}, {\(∀ \+\(F, g1, g2, \(p\&-\)\)\)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}})} ]}})

A scheme (a "functor"):

(Underscript[∀ , A, lc, df])pair–completion[A,lc,df] ⟺
   ({{(Underscript[∀ , F])A[F] =A[F, pairs[F]]}, {(Underscript[∀ , F])A[F, ⟨⟩]=F
}, {\(∀ \+\(F, g1, g2, \(p\&-\)\)\)A[\(F, ⟨⟨g1, 
                              g2⟩, 
                            p\&_⟩\)]=  ....lc ...df ...
          } }})

Functor Notation in Theorema

Definition["Groebner extension" ,any[R],
Groebner–extension[R]   =Functor[N,\(any[C, k, p, p\&_, q, q\&_, x, X, y, y\&_, Y]\),
	({{(Underscript[rd, N])[x, y]  =x(Underscript[-, R])(Underscript[rdm, R])[x, 
                              y](Underscript[*, R])y
}, {(Underscript[( trd), N])[x, Y] =(Underscript[trd, N])[x, Y, 
                        1] }, {(Underscript[trd, N])[x, Y, k]   =
{({{x, ⇐, k > \[LeftBracketingBar]Y\[RightBracketingBar]}, {where[x1 = (Underscript[rd, N])[x, (Subscript[Y, k])],
{({{(Underscript[trd, N])[x1, Y, 1], ⇐, \(x\( > \+R\)x1\)}, {(Underscript[trd, N])[x, Y, k + 1], ⇐, otherwise}})} ], ⇐, otherwise}})}
}, {\(\(cpd\+N[x, y]\  (*\ 
                        the\ critical\ pair\ difference\ of\ x\ and\ y\ *)  = 
where[lxy = lcrd\+R[x, y], 
                        rd\+N[lxy, x]\( - \+R\)rd\+N[lxy, 
                            y]]\)\(\ \)\(
\)
                    \)}, {(Underscript[Gb, N])[X]  = (Underscript[Gb, N])[X, pairs[X]]}, {(Underscript[Gb, N])[X, ⟨⟩] = 
                      X}, {\(Gb\+N[
                          X, ⟨⟨x, 
                              y⟩, 
                            p\&_⟩]\)=
where[h = (Underscript[trd, N])[(Underscript[cpd, N])[x, y], X],
{({{\(Gb\+N[
                                      X, ⟨p\&_⟩]\), ⇐, h = (Underscript[0, N])}, {\(Gb\+N[
                                      X⌢
                                        h, ⟨p\&_⟩ ≍ ⟨\(⟨X\_k, 
                                        h⟩\)\( \[VerticalSeparator] \+\(k = 
                                        1, …, \[LeftBracketingBar]X\[RightBracketingBar]\)\)⟩]\), ⇐, otherwise}})} ]
}, {(Underscript[rdGb, N])[X]     = (Underscript[ard, N])[(Underscript[Gb, N])[X]]}, {(Underscript[ard, N])[⟨⟩] = ⟨⟩}, {\(ard\+N[⟨p, q\&_⟩] = 
                      ard\+N[⟨⟩, 
                        p, ⟨q\&_⟩]\)}, {(Underscript[ard, N])[X, 
                        p, ⟨⟩]=where[h = (Underscript[trd, N])[p, X],
{({{X, ⇐, h = (Underscript[0, N])}, {X⌢p, ⇐, otherwise}})} ]}, {\(ard\+N[X, 
                        p, ⟨q, q\&_⟩]\)=where[\(h = 
                            trd\+N[p, 
                              X ≍ ⟨q, 
                                  q\&_⟩]\),
{({{\(ard\+N[X, 
                                    q, ⟨q\&_⟩]\), ⇐, h = (Underscript[0, N])}, {\(ard\+N[X⌢p, 
                                    q, ⟨q\&_⟩]\), ⇐, otherwise}})} ]}, {(Underscript[( tcrd), N])[x, Y]  (* 
                        the total cofactor reduction of x modulo tuple Y *)  = (Underscript[tcrd, N])[x, Y, 
                        1, ⟨(Underscript[0, N]) (Underscript[\[VerticalSeparator] , k = 1, …, \[LeftBracketingBar]Y\[RightBracketingBar]])⟩]}, {(Underscript[tcrd, N])[x, Y, k, C]     =
{({{⟨x, C⟩, ⇐, k > \[LeftBracketingBar]Y\[RightBracketingBar]}, {where[c = (Underscript[rdm, N])[x, (Subscript[Y, k])],\(x1 = x\( - \+N\)c\(*\+N\)Y\_k\),
{({{\(tcrd\+N[x1, Y, 1, 
                                        C\_\(k ⇤ C\_k\( + \+N\)c\)]\), ⇐, \(x\( > \+N\)x1\)}, {(Underscript[tcrd, N])[x, Y, k + 1, C], ⇐, otherwise}})} ], ⇐, otherwise}})}}})
	]]

Another Example

The scheme

(Underscript[∀ , F, C, D])conservation–theorem[F, C, 
          D]⟺
(Underscript[∀ , f])(C[
                f] \[Implies] D[F[f]])

captures the ubiquitous idea of a "conservation" theorem: If the domain f is in the category C then F[f] (the domain that results by applying functor F to f) is in category D.

Summarizing

Given a knowledge base on certain functions and predicates (of any order), one may apply (instantiate) schemes for generating ("inventing") lots of proposals for (interesting) definitions, propositions, problems, and methods (algorithms) for solving problems.

This may semi-automate the "easy" part of exploring a theory in a systematic way and may take away tedious formula typing.

Then we call semi-automated provers for disproving / disproving part of the proposed knowledge. This may take away another part of tedious exploration.

Whatever is left, is (called) "non-trivial".  (This is a relative notion of "triviality" !)

This approach is a "bottom-up" approach. Now let's put in some salt by a "top-down" idea: learning from failing proofs and thereby invent something.

We illustrate the idea in the case of algorithm invention ("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]].

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

Algorithm Synthesis by "Lazy Thinking" (BB 2002)

"Lazy Thinking" Method for Algorithm Synthesis = 
      My Advice to "Humans" (or "Computers") How to Invent Algorithms.

Given: A problem P.           Find: An algorithm A for P.

Learn how to prove.

Completely understand the problem P.  ("Specification" of the problem.)

Collect (discover, prove) "complete" knowledge on the auxiliary notion appearing in the problem P.

Consider known fundamental ideas of how to structure algorithms in terms of subalgorithms ("algorithm schemes A"). 
Try one scheme A after the other.

For the chosen scheme A, try to prove   (Underscript[∀ , x]) P[ x, A[x]]: From the failing proof construct specifications for the subalgorithms B occurring in A.

Literature

There is a rich literature on algorithm synthesis methods, see survey

[Basin et al. 2004] D. Basin, Y. Deville, P. Flener, A. Hamfelt, J. F. Nilsson.  Synthesis of Programs in Computational Logic. In: M. Bruynooghe, K. K. Lau (eds.), Program Development in Computational Logic, Lecture Notes in Computer Science, Vol. 3049, Springer, 2004, pp. 30-65.

My method is in the class of "scheme-based" methods. Closest (but essentially different):

[Lau et al. 1999] K. K. Lau, M. Ornaghi, S. Tärnlund. Steadfast logic programs. Journal of Logic Programming, 38/3, 1999, pp. 259-294.

And the work of A. Bundy and his group (U of Edinburgh) on the automated invention of induction schemes.

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

Problem: Synthesize "sorted" such that

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

("Correctness Theorem")

Knowledge on Problem:

(Underscript[∀ , x, y])(is–sorted–version[x, y]⇔({{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: Divide and Conquer

(Underscript[∀ , x])(sorted[x]={({{S[x], ⇐, is–trivial–tuple[x]}, {M[sorted[L[x]],sorted[R[x]]], ⇐, otherwise}})})

S, M, L, R  are unknowns.

We now start an (automated) induction prover for proving the correctness theorem and analyze the failing proof: see notebooks with failing proofs.

Automated Invention of Sufficient Specifications for the Subalgorithms

A simple (but amazingly powerful) rule    ( m  ... an unknown subalgorithm ):

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

The Result of Applying Lazy Thinking in the Sorting Example

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])(is–trivial–tuple[x]\[Implies]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: the specifications generated are not only sufficient but natural !

What Do We Have Now?

Case A: We find algorithms S0, M0, L0, R0 in our knowledge base for which the properties specified above for S, M, L, R are already contained in the knowledge base or can be derived (proved) from the knowledge base.
In this case, we are done, i.e. we have synthesized a sorting algorithm.

Case B: We do not find such algorithms S0, M0, L0, R0   in our knowledge base.
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.)

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

Example: Synthesis of Insertion-Sort

Synthesize A such that

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

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

How Far Can We Go With the Method ?

Can we automatically synthesize algorithms for non-trivial problems?  What is "non-trivial"?

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

"Non-trivial": The invention of the notion of S-polynomial and the characterization of Gröbner-bases by finitely many S-polynomial checks.

With the "Lazy Thinking" method, it is possible to invent the essential idea of the B.B.'s Gröbner bases algorithm fully automatically: See [BB 2005].

The Problem of Constructing Gröbner Bases

Find algorithm Gb such that

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

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

(Subscript[-> , G])  ...  a division step.

Confluence of Division  (Subscript[-> , 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]].}}))

using the above scheme for A  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 can be done automatically. (Ongoing PhD thesis by 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\)).

Newman's lemma (1942):

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

Definition of "f1 and f2 have a common successor":

\(f1\(↓\^*\)f2\) ⇔ (Underscript[∃ , g])({({{\(f1\( -> \^*\)g\)}, {\(f2\( -> \^*\)g\)}})} )}

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 the Specification Generation Algorithm

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.

Summarize the (Automatically Generated) Specifications of the Subalgorithm lc

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](lc[g1, g2] | p)) ,

and the requirements:

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

Now this problem can be attacked independently of any Gröbner bases theory, ideal theory etc.

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 we are basically stuck right at the beginning.

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

I think we should put all our current achievements in "symbolic computatoin" (computer algebra, automated reasoning, etc.) together for coming up with coherent systems that allow to build up 

     - verified
     - well-structured, restructurable, extensible
     - globally accessible
     - mathematical knowledge (definitions, propositions, problems, methods) bases.

Algorithms on the object level must be "shiftable" to the meta-level for becoming (part of) reasoning methods on the meta-level. (Reflexion is an essential ingredient of intelligent mathematical theory exploration.)

This will have a drastic effect on

how we will be able to do research in mathematics

how we will be able to store, publish, evaluate, organize, access mathematical knowledge

how we will be able to teach mathematics.

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 2005]
B. Buchberger. 
Towards the Automated Synthesis of a Gröbner Bases Algorithm.
RACSAM (Review of the Royal Spanish Academy of Science), Vol. 98/1, 2005, pp.  65-75.