Einleitung

Symbolisches Rechnen: Beispiele: Zahlen

Symbolisches Rechnen: Beisp.: Funktionen

Symbolisches Rechnen: Motivation

hat weitreichende Anwendungen:

ist nützlich im Studium, verwendet und vertieft:

Überblick

Literatur

Software

Beispiel: S.R. und Term-Ersetzung

Regeln für symbolisches Differenzieren (nach t):

 D(t) -> 1         D(constant) -> 0
 D(+(x,y)) -> +(D(x),D(y))
 D(*(x,y)) -> +(*(y,D(x)),*(x,D(y)))
 D(-(x,y)) -> -(D(x),D(y))

Robert Floyd 1967, zitiert in: Nachum Dershowitz: 33 Examples of Termination,

https://doi.org/10.1007/3-540-59340-3_2

Beispiel: Termersetzung (cont.)

data E = Zero | One | T 
       | Plus E E | Times E E  deriving Show

e :: E
e = let b = Plus T One in Times b b

d :: E ->  E
d e = case e of
    Zero -> Zero ; One -> Zero ; T -> One
    Plus x y -> Plus (d x) (d y)
    Times x y -> 
        Plus (Times y (d x)) (Times x (d y))

Beispiel: Inverse Symbolic Calculator

Hausaufgaben KW 15, Organisatorisches

  1. zum Haskell-Programm zum Symb. Differenzieren:

    • füge Syntax und Regel für Quotienten hinzu

    • schlage Regeln zur Vereinfachung vor

  2. ISC Simple Lookup and Browser sagt für \(\sqrt{2+\sqrt{3}}\):

    Mixed constants with 5 operations
1931851652578136 = 1/2/sin(Pi/12)

    begründen Sie das (geometrisch oder schriftlich)

  3. ein Polynom mit Nullstelle \(\sqrt[2]{2} +\sqrt[3]{3}\) bestimmen, nachrechnen.

  4. Geonext: Satz von Napoleon illustrieren (gleichseitige Dreiecke über den Seiten eines beliebigen Dreiecks)

  5. eigener Rechner: rlwrap maxima installieren,

    Rechner im Pool: ssh und tmux ausprobieren, auch Management von Sessions, Windows, Panes (split horizontal, vertikal), vgl. https://news.ycombinator.com/item?id=26670708

Organisatorisches:

Zahlen

Überblick

Darstellung natürlicher Zahlen

Natürliche Zahlen, Addition

Rekursive Multiplikation

Karatsuba-Multiplikation

Ganze Zahlen

Rationale Zahlen

Explosion der Stellenanzahl (Beispiel)

Endliche und unendliche Dezimalbrüche

Berechenbare reelle Zahlen

Potenzreihen, Exponentialfunktion

Potenzreihe für Wurzelfunktion

Logarithmen

Taylor-Entwicklung \(\log(1+x)=x-x^2/2+x^3/3- \ldots\)

konvergiert sehr langsam für \(x=1\), gar nicht für größere \(x\).

J.R. Young, 1835, siehe v. Mangoldt/Knopp, Bd. 2, S. 127 \[\begin{aligned} a = \log (16/15) &=& 4\log 2-1 \log 3-\log 5, \\ b = \log (25/24) &=& \dots \\ c = \log (81/80) &=& \dots \end{aligned}\] Umstellung ergibt \(\log 2 = 7a + 5b + 3c , \dots\) Aufgaben:

Pi

darüber gibt es ganze Bücher (Aufgabe: finde Beispiele)

Ansatz: Taylor-Entwicklung von \(\arctan x\)

\[\arctan x = x - x^3/3 + x^5/5 - \dots\]

(J. Machin, 1706, 100 Stellen; W. Shanks, 1873, 707 St.)

Hausaufgaben

  1. Multiplikation in GMP (GNU Multiprecision Library) https://gmplib.org/manual/Multiplication-Algorithms

    1. Karatsuba-Rechnung ist dort etwas anders als hier auf der Folie, warum?

    2. GHC verwendet GMP für den Typ Integer.

      Bestimmen Sie experimentell den Anstieg der Rechenzeit bei Verdopplung der Stellenzahl, z.B.

      :set +s
x = 10^10^8 :: Integer
odd x -- damit x ausgewertet wird
odd ((x-1)*(x+1)) -- die eigentliche Messung
  True
  (3.73 secs, 166,159,792 bytes)
y = x*x -- hat doppelte Stellenzahl

      Ist die Anzahl der Bytes plausibel?

      Diskutieren Sie mögliche verkürzte Auswertungen für odd .... Kann GMP/GHC das?

    3. Zusatz: warum ist (oder erscheint) (x+1)^2 schneller als (x+1)*(x+1)?

  2. diskutieren (Zusatz: implementieren) Sie die Darstellung von ganzen Zahlen mit negativer Basis \(B\le -2\)

    (und nichtnegativen Ziffern \(\in\{0,\dots,|B|-1\}\) wie bisher)

    Bsp: \(B=-2\),

    \(-3 = 1\cdot B^0 + 0\cdot B^1 + 1\cdot B^2+1\cdot B^3 =1+0+4-8\)

    1. Eindeutigkeit, Konstruktion

    2. Arithmetik (Nachfolger, Addition, Multiplikation)

  3. Bestimmen Sie die Taylor-Reihe für den Arcustangens an der Stelle 0

    wie auf Folie Potenzreihe für Wurzelfunktion

    Bestimmen Sie damit \(x=\arctan(1/2), y=\arctan(1/3)\) auf (z.B.) 20 Stellen.

    Begründen Sie \(x+y=\pi/4\). Rechnen Sie den Wert für \(\pi\) aus und vergleichen Sie mit einer verläßlichen Quelle.

    Kann man \(\pi\) nach diesem Verfahren, aber mit anderen Parametern, besser bestimmen? (mehr Stellen bei gleichem Aufwand)

  4. Bestimmen Sie die Taylor-Reihe für den (natürlichen) Logarithmus an der Stelle 1. Bestimmen Sie damit \(a=\log(6/5), b=\log(9/8), c=\log(10/9)\) auf (z.B.) 100 Stellen und daraus \(\log 2\) als eine Linearkombination.

  5. wie bestimmt man \(\sqrt{3}\), \(\sqrt{5}\), \(\sqrt[3]{2}\)

    Hinweis: \(\sqrt[3]{2}\) als Fixpunkt von \(x \mapsto (2x + 2/x^2)/3\),

    diese Gewichte ergeben quadratische Konvergenz,

    ist äquivalent zu Bestimmung der Nullstelle von \(f(x)=x^3-2\) nach Newton-Verfahren:

    \(f'(x)=3x^2, x\mapsto x - f(x)/f'(x) = \dots\)

  6. Jerzy Karczmarczuk: The Most Unreliable Technique in the World to compute pi, 2003? https://web.archive.org/web/20051017081559/http://users.info.unicaen.fr/~karczma/arpap/lazypi.ps.gz

