Die Zukunft 
der algorithmischen Mathematik:  
Kann mathematische Forschung automatisiert werden?

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

Vortrag am 21. November 2006 in Graz
Abendveranstaltung von OCG und OVE

Copyright Note:  Copyright Bruno Buchberger 2006.
This file may be copied and stored under the following conditions:
-  The file is kept unchanged including this copyright note.
-  A mail is sent to bruno.buchberger@jku.at
-  If material from this file is used, the talk should be appropriately cited.

Durchgehendes Beispiel:  Die Theorie der Gröbner-Basen

Ein Problem aus der "realen" Welt:

Was ist mehr wert?                       (Wenn 1 Kamel so viel wert ist wie 7 Schafe.)

Lösung ohne Mathematik ?

Lösung mit Mathematik

\(TraditionalForm\`\(\(\ \ \ \ \)\(Mathematik\ ist\ charakterisiert\ durch\ die\ Methode, \ das\ \(\("Schließen"\)\(.\)\)\)\)\)

In unserem Beispiel:

Das Addieren, Multiplizieren, Vergleichen von Zahlen (in Dezimaldarstellung) wird so genau verstanden, dass jeder "Computer" das machen kann:

257   *  348   =
                   771
                   1028
                      2056
                  -----------
                    89436

257 * 348

Ein Teil des Lebens wird damit "automatisiert":

Problemlösen auf "Knopfdruck", keine "Einsicht" nötig, ...

Mathematik ist im Zentrum der Automatisierung.

Automatisierung des "Schließens" ("Rechnens", Arbeitens in Modellen, ...).

Prinzip der Mathematik: Einmal gründlich  (an den Grund gehend) denken, und (unendlich) oft nicht mehr denken müssen.

Beispiel: Einmal beweisen, dass Multiplizieren und Addieren "distributiv" sind und dann nur mehr mit dem "kleinen 1 x 1" rechnen müssen.

für  alle x, y, z:     ( x + y ) * z  =  x * z  +  y * z

257  *   348  =    (2 H + 5 Z + 7 E) * (3 H + 4 Z + 8 E) =  ( 6 H*H + ....   +  56 E)

"Das Wunder" der Mathematik: Beweise über unendlich viele Situationen sind in endlich vielen Denkschritten möglich!

Durchgehendes Beispiel:  Die Theorie der Gröbner-Basen

Mathematisches Wissen und mathematische Methoden

In der Mathematik erfindet und beweist man Wissen und Methoden.

Wissen und Methoden sind nur zwei Seiten derselben Medaille.

Nur eine Seite auszuleben, ist eine gewaltige Verarmung der Mathematik.

Die letzten 40 Jahre Mathematik haben eine Explosion der  mathematischen "Algorithmik" (Methoden) gebracht.

Die Motivation dafür kam aus "dem Computer"  (eine mathematische Erfindung!)

Die neue mathematische Algorithmik ist auf neuem mathematischen Wissen gegründet.

Beispiele: Computer-Analysis, Computer-Algebra, Kryptographie, ...,  automatisches Beweisen.

Beispiel: Groebner-Basen (BB 1965, ...)

Warum sind Gröbner-Basen wichtig?

Was  sind Gröbner-Basen?

Wie kann man Gröbner-Basen berechnen?

Warum Groebner-Basen?

Dutzende fundamentaler Probleme der Mathematik können auf das Problem der Konstruktion von Gröbner-Basen zurückgeführt werden. Es werden ständig mehr.

Dementsprechend: 10 Lehrbücher, 1000 Publikationen, 3000 Citations, millionenfach installiert, eigenes Stichwort in der AMS-Klassifikation der Mathematik

Siehe Special Semester on Gröbner Bases: www.risc.uni-linz.ac.at

Übersicht: B. B., F. Winkler. Gröbner Bases: Theory and Applications. Cambridge University Press, 1998. 560 pages.

Was sind Groebner-Basen?

Eine Art "kanonische Form" von nicht-linearen ("polynomialen")  (Gleichungs-) systemen.

Linearkombinationen von Polynomen

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

Führende Potenzprodukte:

Linearkombinationen von (Subscript[f, 1]) von (Subscript[f, 2]), z.B.

g = (y) (Subscript[f, 1]) +  (-x + 2) (Subscript[f, 2])

Beobachtung:  führendes Potenzprodukt  (x^3)   von g ist
     weder ein Vielfaches von   x y     of (Subscript[f, 1])
     noch ein Vielfaches von     (y^2)    of (Subscript[f, 2]).

Definition

Polynommenge F heißt Groebner-Basis, wenn das obige Phänomen nicht passieren kann, d.h. wenn

für alle (Subscript[f, 1]),...,(Subscript[f, m])∈ F und alle (unendlich vielen) Polynome (Subscript[h, 1]),...,(Subscript[h, m]),
          führendes Potenzprodukt von  (Subscript[h, 1]) (Subscript[f, 1]) +  ...   +  
        (Subscript[h, m]) (Subscript[f, m]) 
          ist Vielfaches des führenden Potenzprodukts von mindestens einem der Polynome in F.

Gegenbeispiel und Beispiel einer Gröbner-Basis

Gegenbeispiel: Die Menge    {-2 y+x y,-(x^2)+(y^2)} von oben ist keine Gröbner-Basis. Warum?

Beispiel:       Die Menge   {-2 (x^2) + (x^3),-2 y+x y,-(x^2)+(y^2)} ist eine Gröbner-Basis. Warum?

Der Hauptsatz der Theorie der Gröbner-Basen (BB 1965):

F ist eine Gröbner-Basis  ⟺   (Underscript[∀ , (Subscript[f, 1]), (Subscript[f, 2]) ∈ F])  rest[ F, S–Polynom[(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))

Beweis: nichttrivial, kombinatorisch.

Das Theorem reduziert einen unendlichen Test auf einen endlichen Test, nämlich ...

Die Kraft der Gröbner-Basen Theorie beruht auf diesem Satz (in der Erfindung des Begriffs des S-Polynoms) und seinem Beweis.

Das Problem der Konstruktion  von Gröbner-Basen

Gegeben F,  finde G,   sodass G eine (endliche) Gröbner-Basis ist
                                            und F und G dieselbe Menge von Linearkombinationen erzeugen.

Ein Algorithmus zur  Konstruktion  von Gröbner-Basen (BB 1965)

Nochmals der Hauptsatz:

F ist eine Gröbner-Basis  ⟺   (Underscript[∀ , (Subscript[f, 1]), (Subscript[f, 2]) ∈ F])  rest[ F, S–Polynom[(Subscript[f, 1]), (Subscript[f, 2])]] = 0.

Darauf basiert der folgende Algorithmus zur Konstruktion von Gröbner-Basen:

G:= F. 
für alle Paare (Subscript[f, 1]), (Subscript[f, 2]) ∈ G:

      h := rest[ G, S–Polynom[(Subscript[f, 1]), (Subscript[f, 2])]] 
      
      Wenn h = 0, betrachte das nächste Paar.
      
      Wenn h ≠ 0, für h zu G hinzu und iteriere.

Termination des Algorithmus

Mit Dickson's Lemma (Dickson 1913, BB 1970).

Beispiel einer Anwendung: Beliebige nichtlineare Gleichungssysteme

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

{time, G} = GroebnerBasis[F]  //  Timing

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

Beispiel einer Anwendung: Invariantentheorie

Frage:  Kann

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

polynomial durch die Polynome in folgender Menge ausgedrückt werden:

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

?

(Diese Polynomie sind die "Fundamentalinvarianten der Gruppe" (Subscript[ℤ, 4])).

Reduktion auf die Berechnung von Gröbner-Basen

{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]

Theorem (Sweedler, Sturmfels et al. 1988): h kann durch ausgedrückt werden F iff der Rest bzgl. der "Groebner-Basis von F mit Hilfsvariablen" ein Polynom in den Hilfsvariablen ist (das die Darstellung liefert).

(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[x, 1])^6) (Subscript[x, 2]) - (Subscript[x, 1]) ((Subscript[x, 2])^6) can not be expressed by the fundamental invariants in I.

Beispiel einer Anwendung: Färben von Graphen

Problem:

Find alle zulässigen Färbungen in k Farben eines Graphen mit n Knoten und Kanten E.

Beispiel: 3 Farben,  4 Knoten und  Kanten {1,2}, {1,3}, {2,3}, {3,4}:

Zulässig:

Nicht zulässig:

Reduktion auf die Konstruktion von Gröbner-Basen

Theorem (D. Bayer, 1980): Die zulässigen Färbungen entsprechen 1-1 den Lösungen des folgenden Gleichungssystems:

{ -1 + 
        ((Subscript[x, 1])^3),      ...  at vertex 1 color is a 3 - 
        ary root of 1
 - 1 + 
        ((Subscript[x, 2])^3),    ...  at vertex 2 color is a 3 - 
        ary root of 1
 - 1 + 
        ((Subscript[x, 3])^3), 
-1 + 
        ((Subscript[x, 4])^3), 
((Subscript[x, 1])^2) + (Subscript[x, 1]) (Subscript[x, 2]) + 
        ((Subscript[x, 2])^2),   ... the colors at 1 and 2 must be different, 
((Subscript[x, 1])^2) + (Subscript[x, 1]) (Subscript[x, 3]) + 
        ((Subscript[x, 3])^2), 
((Subscript[x, 2])^2) + (Subscript[x, 2]) (Subscript[x, 3]) + 
        ((Subscript[x, 3])^2), 
((Subscript[x, 3])^2) + (Subscript[x, 3]) (Subscript[x, 4]) + 
        ((Subscript[x, 4])^2)}

Lösung durch Gröbner-Basen

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

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

Leicht umgeordnet:

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

Zum Beispeil, {(Subscript[x, 1]) -> 1, (Subscript[x, 2]) -> -(((-1))^(1/3)), 
        (Subscript[x, 3]) -> -1 + (((-1))^(1/3)), 
        (Subscript[x, 4]) -> -(((-1))^(1/3))}entspricht

Beispiel einer Anwendung: Ganzzahlige Optimierung

Beispiel (B. Sturmfels):

Was ist die minimale Anzahl von Münzen (z.B. p Pennies, n Nickels, d Dimes, q Quarters), um einen bestimmten Wert, z.B. 117, darzustellen:

Reduktion auf die Konstruktion von Gröbner-Basen (C. Traverso et al. 1986):

Kodiere die Werte p, n, d, q als Exponenten von Potenzprodukten!

Kodiere die Zielfunktion als den verallgemeinerten Grad der Potenzprodukte!

Kodiere die Wechsel-Reglen  zwischen den Münzen als Polynome:

F = {(P^5) - N, (P^10) - D, (P^25) - Q}

Berechne nun die Gröbner-Basis  von F (bzgl. einer Grad-Ordnung):

G = 
      GroebnerBasis[F, MonomialOrder -> DegreeLexicographic]

Nun kann man sicher sein, dass jede zulässige Lösung (z.B. (p=17, n=10, d=5, q=0),  durch Restbildung bzgl. G, zu einer minimnalen Lösung führt.

PolynomialReduce[(P^17) (N^10) (D^5), G, , 
      MonomialOrder -> DegreeLexicographic]

Antwort: nimm 4 quarters, 1 dime, 1 nickel, 2 pennies.

Durchgehendes Beispiel:  Die Theorie der Gröbner-Basen

Beispiel: Automatisches Beweisen (Widerlegen) in der  Geometrie (BB, Stifter, Kutzler, Kapur, ... 1984, ...)

Reduktion auf das Problem der Konstruktion von Gröbner-Basen:
                Geo Theorem        ⟶  ( durch Koordinatisierung )
               (Underscript[∀ , x, y,   ... ])( poly1(x,y,...)=0 ∧ ... => poly(x,y,...)=0 )   ⟶
               
               ¬ (Underscript[∃ , x, y,   ... ]) (  poly1(x,y,...)=0 ∧ ... ∧ poly(x,y,...)≠0 )  ⟶
               
               ¬(Underscript[∃, x,y, ...,a])(  poly1(x,y,...)=0 ∧ ... ∧  a . poly(x,y,...) - 1 = 0 )

Die letzte Frage kann durch den Gröbner-Basen-Algorithmus entschieden werden!

Beispiel: Pappus-Theorem

Geometrischer Inhalt:

Formulierung im Lehrbuch:

Seien A, B,  C und A1, B1,  C1  auf zwei Geraden und P = A B1 ⋂ A1 B, Q = A C1 ⋂ A1 C, S = B C1 ⋂ B1 C. Dann sind P, Q, und S  kollinear.

Input in den GB-Beweiser:

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

Aufruf:

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

Folgender Beweis wird nun automatisch erzeugt:

Was haben wir gemacht?

Die Algorithmik aus einem Bereich der Mathematik (z.B.Theorie der Gröbner-Basen für Polynome) 

kann auf der "Meta-Ebene" eines anderen Bereichs der Mathematik (z.B. Koordinatengeometrie) 

zur Automatisierung des Beweisens führen.

Durchgehendes Beispiel:  Die Theorie der Gröbner-Basen

Beispiel: Automatisches Erfinden und Beweisen der Theorie der Gröbner-Basen (BB 2005, ...)

Begriff des S-Polynoms
Hauptsatz
Algorithmus zur Konstruktion der Gröbner-Basen

Was ich mit diesem Beispiel zeigen möchte:

Eine  Kombination von 
      -  (automatischem)   Beweisen
      -  (automatischer) Anwendung  von Formel-Schemata zum Erfinden
      -  und (automatischer) Analyse von misslungenen Beweisen

ergibt eine erstaunliche leistungsfähige Methode zur (automatischen) Erfindung von Algorithmen ("lazy thinking method",  BB 2002).

Leistungsfähig: kann auch für nicht-triviale Probleme Algorithmen erfinden.

(Insbesondere leistungsfähig genug, um meine eigene Problemlösekraft zu ersetzen.)

"Non-trivial"

Konstruktion von Gröbner-Basen:
               - zur Zeit der Erfindung (1965, BB) wurde das Problem als "algorithmisch unlösbar" eingestuft
               - zahlreiche nicht-triviale Anwendungen
               - noch nicht durch andere Synthesemethoden synthetisiert.

Das Problem der Algorithmen-Synthese (-Erfindung)

Gegeben eine Problemspezifikation P (eine prädikatenlogische Formel), finde einen Algorithmus A, sodass

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

Ein allgemeiner Algorithmen-Synthese-Algorithmus kann nicht existieren, aber ...

Literatur

Reichhaltige Literatur, siehe Übersichtsartikel:

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

"Lazy thinking" gehört zu den  "scheme-based" Methoden.

Algorithmen-Synthese durch "Lazy Thinking" (BB 2002)

Gegen:  Problemspezifikation P.           Find: Algorithmus A für P.

Wir nehmen an, dass wir  "vollständiges" Wissen über alle Begriffe, die in P vorkommen, haben.

Betrachte fundamentale Ideen (" Algorithmen-Schemata")  wie man Algorithmen A aus Unter-Algorithmen B, C, ... komponiert.
Probiere ein Schema nach dem anderen:

Für das gewählte Schema A, versuche zu beweisen (Underscript[∀ , x]) P[ x, A[x]]: Aus dem  misslungenen  Beweis  konstruiere Specificationen für die Subalgorithmsen B, ...

Automatische Erfindung von  hinreichenden Specificationen für die  Unteralgorithmen

Eine einfache (aber erstaunlich starke) Regel    ( B  ... ein unbekannter  Unteralgorithmus):

Sammle die  temporären Annahmen  T[ x0, ... A [  ],  ...  ]
und temporären Ziele G[ x0, ...B  [ ...  A [  ] ... ]  ]

und produziere die  Spezifikation

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

Details: siehe  [BB 2003] und die Beispiele unten.

The method  works well on simple problems like sorting

See [Buchberger 2003].

For example, using the  divide-and-conquer scheme

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

the method finds (in approx. 2 minutes on a laptop) that all subalgorithms S, M, L, R satisfying the following specifications make A a correct sorting algorithm:

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

Now we can continue, recursively, with synthesizing - or retrieving - algorithms S, M, L, R satisfying the above specifications.

Wie weit trägt die Methode?

Erfolgreiche  Synthese eines Algorithmus zur Konstruktion von Gröbner-Basen:

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.

Das Problem der Konstruktion von Gröbner-Basen

Finde Algorithmus Gb sodass

(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])  ...  ein Divisionsschritt.

Konfluenz der Division  (Subscript[-> , G])

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

Die entscheidende Idee in der Gröbner-Basen-Theorie (BB 1965)

Es genügt, die folgenden (endlich vielen) Polynome anzuschauen,

least–common–multiple[lp[g1], lp[g2]]

( g1 und g2 in der gegebenen endlichen Menge von Polynomen F.)

Die entscheidende Frage also

Kann "Lazy Thinking"  automatisch diese Idee produzieren  (und als korrekt erweisen)?

Starten wir also mit "Lazy Thinking" für die Eingabespezifikation.

Vorhandenes Wissen

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

etc.

Wähle ein Algorithmen-Schema

Zum Beispiel: ein Schema, das für alle mathematische Strukturen anwendbar ist, in welcher es eine "Reduktionsoperation"
           rd[ f, g]   (Result der "Reduktion von f mit g") gibt, die  satisfying  rd[f,g] ⪯ f   erfüllt.

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

Beginne nun den (automatischen) Korrektheitsbeweis

Mit der heutigen automatischen Beweis-Technologie im Theorema-System  [BB et al. 1995, ...] können solche Beweise automatisch gemacht werden. (PhD Thesis meines Studenten A. Craciun.)

Details

Zunächst kann bewiesen werden, dass für die am Ende des Algorithmus vorliegende Basis G Folgendes gilt:

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

Wir versuchen nun zu beweisen:

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

(Hier beschränken wir uns auf die dritte, die wichtigste Eigenschaft).

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

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 that lc[g1,g2] is reducible w.r.t. g1 and g2. The other cases are easy.)

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.

Wir sind nun auf einem toten Punkt im Beweis angelangt

Durch Anwenden der obigen Regel zur Extraktion von Spezifikationen für Unteralgorithmen aus misslungenen Beweisen, sieht man, dass man mit dem Beweis fortfahren könnte, wenn  lc[g1,g2] die folgende Bedingung erfüllte:

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

Zusammenfassung der (automatisch erzeugten) hinreichenden Spezifikationen des Unteralgorithmus lc

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

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

So ein Unteralgorithmus lc can aber nun mit elementarsten Mitteln gefunden werden (Mittelschulmathematik!)

Ein geeigneter Algorithmus lc

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

ist ein geeigneter Unteralgorithmus.

Heureka! Die wesentliche Funktion lc wurde automatisch synthetisiert.

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

Konklusion

Symbolic Computation ist Selbstanwendung der Mathematik.

Die gesamte Mathematik ist in gewisser Weise Symbolic Computation.

Die Fortentwicklung der Mathematik passiert durch permanente Entfaltung höherer Stufen durch Anwendung niederer Stufen auf der jeweiligen Meta-Ebene.

Mathematik ist Automatisierung

Es gibt keine Grenzen für die Automatisierung in der Mathematik 
("Mathematik ist Gödelsch")

Konsequenzen für mathematische Forschung, Anwendung, Lehre

Mathematik und Meditation spannen die diametralen Bewegungen des Bewusstseins auf

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.