Symbolisches Rechnen Vorlesung Wintersemester 2006, 2014

Transcript

Symbolisches Rechnen Vorlesung Wintersemester 2006, 2014 Johannes Waldmann, HTWK Leipzig 11. Dezember 2015 Symbolisches Rechnen: Definition I Rechnen mit Funktionen. (mit Ausdrucken, die Funktionen bezeichnen, ¨ d.h. gebundene Variablen enthalten) Bsp: expand(λx.(x + 1)2 ) = λx.(x 2 + 2x + 1) I im Gegensatz zum numerischen Rechnen (mit Zahlen) wie in der Mathematik (leider) ublich: der Binder (λ) wird nicht ¨ notiert, die gebundenen Variablen sehen dadurch frei aus: expand((x+1)ˆ2); Symbolisches Rechnen: Motivation hat weitreichende Anwendungen: I Losen ¨ von (parametrisierten) Aufgabenklassen (fur ¨ numerisches Rechnen muß Parameter fixiert werden) I exaktes Losen ¨ von Aufgaben (numer. R. mit Maschinenzahlen: nur Approximation) I experimentelle, explorative, exakte Mathematik ist nutzlich im Studium, benutzt und vertieft: ¨ I I I Mathematik (Analysis, Algebra) Algorithmen-Entwurf, -Analyse Prinzipien von Programmiersprachen ¨ Uberblick I Grundlagen (6 Wochen) I I I Vertiefung (6) I I I I Term-Ersetzungs-Systeme (Differentiation, Vereinfachung) exaktes Rechnen mit (beliebig großen) Zahlen Vektoren (Gitterbasen) ¨ Polynome, Grobnerbasen Geometrische Konfigurationen und Beweise Ausblick (2): Musik-Notationen, Beweisuberpr ufer, ... ¨ ¨ Literatur I I Wolfram Koepf: Computeralgebra, Springer, 2006. http: //www.mathematik.uni-kassel.de/˜koepf/CA/ ¨ Hans-Gert Grabe: Einfuhrung in das Symbolische ¨ ¨ Rechnen, Grobnerbasen und Anwendungen, Skripte, ¨ Leipzig http://www.informatik. Universitat uni-leipzig.de/˜graebe/skripte/ I Franz Baader and Tobias Nipkow: Term Rewriting and All That, Cambridge, 1998. http://www21.in.tum.de/˜nipkow/TRaAT/ I Gerhard Nierhaus: Algorithmic Composition, Springer, 2009. Software I Maxima http://maxima.sourceforge.net/ Hinweis: benutze rlwrap maxima I GHC http://www.haskell.org/ghc/ I Geogebra http://www.geogebra.org/ I Coq/Coqide http://coq.inria.fr/, Isabelle/HOL http://isabelle.in.tum.de/ Beispiel: S.R. und Term-Ersetzung Regeln fur ¨ 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, http://citeseerx.ist.psu.edu/viewdoc/ summary?doi=10.1.1.31.9447 I ¨ Korrektheit? Termination? Komplexitat? I Strategie (Auswahl von Regel und Position)? I ausreichend? angemessen? 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 http: //oldweb.cecm.sfu.ca/projects/ISC/ISCmain.html zur Bestimmung ganzzahliger Relationen (z.B. zwischen Potenzen einer numerisch gegebenen Zahl) sqrt(2+sqrt 3) ==> 1.9318516525781366 Roots of polynomials of degree less than or equal to 1931851652578136 = -1+4*xˆ2-xˆ4 mit LLL-Algorithmus (Lenstra, Lenstra, and Lovasz, 1982), der einen kurzen Vektor in geeignetem Gitter bestimmt. Hausaufgaben KW 42 I zum Haskell-Programm zum Symb. Differenzieren: I I I ISC I I fuge Syntax und Regel fur ¨ ¨ Quotienten hinzu schlage Regeln zur Vereinfachung vor p √ 2+ 3 verifziere diese Behauptung fur ¨ Mixed constants with 5 operations 1931851652578136 = 1/2/sin(Pi/12) √ √ 2 bestimme ein Polynom mit Nullstelle 2 + 3 3 ¨ Ubung KW 42 zu Aufgabenblatt Geometrie http://www.imn.htwk-leipzig.de/˜waldmann/edu/ ws14/sym/SR-1/Aufgaben.pdf I Skizze zu Aufgabe 4 (kein Beweis), Begriff kollinear I Beweis Aufgabe 7 (von Hand) I Aufgabe 6 fur ¨ Zukunft ¨ die nahere Beispiele aus Einf. Symb. Rechn. http://www.imn.htwk-leipzig.de/˜waldmann/edu/ ws14/sym/SR-1/folien.pdf I Kreisgleiter (Folie 13) herleiten und nachrechnen (maxima) e : subst(r*(x+1),y, xˆ2+yˆ2-1); s : solve(e, x); subst (part (s,2), e); ratsimp (%); Beachte: Vorzeichenfehler auf Folie. Symbolisches Differenzieren I . . . von Quotienten: ¨ Termbaume, Positionen I I I I I Signatur Σ: Menge von Funktionssymbolen mit Stelligkeit, Bsp. {(s, 1), (z, 0), (p, 2)}, Term(Σ) ist die kleinste Menge M mit . . . Pos(t): Menge der Positionen in t ∈ Term(Σ): . . . t(p) Symbol an Position p in t t |p Teilterm an Position p in t Beispiele: I I I Term t = p(z, s(s(z))), Positionen Pos(t) = {, 1, 2, 21, 211}, Symbol t(2) = s, Teilterm t|2 = s(s(z)), Baum-Bereiche Def: Menge P ⊆ N∗ heißt Baum-Bereich (tree domain), wenn (. . . es einen Term t gibt, so daß P = Pos(t) — das soll aber ohne Benutzung des Term-Begriffs definiert werden) I ∈P I P abgeschlossen unter . . . Hinweise: definiere und benutze Relationen [baab] = 6 > [aabab] = . . . > [aaaabb] = . . . Def: (D, >, [·]) ist wohlfundierte monotone Algebra I I keine unendlichen absteigenden Ketten in (D, >) Monotonie: ∀c ∈ Σ, x ∈ D, y ∈ D : x > y ⇒ [c](x) > [c](y ) Def: Algebra ist kompatibel mit R: I Kompatibilitat: ¨ ∀(l, r ) ∈ R, x ∈ D : [l](x) > [r ](x) Satz: →R terminiert ⇐⇒ ∃ wfmA, die mit R kompatibel ist. Beispiel wfmA Signatur Σ = {P/2, S/1, Z /0}. Regelmenge R = {P(Z , y) → y , P(S(x), y ) → S(P(x, y )) verschiedene Σ-Algebren uber N, uberpr ufe ¨ ¨ ¨ Eigenschaften. Welche liefert einen Terminationsbeweis fur ¨ R? I I I [P](x, y ) = x + y, [S](x) = x + 1, [Z ] = 0 [P](x, y ) = 2x, [S](x) = x + 1, [Z ] = 1 [P](x, y ) = 2x + y + 1, [S](x) = x + 1, [Z ] = 0 Aufgabe: finde kompatible wfmA fur ¨ R ∪ {M(Z , y) → Z , M(S(x), y ) → P(M(x, y), y )} Aufgabe: . . . fur ¨ A(A(D, x), y) → A(x, A(x, y)) Merke: kompatibel: links > rechts, Modell: links = rechts, Systematik wfmA Beispiele benutzten lineare Funkt. uber N. Erweiterungen: ¨ Polynome uber N ¨ lineare Funktionen (Matrizen) uber Nd ¨ I . . . uber anderen Halbringen, wie ({−∞} ∪ N, max, +) ¨ ¨ ¨ fur man losen: ¨ jedes solche Klasse von Algebren mochte das Verifikations-Problem: I Monotonie, Kompatibilitat ¨ mit R I I das Synthese-Problem: I gegeben R, gesucht R-kompatible wfmA ¨ (z.B. Losen des Constraint-Systems fur ¨ Koeffizienten) siehe http://www.termination-portal.org/ Aufgaben (evtl. autotool) bestimme wfmAs fur ¨ I I I Peano-Multiplikation (Variante A: ohne Additionsregeln, B: mit) symbolisches Differenzieren {p ∧ (q1 ∨ q2 ) → (p ∧ q1 ) ∨ (p ∧ q2 ), (p1 ∨ p2 ) ∧ q → (p1 ∧ q) ∨ (p2 ∧ q)}. beweise: I I das Verifikationsproblem fur ¨ lineare Interpretationen (uber ¨ N, uber Nd ) ist entscheidbar ¨ das Syntheseproblem fur ¨ lineare Interpretationen mit Anstieg 1 (d.h. [f ](x1 , . . . , xk ) = x1 + . . . + xk + cf ) ist entscheidbar. Motivation gesucht ist Entscheidungsverfahren fur ¨ das Wortproblem: I Eingabe: E uber Σ, s, t ∈ Term(Σ, V ) ¨ I Frage: s ≈E t Plan: Vergleich der →E -Normalformen von s, t. Beispiel: E = {(P(Z , y), y), (P(S(x), y), S(P(x, y))}, s = P(S(S(Z )), x), t = S(P(P(Z , S(Z )), x)), Probleme: 1. Existenz und 2. Eindeutigkeit der Nf. Bsp: E = {(aba, )}, s = abbbaa, t = bba Motivation (II) gesucht ist Entscheidungsverfahren fur ¨ s ≈E t Plan: Vergleich der →E -Normalformen von s, t. Probleme: 1. Existenz und 2. Eindeutigkeit der Nf. ¨ Losung: I I (Ziel): 1. Termination und 2. Konfluenz ¨ (Verfahren): Vervollstandigung. Bsp: E = aba ≈ , abbbaa ≈E bba? Orientiere aba → , nicht konfluent wegen ba ← ababa → ab, neue Regel ba → ab, nicht konfluent wegen . . . , neue Regel . . . , konfluent? terminierend? NFs von s, t? Konfluenz Eine zweistellige Relation ρ heißt konfluent, wenn ∀x, y1 , y2 : ρ∗ (x, y1 ) ∧ ρ∗ (x, y2 ) ⇒ ∃z : ρ∗ (y1 , z) ∧ ρ∗ (y2 , z) (Bild ist einfacher zu merken) I Satz: wenn ρ auf M konfluent ist, dann besitzt jedes x ∈ M ¨ hochstens eine ρ-Normalform. I Beachte: es wird nicht behauptet, daß x uberhaupt eine ¨ Normalform besitzt. ¨ sich Konfluenz Falls ρ jedoch terminiert, dann laßt charakterisieren und entscheiden durch einen Hilfsbegriff ¨ (lokale Konfluenz, spater) Lokale Konfluenz I Eine zweistellige Relation ρ heißt lokal konfluent, wenn ∀x, y1 , y2 : ρ(x, y1 ) ∧ ρ(x, y2 ) ⇒ ∃z : ρ∗ (y1 , z) ∧ ρ∗ (y2 , z) I Beachte: es gibt Relationen ρ, die lokal konfluent sind, aber nicht konfluent. I Satz: wenn ρ terminiert und lokal konfluent ist, dann ist ρ konfluent. lokale Konfluenz erkennt man durch Betrachtung von ¨ Uberlappungen von linken Regelseiten. diese (Teilterme der) linke Seiten enthalten Variablen, deswegen muß man unifizieren. Unifikation—Begriffe I Substitution: partielle Abbildung σ : V → Term(Σ, V ), so daß kein v ∈ dom σ in img σ vorkommt. I Substitution σ auf Term t anwenden: tσ (definiert durch Induktion uber t) ¨ I Produkt von Substitutionen: so definiert, daß t(σ1 ◦ σ2 ) = (tσ1 )σ2 (wie geht das genau?) I die so definierten Substitutionen sind idempotent: σ ◦ σ = σ. Unifikation—Definition Unifikationsproblem (unvollst.) I I Eingabe: Terme t1 , t2 ∈ Term(Σ, V ) Ausgabe: eine Substitution σ = mgu(t1 , t2 ) mit: I σ unifiziert t1 , t2 : t1 σ = t2 σ. Beispiele: bestimme jeweils Menge der Unifikatoren von: I I I I f (X ), f (a) X , f (Y ) f (X ), g(Y ) X , f (X ) ¨ Fur man bestimmte ¨ den Fall mehrerer Unifikatoren mochte ¨ ¨ auswahlen. (⇒ vollst. Def. nachste Folie) Unifikation—Definition (vollst.) I I Eingabe: Terme t1 , t2 ∈ Term(Σ, V ) Ausgabe: eine Substitution σ = mgu(t1 , t2 ) mit: I I σ unifiziert t1 , t2 : t1 σ = t2 σ. σ ist minimal bzgl. ≤ unter allen Unifikatoren von t1 , t2 ¨ benutzt Pra-Ordnung auf Substitutionen: σ1 ≤ σ2 ⇐⇒ ∃τ : σ1 ◦ τ = σ2 Satz: jedes Unifikationsproblem ist entweder gar nicht oder bis ¨ auf Umbenennung eindeutig losbar ¨ Bem: Pra-Ordung: transitiv und symmetrisch. (Beweis?) Warum ist ≤ keine Halbordnung? Unifikation—Algorithmus mgu(s, t) nach Fallunterscheidung I I I s ist Variable: . . . t ist Variable: symmetrisch s = f (s1 , s2 ) und t = g(t1 , t2 ): . . . Bemerkungen: I I I korrekt, ubersichtlich, aber nicht effizient, ¨ ¨ ¨ es gibt Unif.-Probl. mit exponentiell großer Losung (U) mit komprimierter Darstellung: Linearzeit. autotool-Quelltexte Substitution und Unifikation: http://autolat.imn.htwk-leipzig.de/gitweb/?p=tool; a=tree;f=collection/src/Prolog;hb=for-ghc-7.8 Kritische Paare Fur Σ: falls ¨ ein Termersetzungssystem R uber ¨ I I I I (l1 → r1 ) und (l2 → r2 ) sind Regeln in R ohne gemeinsame Variable (ggf. vorher umbenennen!) es gibt p ∈ Pos(l1 ) so daß l1 [p] und l2 unifizierbar sind d. h., es existiert mgu σ mit l1 [p]σ = l2 σ falls (l1 → r1 ) = (l2 → r2 ) (vor Umbenennung), dann p 6=  dann heißt (r1 σ, (l1 σ)[p := r2 σ]) kritisches Paar von R. Ein kritisches Paar (s, t) von R heißt zusammenfuhrbar, falls ¨ ∗ ∗ ∃u : s →R u ∧ t →R u. Satz: ein Termersetzungssystem ist genau dann lokal konfluent, wenn alle kritische Paare zusammenfuhrbar sind. ¨ Orthogonale Systeme I ein TES R uber Σ heißt nichtuberlappend, wenn R keine ¨ ¨ kritischen Paare besitzt. I ein TES R heißt linkslinear, wenn in keiner linken Regelseite eine Variable mehrfach vorkommt. I ein TES R heißt orthogonal, falls es linkslinear und nichtuberlappend ist. ¨ Satz: jedes orthogonale System ist konfluent. Funktionale Programmierung ≈ System R ist orthogonal und ¨ . . . (nachste Folie) Konstruktor-Systeme I Fur Σ: ein Symbol f ∈ Σ heißt definiert, wenn ¨ TES R uber ¨ es als Wurzel einer linken Regelseite in R vorkommt. I Alle anderen Symbole heißten Konstruktoren. I R heißt Konstruktor-System, falls in jeder linken Seite nur ein definiertes Symbol vorkommt (und zwar in der Wurzel). Beispiele: {P(Z , y ) → . . . , P(S(x), y ) → . . . , M(Z , y ) → . . . , M(S(x), y ) → . . . } ist Konstruktor-System, definierte Symbole sind {P, M}, Konstruktoren sind {S, Z } aber {A(A(D, x), y) → A(x, A(x, y ))} nicht. ¨ Vervollstandigung (basic) . . . ist Algorithmus mit dieser Spezifikation I I Eingabe: Gleichungssystem E Ausgabe: Ersetzungssystem R mit Eigenschaften: I I R ist konvergent (:= terminierend und konfluent) ≈R = ≈E ¨ Implementierung: zusatzliche Eingabe: eine wfmA A I I ordne Paare aus E bzgl. >A , Resultat R0 wiederhole bis Ri+1 = Ri : Ri+1 := Ri ∪ die folgenden Paare: ∀(s, t) ∈ CP(Ri ): I I ¨ wahle s0 ∈ NfRi (s), t 0 ∈ NfRi (t) 0 falls s 6= t 0 , ordne (s0 , t 0 ) bzgl. >A . ¨ Korrektheit? Termination? beachte: 3 Fehlermoglichkeiten ¨ Vervollstandigung (improved) ¨ bei einfacher Vervollstandigung: I jedes neue kritische Paar muß sofort orientiert werden. I manche sind evtl. nicht orientierbar alternativer Ansatz: I das Orientieren aufschieben, I bis neue Regeln vorliegen, die zur Umformung des Paares ¨ benutzt werden konnen I so daß das umgeformte Paar orientierbar ist ¨ (nichtdeterministischer) Vervollstandigungsalgorithmus wird formuliert mittels Inferenzsystem ¨ Inferenzsystem fur ¨ Vervollstandigung (Leo Bachmair 1991, zitiert in Baader/Nipkow) I I I Grundbereich: Paare (E, R) , Start: (E0 , ∅), Ziel: (∅, Rn ) Invariante: →Rk ⊆>A und ≈E0 =≈Ek ∪Rk S Fairness: CP(Rn ) ⊆ k Ek ¨ Regeln (weiter evtl. in Ubung) I I I I deduce: (s ←R u →R t) ⇒ (E, R) ` (E ∪ {s ≈ t}, R) orient: (s >A t) ⇒ (E ∪ {s ≈ t}, R) ` (E, R ∪ {s → t}) delete: (E ∪ {s ≈ s}, R) ` (E, R) simplify: (s →R u) ⇒ (E ∪ {s ≈ t}, R) ` (E ∪ {u ≈ t}, R). Korrektheit? Warum ist einfache Vervollst. ein Spezialfall? ¨ Vervollstandigung heute I Anwendung in Theorembeweisern z.B. http://www.waldmeister.org/ I Competition: http://www.cs.miami.edu/˜tptp/CASC/ Forschung z.B. an U Innsbruck http://cl-informatik.uibk.ac.at/mkbtt/ ¨ ¨ ¨ wahle/ andere Terminationsordnung wahrend der Rechnung I I Veranschaulichung (GUI) http: //cl-informatik.uibk.ac.at/software/kbcv/ Werbung: ISR 2015 8th International School on Rewriting ISR 2015 August 10-14, Leipzig, Germany http://www.imn.htwk-leipzig.de/ISR2015/ I basic course (Prof. Aart Middeldorp, UIBK) I advanced courses (verschiedene) kann als Wahlfach belegt werden wir suche Studenten, die bei Vorbereitung und Durchfuhrung ¨ mithelfen lokale Organisation: A. Geser, J. Waldmann. Teilbarkeit, Ringe, Ideale Wiederholung: fur ¨ ganze Zahlen: I Def. (a | c) := (∃b : a · b = c). Bsp: 2 | 12, −5 | 15 ¨ Ubung: was stimmt: 3 | 0, 3 | 3, 0 | 3, 0 | 0 I ¨ Def. gcd (großter gemeinsamer Teiler) I ¨ Merke: großter“ ist irrefuhrend, es geht nicht um <. ¨ ” Zur Definition wird nur | benutzt. I Bestimmung des gcd durch Algorithmus von Euklid Beachte: jetzt brauchen wir >. Diese Ideen (Begriffe und Algorithmen) sollen verallgemeinert werden (auf Polynome, Vektoren). Algorithmus von Euklid input: a >= 1, b >= 1; // a = A, b = B while (a /= b) { // Invariante: gcd(a,b) = gcd(A,B) // Variante: max (a,b) if a > b then a := a - b else b := b - a } output: a // a = gcd(A,B) Beweis: I I I Termination: die Variante ist ∈ N und streng fallend. Korrektheit: die Invarianz folgt aus gcd(a, a) = a, gcd(a − b, b) = gcd(a, b). Beweise dafur: ¨ mit gcd-Definition. Erweiterter Algorithmus von Euklid Satz: g = gcd(a, b) ⇒ ∃p, q : ap + bq = g Bsp: 3 = gcd(15, 21), p = . . . , q = . . . . Beweis: konstruktiv, (p, q) ausrechnen durch: egcd :: N -> N -> (Z,Z) egcd a b = if b == 0 then ( ... , ... ) else let (d , m) = divMod a b (p’ , q’) = egcd b m in ( ... , ... ) Beweis fur ¨ Algorithms: I Korrektheit nach Konstruktion I Termination durch Variante: . . . Euklid — Zusammenfassung wesentliche Argumente sind: I Korrektheit: Subtraktion von Vielfachen bzw. Berechnung des Restes: Resultat ist im erlaubten Bereich“ ” (ist ein Vielfaches des gcd) I Termination: Rest ist kleiner als Divisor. andere Bereiche, in denen das funktioniert? Ringe Ring (R, 0, 1, +, ·) I I (R, 0, +) ist komm. Gruppe, Distributivgesetz fur ¨ · und + (R, 1, ·) ist Monoid, Bsp fur ¨ Ringe: I I Z, Q, C (nicht: N) R ist Ring ⇒ I I I I Matrizen uber R bilden Ring R d×d ¨ Polynome uber R, in Variable X bilden Ring R[X ]. ¨ Polynome uber R, in Variablen X1 , . . . , Xk bilden Ring ¨ R[X1 , . . . , Xk ]. Vektoren R d ? Nein, denn . . . Ideale I Ring (R, 0, 1, +, ·). Def. Menge I ⊆ R heißt (Links-)Ideal, wenn I + I ⊆ I und R · I ⊆ I. I Bsp: R = Z, I = 2Z = Menge der geraden Zahlen. ungerade Zahlen? nichtnegative gerade Zahlen? I Def: das von einer Menge M erzeugte Ideal: hMi := ¨ das (bzgl. Inklusion) kleinste Ideal, das M enthalt. T (equiv.) {I | I ist Ideal und M ⊆ I} I Bsp: h{2}i in Z? h{15, 21}i in Z? (Schreibweise: h15, 21i) I Def: R heißt Hauptidealring, falls jedes Ideal von einem Element erzeugt wird. Bsp: Z, Q[X ]. ¨ Z[X ]? Kein HI-Ring: Q[X , Y ] (Hinweis: hX , Y i). — U: Euklidische Ringe I Def: (R, | · |) ist Euklidischer Ring, falls | · | : R \ {0} → N und ∀a, b ∈ R : b 6= 0 ⇒ ∃q, r : a = b · q + r ∧ |r | < |b|. I Beispiele: (Z, | · |), (Q[X ], deg). ¨ (Pol. in mehreren Variablen nicht, ⇒ Grobnerbasen) I Def: Euklidischer Algorithmus: (a, b) → (b, r ) → · · · → (g, 0). I Lemma: . . . terminiert und hgi = ha, bi. I Satz: (R, | · |) ist Euklidischer Ring ⇒ R ist Hauptidealring. Beweis: I Sei I Ideal in R. Zu konstruieren ist e mit I = hei. ¨ Wahle e ∈ I \ {0} minimal bzgl. | · |. Zeige: I = hei. I Falls f ∈ I \ hei, dann betrachte Euklid (f , e) 7→ g. I g ∈ hf , ei ⊆ I. I Weil e minimal in I, gilt hgi = hei und f ∈ hei. I Polynom-Division I Satz: ∀a, b ∈ Q[X ] : b 6= 0 ⇒ ∃q, r : a = b·q+r ∧deg(r ) < deg(b) I Beweis: konstruktiv durch Angabe eines Algorithmus. Benutze: a 6= 0 ⇒ a = lc a * lt a + red a mit deg(red a) |b2 |) I Satz: . . . erzeugt LG-reduzierte Basis in poly. Zeit. Korrektheit offensichtlich, Laufzeit: folgt aus |b10 |2 < |b1 |2 /3. Eigenschaften von Gittern I jedes Gitter Γ hat eine Basis B = {b1 , . . . , bn }: ∀x ∈ Γ : ∃c1 , . . . , cn ∈ Z : x = b1 c1 + . . . + bn cn I je zwei Basen B, B 0 fur ¨ Γ gilt: ∃T ∈ Zn×n : B 0 = BT . 0 ¨ (B und B sind aquivalent, B ∼ B0) Dann det T ∈ {−1, 1}. ⇒ folgende Def. ist erlaubt: I Die Determinante eines Gitters det Γ ist | det B| fur ¨ eine beliebige Basis B von Γ. det Γ ist das Volumen des Parallel-Epipeds (Spates) aus den Basisvektoren. Orthogonale Basen (hier alles uber Rn anstatt Zn ) ¨ I Def. Vektoren x, y sind orthogonal, falls hx, y i = 0 I Basis B = [b1 , . . . , bn ] orthogonal: i 6= j ⇒ hbi , bj i = 0 m.a.W., B · B T ist eine Diagonalmatrix. ¨ Satz: Jede Basis B besitzt eine aquivalente orthogonale Basis B ∗ , bestimme B ∗ durch Gram-Schmidt-Orthogonalisierung (GSO) bi∗ := bi − πspan(b1 ,...,bi−1 ) (bi ) nach: I I Satz: fur ¨ µ = hx, y i/hy , y i gilt hx − µy, yi = 0 I Bezeichnung: µi,j := hbi , bj∗ i/hbj∗ , bj∗ i. Bestimmung von det Γ durch GSO I I mit GSO kann man die Determinante eines beliebigen Gitters mit Basis B schnell ausrechnen: bestimme O-Basis B ∗ mit B ∼ B ∗ und Q T det(B ∗ · B ∗ ) = i |bi∗ |2 und det(B ∗ · B ∗ T ) = det(B ∗ ) det(B ∗ T ) = det(B ∗ )2 Q (Hadamard) fur ¨ jede Basis B fur ¨ Γ gilt b∈B |b| ≥ det Γ. Beweis: det Γ = det B = det B ∗ und |bi | ≥ |bi∗ | wg. Projektion ¨ Vektorlangen in Gittern I gegeben: Gitter Γ (durch Basis B). ¨ gesucht: Abschatzung fur ¨ λ := min{|x| : x ∈ Γ \ {0}} I λ ≥ mini |bi∗ | mit {b1∗ , . . .} = B ∗ = GSO(B) I (Minkowski): det Γ ≥ vol Balld (λ/2) = (λ/2)d vol Balld (1) vol Balld (1) ≥ vol W √ √ mit W = Wurfel ¨√ mit Eckenmenge {−1/ d, +1/ d}d vol W = (2/ d)d √ √ aus det √ Γ ≥ (λ/2)d (2/ d)d folgt λ ≤ det Γ1/d d ¨ Faktor d“ kann noch verbessert werden. (evtl. U) ” Gitterbasisreduktion (naiv) direkte Verallgemeinerung von Dimension 2: I I I I I Gitter Γ mit Basis B, while (existieren i 6= j, q ∈ Z \ {0} mit |bi − qbj | < |bi |) do bi := bi − qbj ¨ q so wahlen, daß |bi − qbj | minimiert wird (bestimme Minimum einer quadr. Funktion) Implementierung auf Lattice Reduction Challenge anwenden: fur ¨ d = 200 OK, fur ¨ d ≥ 300 nicht. naive Idee muß modifiziert werden: Algorithmus von Lenstra, Lenstra, Lovasz. LLL-reduzierte Basen (size condition) Idee: reduziere bi bzgl. bj∗ (nicht: bj ) I Gitter Γ, Basis B in Zd , O-Basis B ∗ = GSO(B) in Qd . I Def µi,j = hbi , bj∗ i/hbj∗ , bj∗ i, ¨ Def: B heißt großenreduziert, falls ∀i > j : |µi,j | ≤ 1/2. I I I Algorithmus (size reduction) while (existiert i > j mit |µi,j | > 1/2) do bi := bi − bµi,j e · bj ¨ Satz: diese Alg. liefert eine zu B aquivalente ¨ großenreduzierte Basis . . . in Polynomialzeit (quadratisch) LLL-reduzierte Basen (Lovasz condition) I Def. Lovasz-Bedingung (mit Parameter δ) an Stelle i: |πspan(b1 ,...,bi−1 ) (bi )|2 ≤ δ · |πspan(b1 ,...,bi−1 ) (bi+1 )|2 ¨ |b∗ |2 ≤ δ · |b∗ + µi+1,i b∗ |2 equiv. (U) i i+1 i I ∗ |2 alternativ: |bi∗ |2 ≤ 2|bi+1 (nach V. Shoup, siehe v.z.Gathen: MCA, Notes 16.2) ¨ Algorithmus (LLL): do { großenreduktion; wenn ∃i : ¬Lovaszδ (i), dann bi ↔ bi+1 ; continue } I I liefert (1.) Basis mit kurzen Vektor (2.) in Polynomialzeit LLL-Algorithmus: Korrektheit ¨ 1. Satz: B großenu. Lovasz-reduziert ⇒ |b1 | ≤ 2(d−1)/2 λ(Γ) LLL-Algorithmus: Termination, Laufzeit 2. Satz: der Wert von I I P i log det(span(b1 , . . . , bi )) ¨ ist anfangs beschrankt durch . . . ¨ ¨ bleibt bei Großenreduktion unverandert I sinkt bei Tausch um eine Konstante ¨ (der von δ abhangt - wie? ¨ Daraus ergibt sich der Bereich der fur Werte) ¨ δ zulassigen I ist immer ≥ 0 Folgerung: Laufzeit von LLL ist polynomiell in der Dimension. ¨ Quellen, Erganzungen https://cseweb.ucsd.edu/classes/wi12/ cse206A-a/lec3.pdf http://www.cims.nyu.edu/˜regev/teaching/ lattices_fall_2004/ln/lll.pdf http://www.latticechallenge.org/ ¨ sollte man mal ausprobieren: welche Vektorlangen man durch naive Implementierung der Reduktion erreicht. Akustische Signale (Audiodaten) I ¨ ¨ (physikalisch) Gerausch = Folge von Luftdruckanderungen ¨ . . . die sich wellenformig ausbreitet und (u.a.) vom Ohr wahrgenommen wird I (mathematisch) Abbildung von R (Zeit) nach R (Druck) I (informatisch) Bsp. Audio-Synthese Audiosynthese mit Csound I Barry Vercoe, MIT Media Lab, 1968: Music 360, 1973: Music 11, 198*: Csound, http://www.csounds.com/ Software-Synthesizer I Anton Kholomiov: https://hackage.haskell.org/ package/csound-expression Haskell-API fur ¨ csound ghci :m + Csound.Base Csound.IO dac $ osc 440 -- Audio-Ausgabe renderCsd ( osc 440 ) >>= putStrLn -- Quelltext Partituren verwendet: I ¨ Atome: Note (Dauer, Hohe) und Pause (Dauer) I Verknupfungen: nacheinander, wiederholt, gleichzeitig ¨ Werkzeuge (Beispiele): I Han-Wen Nienhuys, Jan Nieuwenhuizen (2003) http://www.lilypond.org/pdf/xivcim.pdf I Paul Hudak, . . . : Haskore Music Notation — An Algebra of Music, JFP 1995 http://citeseerx.ist.psu.edu/ viewdoc/summary?doi=10.1.1.36.8687 Paul Hudak, Henning Thielemann: https://hackage.haskell.org/package/haskore An Algebra of Music (Semantik) Modul haskore-vintage:Haskore.Performance die semantische Algebra: I I Grundbereich: Musikstucke ¨ (als Folge von Ereignissen, monoton nach Zeitpunkt) data Event = Event {eTime::Time, eDur::DurT , ePitch::AbsPitch, eVol::Volume} type Performance = [Event] Operationen: I I I herstellen: Noten, Pausen verknupfen: nacheinander (++), nebeneinander merge ¨ bearbeiten: Tempo skalieren, transponieren An Algebra of Music (Syntax, Interpretation) die syntaktische Algebra (Term-Algebra) data Music = Note Pitch Dur [Attribute] | Rest Dur | Music :+: Music | Music :=: Music | Tempo (Ratio Int) Music | Transpose Int Music die Interpretationsfunktion perform :: PMap -> Context --> Music --> Performance -let m = Note (C,4) 1 [] let p = perform defPMap defCon let s = performToMidi p defUpm outputMidiFile "test.midi" s ˆ Parameter ˆ Syntax ˆ Semantik m An Algebra of Music (Eigenschaften) Beispiele: I nacheinander“ ist assoziativ : ” perform pmap ctxt (a :+: (b :+: c)) == perform pmap ctxt ((a :+: b) :+: c) I Transpose t ist Homomorphismus: . . . Diskutiere: I neutrale Elemente? I kommutativ? I distributiv? (wer uber wen? von links, von rechts?) ¨ I ist Performance ein Halbring? Partitur und Auffuhrung ¨ perform :: ... -> Music -> Performance I Komponist Rhys Chatham, http://www.rhyschatham.net/ http://www.allmusic.com/artist/mn0000759643 Guitar Trio (1977) sieht so aus: Note (C,2) 1 [] und dauert 30 min. eingespielt z.B. von Band Of Susans auf LP The Word and The Flesh 1991. I John Cage (1912-1992): As Slow As Possible wird seit 2001 in Halberstadt aufgefuhrt ¨ http://www.aslsp.org/, wird 639 Jahre dauern, ¨ nachster Klangwechsel: 5. September 2020. ¨ Strome I Semantik: (unendliche) Folge von Werten (z.B. Noten) I Realisierung I I Software: OO: Iterator, funktional (lazy) : data Stream a = Cons a (Stream a) Mathematik: I I I im Bereich Formale Sprachen: ω-Wort, s ∈ Aω = {f | f : N → A} im Bereich Algebra: formale Potenzreihe P S(x) = s0 + s1 x 1 + s2 x 2 + . . . = i∈N si x i Analysis: S heißt die erzeugende Funktion fur ¨ s Herbert Wilf: Generatingfunctionology (1990), http: //www.math.upenn.edu/˜wilf/DownldGF.html ¨ Rechnen mit Stromen (I) data Stream a = Cons a (Stream a) Spezifikation und Verarbeitung durch Gleichungssysteme: Beispiele: I o :: Stream Int ; o = Cons 1 o P erz. Fkt. o = 1 + x · o, o = 1/(1 − x), o = i∈N 1 · x i I map :: (a -> b) -> Stream a -> Stream b map f (Cons x xs) = Cons (f x) (map f xs) s = Cons 1 (map (\ c -> c + 1) s) erzeugende Funktion s = 1 + x · (o + s) ¨ Rechnen mit Stromen (II) data Stream a = Cons { head :: a, tail :: Stream a } zipWith :: (a -> b -> c) -> Stream a -> Stream b -> Stream c zipWith f (Cons x xs) (Cons y ys) = Cons (f x y) (zipWith f xs ys) f = Cons 0 (Cons 1 (zipWith (+) f (tail f))) geschlossener (algebraischer) Ausdruck fur ¨ erzeugende Funktion? Die Papier-Falt-Folge I Definition: f0 = Papierstreifen fk + 1 = falte fk nach links, so daß rechtes Ende auf linkem Ende landet. I Anfangswerte: f0 = , f1 = 1, f2 = 110, f3 = 1101100, . . . I Eigenschaften: I I I fk +1 = fk · 1 · . . . ¨ von fk+1 , damit exist. f := (limk fk ) ∈ {0, 1}ω fk ist Prafix f = merge((10)ω , f ) merge (Cons x xs) ys = Cons x (merge ys xs) zz = Cons 1 (Cons 0 zz) ; f = merge zz f I f ist uberschneidungsfreier Pfad (1 = links, 0 = rechts) ¨ Klassische Musiktheorie I (Bsp.) die Papier-Falt-Folge f kann man als Tonfolge: ¨ das klingt: unregelmaßig, aber langweilig (weil ziellos) I wodurch wird eine Tonfolge zu Musik? dadurch, daß sie einen Komponisten und einen Interpreten ¨ hat, der ein Gefuhl bzw. beim Horer ¨ ausdrucken ¨ hervorrufen will. I ¨ Wollen reicht aber nicht (Kunst kommt von Konnen, . . . ), es gibt Regeln, die beschreiben, ¨ wann Tone wohlklingen (Harmonie, Akkorde) und Tonfolgen spannend sind (Kontrapunkt, Stimmfuhrung) ¨ Leipziger Musikpraktiker und -Theoretiker I Johann Sebastian Bach (1685–1750) http://www.bachmuseumleipzig.de/, http://imslp.org/wiki/Bach-Gesellschaft_ Ausgabe_(Bach,_Johann_Sebastian) I Hugo Riemann (1849–1919) (Hugo-Riemann-Straße: Floßplatz — Bayrischer Platz) Handbuch der Harmonie- und Modulationslehre (1905) https: //archive.org/details/handbuchderharmo00riem Lehrbuch des einfachen, doppelten und imitierenden Contrapunkts (1908) https: //archive.org/details/lehrbuchdeseinfa1908riem Mathematische Musiktheorie ¨ (1990) Guerino Mazzola: Die Geometrie der Tone I Differentialgeometrie: M ist Mannigfaltigkeit: I I ¨ sich durch lokale Karten uberdecken M laßt ¨ (∀x ∈ M : Umgebung von x sieht aus wie ein Rd ) uberlappende Karten passen (diff.bar) zusammen ¨ Motivation in der Mathematik: exakte √ Definition mehrdeutiger Funktionen“, z.B. x 7→ x in C. ” ¨ Riemannsche Flache (Bernhard Riemann, 1826–1866) I musikalische Komposition als Mannigfaltigkeit: I I die lokalen Karten sind Akkorde, A1 paßt zu A2 , wenn A1 ∩ A2 6= ∅ (das ist eine sehr stark vereinfachte Darstellung) Literatur Mathem. Musiktheorie I ¨ ¨ Guerino Mazzola: Geometrie der Tone, Birkhauser 1990. (https://zbmath.org/?q=an:0729.00008) I Thomas Noll: Ist der Tonraum flach oder gekrummt?, Berlin ¨ 2001, http://www.visual-geometry.de/unheard/ materialien/skripte/Tonraum/Tonraum30.11.html I Gerhard Nierhaus: Algorithmic Composition, Springer 2009. (http://www.computermusicjournal.org/ reviews/34-3/doornbusch-nierhaus.html) I Christian Krattenthaler: Musik und Mathematik, http://www.mat.univie.ac.at/˜kratt/artikel/ musimath.html Intern. Math. Nachrichten 224(2013) 29-60, http://www.oemg.ac.at/IMN/ Quelltexte die Beispiele aus der Vorlesung: https://git.imn.htwk-leipzig.de/ws14-code/sr git clone https://git.imn.htwk-leipzig.de/ws14-code/ cd sr cabal sandbox init cabal install cabal haddock --executable --hyperlink-source cabal repl Themen und Prinzip symbolisches Rechnen: I nur Syntax: Terme, Termersetzungssysteme I . . . mit Semantik: I I I I Polynome, algebraische Zahlen Gitter, Vektoren Geometrie Musik Prinzip: beantworte semantische Fragen durch syntaktische Umformungen. (Menge der Umformungsregeln: Kalkul.) ¨ Umformungen I I abstrakt: Termination, Konfluenz (lokal, global), Normalformen konkret I I I fur ¨ Terme: (literale) Ersetzungsrelation, wohlfundierte monotone Algebra, Polynominterpretation, kritische Paare, ¨ Vervollstandigung fur ¨ Vektoren: ¨ Großenreduktion, Lovasz-Reduktion, L3 -Algorithmus fur ¨ Polynome/arithmetische Ausdrucke: ¨ (algebraische) Ersetzung, Simplifikator, Rechnen m. algebr. ¨ Zahlen, zulassige Termordnung, S-Polynome, Buchberger-Algorithmus, Euklid als Spezialfall Anwendungen der Algorithmen I Vervollst.-Algorithmus ⇒ Wortproblem entscheiden ⇒ (Gleichungs-)Theorem beweisen I L3 -Algorithmus ⇒ kurzen Gittervektor finden ⇒ Minimalpolynom finden, (Nachricht entschlusseln, Polynom faktorisieren) ¨ I arithm. Ausdruck simplifizieren (auf 0 testen) ⇒ geometrisches Theorem (v. rationalen konstruktiven Typ) beweisen I ¨ Grobnerbasis ausrechnen ⇒ Idealmitgliedschaft entscheiden ⇒ geometrisches Theorem (v. Gleichungstyp) beweisen ¨ Was (konnte der aufgeweckte Student hier noch) tun? I autotool-Aufgaben dokumentieren, verbessern, erweitern https://autotool.imn.htwk-leipzig.de/cgi-bin/ Trial.cgi?lecture=214 I I I I I abstrakte und Termersetzung ¨ Polynome (Euklid, Grobner) Gitter Geometrie (!) geometrische Geradeausprogramme/Theoreme http://autolat.imn.htwk-leipzig.de/gitweb/?p= tool;a=tree;f=collection/src/Geo;hb=for-ghc-7.8 I Intl. School on Rewriting (10.–14. August) http://www.imn.htwk-leipzig.de/ISR2015/