Die denotationelle Semantik Funktionensemantik englisch denotational semantics ist in der Theoretischen Informatik eine von mehreren Moglichkeiten eine formale Semantik fur eine formale Sprache zu definieren Die formale Sprache dient hierbei als mathematisches Modell fur eine echte Programmiersprache Somit kann die Wirkungsweise eines Computerprogramms formal beschrieben werden Konkret kann man etwa bei einer gegebenen Belegung fur Eingabevariablen das Endergebnis fur eine Menge von Ausgabevariablen mit der denotationellen Semantik berechnen Es sind auch allgemeinere Korrektheitsbeweise moglich Bei der denotationellen Semantik werden partielle Funktionen verwendet die Zustandsraume aufeinander abbilden Ein Zustand ist hier eine Belegung von Variablen mit konkreten Werten Die denotationelle Semantik wird induktiv uber die syntaktischen Anweisungskonstrukte der formalen Sprache definiert Abhangig von der gewunschten Programmsemantik werden die partiellen Funktionen gewahlt Neben der denotationellen Semantik gibt es auch die operationelle Semantik und die axiomatische Semantik um die Semantik von formalen Sprachen zu beschreiben Definition der semantischen Funktion f BearbeitenSei Z displaystyle mathcal Z nbsp die Menge aller moglichen Zustande Die Wirkung die eine Anweisung A displaystyle A nbsp auf einen Zustand hat ist formal gesprochen eine Abbildung f A Z Z displaystyle f A colon mathcal Z rightarrow mathcal Z nbsp die einem Zustand z Z displaystyle z in mathcal Z nbsp einen Folgezustand z Z displaystyle z in mathcal Z nbsp zuordnet f displaystyle f nbsp bezeichnet die semantische Funktion und ordnet jedem Anweisungskonstrukt eine Bedeutung zu indem sie eine Zustandsanderung des Programms bewirkt Nachfolgend wird die Wirkung der wichtigsten Kontrollstrukturen einer Programmiersprache auf einen Zustand untersucht Die Bedeutung der leeren Anweisung n u l l displaystyle null nbsp f n u l l z z displaystyle f null z z nbsp dd Die leere Anweisung angewendet auf einen Zustand z displaystyle z nbsp verandert den Zustand nicht Die Semantik einer Anweisungsfolge kann folgendermassen beschrieben werden f A 1 A 2 z f A 2 f A 1 z displaystyle f A 1 A 2 z f A 2 f A 1 z nbsp dd Die Bedeutung dieser Befehlssequenz ist die Wirkung von A 2 displaystyle A 2 nbsp angewendet auf den Zustand der sich ergibt nachdem A 1 displaystyle A 1 nbsp auf z displaystyle z nbsp ausgefuhrt wurde Fur die Wirkung einer Zuweisung auf einen Zustand gilt f x E z w e n n E z z s o n s t displaystyle f x E z begin cases bot amp mathrm wenn E z bot z amp mathrm sonst end cases nbsp dd Das Programm terminiert nicht displaystyle bot nbsp wenn die Anweisung oder der Ausdruck E displaystyle E nbsp angewendet auf Zustand z displaystyle z nbsp nicht terminiert In allen anderen Fallen geht das Programm in einen Zustand z displaystyle z nbsp uber Fur die zwei seitige Alternative gilt f i f B t h e n C 1 e l s e C 2 z f C 1 z w e n n B z t r u e f C 2 z w e n n B z f a l s e s o n s t displaystyle f if B then C 1 else C 2 z begin cases f C 1 z amp mathrm wenn B z true f C 2 z amp mathrm wenn B z false bot amp mathrm sonst end cases nbsp dd Der Folgezustand entspricht C 1 displaystyle C 1 nbsp angewendet auf z displaystyle z nbsp wenn B z t r u e displaystyle B z true nbsp Wenn B z f a l s e displaystyle B z false nbsp so wird der nachfolgende Zustand durch C 2 displaystyle C 2 nbsp angewendet auf z displaystyle z nbsp bestimmt In allen anderen Fallen terminiert das Programm nicht Die Bedeutung der Wiederholung definiert sich rekursiv zu f w h i l e B d o L z z w e n n B z f a l s e w e n n B z L z f w h i l e B d o L L z s o n s t displaystyle f while B do L z begin cases z amp mathrm wenn B z false bot amp mathrm wenn B z bot lor L z bot f while B do L L z amp mathrm sonst end cases nbsp dd Falls B z f a l s e displaystyle B z false nbsp so bewirkt die While Anweisung keine Zustandsanderung Wenn B z displaystyle B z bot nbsp oder L z displaystyle L z bot nbsp so terminiert das gesamte Programm nicht In allen anderen Fallen wird erneut die Wiederholungsanweisung w h i l e B d o L displaystyle while B do L nbsp auf den Zustand angewendet der sich nach Ausfuhrung von L z displaystyle L z nbsp ergibt Durch diese rekursive Definition kann man nicht auf die Wirkung dieser Anweisung schliessen Man ist daher am Fixpunkt der Funktion interessiert der die Semantik der While Schleife beschreibt Fixpunkt der While Semantik BearbeitenDer Fixpunkt der Funktion die die Semantik der While Schleife beschreibt wird nachfolgend anhand eines einfachen Beispiels erlautert w h i l e x y d o y y 1 displaystyle while x not y do y y 1 nbsp dd Solange x displaystyle x nbsp ungleich y displaystyle y nbsp wird der Wert der Variablen y displaystyle y nbsp um 1 erhoht Um den Fixpunkt dieser Gleichung zu bestimmen bedient man sich des Tarskischen Fixpunktsatzes Dieser Satz besagt dass fur eine geordnete Menge M displaystyle mathcal M nbsp welche ein kleinstes Element besitzt und eine streng monotone Funktion welche M displaystyle mathcal M nbsp auf sich selbst abbildet ein kleinster Fixpunkt existiert Damit der Satz angewendet werden kann muss zuerst eine geordnete Menge fur das Beispiel definiert werden Sei w Z Z Z Z displaystyle w colon mathbb Z times mathbb Z rightarrow mathbb Z times mathbb Z nbsp die partielle Funktion der While Schleife aus dem Beispiel Diese bildet einen Zustand bestehend aus der Belegung x y displaystyle x y nbsp fur die gleichnamigen Variablen in einen anderen Zustand mit der Variablenbelegung x y displaystyle x y nbsp ab Die Variablen x displaystyle x nbsp und y displaystyle y nbsp sind dabei ganzzahlig Sei nun P Z Z displaystyle mathcal P mathbb Z times mathbb Z nbsp die Menge aller partiellen Funktionen w displaystyle w nbsp Die partielle Ordnung displaystyle sqsubseteq nbsp fur zwei partielle Funktionen w displaystyle w nbsp w P Z Z displaystyle w in mathcal P mathbb Z times mathbb Z nbsp sei wie folgt definiert w w dom w dom w w x y x y w x y x y displaystyle w sqsubseteq w Leftrightarrow operatorname dom w subseteq operatorname dom w wedge w x y x y Rightarrow w x y x y nbsp dd Die partielle Abbildung w displaystyle w nbsp ist kleiner gleich w displaystyle w nbsp genau dann wenn der Definitionsbereich von w displaystyle w nbsp eine Teilmenge des Definitionsbereichs von w displaystyle w nbsp ist Zudem muss gelten dass wenn w x y displaystyle w x y nbsp eine Zustandsanderung nach x y displaystyle x y nbsp bewirkt auch Funktion w x y displaystyle w x y nbsp nach x y displaystyle x y nbsp abbildet Das kleinste Element der Menge P Z Z displaystyle mathcal P mathbb Z times mathbb Z nbsp ist die nirgends definierte Funktion displaystyle bot nbsp Um den Satz von Tarski verwenden zu konnen fehlt nun noch eine streng monotone Funktion die P Z Z displaystyle mathcal P mathbb Z times mathbb Z nbsp auf sich selbst abbildet Dazu wird eine Funktion f displaystyle f nbsp definiert f P Z Z P Z Z displaystyle f colon mathcal P mathbb Z times mathbb Z rightarrow mathcal P mathbb Z times mathbb Z nbsp dd Laut obigen Beispiel gilt fur f displaystyle f nbsp f w x y x y w e n n x y w x y 1 s o n s t displaystyle f w x y begin cases x y amp mathrm wenn x y w x y 1 amp mathrm sonst end cases nbsp dd Weiterhin sei w n 1 f w n n N displaystyle w n 1 f w n forall n in mathbb N nbsp dd Nun sind alle Voraussetzungen des Fixpunktsatzes erfullt es existiert ein Fixpunkt Den Fixpunkt berechnet man durch Grenzwertbildung der Funktion f displaystyle f nbsp Um auf den Grenzwert schliessen zu konnen beginnt man mit dem Ausrechnen einzelner Funktionswerte w 0 x y displaystyle w 0 x y bot nbsp da w 0 displaystyle w 0 nbsp das kleinste Element der Menge P Z Z displaystyle mathcal P mathbb Z times mathbb Z nbsp ist w 1 x y displaystyle w 1 x y nbsp ist laut Definition der Funktion f displaystyle f nbsp w 1 x y f w 0 x y x y w e n n x y w 0 x y 1 s o n s t displaystyle w 1 x y f w 0 x y begin cases x y amp mathrm wenn x y w 0 x y 1 bot amp mathrm sonst end cases nbsp dd w 2 x y displaystyle w 2 x y nbsp ergibt sich zu w 2 x y f w 1 x y x y w e n n x y w 1 x y 1 x y 1 w e n n x y 1 s o n s t displaystyle w 2 x y f w 1 x y begin cases x y amp mathrm wenn x y w 1 x y 1 begin cases x y 1 amp mathrm wenn x y 1 bot amp mathrm sonst end cases end cases nbsp dd Fur w n displaystyle w n nbsp kann formuliert werden w n x y f w n 1 x y x x w e n n x n 1 y x s o n s t displaystyle w n x y f w n 1 x y begin cases x x amp mathrm wenn x n 1 leq y leq x bot amp mathrm sonst end cases nbsp dd Der Grenzwert w w n n N displaystyle w infty w n forall n in mathbb N nbsp sei nun w x y x x w e n n y x s o n s t displaystyle w infty x y begin cases x x amp mathrm wenn infty leq y leq x bot amp mathrm sonst end cases nbsp dd Fur den Fixpunkt muss nun gelten dass f w x y w x y displaystyle f w infty x y w infty x y nbsp f w x y x y w e n n x y w x y 1 x x w e n n y lt x s o n s t displaystyle f w infty x y begin cases x y amp mathrm wenn x y w infty x y 1 begin cases x x amp mathrm wenn infty leq y lt x bot amp mathrm sonst end cases end cases nbsp dd Dies kann umgeformt werden zu f w x y x x w e n n y x s o n s t displaystyle f w infty x y begin cases x x amp mathrm wenn infty leq y leq x bot amp mathrm sonst end cases nbsp dd Somit gilt f w x y w x y displaystyle f w infty x y w infty x y nbsp Der Fixpunkt ist gefunden Die Bedeutung der While Schleife aus dem Beispiel ergibt sich aus dem Fixpunkt Die Schleife terminiert wenn y x displaystyle y leq x nbsp und liefert das Tupel x x displaystyle x x nbsp Falls y gt x displaystyle y gt x nbsp so terminiert die Schleife nicht Literatur BearbeitenPeter Schroeder Heister Semantik denotationelle in Jurgen Mittelstrass Hrsg Enzyklopadie Philosophie und Wissenschaftstheorie 2 Auflage Band 7 Re Te Stuttgart Metzler 2018 ISBN 978 3 476 02106 9 S 341 342 untechnische allgemeine Beschreibung mit Literaturverzeichnis Abgerufen von https de wikipedia org w index php title Denotationelle Semantik amp oldid 191648500
