Symbolisches Rechnen Vorlesung Wintersemester 2006, 2014

Symbolisches Rechnen
Vorlesung
Wintersemester 2006, 2014
Johannes Waldmann, HTWK Leipzig
11. Dezember 2015
Symbolisches Rechnen: Definition
I
Rechnen mit Funktionen.
(mit Ausdrücken, 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) üblich: der Binder (λ) wird nicht
notiert, die gebundenen Variablen sehen dadurch frei aus:
expand((x+1)ˆ2);
Symbolisches Rechnen: Motivation
hat weitreichende Anwendungen:
I
I
I
Lösen von (parametrisierten) Aufgabenklassen
(für numerisches Rechnen muß Parameter fixiert werden)
exaktes Lösen von Aufgaben
(numer. R. mit Maschinenzahlen: nur Approximation)
experimentelle, explorative, exakte Mathematik
ist nützlich im Studium, benutzt und vertieft:
I
I
I
Mathematik (Analysis, Algebra)
Algorithmen-Entwurf, -Analyse
Prinzipien von Programmiersprachen
Überblick
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, Gröbnerbasen
Geometrische Konfigurationen und Beweise
Ausblick (2): Musik-Notationen, Beweisüberprüfer, . . .
Literatur
I
Wolfram Koepf: Computeralgebra, Springer, 2006. http:
//www.mathematik.uni-kassel.de/˜koepf/CA/
I
Hans-Gert Gräbe: Einführung in das Symbolische
Rechnen, Gröbnerbasen und Anwendungen, Skripte,
Universität Leipzig http://www.informatik.
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 fü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, http://citeseerx.ist.psu.edu/viewdoc/
summary?doi=10.1.1.31.9447
I
Korrektheit? Termination? Komplexität?
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
füge Syntax und Regel für Quotienten hinzu
schlage Regeln zur Vereinfachung vor
p
√
verifziere diese Behauptung für 2 + 3
Mixed constants with 5 operations
1931851652578136 = 1/2/sin(Pi/12)
√
√
2
bestimme ein Polynom mit Nullstelle 2 + 3 3
Übung 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 für die nähere Zukunft
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:
Termbäume, 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 <u (up) und <l
(left).
Def: ein Term t über Signatur Σ ist Abbildung von einem
Baumbereich P nach Σ
Einsetzen an Position
I
t[p := s] in t an Position p den Term s einsetzen
Übung: definiere das exakt:
I
für Term als Zeichenketten
I
für Term als Abbildung von Baumbereich
Variablen, Substitutionen
I
I
I
I
I
Term(Σ, V ): Menge der Terme mit Symbolen aus Σ und
Variablen aus V .
Vereinbarung: Variablen am Ende des Alphabets (x, y, . . .),
Funktionssymbole am Anfang (f , g, a, b, . . .)
Menge der in einem Term t vorkommende Variablen: Var(t)
Substitution σ ist Abbildung V → Term(Σ, W )
eine Substitution σ angewendet auf einen Term t erzeugt
Term tσ
Beispiel t = f (x), Var(t) = {x}, σ : x 7→ p(0, 0),
tσ = f (p(0, 0)).
Regeln
I
Regel (l, r ), Schreibweise (l → r ), mit l, r ∈ Term(Σ, V )
I
Regel (l → r ) an Position p in t ∈ Term(Σ) anwenden, um
s zu erhalten, Schreibweise t →(l→r ),p s
∃σ : V → Term(Σ) : t|p = lσ ∧ t[p := r σ] = s
Beispiel: Regel (l, r ) = (f (x), g(x, x)), Term t = h(1, f (f (2))).
Position p = [2] ∈ Pos(t), Teilterm t|p = f (f (2)),
Substitution σ : x 7→ f (2) mit t|p = lσ,
auf r anwenden: r σ = g(f (2), f (2)),
in t einsetzen: s = t[p := r σ] = h(1, r σ) = h(1, g(f (2), f (2))).
Regelsysteme
I
I
R eine Menge von Regeln, definiert Relation (einmalige
Anwendung irgendeiner Regel irgendwo):
→R := {(t, s) | ∃(l, r ) ∈ R, p ∈ Pos(t) : t →(l,r ),p s}
transitive Hülle →+
R (mehrmalige Regelanwendung)
liefert nichtdeterministisches Berechnungsmodell (vgl.
Grammatiken/Wortersetzungssysteme)
Fragen:
I
I
jede Rechnung endet? (Termination) nach welcher Zeit?
jede Rechnung endet mit genau einem Resultat?
dabei: Resultat = Term, auf den keine Regel anwendbar ist =
Normalform.
Aufgaben
Signatur (mit Stelligkeiten): Σ = {e0 , s1 , p2 , m2 , h2 }
I
I
I
Rp = {p(e, y) → y , p(s(x), y) → s(p(x, y))}
Rm = Rp ∪ {m(e, y ) → e, m(s(x), y ) → p(m(x, y), y)}
Rh = Rm ∪ {h(x, e) → s(e), h(x, s(y )) → m(h(x, y ), x)}
Fragen (leicht):
Menge der Rh -Normalformen?
Normalformen (Existenz? Eindeutigkeit?) von:
p(s(p(s(e), s(e))), s(e)), m(s(s(e)), s(s(e))),
h(s(s(e)), s(s(s(e)))).
(schwerer) Σ = {a2 , d 0 }, R = {a(a(d, x), y ) → a(x, a(x, y ))}:
Normalformen? Ableitungslängen?
I
I
Termersetzung/Anwendungen
Termersetzung ist
I
I
I
I
Turing-vollständiges Berechnungsmodell
Grundlage für funktionale Programmierung
Grundlage für Symbolisches Rechnen
(Grundlage für XML-Transformationen mit XSLT, . . . )
Für Anwendungen wichtig sind
I
I
I
Termination (keine unendlich langen Rechnungen)
Konfluenz (eindeutige Ergebnisse von Rechnungen)
Ableitungskomplexität (Länge von Rechnungen als
Funktion der Startgröße)
Term-Ersetzung und Computeralgebra
Regeln (Term-Ersetzungs-System) für das Differenzieren:
Dx (x) = 1, wenn x ∈
/ A : Dx (A) = 0
Dx (A + B) = Dx (A) + Dx (B)
Dx (A · B) = . . . , Dx (A/B) = . . .
Dx (log x) = 1/x, Dx (sin x) = cos x, . . .
Dazu braucht man aber noch Vereinfachungsregeln.
Wie drückt man die Kettenregel Dx (f (g(x)) = . . . aus?
Hier sind f und g Variablen, aber zweiter Ordnung (bezeichnen
Funktionen).
Regeln für das Integrieren?
Existenz und Eindeutigkeit von Normalformen?
Termination und Normalisierung
Für eine zweistellige Relation ρ auf M
(zum Beispiel eine Ersetzungsrelation →R auf Term(Σ))
I
ρ ist terminierend (stark normalisierend), falls es keine
unendliche lange ρ-Folge gibt
d. h. ρ(x0 , x1 ), ρ(x1 , x2 ), ρ(x2 , x3 ), . . .
I
ρ is schwach normalisierend, falls zu jedem x0 ∈ M eine
ρ-Folge zu einer ρ-Normalform führt
Beachte: es gibt ρ, die schwach, aber nicht stark normalisieren.
Normalformen
Für eine zweistellige Relation ρ auf M
(zum Beispiel eine Ersetzungsrelation →R auf Term(Σ))
heißt x ∈ M eine ρ-Normalform, falls ¬∃y ∈ M : ρ(x, y).
Beachte: für passende ρ und x kann vorkommen:
I
p hat mehrere Normalformen
I
p hat keine Normalform
Übung Termersetzung
I
I
Der Ellipse 9 x 2 + 16 y 2 = 144 soll ein flächenmäßig
möglichst großes Rechteck einbeschrieben werden,
dessen Seiten parallel zu den Koordinatenachsen liegen.
Bestimmen Sie die Abmessungen dieses Rechtecks.
Lösung (Vorschlag):
f : subst
( [solve(9*xˆ2+16*yˆ2=144,y) [2]], x*y );
plot2d (f, [x, -4, 4]);
solve ( diff(f,x),x );
Definitionen Termersetzung,
Definiere t 0 = t[p := s] mittels Baumbereichen:
I
I
I
Variante A: Funktion als Menge von geordneten Paaren
t 0 = t \ {(p · q, z) | q ∈ N∗ } ∪ {(p · q, z) | (q, z) ∈ s}
Variante B: Funktion als Berechnungsvorschrift
t 0 (q) = if p ≤up q then s(p \ q) else t(q)
mit (partieller) Funktion p \ q (Linksdivision): wenn p · r = q,
dann r , sonst ⊥, Bsp: 12 \ 1231 = 31
Struktur von Termen ansehen
Maxima-Trainingsaufgaben
Dreicksgeometrie, Standardbezeichnungen c = AB, usw.
I bestimme die Höhe hc (auf der Seite c). Ansatz: hc teilt c
in p + q:
solve([pˆ2+hˆ2=bˆ2,qˆ2+hˆ2=aˆ2,p+q=c],[p,q,h]);
I bestimme daraus die Fläche des Dreiecks als Fkt. von
a, b, c
I bestimme daraus den Inkreisradius r .
I berechne den Umkreisradius R.
Ansatz: der Umkreismittelpunkt O(c/2, y) hat von A(0, 0)
und C(p, hc ) den gleichen Abstand R.
Gleichungssystem für R, y unter Verwendung (d.h.
Substitution) von hc , p.
Oder: O liegt auf der Mittelsenkrechten von AC.
I beweise R ≥ 2r . Wann gilt Gleichheit?
Beweise explizit, daß Multiplikation von 3 × 3-Matrizen
assoziativ ist.
I Matrix-Konstruktion mit
genmatrix (lambda([i,j],i*j), 3, 3)
Gleichungssysteme (Syntax)
Def: ein Gleichungssystem E über einer Signatur Σ ist eine
Menge von Paaren (l, r ) ∈ Term(Σ, V )2 , geschrieben l ≈ r
∗
Def: die Relation ≈E ist (→E ∪ →−
E) .
5
3
Bsp: E1 = {f (a) ≈ a, f (a) ≈ a}. Zeige f (a) ≈E1 a.
Bsp: E2 = {f (f (x)) ≈ g(x)}. Zeige f (g(x)) ≈E2 g(f (x)).
Bsp: Die Relation ≈Di ist entscheidbar für
I
I
D1 = {f (f (x, y ), z) ≈ f (x, f (y, z))}
D2 = {f (f (x, y), z) ≈ f (x, f (y, z)), f (x, y) ≈ f (y , x)}
≈C ist nicht entscheidbar für C = {A(A(K , x), y) ≈ x,
A(A(A(S, x), y ), z) ≈ A(A(x, z), A(y , z))}
Algebren (Semantik)
Def. eine Algebra A zur Signatur Σ ist: eine Menge (domain) DA
und für jedes k-stellige c aus Σ eine Funktion [c]A : D k → D.
Bsp. Σ = {P/2, S/1, Z /0}, D = N,
[P](x, y ) = x + y, [S](x) = x + 1, [Z ] = 0.
Def: Wert eines Terms t ∈ Term(Σ, V ) in A
unter Belegung α : Var(t) → D, Notation [t, α]
Bsp. [P(S(Z ), a), {(a, 5)}] = 6
beachte verschiedene Wortbedeutungen von Algebra“:
”
I “high school algebra”: Umformen von Ausdrücken.
I lineare, höhere, usw. Algebra: untersucht Polynome usw.
I abstrakte Algebra: allgemein Mengen mit Operationen.
Modelle
Def. eine Gleichung l ≈ r ist gültig in einer Σ-Algebra
A = (DA , [·]A ), geschrieben A |= l ≈ r , falls für jede Belegung
α : Var(l) ∪ Var(r ) 7→ DA gilt: [l, α] = [r , α]
Def. eine Σ-Algebra (D, [·]) heißt Modell
für ein Gls. E über Σ, wenn ∀(l ≈ r ) ∈ E : A |= l ≈ r .
Bsp: [P](x, y ) = x + y, [S](x) = x + 1, [Z ] = 0 ist Modell für
E = {P(Z , y ) ≈ y , P(S(x), y ) ≈ S(P(x, y ))}.
Übung: gibt es andere Modelle dafür?
Syntaktische u. semantische Äq. von Termen
Bsp. E = {P(Z , y) ≈ y , P(S(x), y) ≈ S(P(x, y))}.
I
syntaktische Äquivalenz: ≈E
I
semantische Äquivalenz: E |= s ≈ t
I
I
I
Def. E |= s ≈ t: für jedes Modell A von E gilt A |= s ≈ t.
Bsp: E |= P(S(S(Z )), y) ≈ S(S(y )).
Übung: gilt E |= P(x, y ) ≈ P(y , x)?
Satz (Birkhoff): s ≈E t ⇐⇒ E |= s ≈ t.
Gleichungstheoreme und induktive Th.
Bsp. E = {P(Z , y) ≈ y , P(S(x), y) ≈ S(P(x, y))}.
Gilt E |= P(x, y ) ≈ P(y, x)?
Nein. Betrachte[S](x)
Modell A
N:2 +[Z
= 0,1
= fürif E2|xüber
then
x ]else
[P](x, y) = if 2|x then x + y else 1
A 6|= P(x, y) ≈ P(y , x), betrachte α = {(x, 2), (y , 1)}.
Nach Satz von Birkhoff folgt P(x, y) 6≈E P(y , x).
Beachte: ¬∃t ∈ Term(Σ, ∅) : [t]A = 1.
Für alle s, t ∈ Term(Σ, ∅) gilt P(s, t) ≈E P(t, s).
Sprechweise: P(x, y ) ≈ P(y, x) ist ein induktives Theorem in E
(aber kein Gleichungs-Theorem)
Aufgaben
I
I
I
I
Für E = {aba(x) ≈ x}: gilt abbbaa(x) ≈E bba(x)?
F = {f (x, f (y, z)) ≈ f (f (x, y ), z), f (e, x) ≈ x, f (i(x), x) ≈
e}. Zeige f (x, e) ≈F x.
G = {f (x, f (y , z)) ≈ f (f (x, y), z), f (f (x, y ), x) ≈ x}. Zeige
f (x, x) ≈G x und f (f (x, y), z) ≈G f (x, z)
H = {f (x, f (y, z)) ≈ f (f (x, y ), z), f (e, x) ≈ x, f (x, i(x)) ≈
e}. Zeige f (x, e) 6≈H x.
Quellen: http://www.cs.vu.nl/˜tcs/trs/,
Franz Baader und Tobias Nipkow: Term Rewriting and All That,
http://www21.in.tum.de/˜nipkow/TRaAT/
Autotoolisierung dieser Aufgaben? (zwei Fälle)
Motivation
gibt es unendliche Ableitungen in den Systemen
I
I
I
I
ba → ab, ba → aab, 100 → 00110
A(A(D, x), y) → A(x, A(x, y ))
Regeln zum symbolischen Differenzieren
Regeln zum Vereinfachen arithmetischer Ausdrücke usw.
vgl: warum und wie wird iterierte Regelanwendung
(tellsimp,tellsimpafter) in Maxima verhindert?
Anwendung (später): Vervollständigungs-Algorithmus
I
I
zum Entscheiden der syntaktischen Kongruenz ≈E
zum E. des Polynom-Ideal-Problems: Q ∈ hP1 , P2 , . . .i
Quellen
I
Zohar Manna and Steven Ness: On the termination of
Markov algorithms, 1970.
Dallas Lankford: On Proving term rewriting systems are
Noetherian, 1979.
siehe http://perso.ens-lyon.fr/pierre.lescanne/
not_accessible.html#termination
I
Nachum Dershowitz: 33 Examples of Termination, 1995.
http://www.math.tau.ac.il/˜nachumd/papers/
printemp-print.pdf
TeReSe (Lite), VU Amsterdam, 2008.
http://www.cs.vu.nl/˜tcs/trs/ (Lect. 5, 6)
Monotone Algebren, Interpretationen
Beispiel:
I
I
I
I
Regel ba → aab
Ableitung bba → baab → aabab → aaaabb
Interpretation in N: [a](x) = x + 1, [b](x) = 3x, [] = 0
[baa] = 9 > [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
Kompatibilität: ∀(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 über N, überprüfe Eigenschaften.
Welche liefert einen Terminationsbeweis für 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 für
R ∪ {M(Z , y) → Z , M(S(x), y ) → P(M(x, y), y )}
Aufgabe: . . . für A(A(D, x), y) → A(x, A(x, y))
Merke: kompatibel: links > rechts, Modell: links = rechts,
Systematik wfmA
Beispiele benutzten lineare Funkt. über N. Erweiterungen:
I
I
I
Polynome über N
lineare Funktionen (Matrizen) über Nd
. . . über anderen Halbringen, wie ({−∞} ∪ N, max, +)
für jedes solche Klasse von Algebren möchte man lösen:
das Verifikations-Problem:
I
Monotonie, Kompatibilität mit R
das Synthese-Problem:
I
gegeben R, gesucht R-kompatible wfmA
(z.B. Lösen des Constraint-Systems für Koeffizienten)
siehe http://www.termination-portal.org/
Aufgaben
(evtl. autotool) bestimme wfmAs für
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 für lineare Interpretationen (über
N, über Nd ) ist entscheidbar
das Syntheseproblem für lineare Interpretationen mit
Anstieg 1 (d.h. [f ](x1 , . . . , xk ) = x1 + . . . + xk + cf ) ist
entscheidbar.
Motivation
gesucht ist Entscheidungsverfahren für das Wortproblem:
I
Eingabe: E über Σ, 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 für s ≈E t
Plan: Vergleich der →E -Normalformen von s, t.
Probleme: 1. Existenz und 2. Eindeutigkeit der Nf.
Lösung:
I
(Ziel): 1. Termination und 2. Konfluenz
I
(Verfahren): Vervollständigung.
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
höchstens eine ρ-Normalform.
I
Beachte: es wird nicht behauptet, daß x überhaupt eine
Normalform besitzt.
Falls ρ jedoch terminiert, dann läßt sich Konfluenz
charakterisieren und entscheiden durch einen Hilfsbegriff
(lokale Konfluenz, später)
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
Überlappungen 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 über 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 )
Für den Fall mehrerer Unifikatoren möchte man bestimmte
auswählen. (⇒ vollst. Def. nächste 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 lösbar
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, übersichtlich, aber nicht effizient,
es gibt Unif.-Probl. mit exponentiell großer Lösung (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
Für ein Termersetzungssystem R über Σ: falls
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 zusammenführbar, falls
∃u : s →∗R u ∧ t →∗R u.
Satz: ein Termersetzungssystem ist genau dann lokal
konfluent, wenn alle kritische Paare zusammenführbar sind.
Orthogonale Systeme
I
ein TES R über Σ heißt nichtüberlappend, 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
nichtüberlappend ist.
Satz: jedes orthogonale System ist konfluent.
Funktionale Programmierung ≈ System R ist orthogonal und
. . . (nächste Folie)
Konstruktor-Systeme
I
Für TES R über Σ: ein Symbol f ∈ Σ heißt definiert, wenn
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.
Vervollständigung (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: zusätzliche 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
wähle s0 ∈ NfRi (s), t 0 ∈ NfRi (t)
falls s0 6= t 0 , ordne (s0 , t 0 ) bzgl. >A .
Korrektheit? Termination? beachte: 3 Fehlermöglichkeiten
Vervollständigung (improved)
bei einfacher Vervollständigung:
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 können
I
so daß das umgeformte Paar orientierbar ist
(nichtdeterministischer) Vervollständigungsalgorithmus wird
formuliert mittels Inferenzsystem
Inferenzsystem für Vervollständigung
(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 Übung)
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?
Vervollständigung 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/
wähle/ändere Terminationsordnung während 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 Durchführung
mithelfen
lokale Organisation: A. Geser, J. Waldmann.
Teilbarkeit, Ringe, Ideale
Wiederholung: für ganze Zahlen:
I
Def. (a | c) := (∃b : a · b = c).
Bsp: 2 | 12, −5 | 15
I
Übung: was stimmt: 3 | 0, 3 | 3, 0 | 3, 0 | 0
I
Def. gcd (größter gemeinsamer Teiler)
Merke: größter“ ist irreführend, 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 dafür: 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 für 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 für · und +
(R, 1, ·) ist Monoid,
Bsp für Ringe:
I
I
Z, Q, C (nicht: N)
R ist Ring ⇒
I
I
I
I
Matrizen über R bilden Ring R d×d
Polynome über R, in Variable X bilden Ring R[X ].
Polynome über 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 enthält.
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 ].
Kein HI-Ring: Q[X , Y ] (Hinweis: hX , Y i). — Ü: Z[X ]?
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, ⇒ Gröbnerbasen)
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.
I
Wähle 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.
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)<deg a (Vereinbarung:deg(0) = −∞)
a : b =
if deg a < deg b then (0, a) else
let t = (lc a / lc b) * Xˆ(deg a - deg b)
(q,r) = (red a - t * red b) : b
in (t + q, r)
I
(x 10 − 1) : (x 4 − 1) = . . . Rest . . .
I
gcd(x 10 − 1, x 4 − 1) = . . . = . . . · (x 10 − 1) + . . . · (x 4 − 1)
Euklid für Vektoren?
I
im folgenen Abschnitt (Gitter) ist der Grundbereich eine
Menge von Vektoren
I
die wesentliche algorithmische Idee ist ebenfalls:
oft genug einen vom anderen abziehen,
”
um einen kurzen Vektor zu erhalten“
I
der Bereich ist kein Ring
(man kann Vektoren addieren, aber nicht multiplizieren),
I
. . . aber ein Modul
(man kann Vektor mit Skalar multiplizieren)
I
wir betrachten als interessante Teilmengen:
nicht Ideale, sondern Gitter.
Definitionen, Beispiele
Def. Gitter Γ ⊆ Zd ist diskrete additive Gruppe
I
diskret: ∀r ≥ 0 : | Balld (r ) ∩ Γ| < ∞,
I
d-dimensionale Kugel: Balld (r ) = {x ∈ Rd : |x| ≤ r }.
I
additive Gruppe: x, y ∈ Γ ⇒ (x + y ) ∈ Γ ∧ (x − y ) ∈ Γ.
Bsp:
Γ1 = {(x1 , x2 , x3 ) | x1 + x2 + x3 ≡ 0 (mod 5)}
Γ2 = {c1 · (4, 0, 1) + c2 · (4, 1, 0) + c3 · (5, 0, 0) | c1 , c2 , c3 ∈ Z}
Γ3 = {d1 · (1, −1, 0) + d2 · (0, 1, −1) + d3 · (4, 0, 1) | d1 , d2 , d3 ∈ Z}
Diese Gitter sehen verschieden aus, sind aber gleich!
Bsp: für v = (4, 7, −1) zeige v ∈ Γ1 , v ∈ Γ2 , v ∈ Γ3 .
Short(est) Vector Problem SVP
I
I
Eingabe: (eine Basis B für) ein Gitter Γ, eine Zahl D
Ausgabe:
ein Vektor v ∈ Γ \ {0} mit |v | ≤ D, falls existiert.
Beweis für v ∈ Γ durch c ∈ Zd mit v = c · B
Komplexität ist hoch
I
I
man kann damit Geheimnisse verstecken
effiziente Näherungsverfahren sind interessant
Anwendungen (außer Krypt.) bei
I
I
Faktorisieren v. Polynomen , • ganzzahliger Optimierung
Bestimmen von (Minimal)Polynomen für algebraische
Zahlen, die nur numerisch approximiert vorliegen
Gitter zur Best. v. Min.-Polynomen
gegeben: α ∈ R, B ∈ N, ∈ R
gesucht: Polynom p ∈ Z[X ] mit Koeffz ≤ B und |p(α)| ≤ Ansatz: wähle d ∈ N, F ∈ N groß genug
und bestimme kurzen Vektor inGitter mit Basis



1 0 0 0 0 10000
1 0 ... 0
F
0 1 0 0 0 31462 
0 1 . . . 0 bF αc 




0 0 1 0 0 98989 


.


.


.
0 0 0 1 0 311448
0 0 . . . 1 bF αd c
0 0 0 0 1 979897
Bsp: α = 3.14626, d = 4, F = 104
Kurzer Vektor? (Hinweis: letzte Komponente: 7)
Wie kann man aus diesem Vektor das Polynom ablesen?
SVP-Algorithmen (Ansatz)
I
I
man bestimmt nicht nur einen kurzen Vektor in Γ,
sondern eine Basis aus kurzen Vektoren.
Man transformiert die gegebene Basis schrittweise.
In jedem Schritt wird ein Basisvektor bi ersetzt durch
bi0 = bi − mbj für ein geeignetes m ∈ Z mit |bi0 | < |bi |.
zu untersuchen sind
I
I
I
Korrektheit (Teil 1) — trivial, jederzeit bi ∈ Γ
Strategie (Auswahl von i, j) und Laufzeit
Korrektheit (Teil 2) — wenn so kein Vektor b mit |b| < D
gefunden wird, gibt es dann überhaupt keinen?
Ziel: guter Trade-Off zw. Genauigkeit und Geschwindigkeit.
Gitterbasisreduktion in 2D (evtl. Ü)
Bsp: h(12, 2), (13, 4)i
I
Def: B = [b1 , b2 ] ist Lagrange-Gauß-reduziert,
falls ∀q ∈ Z : |b1 | ≤ |b2 | ≤ |b2 + qb1 |.
I
Satz: [b1 , b2 ] LG-reduz. B. für Γ ⇒ b1 ist kürzester V. in Γ.
I
Algorithmus:
do { µ = hb2 , b1 i/hb1 , b1 i; (b2 , b1 ) := (b1 , b2 − bµeb1 )
} while (|b1 | > |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 für Γ gilt: ∃T ∈ Zn×n : B 0 = BT .
(B und B 0 sind äquivalent, B ∼ B 0 )
Dann det T ∈ {−1, 1}. ⇒ folgende Def. ist erlaubt:
I
Die Determinante eines Gitters det Γ ist | det B| für eine
beliebige Basis B von Γ.
det Γ ist das Volumen des Parallel-Epipeds (Spates) aus
den Basisvektoren.
Orthogonale Basen
(hier alles über 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.
I
Satz: Jede Basis B besitzt eine äquivalente orthogonale
Basis B ∗ , bestimme B ∗ durch
Gram-Schmidt-Orthogonalisierung (GSO)
bi∗ := bi − πspan(b1 ,...,bi−1 ) (bi ) nach:
I
Satz: für µ = 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) für jede Basis B für Γ gilt b∈B |b| ≥ det Γ.
Beweis: det Γ = det B = det B ∗
und |bi | ≥ |bi∗ | wg. Projektion
Vektorlängen in Gittern
I
gegeben: Gitter Γ (durch Basis B).
gesucht: Abschätzung für λ := 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
√ d
√
d,
+1/
d}
mit W = Würfel
mit
Eckenmenge
{−1/
√
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 wählen, daß |bi − qbj | minimiert wird
(bestimme Minimum einer quadr. Funktion)
Implementierung auf Lattice Reduction Challenge
anwenden: für d = 200 OK, für 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,
I
Def: B heißt größenreduziert, falls ∀i > j : |µi,j | ≤ 1/2.
I
Algorithmus (size reduction)
while (existiert i > j mit |µi,j | > 1/2) do bi := bi − bµi,j e · bj
I
Satz: diese Alg. liefert eine zu B äquivalente
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
∗ +µ
∗ 2
equiv. (Ü) |bi∗ |2 ≤ δ · |bi+1
i+1,i bi |
I
∗ |2
alternativ: |bi∗ |2 ≤ 2|bi+1
(nach V. Shoup, siehe v.z.Gathen: MCA, Notes 16.2)
I
Algorithmus (LLL): do { größenreduktion;
wenn ∃i : ¬Lovaszδ (i), dann bi ↔ bi+1 ; continue }
I
liefert (1.) Basis mit kurzen Vektor (2.) in Polynomialzeit
LLL-Algorithmus: Korrektheit
1. Satz: B größen- u. Lovasz-reduziert ⇒ |b1 | ≤ 2(d−1)/2 λ(Γ)
LLL-Algorithmus: Termination, Laufzeit
2. Satz: der Wert von
P
i
log det(span(b1 , . . . , bi ))
I
ist anfangs beschränkt durch . . .
I
bleibt bei Größenreduktion unverändert
I
sinkt bei Tausch um eine Konstante
(der von δ abhängt - wie?
Daraus ergibt sich der Bereich der für δ zulässigen Werte)
I
ist immer ≥ 0
Folgerung: Laufzeit von LLL ist polynomiell in der Dimension.
Quellen, Ergänzungen
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 Vektorlängen man durch
naive Implementierung der Reduktion erreicht.
Akustische Signale (Audiodaten)
I
(physikalisch) Geräusch = Folge von Luftdruckänderungen
. . . die sich wellenförmig 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 für csound
ghci
:m + Csound.Base Csound.IO
dac $ osc 440 -- Audio-Ausgabe
renderCsd ( osc 440 ) >>= putStrLn -- Quelltext
Partituren
verwendet:
I
Atome: Note (Dauer, Höhe) und Pause (Dauer)
I
Verknüpfungen: 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: Musikstücke
(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
verknüpfen: 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 über wen? von links, von rechts?)
I
ist Performance ein Halbring?
Partitur und Aufführung
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 aufgeführt
http://www.aslsp.org/, wird 639 Jahre dauern,
nächster Klangwechsel: 5. September 2020.
Ströme
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 für s
Herbert Wilf: Generatingfunctionology (1990), http:
//www.math.upenn.edu/˜wilf/DownldGF.html
Rechnen mit Strömen (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 Strömen (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 für 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 · . . .
fk ist Präfix von fk+1 , damit exist. f := (limk fk ) ∈ {0, 1}ω
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 überschneidungsfreier 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 Gefühl ausdrücken bzw. beim Hörer
hervorrufen will.
I
Wollen reicht aber nicht (Kunst kommt von Können, . . . ),
es gibt Regeln, die beschreiben,
wann Töne wohlklingen (Harmonie, Akkorde)
und Tonfolgen spannend sind (Kontrapunkt, Stimmführung)
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
Guerino Mazzola: Die Geometrie der Töne (1990)
I
Differentialgeometrie: M ist Mannigfaltigkeit:
I
I
M läßt sich durch lokale Karten überdecken
(∀x ∈ M : Umgebung von x sieht aus wie ein Rd )
überlappende Karten passen (diff.bar) zusammen
Motivation in der Mathematik: exakte √
Definition
mehrdeutiger Funktionen“, z.B. x 7→ x in C.
”
Riemannsche Fläche (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 Töne, Birkhäuser 1990.
(https://zbmath.org/?q=an:0729.00008)
I
Thomas Noll: Ist der Tonraum flach oder gekrümmt?, 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: Kalkül.)
Umformungen
I
I
abstrakt:
Termination, Konfluenz (lokal, global), Normalformen
konkret
I
I
I
für Terme:
(literale) Ersetzungsrelation, wohlfundierte monotone
Algebra, Polynominterpretation, kritische Paare,
Vervollständigung
für Vektoren:
Größenreduktion, Lovasz-Reduktion, L3 -Algorithmus
für Polynome/arithmetische Ausdrücke:
(algebraische) Ersetzung, Simplifikator, Rechnen m. algebr.
Zahlen, zulässige 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 entschlüsseln, Polynom faktorisieren)
I
arithm. Ausdruck simplifizieren (auf 0 testen)
⇒ geometrisches Theorem (v. rationalen konstruktiven
Typ) beweisen
I
Gröbnerbasis ausrechnen
⇒ Idealmitgliedschaft entscheiden ⇒ geometrisches
Theorem (v. Gleichungstyp) beweisen
Was (könnte 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, Gröbner)
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/

Download Report