Mod - 3.1 3 Terme und Algebren 3.1 Terme In allen formalen Kalkülen benutzt man Formeln als Ausdrucksmittel. Hier betrachten wir nur ihre Struktur - nicht ihre Bedeutung. Wir nennen sie Terme. Terme bestehen aus Operationen, Operanden, Konstanten und Variablen: a + 5 blau ? gelb = grün heart > diamond Terme werden nicht "ausgerechnet". Operationen, Konstanten und Variablen werden als Symbole ohne Bedeutung betrachtet. Notation von Termen: Infix-, Postfix-, Präfix- und Baum-Form Umformung von Termen: Grundlage für die Anwendung von Rechenregeln, Gesetzen Für Variable in Termen werden Terme substituiert: in a + a = 2asteriskmath a substituiere a durch 3asteriskmath b 3asteriskmath b + 3asteriskmath b = 2asteriskmath 3asteriskmath b Unifikation: Terme durch Substitution von Variablen gleich machen, z. B. um die Anwendbarkeit von Rechenregeln zu prüfen (c) 2007 bei Prof. Dr. Uwe Kastens -------------------------------------------------------------------------------- Vorlesung Modellierung WS 2011/12 / Folie 301 Ziele: Informelle Übersicht in der Vorlesung: Erläuterungen dazu * Terme als Strukturen erklären. * Terme umformen ohne zu "rechnen". -------------------------------------------------------------------------------- Mod-3.2 Sorten und Signaturen Terme werden zu einer Signatur gebildet. Sie legt die verwendbaren Symbole und die Strukturierung der Terme fest. Signatur summation := (S, F), S ist eine Menge von Sorten, F ist eine Menge von Operationen. Eine Sorte s element S ist ein Name für eine Menge von Termen, z. B. ARITH, BOOL; verschiedene Namen benennen disjunkte Mengen Eine Operation f element F ist ein Operatorsymbol, beschrieben durch Anzahl der Operanden (Stelligkeit), Sorten der Operanden und Sorte des Ergebnisses 0-stellige Operatoren sind Konstante, z. B. true, 1 Beispiele: Signatur summation ) einzelne Operatoren: BOOL := (SBOOL, FBOOL Name Operandensorten Ergebnissorte SBOOL := { BOOL }, +: ARITH x ARITH -> ARITH FBOOL := <: ARITH x ARITH -> BOOL { true: -> BOOL, logicaland : BOOL x BOOL -> BOOL false: -> BOOL, true: -> BOOL logicaland : BOOL x BOOL-> BOOL, 1: -> ARITH logicalnot : BOOL -> BOOL } (c) 2011 bei Prof. Dr. Uwe Kastens -------------------------------------------------------------------------------- Vorlesung Modellierung WS 2011/12 / Folie 302 Ziele: Begriff der Signatur verstehen in der Vorlesung: * Erläuterung der Begriffe * Beispiele für Terme zu Signaturen * Hinweis: Der Name Signatur wird 2-fach verwendet: wie hier definiert und als "Signatur einer Funktion (siehe Folie Mod-2.11)". -------------------------------------------------------------------------------- Mod - 3.3 Korrekte Terme In korrekten Termen muss jeweils die Zahl der Operanden mit der Stelligkeit der Operation und die Sorten der Operandenterme mit den Operandensorten der Operation übereinstimmen. Induktive Definition der Menge tau der korrekten Terme der Sorte s zur Signatur Sigma = (S, F): Sei die Signatur Sigma = (S, F). Dann ist t ein korrekter Term der Sorte selement S, wenn gilt * t = v und v ist der Name einer Variablen der Sorte s, oder * t = f (t1, t2, .., tn), also die Anwendung einer n-stelligen Operation f: s1 x s2 x ... x sn -> s element F wobei jedes ti ein korrekter Term der Sorte si ist mit n greaterequal 0 (einschließlich Konstante f bei n = 0) und i element {1, ..., n} f (t1,..., tn) ist ein n-stelliger Term; die ti sind seine Unterterme. Korrekte Terme, die keine Variablen enthalten, heißen Grundterme. Beispiele: korrekte Terme zur Signatur summation BOOL: false logicalnot true true logicaland x logicalnot ( a logicaland b) x logicaland logicalnot y nicht korrekt:a logicalnot b logicalnot ( logicaland b) (c) 2010 bei Prof. Dr. Uwe Kastens -------------------------------------------------------------------------------- Vorlesung Modellierung WS 2011/12 / Folie 303 Ziele: Regeln zur Struktur von Termen in der Vorlesung: * Terme zu den Signaturen von Mod-3.2 konsturieren. * Beispiele für falsche Terme. * Vergleich mit Typregeln in Programmiersprachen. Verständnisfragen: * Welche Terme kann man aus den Operationen 0: -> N0 und succ: N0 -> N0 bilden? * Geben Sie einige Terme zu den Signaturen von Mod-3.2 an. -------------------------------------------------------------------------------- Mod - 3.4 Notationen für Terme Notation eines n-stelligen Terms mit Operation (Operator) f und Untertermen t1, t2, ..., tn: Bezeichnung Notation Beispiele Funktionsform: Operator vor der geklammerten Folge seiner Operanden f (t1, t2, ..., tn) logicaland (< (0, a), logicalnot (< (a, 10))) Präfixform: Operator vor seinen Operanden f t1 t2 ... tn logicaland < 0 a logicalnot < a 10 Postfixform: Operator nach seinen Operanden t1 t2 ... tn f 0 a < a 10 < logicalnot logicaland Infixform 2-stelliger Operator zwischen seinen (beiden) Operanden t1 f t2 0 < a logicaland logicalnot a < 10 Die Reihenfolge der Operanden ist in allen vier Notationen gleich. (c) 2007 bei Prof. Dr. Uwe Kastens -------------------------------------------------------------------------------- Vorlesung Modellierung WS 2011/12 / Folie 304 Ziele: Verschiedene Notationen für denselben Term in der Vorlesung: An weiteren Beispielen erläutern: * Struktur der Notationen * Beispiele für 2-, 1- und 3-stellige Operationen * Umformungen Verständnisfragen: * Kennzeichnen Sie alle Teilterme eines Terms in den 4 Formen! * Wie finden Sie in der Postfixform die Operanden zu einem Operator? * Können in einem Term in Infixform die Operanden immer eindeutig zugeordnet werden? -------------------------------------------------------------------------------- Mod - 3.5 Präzedenzen und Klammern für Infixform Die Infixform benötigt Klammern oder Präzedenzen, um Operanden an ihren Operator zu binden: Ist in x + 3 * y die 3 rechter Operand des + oder linker Operand des * ? Klammern beeinflussen die Struktur von Termen in der Infixform: z. B. (x + 3) * y oder x + (3 * y) Redundante Klammern sind zulässig. Ein Term ist vollständig geklammert, wenn er und jeder seiner Unterterme geklammert ist: z. B. ((x) + ((3) * (y))) Für die Infixform können den Operatoren unterschiedliche Bindungsstärken (Präzedenzen) zugeordnet werden, z. B. bindet * seine Operanden vereinbarungsgemäß stärker an sich als +, d. h. * hat höhere Präzedenz als +. Damit sind x + 3 * y und x + (3 * y) verschiedene Schreibweisen für denselben Term. Für aufeinanderfolgende Operatoren gleicher Präzedenz muss geregelt werden, ob sie ihre Operanden links-assoziativ oder rechts-assoziativ binden: links-assoziativ: x + 3 + y steht für (x + 3) + y rechts-assoziativ: x ** 3 ** y steht für x ** (3 ** y) Funktionsform, Präfixform, Postfixform benötigen weder Regeln für Präzedenz oder Assoziativität noch zusätzliche Klammern! (c) 2010 bei Prof. Dr. Uwe Kastens -------------------------------------------------------------------------------- Vorlesung Modellierung WS 2011/12 / Folie 305 Ziele: Präzedenzen verstehen in der Vorlesung: An weiteren Beispielen erläutern: * notwendige, redundante und vollständige Klammerung von Termen, * Verwechselung mit Klammern 1-elementiger Folgen vermeiden, * Präzedenzen und Assoziativität, * Präzedenzen in Programmiersprachen Verständnisfragen: * Weshalb benötigen Präfix- und Postfixform keine Klammern? * Welche Präzedenzen haben die Operatoren in Java? -------------------------------------------------------------------------------- Mod - 3.6 Terme als Bäume Terme kann man als Bäume darstellen (Kantorowitsch-Bäume): Term: 0 < a logicaland a < 10 logicaland Wurzel Operatoren innere Knoten { } < < Blätter Variable und 0 a a 10 Konstante des Baumes Aus einem Durchlauf des Baumes in logicaland Pfeilrichtung erzeugt man * Präfixform, wenn man beim ersten Besuch * Postfixform, wenn man beim letzten Besuch < < * Infixform, wenn man beim vorletzten Besuch (bei 2-stelligen Operatoren) 0 a a 10 den Operator aufschreibt. (c) 2007 bei Prof. Dr. Uwe Kastens -------------------------------------------------------------------------------- Vorlesung Modellierung WS 2011/12 / Folie 306 Ziele: Zusammenhang der Darstellungen verstehen in der Vorlesung: * Bäume erläutern * Baumdurchläufe erläutern * Rekursive Definition der Notationen Verständnisfragen: * Wie hängen Baumdarstellung und vollständig geklammerte Terme zusammen? -------------------------------------------------------------------------------- Mod - 3.7 Substitution und Unifikation Eine Substitution beschreibt, wie in einem Term vorkommende Variablen durch Terme ersetzt werden. Eine einfache Substitution sigma = [ v / t ] ist ein Paar aus einer Variablen v und einem Term t zur Signatur summation . v und t müssen dieselbe Sorte s haben. Beispiel: sigma = [ x / 2*b ] Die Anwendung einer Substitution sigma auf einen Term u schreibt man u sigma , z. B. (x+1) [x / 2*b]. Die Anwendung einer einfachen Substitution u sigma mit sigma = [ v / t ], ist definiert durch * u [ v / t ] = t , falls u die zu ersetzende Variable v ist, * u [ v / t ] = u , falls u notequal v und u eine Konstante oder eine andere Variable ist, * u [ v / t ] = f (u1 [ v / t ], u2 [ v / t ], ..., un [ v / t ]) , falls u = f (u1, u2, ..., un) D. h. in u werden alle Vorkommen der Variablen v gleichzeitig durch den Term t ersetzt. Kommt v auch in t vor, so wird es nicht nochmals ersetzt! Beispiele: (x + 1) [ x / 2*b ] = (2*b + 1) (x - x) [ x / 3 ] = (3 - 3) (x + y) [ y / y*y ] = (x + y*y) (c) 2007 bei Prof. Dr. Uwe Kastens -------------------------------------------------------------------------------- Vorlesung Modellierung WS 2011/12 / Folie 307 Ziele: Formale Definition des Einsetzens für Variable in der Vorlesung: An Beispielen erlätern: * konsistentes Ersetzten mehrerer Vorkommen * gleichzeitiges Ersetzen * Ersetzen wird nicht iteriert * Variable können ungebunden bleiben Hinweis: Wir haben hier nicht die Notation aus dem Skript vom WS 2000/2001 und nicht die aus dem Buch von Goos verwendet! Dort werden die Paare in umgekehrter Reihenfolge angegeben: [Term/Variable]. Verständnisfragen: Geben Sie Beispiele für Substitutionen zu Termen der Signatur zu BOOL an. -------------------------------------------------------------------------------- Mod - 3.8 Mehrfache Substitution In einer mehrfachen Substitution sigma = [ v1 / t1, ..., vn / tn] müssen alle Variablen vi paarweise verschieden sein. In jedem vi / ti müssen vi und ti jeweils derselben Sorte si angehören. sigma wird dann auf einen Term u wie folgt angewandt: * u sigma = ti, falls u = vi für ein i element {1, ..., n}, * u sigma = u , falls u eine Konstante ist oder eine Variable, die nicht unter vi für ein i element {1, ..., n} vorkommt, * u sigma = f (u1 sigma , u2 sigma , ..., un sigma ) , falls u = f (u1, u2, ..., un) D. h. sigma ist die gleichzeitige Substitution aller Vorkommen jeder Variablen vi jeweils durch den Term ti. Beispiele: sigma = [ x / 2asteriskmath b, y / 3 ] (x + y) sigma = (2asteriskmath b + 3) (y + aasteriskmath y) sigma = (3 + aasteriskmath 3) (x asteriskmath y) [ x / y, y / yasteriskmath y ] = (y asteriskmath (y asteriskmath y)) Die leere Substitution wird [ ] notiert. Für alle Terme t gilt t [ ] = t. Außerdem gilt [v / v] = [ ] für jede Variable v. (c) 2011 bei Prof. Dr. Uwe Kastens -------------------------------------------------------------------------------- Vorlesung Modellierung WS 2011/12 / Folie 308 Ziele: Mehrfache Substitutionen verstehen in der Vorlesung: An Beispielen erlätern: * konsistentes Ersetzten mehrerer Variablen, -------------------------------------------------------------------------------- Mod - 3.8a Hintereinanderausführung von Substitutionen Auf einen Term können mehrere Substitutionen hintereinander ausgeführt werden, z. B. u sigma 1 sigma 2 sigma 3 = ((u sigma 1) sigma 2) sigma 3 (x+y) [x/yasteriskmath x] [y/3] [x/a] = (yasteriskmath x+y) [y/3] [x/a] = (3asteriskmath x+3) [x/a] = (3asteriskmath a+3) Mehrere Substitutionenen hintereinander können als eine Substitution angesehen werden: z. B. u sigma 1 sigma 2 sigma 3 = u (sigma 1 sigma 2 sigma 3) = u sigma Mehrere einfache Substitutionen hintereinander kann man in eine mehrfache Substitution mit gleicher Wirkung umrechnen: Die Hintereinanderausführung [ x1 / t1, ..., xn / tn ] [ y / r ] hat auf jeden Term die gleiche Wirkung wie falls y unter den xi vorkommt [ x1 / (t1[ y / r ]), ..., xn / (tn [ y / r ])] falls y nicht unter den xi vorkommt [ x1 / (t1[ y / r ]), ..., xn / (tn [ y / r ]), y / r ] Beispiel: [ x / yasteriskmath x ] [ y / 3 ] [ x / a ] = [ x / 3asteriskmath x, y / 3] [ x / a ] = [ x / 3asteriskmath a, y / 3 ] (c) 2007 bei Prof. Dr. Uwe Kastens -------------------------------------------------------------------------------- Vorlesung Modellierung WS 2011/12 / Folie 308a Ziele: Umgang mit Substitutionen verstehen in der Vorlesung: An Beispielen erlätern: * Hintereinanderausführung, * Umrechnung. Verständnisfragen: Begründen Sie die Regel für die Umrechnung. -------------------------------------------------------------------------------- Mod - 3.9 Umfassende Terme Rechenregeln werden mit allgemeineren Termen formuliert, die auf speziellere Terme angewandt werden, z. B. Distributivgesetz: a asteriskmath (b + c) = a asteriskmath b + a asteriskmath c angewandt auf 2 asteriskmath (3 + 4asteriskmath x) = 2 asteriskmath 3 + 2 asteriskmath 4asteriskmath x Ein Term s umfasst einen Term t, wenn es eine Substitution sigma gibt, die s in t umformt: s sigma = t s umfasst t, ist eine Quasiordnung, d. h. die Relation umfasst ist transitiv: sei r sigma 1 = s, s sigma 2 = t, dann ist r (sigma 1 sigma 2) = t reflexiv: t [ ]= t, mit der leeren Substitution [ ] Eine Halbordnung ist umfasst nicht, weil nicht antisymmetrisch: Terme, die sich nur in den Variablennamen unterscheiden, kann man ineinander umformen, z. B. 2asteriskmath x [ x / y ] = 2asteriskmath y und 2asteriskmath y [ y / x ] = 2asteriskmath x Deshalb gilt zwar der allgemeinere Term a asteriskmath (b + c) umfasst den spezielleren 2 asteriskmath (3 + 4asteriskmath x), aber nicht immer ist ein Term s allgemeiner als ein Term t, wenn s umfasst t: 2*x und 2*y (c) 2007 bei Prof. Dr. Uwe Kastens -------------------------------------------------------------------------------- Vorlesung Modellierung WS 2011/12 / Folie 309 Ziele: Terme als Muster verstehen in der Vorlesung: * Substitution als Anwendung einer Rechenregel * Erläuterung der Relation "umfasst" * weitere Beispiele Verständnisfragen: Warum ist es nicht völlig korrekt, zu sagen, dass t spezieller ist als s, wenn s t umfasst? -------------------------------------------------------------------------------- Mod - 3.10 Unifikation Die Unifikation substituiert zwei Terme, sodass sie gleich werden. Zwei Terme s und t sind unifizierbar, wenn es eine Substitution sigma gibt mit s sigma = t sigma . sigma heißt Unifikator von s und t. Beispiel: Terme: s = (x + y) t = (2 + z) Unifikatoren: sigma 1 = [ x / 2, y / z ] sigma 2 = [ x / 2, z / y ], sigma 3 = [ x / 2, y / 1, z / 1 ] sigma 4 = [ x / 2, y / 2, z / 2 ] ... Ist sigma ein Unifikator von s und t und tau eine Substitution, dann ist auch die Hintereinanderausführung sigma tau = sigma ` auch ein Unifikator von s und t. Ein Unifikator sigma heißt allgemeinster Unifikator der Terme s und t, wenn es zu allen anderen Unifikatoren sigma ` eine Substitution tau gibt mit sigma tau = sigma `. Im Beispiel sind sigma 1 und sigma 2 allgemeinste Unifikatoren, z. B. sigma 1 [ z / 1 ] = sigma 3 Es kann mehrere allgemeinste Unifikatoren geben. Sie können durch Umbenennen von Variablen ineinander überführt werden, z. B. sigma 1 [ z / y ] = [ x / 2, y / z ] [ z / y ]= [ x / 2, y / y, z / y ] = [ x / 2, z / y ] = sigma 2 (c) 2007 bei Prof. Dr. Uwe Kastens -------------------------------------------------------------------------------- Vorlesung Modellierung WS 2011/12 / Folie 310 Ziele: Allgemeines Prinzip Unifikation verstehen in der Vorlesung: An Beispielen zeigen: * Unifikatoren * nicht unifizierbare Terme * allgemeinste Unifikatoren machen keine unnötigen Festlegungen. * Zur letzten Zeile der Folie: Eine Substitution [y/y] hat keine Wirkung, also [y/y] = []. In mehrfachen Substitutionen kann man Komponenten der Formy/y weglassen und Komponenten vertauschen, ohne die Wirkungder Substitution zu ändern. Verständnisfragen: * Wie müssen 2 Terme beschaffen sein, damit es Unifikatoren gibt, die verschieden sind von den allgemeinsten Unifikatoren? Hinweis: Nur wenn ein allgemeinster Unifikator noch Variablen offen lässt, kann es speziellere geben. -------------------------------------------------------------------------------- Mod - 3.11 Unifikationsverfahren Unifikation zweier Terme s und t nach Robinson: Seien s und t Terme in Funktionsschreibweise. Dann ist das Abweichungspaar A(s, t) = (u, v) das erste Paar unterschiedlicher, korrespondierender Unterterme u und v, das man beim Lesen von links nach rechts antrifft. Algorithmus: 1. Setze sigma = [ ] (leere Substitution) 2. Solange es ein Abweichungspaar A(s sigma , t sigma ) = (u, v) gibt wiederhole: a. ist u eine Variable x, die in v nicht vorkommt, dann ersetze sigma durch sigma [ x / v ], oder b. ist v eine Variable x, die in u nicht vorkommt, dann ersetze sigma durch sigma [ x / u ], c. sonst sind die Terme s und t nicht unifizierbar; Abbruch des Algorithmus. 3. Bei Erfolg gilt s sigma = t sigma und sigma ist allgemeinster Unifikator. Beachte, dass bei jeder Iteration die bisherige Substitution auf die vollständigen Terme s, t angewandt wird. (c) 2007 bei Prof. Dr. Uwe Kastens -------------------------------------------------------------------------------- Vorlesung Modellierung WS 2011/12 / Folie 311 Ziele: Terme systematisch unifizieren in der Vorlesung: * Verfahren an Beispielen zeigen. * Begründen, weshalb die Substitution immer wieder auf s und t angewandt wird. * Begründen, weshalb in 2a und 2b geprüft wird, ob die Variable x in dem Unterterm vorkommt. Verständnisfragen: * Zeigen sie an einem Beispiel, dass es nötig ist, in 2a und 2b zu prüfen ob die Variable x in dem Unterterm vorkommt. -------------------------------------------------------------------------------- Mod - 3.12 Beispiel für Unifikationsverfahren Unifikation zweier Terme s und t nach Robinson: s = + (* (2, x), 3) t = + (z, x) sigma = [ ] Schritt Abweichungspaar 1 s sigma = + (* (2, x), 3) Fall 2b: sigma = [ ] [ z / * (2, x) ] t sigma = + (z, x) Abweichungspaar 2 s sigma = + (* (2, x), 3) Fall 2b: sigma = [ ] [ z / * (2, x) ] [ x / 3 ] t sigma = + (* (2, x), x) 3 s sigma = + (* (2, 3), 3) sigma = [ z / * (2, x)] [ x / 3 ] = t sigma = + (* (2, 3), 3) allgemeinster Unifikator: [ z / * (2, 3), x / 3 ] (c) 2007 bei Prof. Dr. Uwe Kastens -------------------------------------------------------------------------------- Vorlesung Modellierung WS 2011/12 / Folie 312 Ziele: Verfahren von Robinson anwenden in der Vorlesung: Verfahren an Beispielen zeigen. -------------------------------------------------------------------------------- Mod - 3.13 3.2 Algebren Eine Algebra ist eine formale Struktur, definiert durch eine Trägermenge, Operationen darauf und Gesetze zu den Operationen. In der Modellierung der Informatik spezifiziert man mit Algebren Eigenschaften veränderlicher Datenstrukturen und dynamische Systeme, z. B. Datenstruktur Keller oder die Bedienung eines Getränkeautomaten. Wir unterscheiden 2 Ebenen: abstrakte Algebra und konkrete Algebra: Eine abstrakte Algebra spezifiziert Eigenschaften abstrakter Operationen, definiert nur duch eine Signatur - Realisierung durch Funktionen bleibt absichtlich offen Trägermenge: korrekte Terme zu der Signatur Gesetze erlauben, Vorkommen von Termen durch andere Terme zu ersetzen z. B. logicalnot false minus > true pop (push (k, t)) minus > k Eine konkrete Algebra zu einer abstrakten Algebra definiert konkrete Funktionen zu den Operationen der Signatur, so dass die Gesetze in Gleichungen zwischen den Funktionstermen übergehen. Sie beschreibt so eine Implementierung der spezifizierten Datenstruktur, bzw. des Systems (c) 2011 bei Prof. Dr. Uwe Kastens -------------------------------------------------------------------------------- Vorlesung Modellierung WS 2011/12 / Folie 313 Ziele: Vorschau zur Modellierung mit Algebren in der Vorlesung: Erläuterungen dazu -------------------------------------------------------------------------------- Mod - 3.14 Abstrakte Algebra Eine abstrakte Algebra A = (tau , Sigma , Q) ist definiert durch die Menge korrekter Terme tau zur Signatur Sigma und eine Menge von Axiomen (Gesetzen) Q. Axiome haben die Form t1 -> t2, wobei t1, t2, korrekte Terme gleicher Sorte sind, die Variablen enthalten können. Die Algebra definiert, wie man Terme mit den Axiomen in andere Terme umformen kann. Mit Axiomen umformen heißt: Unter Anwenden eines Axioms t1 -> t2 kann man einen Term s1 in einen Term s2 umformen. Wir schreiben s1 -> s2, wenn gilt: * s1 und s2 stimmen in ihren "äußeren" Strukturen überein und unterscheiden sich nur durch die Unterterme r1 und r2 an entsprechenden Positionen in s1 und s2, und * es gibt eine Substitution sigma , sodass gilt t1 sigma = r1 und t2 sigma = r2 Terme s1 = ......... r1 ........ -> ......... r2 ........ = s2 t1 sigma t2 sigma Axiom t1 -> t2 s ist in t umformbar, wenn es eine endliche Folge von Termen s = s0, s1, ..., sn = t mit si-1 -> si gibt; wir schreiben dann s -> t. "->" ist transitiv. Wenn es auch irreflexiv ist (so sollten die Axiome gewählt werden), ist es eine strenge Halbordnung. (c) 2011 bei Prof. Dr. Uwe Kastens = = -------------------------------------------------------------------------------- Vorlesung Modellierung WS 2011/12 / Folie 314 Ziele: Axiome definieren Terme als gleichbedeutend in der Vorlesung: * Anwendungen von Axiomen auf Termpaare zeigen (Substitution) * Beispiel: Kommutativgesetz anwenden Verständnisfragen: Erklären Sie Anwendungen des Kommutativgesetzes präzise in der definierten Terminologie. -------------------------------------------------------------------------------- Mod - 3.15 Beispiel: abstrakte Algebra Bool Signatur Sigma = ({BOOL}, F) Axiome Q: für alle x,y der Sorte BOOL gilt Operationen F: Q1: logicalnot true minus > false true: -> BOOL Q2: logicalnot false minus > true false: -> BOOL Q3: true logicaland x minus > x logicaland : BOOL x BOOL -> BOOL Q4: false logicaland x minus > false logicalor : BOOL x BOOL -> BOOL Q5: x logicalor y minus > logicalnot (logicalnot x logicaland logicalnot y) logicalnot : BOOL -> BOOL Die Axiome sind geeignet, alle korrekten Terme ohne Variablen in in einen der beiden Terme true oder false umzuformen. true und false heißen Normalformen (siehe Folie 3.20). (c) 2011 bei Prof. Dr. Uwe Kastens -------------------------------------------------------------------------------- Vorlesung Modellierung WS 2011/12 / Folie 315 Ziele: Beispiel für eine abstrakte Algebra in der Vorlesung: * Algebra Bool erläutern * Gesetze anwenden * Weitere Gesetze formulieren -------------------------------------------------------------------------------- Mod - 3.16 Konkrete Algebra Zu einer abstrakten Algebra Aa = (tau , (S, F), Q), kann man konkrete Algebren wie Ak = (Wk, Fk, Q) angeben, wobei Wk eine Menge von Wertebereichen ist, je einer für jede Sorte aus S, Fk eine Menge von Funktionen ist, je eine für jede Operation aus F. Die Definitions- und Bildbereiche der Funktionen müssen konsistent den Sorten der Operationen zugeordnet werden. Den Axiomen Q müssen Gleichungen zwischen den Funktionstermen in den Wertebereichen entsprechen. Es können in der konkreten Algebra noch weitere Gleichungen gelten. Eine konkrete Algebra heißt auch Modell der abstrakten Algebra. (c) 2011 bei Prof. Dr. Uwe Kastens -------------------------------------------------------------------------------- Vorlesung Modellierung WS 2011/12 / Folie 316 Ziele: Zusammenhang zwischen konkreter und abstrakter Algebra verstehen in der Vorlesung: Am Beispiel Mod-225a erläutern -------------------------------------------------------------------------------- Mod - 3.17 Beispiel für eine konkrete Algebra Beispiel: eine konkrete Algebra FSet zur abstrakten Algebra Bool: konkrete Algebra FSet abstrakte Algebra Bool Wk: {emptyset , {1}} Sorte BOOL Fk: {1} true emptyset false Mengendurchschnitt intersection logicaland Mengenvereinigung union logicalor Mengenkomplement bezüglich {1} logicalnot Axiome Q: Man kann zeigen, dass die Axiome Gleichungen zwischen den Termen in Wk entsprechen: z. B. emptyset intersection x = emptyset entspricht false logicaland x -> false Die boolesche Algebra mit den üblichen logischen Funktionen ist natürlich auch eine konkrete Algebra zur abstrakten Algebra Bool. (c) 2011 bei Prof. Dr. Uwe Kastens -------------------------------------------------------------------------------- Vorlesung Modellierung WS 2011/12 / Folie 317 Ziele: Beispiel für Zusammenhang zwischen konkreter und abstrakter Algebra in der Vorlesung: Beispiel mit Folie Mod-3.16 erläutern * Funktionstafeln der konkreten Funktionen angeben * Gültigkeit der Gleichungen zu den Axiomen zeigen * Ebenso für die konkrete boolesche Algebra Übungsaufgaben: Tauschen Sie in FSet die Funktionen zu T und F. Gelten die Gleichungen zu den Axiomen noch? Verständnisfragen: * Zeigen Sie, dass die Gleichungen zu allen Axiome Q von Bool in FSet gelten. -------------------------------------------------------------------------------- Mod - 3.18 Beispiel 2.2: Datenstruktur Keller Die Eigenschaften einer Datenstruktur Keller beschreiben wir zunächst informell. Folgende Operationen kann man mit einem Keller ausführen: create Stack: liefert einen leeren Keller push: fügt ein Element in den Keller ein pop: entfernt das zuletzt eingefügte Element top: liefert das zuletzt eingefügte und nicht wieder entfernte Element empty: gibt an, ob der Keller leer ist. Die Eigenschaften der Datenstruktur Keller sollen präzise durch eine abstrakte Algebra spezifiziert werden. Beispiele Tellerstapel Aktenstapel Laufzeitkeller push pop push pop Aufruf Rückkehr zum Aufrufer (c) 2011 bei Prof. Dr. Uwe Kastens -------------------------------------------------------------------------------- Vorlesung Modellierung WS 2011/12 / Folie 318 Ziele: Das Kellerprinzip informell verstehen in der Vorlesung: * Keller-Prinzip: Last-in-first-out (LIFO) * Beispiele erläutern * Anwendung eines Kellers: Infix in Postfix umwandeln Verständnisfragen: * Erklären Sie das Kellerprinzip an der Abarbeitung von Funktions- bzw. Methodenaufrufen in Programmen. -------------------------------------------------------------------------------- Mod - 3.19 Beispiel: Abstrakte Algebra spezifiziert Keller Abstrakte Algebra Keller: Signatur Sigma = (S, F), Sorten S = {Keller, Element, BOOL}, Operationen F: createStack: -> Keller push: Keller x Element -> Keller pop: Keller -> Keller top: Keller -> Element empty: Keller -> BOOL Axiome Q: für beliebige Terme t der Sorte Element und k der Sorte Keller gilt: K1: empty (createStack) -> true K2: empty (push (k, t)) -> false K3: pop (push (k, t)) -> k K4: top (push (k, t)) -> t Keller ist die Sorte, deren Terme Kellerinhalte modellieren. Element und BOOL sind Hilfssorten der Algebra. Implementierungen der abstrakten Algebra Keller können durch konkrete Algebren dazu beschrieben werden. (c) 2011 bei Prof. Dr. Uwe Kastens -------------------------------------------------------------------------------- Vorlesung Modellierung WS 2011/12 / Folie 319 Ziele: Abstrakte Algebra als Spezifikation verstehen in der Vorlesung: * Terme umformen * K3 mit LIFO begründen * Anschauliche Darstellungen und Implementierungen von Kellerinhalten entsprechen konkreten Algebren Verständnisfragen: * Geben sie verschiedene Terme an, die zu top (push (createStack, 1)) und zu push (push (createStack, 1), 2) gleichbedeutend sind. -------------------------------------------------------------------------------- Mod - 3.20 Klassifikation von Operationen Die Operationen einer Algebra werden in 3 disjunkte Mengen eingeteilt: Konstruktoren: Ergebnissorte ist die definierte Sorte Hilfskonstruktoren: Ergebnissorte ist die definierte Sorte und sie können durch Axiome aus Termen entfernt werden Projektionen: andere Ergebnissorte z. B. in der Keller-Algebra: definierte Sorte ist Keller createStack: -> Keller Konstruktor push: Keller x Element -> Keller Konstruktor pop: Keller -> Keller Hilfskonstruktor (K3 entfernt ihn) top: Keller -> Element Projektion empty: Keller -> BOOL Projektion (c) 2011 bei Prof. Dr. Uwe Kastens -------------------------------------------------------------------------------- Vorlesung Modellierung WS 2011/12 / Folie 320 Ziele: Einteilung der Operationen in der Vorlesung: * Klassifikation erläutern * Konstruktoren zur Algebra Bool angeben. Verständnisfragen: * Klassifizieren Sie die Operationen der Algebra Bool. -------------------------------------------------------------------------------- Mod - 3.20a Normalform Terme ohne Variable der definierten Sorte sind in Normalform, wenn sie nur Konstruktoren enthalten kein Axiom anwendbar ist. Normalform-Terme der Algebra Bool sind: true false Normalform-Terme der Keller-Algebra haben die Form: push (.... push (createStack, n1) , ...), nm), mit m greaterequal 0 Die Terme in Normalform sind die minimalen Elemente bzgl. der strengen Halbordnung ->. Terme s, t, die in dieselbe Normalform umformbar sind, heißen gleichbedeutend, s equivalence t. Undefinierte Terme: Terme der definierten Sorte, die man nicht in eine Normalform umformen kann, werden als undefiniert angesehen. Sie modellieren eine Fehlersituation, z. B. pop (createStack) Für manche Projektionen gibt es nicht zu jedem Term in Normalform ein anwendbares Axiom; dies modelliert auch Fehlersituationen, z. B. top (createStack) (c) 2011 bei Prof. Dr. Uwe Kastens -------------------------------------------------------------------------------- Vorlesung Modellierung WS 2011/12 / Folie 320a Ziele: Reduktion von Termen auf ihre Normalform in der Vorlesung: * Reduzierbarkeit auf Normalform durch strukturelle Induktion zeigen * Undefinierte Terme erläutern Verständnisfragen: * Gibt es undefinierte Terme in der Algebra Bool? -------------------------------------------------------------------------------- Mod - 3.21 Anwendungen algebraischer Spezifikationen: Eigenschaften aus den Axiomen erkennen Beispiel: Keller 1. K3: pop (push (k, t)) -> k Keller-Prinzip: zuletzt eingefügtes Element wird als erstes wieder entfernt (last-in-first-out, LIFO) 2. top: Keller -> Element K4: top (push (k, t)) -> t top ist die einzige Operation, die Keller-Elemente liefert: Nur auf das zuletzt eingefügte, nicht wieder entfernte Element kann zugegriffen werden. 3. push (.... push (createStack, n1) , ...), nm), mit mgreaterequal 0 K3: pop (push (k, t)) -> k Zählt man in einem Term von innen nach außen die push-Operationen positiv und die pop- Operationen negativ, und ist der Wert immer nicht-negativ, so ergibt sich die Anzahl der Elemente im Keller, andernfalls ist der Term undefiniert. Begründung: Rückführung auf Normalform, eine push-Operation für jedes Element im Keller. (c) 2011 bei Prof. Dr. Uwe Kastens -------------------------------------------------------------------------------- Vorlesung Modellierung WS 2011/12 / Folie 321 Ziele: Axiome spezifizieren Eigenschaften in der Vorlesung: * Die drei Beispiele erläutern * Über Keller nachdenken, ohne sie zu implementieren -------------------------------------------------------------------------------- Mod - 3.22 Spezifikation um Operationen erweitern Erweitere die Keller-Spezifikation um eine Operation size. Sie soll die Anzahl der Elemente im Keller liefern. 1. Operation size in die Signatur einfügen: size: Keller -> NAT 2. Ergebnis-Sorte NAT zu den Sorten zufügen: S = {Keller, Element, BOOL, NAT} 3. Axiome zufügen, so dass size für jeden Keller-Wert definiert ist: K7: size (createStack) -> null K8: size (push (k, t)) -> succ (size (k)) 4. Weil in der Normalform nur createStack und push vorkommen, braucht size nur für solche Terme definiert zu werden. Dabei wird vorausgesetzt, dass folgende Algebra bekannt ist: Sorten: S = {NAT} Operationen: null: -> NAT, succ: NAT -> NAT (succ (n) modelliert den Nachfolger von n, also n + 1.) (c) 2007 bei Prof. Dr. Uwe Kastens -------------------------------------------------------------------------------- Vorlesung Modellierung WS 2011/12 / Folie 322 Ziele: Operationen und Axiome entwerfen in der Vorlesung: Schritte zur Erweiterung der Spezifikation zeigen Verständnisfragen: Erweitern Sie die Spezifikation um eine Operation, die 2 Elemente einfügt. -------------------------------------------------------------------------------- Mod - 3.24 Realisierung der Spezifikation durch eine konkrete Algebra Beispiel: eine Realisierung von Kellern durch Funktionen auf Folgen von natürlichen Zahlen: Zuordnung der Sorten: konkret abstrakt Bool BOOL Iota N0 Element N-Folge = Iota N asteriskmath Keller Signatur und Zuordnung von Funktionen konkret abstrakt newFolge: -> N-Folge createStack append: N-Folge x Iota N0 -> N-Folge push remove: N-Folge -> N-Folge pop last: N-Folge -> Iota N top noElem: N-Folge -> Bool empty Definition der Funktionen newFolge( ) -> () append ((a1, ..., an), x) -> (a1, ..., an, x) remove ((a1, ..., an - 1, an)) -> (a1, ..., an-1) last ((a1, ..., an)) -> an noElem (f) -> f = () Gültigkeit der Axiome zeigen (c) 2011 bei Prof. Dr. Uwe Kastens -------------------------------------------------------------------------------- Vorlesung Modellierung WS 2011/12 / Folie 324 Ziele: Beispiel für eine Realisierung in der Vorlesung: Funktionen erläutern * Zuordnung erläutern * Gültigkeit der Axiome zeigen Übungsaufgaben: Mit der Klasse Vector aus java.lang kann man Keller implementieren. Schlagen sie in der Dokumentation nach und begründen Sie, dass sich die Methoden addElement, removeElemenAt, lastElement, und size dafür eignen. -------------------------------------------------------------------------------- Mod - 3.25 Keller in Algorithmen einsetzen Aufgabe: Terme aus Infixform in Postfixform umwandeln gegeben: Term t in Infixform, mit 2-stelligen Operatoren unterschiedlicher Präzedenz; (zunächst) ohne Klammern gesucht: Term t in Postfixform Eigenschaften der Aufgabe und der Lösung: 1. Reihenfolge der Variablen und Konstanten bleibt unverändert 2. Variablen und Konstanten werden vor ihrem Operator ausgegeben, also sofort 3. In der Infixform aufeinander folgende Operatoren echt steigender Präzedenz stehen in der Postfixform in umgekehrter Reihenfolge; also kellern. 4. Operatorkeller enthält Operatoren echt steigender Präzedenz. Es gilt die Kellerinvariante KI: Sei push (... push (CreateStack, opr1), opr2), ...) dann gilt Präzedenz (opri ) < Präzedenz (opri+1) (c) 2011 bei Prof. Dr. Uwe Kastens -------------------------------------------------------------------------------- Vorlesung Modellierung WS 2011/12 / Folie 325 Ziele: Kelleranwendung verstehen in der Vorlesung: * Erläuterung der Eigenschaften * Eigenschaften der Aufgabe verstehen, bevor sie gelöst wird * Kellerinvariante: Eine Aussage, die für die Benutzung des Kellers immer gelten muss. Verständnisfragen: Wie werden bei diesen Regeln aufeinander folgende Operatoren gleicher Präzedenz behandelt? -------------------------------------------------------------------------------- Mod - 3.26 Algorithmus: Infix- in Postfixform wandeln Die Eingabe enthält einen Term in Infixform; die Ausgabe soll den Term in Postfixform enthalten Variable: keller element Keller; symbol element Operator union ElementarOperand keller = createStack(); solange Eingabe nicht leer wiederhole {KI} lies symbol falls symbol element ElementarOperand gib symbol aus falls symbol element Operator {KI} solange not empty (keller) logicaland Präzedenz (top (keller)) greaterequal Präzedenz (symbol) wiederhole {KI} gib top (keller) aus; keller = pop (keller); keller = push(keller, symbol); {KI} a b c * - a - b * c solange not empty (keller) wiederhole gib top(keller) aus; keller = pop(keller); * An den Stellen {KI} gilt die Kellerinvariante. - (c) 2011 bei Prof. Dr. Uwe Kastens -------------------------------------------------------------------------------- Vorlesung Modellierung WS 2011/12 / Folie 326 Ziele: Benutzung der Kelleroperationen verstehen in der Vorlesung: * Algorithmus erläutern * Graphik erläutern * Gültigkeit der Kellerinvariante zeigen -------------------------------------------------------------------------------- Mod - 3.26b Abstrakte Algebra für Teilaspekt des Getränkeautomaten Signatur Sigma = (S, F); sweet white Sorten S := {Add, Choice} Operationen F: sweet: -> Add Knöpfe des Getränkeautomaten zur Auswahl von Zutaten white: -> Add noChoice: -> Choice Die Sorte Choice modelliert die Auswahl; press: Add x Choice -> Choice Add ist eine Hilfssorte Bedeutung der Axiome: Axiome Q: für alle a der Sorte Add und Q1: Knopf nocheinmal drücken für alle c der Sorte Choice gilt: macht Auswahl rückgängig. Q1: press (a, press (a, c)) -> c Q2: Es ist egal, in welcher Q Reihenfolge die Knöpfe 2: press (sweet, press (white, c)) -> press (white, press (sweet, c)) gedrückt werden. Beispiel-Terme: press (white, noChoice) press (sweet, press (white, press (sweet, noChoice))) (c) 2010 bei Prof. Dr. Uwe Kastens -------------------------------------------------------------------------------- Vorlesung Modellierung WS 2011/12 / Folie 326b Ziele: Abfolge von Bedienoperationen modellieren in der Vorlesung: Erläuterungen zu * den beiden Sorten, * den Axiomen: sie identifizieren Terme gleicher Bedeutung; * der Bedeutung der Axiome Übungsaufgaben: Untersuchen und erläutern Sie * Alternativen zu dieser Algebra; * Algebren zur Modellierung von Knöpfen, die nur alternative betätigt werden können. Verständnisfragen: Begründen Sie die Bedeutung der Axiome anhand von Termen. --------------------------------------------------------------------------------