Automatische Differentiation

Motivation, Anwendung

Verfahren zur Gradientenbestimmung

Automatische Differentiation (AD)

Stochastischer Gradientenabstieg

Anwendung: Matrix-Interpretationen

Constraint-Lösen durch Optimieren

Literatur und Software (funktionaler) AD

Aufgaben

  1. (H. Rosenbrock 1960) ein Test für Abstiegsverfahren ist \(f(x,y)=(x^2-y)^2 + y^2/100\),

    Veranschaulichen Sie den Werteverlauf mit rlwrap maxima

    f : (x^2-y)^2 + y^2/100;
plot3d(f,[x,-50,50],[y,-1000,3000]);

    wo ist das globale Minimum?

    in welche Richtung geht der (entgegengesetze) Gradient im Punkt \((20,100)\),

    wo verläuft die Folge der Näherungswerte, wird das globale Minimum erreicht? (1. diskutieren, 2. ausprobieren)

  2. für den Typ N v z: weitere Funktionen implementieren (Division, recip, sqrt, exp, log),

    den so bestimmten Wert des Gradienten mit numerischer Differentiation vergleichen

    diese Fkt. in einer Minimum-Bestimmung verwenden

  3. in neuronalen Netzen wird oft die Funktion \(S : x\mapsto 1/(1+\exp(-x))\) verwendet (sie bildet \(\RR\) monoton steigend auf \([0,1]\) ab)

    bestimmen Sie deren Ableitung symbolisch (zu Fuß oder Maxima), vergleichen mit AD-Implementierung (vorige Aufgabe)

  4. (Fortsetzung) ein \(k\)-stelliges Neuron mit Gewichten \(w_0,w_1,\dots,w_k\in\RR\) ist die Funktion \(x \mapsto S(w_0+\sum_i w_i x_i)\).

    ein vollständig verbundenes Netz mit \(e\) Eingängen und \(n\) Neuronen: das Neuron \(i\) sieht alle Eingänge sowie die Ausgänge der Neuronen \(1 \dots i-1\).

    Bestimmen Sie (mit stochastischem Gradientenabstieg mit AD) die Gewichte eines vollständigen Netzes (mit möglichst wenig Neuronen) für

    • XOR über alle Eingänge

    • Majoriät (falls \(s\) ungerade)

  5. für Optimierungsverfahren 2. Ordnung benötigt man die Hesse-Matrix einer Funktion (diese enthält alle zweiten Ableitungen). Modellieren und berechnen Sie diese durch eine Erweiterung des Typs data N v z.

    Vergleichen Sie mit exakten Werten (Bsp. maxima: hessian((x^2-y)^2,[x,y]);)

  6. (Forschungsaufgabe) Matrix-Interpretationen für Wortersetzungssysteme

    • verbesserte Modellierung (der Zielfunktion) und Parameter (Schrittweite)

    • stochastischer Abstieg (1. Ordnung)

    • Abstiegsverfahren 2. Ord. (oder Quasi-Newton)

    Testfälle

    • (leicht) \(a\to b\), \(ab\to ba\), \(ab\to bba\), \(aa\to aba\),

    • (schwerer) \(a^2b^2\to b^3a^3\), \(\{a^2\to bc, b^2\to ac, c^2\to ab\}\)

      System mit 3 Regeln: es genügt \(>_M\) für eine Regel, für die anderen \(\ge_M\). Wie kann man diese Bedingung als Zielfunktion einer Optimierung realisieren?

      ganzzahlige Lösungen sind bekannt (gefunden durch Bit-Blasting) gibt es kleinere nicht-ganzzahlige?

Polynome

Motivation (I): Polynom-Interpretationen

Motivation (II): Algebraische Zahlen

Bsp: gesucht ist Minimalpolynom für \(y = \sqrt{2} + \sqrt[3]{3}\)

\[\begin{array}{c|cccccc} & 1 & \sqrt[3]{3} & \sqrt{2} & \sqrt{2} \sqrt[3]{3} & \sqrt[3]{3^2} & \sqrt{2} \sqrt[3]{3^2} \\ \hline y^0 & 1 & 0 & 0 & 0 & 0 & 0 \\ y^1 & 0 & 1 & 1 & 0 & 0 & 0 \\ y^2 & 2 & 0 & 0 & 2 & 1 & 0 \\ y^3 & 3 & 6 & 2 & 0 & 0 & 3 \\ y^4 & 4 & 3 & 12& 8 & 12& 0 \\ y^5 & 60& 20& 4 & 15& 3 & 20 \\ \hline y^6 & 17& 90&120& 24& 60& 18 \end{array}\] die letzte Zeile ist linear abhängig von den vorigen (Dimension des Vektorraumes ist \(\le 6\)), ergibt Darstellung von \(y^6\) als rationale Linearkombination von \(y^0,\dots, y^5\).

Motivation (III): Geometrische Örter

Semantik und Syntax von Polynomen

Gruppen, Ringe, Körper

Polynome in einer Variablen

Polynom-Division (über \(\QQ\))

Polynome in mehreren Variablen

Polynom-Darstellung als geordnete Liste

Listen-Darstellung f. mehr Var.

Ideale

Hausaufgaben

  1. Bezeichnungen:

    arithmetisches Mittel \(A(x_1,\dots,x_n)=(\sum x_i)/n\), geometrisches Mittel \(G(x_1,\dots,x_n)=\sqrt[n]{\prod x_i)}\).

    Aufgabe: Stelle \(A(x_1,\ldots,x_4)^4-G(x_1,\ldots,x_4)^4\) als Summe von Quadraten (SOS) von Polynomen dar.

    Hinweis: \(A(x_1,x_2)^2-G(x_1,x_2)^2 = (x_1-x_2)^2/4\) und

    \(A(x_1,x_2,x_3,x_4)=A(A(x_1,x_2),A(x_3,x_4)) \ge A(G(x_1,x_2),G(x_3,x_4)) \ge G(G(x_1,x_2),G(x_3,x_4)) = G(x_1,x_2,x_3,x_4)\).

    Zusatz: \(A(x_1,x_2,x_3)^3-G(x_1,x_2,x_3)^3\) ist kein SOS, kann aber als Bruch mit SOS im Zähler und \((x+y+z)\) im Nenner geschrieben werden. Dazu die SOS-Darstellung der A-G-Ungleichung für die 4 Werte \(x_1,x_2,x_3,t=A(x_1,x_2,x_3)\) benutzen, denn \(A(x_1,x_2,x_3,t)=t\) und \(G(x_1,x_2,x_3,t)^4=G(x_1,x_2,x_3)^3\cdot t\).

    Hintergrund: Bruce Reznick: Some Concrete Aspects of Hilbert’s 17th Problem, 2000, https://faculty.math.illinois.edu/~reznick/.

  2. das Minimalpolynom für \(\sqrt{2}+\sqrt[3]{3}\) nach angegebenem Verfahren ausrechnen und überprüfen.

    Ähnlich für \(\sqrt{3}+\sqrt{5}\) oder (z.B.) \(\sqrt[5]{3}+\sqrt[5]{5}\)

  3. Das Polynom \(P\) für liegt auf Umkreis der Seitenmitten angeben (oder ähnlicher geometrischer Ort im Dreieck).

    o.B.d.A \(A_1=A_2=B_1=0\) annehmen.

    Warum wäre zusätzlich \(C_2=0\) doch eine B.d.A.?

  4. für die in VL angegebene Implementierung von Polynomen:

    eine anderen Koeffizientenbereich (als Rational) benutzen, z.B. Complex Rational

    nichttriviale Rechnungen durchführen (z.B. Division von \(X^{pq}-1\) durch \(X^p-1\)), Ergebnis prüfen,

    Laufzeit messen, Ausführung profilieren, teure Funktionen feststellen, ggf. verbessern

    Vergleichen mit derselben Rechnung in einem richtigen Computer-Algebra-System (maxima, fricas). (Nicht irgendwo online, sondern lokal, damit man messen und vergleichen kann.)

  5. für \(P=X^2Y + XY^2 + Y^2, Q=XY-1, R=Y^2-1\):

    ist \(P\in\operatorname{Ideal}(Q,R)\)?

    Hinweis: nein. Hinweis: Betrachten Sie Werte von \(P\) für die gemeinsamen Nullstellen von \(Q,R\).

  6. gilt \(X^5-Y^2 \in\operatorname{Ideal}(X^2Y-1,XY^2-1)\)?

    Welches Resultat liefert der Nullstellentest?

  7. Zeigen Sie \(\operatorname{Ideal}(X+XY,Y+XY,X^2,Y^2)=\operatorname{Ideal}(X,Y)\).

  8. Entscheiden Sie \(X^2+1 \in \operatorname{Ideal}(X+1)\), \(X^2-y^2\in\operatorname{Ideal}(X+Y)\), geben Sie Algorithmus für \(P\in\operatorname{Ideal}(Q)\) an.

  9. der arktische Halbring \(\mathbb{A}=(\{-\infty\}\cup\NN,\max,-\infty,+,0)\).

    Ist \(\deg\) homomorph (strukturerhaltend) von \((\ZZ[X],+,0,\cdot,1)\) nach \(\mathbb{A}\)?

  10. Def: Monom-Ordnung: total, monoton bzgl. Multiplikation, terminierend.

    Implementieren und Eigenschaften überprüfen/beweisen für graded reverse lexicographic: Ordnen nach absteigender Exponentensumme, bei Gleichheit nach aufsteigender Exponentenfolge

    Bsp. (für \(X > Y\)) \(X^3Y^2 > X^1Y^3\), \(X^3Y^2 > X^4Y^1\).

    Welche Eigenschaft(en) gehen dabei ohne Gradierung verloren?

  11. Für Monom-Ordnung \(>\) bezeichnet \(\operatorname{\textsf{mdeg}}(M)\) für Monome: den Exponentenvektor (in der Reihenfolge der Variablen).

    und für Polynome (\(\neq 0\)): den größten solchen Vektor (ist eindeutig, weil die Ordnung total ist).

    Bsp.: für \(X>Y\) ist \(\operatorname{\textsf{mdeg}}(X^2Y^5)=[2,5]\),

    für lex-Ordnung ist \(\operatorname{\textsf{mdeg}}(X^2Y^5-X^8)=[8,0]\).

    Ausprobieren, beweisen, ergänzen: für Polynome \(f,g\neq 0\) ist \(\operatorname{\textsf{mdeg}}(f\cdot g)=\operatorname{\textsf{mdeg}}(f)+\operatorname{\textsf{mdeg}}(g)\) (komponentenweise Addition)

    Welche Beziehung zw. \(\operatorname{\textsf{mdeg}}(f+g)\) und \(\operatorname{\textsf{mdeg}}(f),\operatorname{\textsf{mdeg}}(g)\)? Ggf. unter welchen Randbedingungen?

Gröbnerbasen

Begriff, Motivation

Literatur

Reduktion von Polynomen

Eigenschaften der Redukton: Termination

Eigenschaften d. Reduktion: Konfluenz?

S-Polynome

Der Buchberger-Algorithmus

Buchberger-Alg., Beispiel

Buchberger-Alg., Eigenschaften

Hausaufgaben

  1. zur Ordnung auf Monomen:

    1. unterschiedliche Ordnungen ((graded) (reverse) lexikografisch) selbst implementieren.

      instance Ord (Mono v) where ...

    2. stimmt die abgeleitete Ordnung newtype Mono v = M [(v, Natural)] deriving (Eq, Ord) mit einer dieser Ordnungen überein?

  2. zur Ordnung auf Polynomen:

    für Polynome in Variablen \(X>Y>Z\): geben Sie möglichst lange \(\gg\)-Ketten an, die bei \(X^3+Y^2Z\) beginnen

    • bzgl. der lexikografische Ordnung auf Monomen

    • bzgl. der grad-lexikografische Ordnung auf Monomen

  3. Kann \(S(f_1,f_2)\) Monome mit höherem Grad enthalten als \(f_1\) und \(f_2\)?

  4. bestimmen Sie nach dem Buchberger-Algorithmus eine Gröbner-Basis \(B\) für \(I=\operatorname{Ideal}(X^2Y-1,XY^2-1)\).

    (auf Papier, mit maxima, mit eigener Impl.)

  5. Benutzen Sie dieses \(B\), um \(X^5 - Y^2\in I\) zu entscheiden.

    (Papier, maxima (poly_grobner_member), eigen)

  6. Geben Sie Polynome \(c_1,c_2\) mit \(X^5-Y^2= c_1(X^2Y-1)+c_2 (XY^2-1)\) an.

    Erweitern Sie dazu den Buchberger-Alg. und das Reduktionsverfahren \(\to_B\).

    (zum Vergleich: Euklid bestimmt \(\gcd(a,b)\), erweiterter Euklid bestimmt \(c,d\) mit \(ac+bd=\gcd(a,b)\).)

  7. Eine Gröbner-Basis \(B\) heißt reduziert, wenn \(\forall b\in B: \neg\exists c: b\to_{B\setminus\{b\}}c\).

    (\(b\) kann nicht durch die jeweils anderen Basis-Elemente reduziert werden)

    Ist die Basis auf Folie Buchberger-Bsp. reduziert? Wenn nein, bestimmen sie eine reduzierte \(B'\).

    Ergänzen Sie die Eigenbau-Implementierung.

    Probieren Sie verschiedene Monom-Ordnungen.

    Die reduzierte Gröbner-Basis eines Polynom-Ideals ist im wesentlichen eindeutig.

  8. Arjen Cohen: Gröbner Bases, an Introduction (in: Some Tapas of Computer Algebra, Springer, 1999):

    it is very hard to provide a good explicit upper bound on [die Laufzeit des Buchberger-Algorithmus], bad examples are known.

    Finden Sie solche bad examples

    1. selbst ausdenken

    2. mit Suchmaschine (welche Testfälle werden in Publikationen verwendet, die verbesserte Algorithmen beschreiben)

    3. brute force

    und messen Sie den Ressourcenverbrauch (maxima, Eigenbau)

Gröberbasen in der Geometrie

Beispiel

Aufgaben und Anschauung Geometrie

  1. Coxeter und Greitzer: Geometry Revisited, 1967

    Bsp. 9-Punkte-Kreis (Feuerbachkreis) Kap. 1.8

  2. Intl. Math. Olympiade, Bsp: Aufgabe 2024/4 https://www.imo-official.org/problems.aspx

  3. dynamische Geometrie-Software Geonext (Univ. Bayreuth, Mathematikdidaktik)

    https://web.archive.org/web/20130605045826/http://geonext.uni-bayreuth.de/

    /opt/jdk/jdk8u442-b06/bin/java -cp /opt/geonext/geonext-1.74/geonext.jar geonext.Geonext

    Export der Zeichenvorschrift im Format i2g

Methode

Methode (Variante)

Anwendungen

Hausaufgaben

  1. Beispiele für geometrische Theoreme aus Skript Gräbe 2018 (Simsonsche Gerade, Miquelscher Punkt, …)

    • mit Geogebra zeichnen, Theorem überprüfen (durch Betrachtung der Lage bei Verschieben von Punkten)

    • algebraisieren (automatisieren!)

    • nach beschriebenen Verfahren lösen (Gröberbasis mit verschiedenen CAS ausrechnen)

  2. ein falsches Theorem beweisen (um zu sehen, wie die Methode die Falsch-Aussage erkennt)

  3. noch offene Aufgaben aus vorigen Wochen, insbesondere zur Eigenimplementierung von Polynomen (Division!) und Buchberger-Algorithmus

  4. bad examples (für Buchberger-Algorithmus) in verschiedenen CAS (viele naive Algebraisierungen von geometrischen Sätzen ergeben aufwendige Rechnungen, aber es gibt auch kleinere schwere Testfälle)

    Beispiel (Verallgemeinerung? Quelle?)

    cyclic4 =
  let [a,b,c,d] = map (var . V) [1 .. 4]
  in  [ a*b*c*d-1
      , a*b*c+b*c*d+c*d*a+d*a*b
      , a*b+b*c+c*d+d*a
      , a+b+c+d
      ]

  5. den Rabinovitch-Trick anwenden für den Satz über die Simson-Gerade in allgemeiner Lage (nur ein Punkt ist fixiert)

    fsimson = prove $ do
  ...
  return $ colinear a' b' c'

    die letzte Zeile ersetzen durch

      z0 <- number
  assert $ ...
  return $ ...

    und Laufzeiten (der naiven Implementierung sowie anderer CAS) vergleichen

  6. die Behandlung von Degenerations-Bedingungen,

    Beispiel: der Satz von Pappus

    pappus = prove $ do
  a  <- point ; b  <- point; c  <- point_on a  b
  a' <- point ; b' <- point; c' <- point_on a' b'
  p <- intersection b c' b' c
  q <- intersection a c' a' c
  r <- intersection a b' a' b
  return $ -- degenerate cases:
           parallel (b-c') (b'-c)
         * parallel (a-c') (a'-c)
         * parallel (a-b') (a'-b)
           -- actual conclusion:
         * colinear p q r

  7. bessere Implementierungen des Buchberger-Verfahrens: nicht jedesmal alle S-Polynome bestimmen und bezüglich aller bisherigen reduzieren.

    Zum Code in poly/Grobner.hs:

    • die Invarianten beweisen

    • die Termination begründen

      • für jede einzelne Reduktion eines (S-)Polynoms

      • für das gesamte Buchberger-Verfahren

Abstrakte Reduktionssysteme (ARS)

Definition, Motivation

Literatur, Quellen

Wiederholung: Relationen

Beispiele

Bezeichnungen (I)

Bezeichnungen (Eigenschaften v. Elementen)

Bezeichnungen (Eigenschaften v. Relationen)

Beziehungen zw. ARS-Eigenschaften

Motivation, Plan

Normalformen

CR und Konfluenz

Konfluenz und Normalformen

Lokale Konfluenz und Konfluenz

Konfluenz ohne Termination

Hausaufgaben

empfohlen: beide (b), 4, 5

  1. TeReSe Ex. 1.3.2

    Def: \((\to_1,\to_2)\) kommutieren schwach: \(\leftarrow_1\cdot\to_2{\subseteq}\to_2^*\cdot\leftarrow_1^*\)

    Def: \((\to_1,\to_2)\) kommutieren: \(\leftarrow_1^*\cdot\to_2^*{\subseteq}\to_2^*\cdot\leftarrow_1^*\)

    1. Satz: wenn \((\to_1,\to_2)\) schwach kommutieren und \(\operatorname{\textsf{SN}}(\to_1\cup \to_2)\), dann kommutieren \((\to_1,\to_2)\).

    2. Gegenbeispiel für: …und \(\operatorname{\textsf{SN}}(\to_1)\wedge\operatorname{\textsf{SN}}(\to_2)\), dann …

  2. TeReSe Ex. 1.3.15, Geser 1990, di Cosmo, Piperno 1995

    1. Wenn \(\leftarrow_1\cdot \to_2{\subseteq}\to_2^+\cdot\leftarrow_1^*\) und \(\operatorname{\textsf{SN}}(\to_2)\), dann kommutieren \((\to_1,\to_2)\).

    2. zeigen, daß \(\operatorname{\textsf{SN}}(\to_2)\) notwendig ist.

  3. TeReSe Ex. 1.3.3, Rosen 1973.

    Def (sub-commutative) \(\operatorname{\textsf{CR}^{\le 1}}(\to):=\leftarrow\cdot\to{\subseteq} \to^{0,1}\cdot\leftarrow^{0,1}\)

    Satz: aus \(\to_1^*{=}\to_2^*\) und \(\operatorname{\textsf{CR}^{\le 1}}(\to_1)\) folgt \(\operatorname{\textsf{CR}}(\to_2)\).

  4. TeReSe Ex 1.3.22.ii

    ein \(R\) mit \(\operatorname{\textsf{WCR}}(R)\wedge\operatorname{\textsf{UNR}}(R)\wedge\neg\operatorname{\textsf{UNC}}(R)\)

  5. alle Gegenbeispiele zu vorigen Aussagen könnte man

    —aber nur, falls es Gegenbeispiele mit endlichem Universum gibt. Das ist nicht immer der Fall.

    Geben Sie eine Eigenschaft vom Typ Prop an https://autotool.imn.htwk-leipzig.de/docs/autotool-collection-1.3/Rewriting-Abstract-Data.html#t:Prop, die

    • erfüllbar ist,

    • aber nicht endlich erfüllbar (d.h., mit endlichen Universum erfüllbar)

  6. Implementierung in Carpa (2018?) mit https://gitlab.imn.htwk-leipzig.de/autotool/all0/-/blob/master/collection/src/Rewriting/Abstract/Solve.hs (2015?) vergleichen.

    Gemeinsamkeit: aussagenlogische Codierung. Unterschied: SAT/BDD. Auswirkungen?

Terme, Ersetzungs-Systeme (Grundl.)

Termbäume, Positionen

Beispiele:

Baum-Bereiche

Einsetzen an Position

Variablen, Substitutionen

Regeln

Regelsysteme

Termersetzung/Anwendungen

Termersetzung ist

Für Anwendungen wichtig sind die Eigenschaften

das ist aber alles unentscheidbar (wg. Turing-Vollst.)

Term-Ersetzung und Computeralgebra

Wort- und Term-Ersetzung

Hausaufgaben zu TRS, SRS

  1. ergänzen: \(t[p_1:=s_1][p_2:=s_2]=\dots\)

  2. Normalformen, Termination, Konfluenz des TRS \[\begin{aligned} \neg(1) \to 0 ,\quad \neg(\neg(x)) \to x\\ 1\wedge x\to x, \quad 0\wedge x\to 0 \\ x\vee y\to \neg(\neg x\wedge\neg y) \end{aligned}\] über Signatur \(\{(0,0),(1,0),(\neg,1), (\vee,2),(\wedge,2)\}\)

    jeweils Beweis (soweit jetzt möglich, später systematisch) oder Gegenbeispiel (mit Reparaturvorschlag)

  3. Die Zug-Relation in Hackenbush auf höchstens binären Bäumen als TRS darstellen. (Signatur, Regeln f. Blau)

  4. (auf Papier) unendliche Ableitungen finden für

    1. \(\{f (0, y) \to f (y, S(0)), f(S(x), y) \to f (x, S(y))\}\)

    2. \(\{f (0, S(x), y) \to g(f (0, x, S(y)), f (x, y, S(S(0))))\)

    3. \(A(A(F,x),y)\to A(A(x,A(F, y)), F)\)

  5. (experimentell) unendliche Ableitungen finden für:

    1. \(\{1000\to 0001110\}\), allgemein \(10^k\to 0^k1^k0\)

    2. \(\{ 0 0 0 0 \to 0 1 0 1 , 1 0 0 1 \to 0 1 0 0 \}\)

    3. \(\{ 0 0 0 0 \to 0 1 1 1 , 1 0 0 1 \to 0 0 1 0 \}\)

    4. \(\{ 0 0 0 0 \to 0 1 1 1 , 1 0 1 1 \to 0 1 1 0 \}\)

  6. nachrechnen (Abschnitt 3.1, Alg. 3.2, Ex. 3.3: auf Zahlenfolgen, diese repräsentieren Terme) und beweisen:

    Ikebuchi, Nakano: On Properties of B terms, 2020 https://doi.org/10.23638/LMCS-16(2:8)2020

Gleichungsdefinierte Strukturen

Gleichungssysteme (Syntax)

Algebren (Semantik)

Modelle

Syntaktische u. semantische Äq. von Termen

Gleichungstheoreme und induktive Th.

Aufgaben

Jetzt ad-hoc, später teilw. systematisch/automatisiert

Quellen: TeReSe Kapitel 7.1; Baader/Nipkow Kapitel 3, 4.

  1. Für \(E=\{ aba(x) \approx x \}\): gilt \(abbbaa(x) \approx_E bba(x)\)?

  2. \(F=\{f(x,f(y,z))\approx f(f(x,y),z), f(e,x)\approx x, f(i(x),x)\approx e\}\). Zeige \(f(x,e)\approx_F x\).

  3. \(G = \{f(x,f(y,z))\approx f(f(x,y),z), f(f(x,y),x)\approx x \}\). Zeige \(f(x,x)\approx_G x\) und \(f(f(x,y),z)\approx_G f(x,z)\)

  4. \(H=\{f(x,f(y,z))\approx f(f(x,y),z), f(e,x)\approx x, f(x,i(x))\approx e\}\). Zeige \(f(x,e)\not\approx_H x\).

    Hinweis: ein Modell für \(H\) konstruieren, in dem die Behauptung nicht gilt. Mit etwas Glück gibt es ein endliches Modell. Mit noch mehr Glück ein so kleines, daß es durch Aufzählen mit https://hackage.haskell.org/package/leancheck gefunden wird. (Sonst: SAT-Kodieren) Ergänzen Sie:

    import Test.LeanCheck
import Test.LeanCheck.Function

check $ \ f i (e :: Bool) ->
  or [not $ holds 100 $ \ x y z -> _ , ... ]

    vereinfachen Sie die Ausgabe, überprüfen Sie die Eigenschaft.

    Zur Sicherheit: das gleiche Verfahren für Aufgabe \(F\) darf nicht funktionieren, denn dort wird behauptet, daß die Folgerung gilt.

Termination

Motivation

Automatische Terminations-Analyse

Historische Quellen zur Termination

Beweisverfahren für Termination

Wohlfundierte monotone Algebren

Wohlfundierte monotone Algebren (II)

Beispiel wfmA: lineare Interpretationen

Signatur \(\Sigma=\{P/2,S/1,Z/0\}\).

Regelmenge \(R=\{P(Z,y)\to y, P(S(x),y)\to S(P(x,y))\)

verschiedene \(\Sigma\)-Algebren über \(\NN\), überprüfe Eigenschaften.

Welche liefert einen Terminationsbeweis für \(R\)?

Aufgabe: finde kompatible wfmA für

\(R\cup \{ M(Z,y) \to Z, M(S(x),y) \to P(y,M(x,y)) \}\)

Merke: kompatibel: links \(>\) rechts, Modell: links \(=\) rechts,

Systematik wfmA

Polynom-Interpretationen

Synthese von Gewichtsfunktionen (für SRS)

Matrix-Interpretationen (für SRS) als wfmA

Matrix-Interpretationen (für TRS) als wfmA

Ableitungskomplexität

Modulare SN-Beweise, relative Termination

Wohl-Quasi-Ordnungen

Aufgaben

SS 25: 5,6,8,9,2,3

  1. Folie Matrix-Interpretationen: das Verifikations-Problem für das Beispiel.

    Beschreiben Sie möglichst genau die Komponenten des Vektors \([w](0,0,1)^T\) für \(w\in \{a,b\}^*\) (Beispiele, allgemein)

    Für Rechnungen mit Matrizen z.B. maxima verwenden.

  2. Wenn

    • \(A=(D_A,>_A,[\cdot]_A)\) eine wfmA kompatibel mit \(R\) und schwach kompatibel mit \(S\),

    • und \(B=(D_B,>_B,[\cdot]_B)\) eine wfmA kompatibel mit \(S\):

    konstruieren Sie eine wfmA mit Universum \(D_A\times D_B\), die kompatibel mit \(R\cup S\) ist.

    Lösungsplan:

    • Operationen: komponentenweise. \([f](x,y)=([f]_A(x),[f]_B(y))\)

    • Ordnung auf dem Universum angeben (unter welchem Namen kennen Sie diese?),

    • Monotonie und Kompatibilität nachweisen.

  3. Für \(A,B, R,S\) wie in voriger Aufgabe:

    wenn \(A\) und \(B\) durch Gewichtsfunktionen \(g_A\), \(g_B\) definiert sind, dann gibt es eine Gewichtsfunktion \(g\), die mit \(R\cup S\) kompatibel ist.

    (also eine kompatible wfmA auf \(\NN\). Nach voriger Aufgabe gibt es eine solche auf \(\NN^2\).)

    Anwenden auf \(R=\{bab\to aaba\}, S=\{a^3\to b\}\), \(g_A=\{a\mapsto 1,b\mapsto 3\}, g_B=\{a\mapsto 1, b\mapsto 0\}\)

  4. durch Beispiele illustrieren: wenn \(\operatorname{\textsf{SN}}(\to_1)\) und \(\operatorname{\textsf{SN}}(\to_2)\) und \((\to_1\cup\to_2)\) transitiv, dann \(\operatorname{\textsf{SN}}(\to_1\cup\to_2)\).

    Beweis ist wohl schwierig

  5. (von Hand, evtl. autotool) bestimme wfmAs für

    • \(\{aa\to bbb,bb\to a\}\)

    • \(\{p\wedge(q_1\vee q_2)\to (p\wedge q_1)\vee (p\wedge q_2),\) \((p_1\vee p_2)\wedge q \to (p_1\wedge q)\vee (p_2\wedge q) \}\).

    • \(A(A(D,x),y) \to A(x,A(x,y))\)

    Hinweis: Dershowitz: 33 examples.

  6. Familien von langen Ableitungen und Terminationsbeweis für die SRS

    • \(R_1 = \{ba \to acb, bc \to abb\}\)

    • \(R_2 = \{ba \to acb, bc \to cbb\}\)

    • \(R_3 = \{ba \to aab, bc \to cbb\}\)

    Hinweis: eines hat doppelt exponentielle Ableitungslängen, eines mehrfach exponentielle, eines ist nichtterminierend.

    Beispiel: einfach exponentielle Ableitungslängen für \(ba\to aab\): \(\forall k: ba^k\to^* a^{2k} b\), \(\forall k: b^ka\to^* a^{2^k} b^k\).

    Hinweis: jede Regelanwendung verlängert um 1, deswegen \(u\to^k v\implies k=|v|-|u|\), man muß also die Schritte nicht zählen, sondern nur die Wortlängen vergleichen.

  7. Geben Sie ein längen-erhaltendes terminierendes SRS mit exponentiellen Ableitungslängen an. Hinweis: Binärzähler.

    Alphabet und Regelanzahl beliebig. Das SRS möglichst kurz (Summe aller Längen aller Regelseiten)

    (Mit einer Regel geht das nicht. Wenn die terminiert, sind die Ableitungslängen höchstens quadratisch.)

  8. Polynom-Interpretationen: Bsp. 6.2.13, 6.2.14, 6.2.15 aus Hans Zantema: Termination (in TeReSe, 2003)

  9. (Masterprojekt/Werkvertrag) Containerisation für Matchbox

    https://git.imn.htwk-leipzig.de/waldmann/pure-matchbox/-/issues/544

    (Masterarbeit) Anwendung, Dokumentation, Verbesserung der Parameter-Optimierung für Beweissuche, Bsp.

    https://git.imn.htwk-leipzig.de/waldmann/pure-matchbox/-/issues/543

Konfluenz und Vervollständigung

Motivation, Beispiel

Kritische Paare

Def: Für ein Termersetzungssystem \(R\) über \(\Sigma\): falls

Bsp: \(\{ f(f(x,y),z)\to_1 f(x,f(y,z)), f(i(x),x) \to_2 e()\}\)

Satz: \((s,t)\in\CP(R) \Rightarrow s\approx_R t\). Beweis: \(s\leftarrow_R l_1\sigma \rightarrow_R t\).

Kritische Paare und (lokale) Konfluenz

Bsp. Kritische Paare für SRS

Bsp. kritische Paare für TRS

kritische Paare angeben, (später: vervollständigen)

  1. \(\{f(x,x)\to a, f(x,g(x))\to b\}\)

  2. \(\{0+y\to_1 y, s(x)+y\to_2 s(x+y),\) \(x+0\to_3 x, x+s(y)\to_4 s(x,y)\}\)

  3. \(\{f(f(x,y),f(y,z))\to y\}\)

  4. \(\{f^5(a)\to a, f^3(a)\to a\}\)

Orthogonale Systeme

Vervollständigung (basic)

…ist Algorithmus mit dieser Spezifikation

Implementierung: zusätzliche Eingabe: eine wfmA \(A\)

Korrektheit? Termination? beachte: 3 Fehlermöglichkeiten

Implementierung der einf. Vervollst.

Vervollständigung (improved)

bei einfacher Vervollständigung:

alternativer Ansatz:

(nichtdeterministischer) Vervollständigungsalgorithmus wird formuliert mittels Inferenzsystem

Inferenzsystem für Vervollständigung

(Leo Bachmair 1991, zitiert in Baader/Nipkow)

Regeln (weiter evtl. in Übung)

Korrektheit?

Warum ist einfache Vervollst. ein Spezialfall?

Aufgabe zu Vervollständigung in autotool

Vervollständigung: Knuth/Bendix, 1970

Wortprobleme für Gruppen, ab 1900

Wiederholung: Unifikation

Wiederholung: Bestimmung des mgu

Dieser Algorithmus ist korrekt, aber nicht effizient.

Hausaufgaben

SS25: 1 (teilweise auch in autotool), 2, 4.

  1. zu Folie Kritische Paare für TRS: kritische Paare ausrechnen.

    Passende wfmA angeben und vervollständigen (soweit möglich).

  2. zu Folie Orthogonale Systeme: für das Beispiel nachrechnen: \(\operatorname{\textsf{WCR}}\), \(\neg\operatorname{\textsf{CR}}\).

    Das durch diese Regelmenge erzeugte ARS mit früheren Beispielen für \(\operatorname{\textsf{WCR}}\) und \(\neg\operatorname{\textsf{CR}}\) vergleichen.

  3. Zeigen Sie Konfluenz von \(\{1 \vee 1 \to 1, x\vee y\to y\vee x\}\). Welche der in der VL genannten Sätze und Methoden sind hier anwendbar?

  4. Beispiele und Beweis: die Dyck-Sprache ist die \(\approx_D\)-Äquivalenzklasse von \(\epsilon\) für \(D=\{ab\to\epsilon\}\).

    Weil \(D\) konvergent ist (Beweis?) ist jede \(\approx_D\)-Äquivalenzklasse durch eine \(D\)-Normalform charakterisiert.

    Diese \(D\)-Normaformen sind \(b^pa^q\). Die \(D\)-Normalisierung ist also eine Abbildung \(f:\{a,b\}^*\to\NN^2\).

    Für \(f(w_1)=(p_1,q_1)\) und \(f(w_2)=(p_2,q_2)\), geben Sie \(f(w_1\cdot w_2)=(p,q)\) als Funktion von \(p_1,q_1,p_2,q_2\) an.

    Auf Deutsch: \(f\) ist ein Monoid-Homomorphismus von \((\{a,b\}^*,\epsilon,\cdot)\) nach \((\NN^2, (0,0), ?)\) und das Fragezeichen ist gesucht. Recherche-Aufgabe: wie heißt dieses Ziel-Monoid?

  5. weitere Regeln für Inferenzsystem für Vervollständigung

    Siehe Winkler et al. (JAR 2013) https://doi.org/10.1007/s10817-012-9249-2 Fig. 1, zitiert aus: Bachmair (TCS 1991).

    entsprechende Erweiterung der Autotool-Aufgabe diskutieren (…und realisieren als Masterarbeit)

    Vergleichen mit der Formulierung des Knuth-Bendix-Algorithmus in Huet (1980) https://hal.inria.fr/inria-00076536/file/RR-0025.pdf

  6. Gruppendarstellungen und Anwendung von Knuth-Bendix: siehe Havas et al.: Some Challenging Group Presentations (J. Austr. Math. Soc., 1999) https://staff.itee.uq.edu.au/havas/1999hhkr.pdf

  7. mit Original-Artikel von Knuth u. Bendix:

    • wie werden Terme notiert?

    • wo steht die Definition von KBO?

    • Vervollständigungsschritte nachrechnen (das Entstehen des CP sowie seine passende Orientierung)

    zur Geschichte von Knuth/Bendix siehe auch Donald Knuth: All Questions Answered, Notices Vol 49(3), https://www.ams.org/notices/200203/fea-knuth.pdf

  8. (als Wiederholung und Ergänzung zu Termination) in KBO: welche Symbole dürfen Gewicht 0 haben? Warum die anderen nicht? (Gegen-Beispiele für \(\operatorname{\textsf{SN}}(>)\) angeben)

    TTT2 (Weboberfläche) kann auch KBO.

Programm \(=\) Beweis

Plan, Motivation

Konjunktion \(=\) Kreuzprodukt

Implikation \(=\) Funktionstyp

Disjunktion \(=\) disj. Vereinigung

Schrittweise Beweis-Konstrukion

Das Falsche, das Wahre

Die Negation

Die Peano-Zahlen

Eigenschaften von Zahlen (Bsp. 1)

Die Sprache/Das System Agda

Aufgaben

exakt formalisieren, Beweis schrittweise entwickeln

Code aus VL verwenden (d.h., keine Standardbibliothek)

(möglichst viel C-c .., möglichst wenig selbst schreiben)

  1. Assoziativität des Oder

  2. \(\neg\neg\neg a \to \neg a\)

  3. Varianten von de Morgan

  4. für Nat: definiere odd (ungerade) (direkt, nicht als Negation von gerade)

    zeige: {x : Nat} -> even x -> odd x -> Absurd

  5. zeige: ungerade plus ungerade ergibt gerade

  6. definiere Multiplikation,

    zeige: ungerade mal ungerade ergibt ungerade

Note: Assoziativität der Addition (usw.) noch nicht, weil wir die Gleichheit noch nicht definiert haben.

Dependent Typen und Muster

Datentypen

Pattern Matching in Funktions-Def.

Anwendung: längen-indizierte Vektoren

Die Gleichheit

Anwendung Gleichheit

Notation für Gleichungsketten

Operator-Syntax in Agda

Aufgaben

exakt formalisieren, Beweis schrittweise entwickeln

Code aus VL verwenden (d.h., keine Standardbibliothek)

(möglichst viel C-c .., möglichst wenig selbst schreiben)

  1. \(x + 0 = x\)

  2. \(x + y = y + x\)

  3. cong-succ verallgemeinern: Aussage gilt nicht nur für succ : Nat -> Nat, sondern für beliebige Funktion f : a -> b

  4. Multiplikation definieren (Induktion über 1. Arg.)

  5. Multiplikation ist assoziativ, kommutativ, distributiv (rechts und links) bzgl. Addition

  6. Verkettung von Listen, von Vektoren

Anwendung: Funktionale Vektoren

Endliche Mengen und Abbildungen

Vektoren, Matrizen

Paare, Records, Spezifikationen

Paare

Records

Spezifikation algebraischer Strukturen

Spezifikation \(=\) Abstrakter Datentyp

Zusammensetzen von Spezifikationen

Bibliotheken für ADTs (Bsp.)

Aufgaben–Dependent Paare

  1. data Exists {A : Set} (P : A -> Set) : Set
  where exists : (x : A) -> (y : P x) -> (Exists P)

    (ist nur eine Umbenennung von Pair) beweise

    {A : Set} (P Q : A -> Set)
   -> Exists (\ x -> Und (P x) (Q x))
   -> Exists (\ x -> P x)

  2. Vertauschen von Quantoren

    p0 : {A B : Set} {P : A -> B -> Set}
   -> Exists (\ x -> Exists (\ y -> P x y))
   -> Exists (\ y -> Exists (\ x -> P x y))

  3. Wiederholung: Die All-Quantifikation wird durch den Funktionspfeil ausgedrückt. Anwendung: Skolemisierung (\(f\) ist die Skolem-Funktion für \(y\) unter \(x\))

    p1 : {A B : Set} {P : A -> B -> Set}
   -> ((x : A) -> Exists (\ y -> P x y))
   -> Exists {A -> B} (\ f -> (x : A) -> P x (f x))

  4. für even wie früher (induktiv definiert)

     {x : Nat} -> even x
  -> Exists (\ y -> times y (succ (succ zero)) == x)
  5. not (Exists (\ x -> Und (even x) (even (succ x))))

Aufgaben–Abstrakte Datentypen

  1. nat-times-monoid : Monoid Nat _ times

  2. für jeden Typ \(A\): Menge der Funktionen \(A\to A\) ist Monoid bezüglich Komposition (Nacheinanderausführung)

  3. (Wiederholung Knuth-Bendix)

    record Gruppe {A : Set}
     (e : A) (_o_ : A -> A -> A) (i : A -> A) : Set where
  field
    left-id : {x : A} -> (e o x) == x
    left-inv : {x : A} -> (i x  o  x) == e
    assoc : {x y z : A}
      -> (x o (y o z)) == ((x o y) o z)

right-id :  {A : Set} {e : A} {_o_ : A -> A -> A} {i : A -> A}
  -> Gruppe e _o_ i -> {x : A} -> (x o e) == x

right-inv : {A : Set} {e : A} {_o_ : A -> A -> A} {i : A -> A}
  -> Gruppe e _o_ i -> {x : A} -> (x  o  i x) == e

  4. Begriff Halbordnung (mit _<=_ : A -> A -> Set) als Record spezifizieren (allgemein),

    konkrete Implementierungen für Nat für x <= y

    • Fallunterscheidung für \(x,y\), Rekursion

    • Exists \ z -> plus x z == y (kann Eigenschaften von plus nachnutzen, auf andere Monoide verallgemeinert werden)

  5. Wenn Relation \(R\) Halbordnung auf Menge \(A\), dann ist auch Relation \(R^-\) Halbordnung auf \(A\)

Plan (vorläufig)