Grundlagen der Programmierung 2 Operationale Semantikprg2/SS2007/...Semantik von Haskell ist...

Grundlagen der Programmierung 2

Operationale Semantik

Prof. Dr. Manfred Schmidt-Schauÿ

Künstliche Intelligenz und Softwaretechnologie

15. Mai 2007

Semantik von Programmiersprachen

Grundlagen der Programmierung 2 - 2 -

Semantik = Bedeutung eines Programms (Programmtextes)

ausgehend vom Syntaxbaum des Programms.

Methoden der Semantik-Definition:


Denotationale Semantik

Transformations-Semantik

axiomatische Semantik



Spezifikation von Wirkung und Ablauf:

Zustand: Speicherbelegung als Datenstruktur oder . . .Pro Programmkonstrukt: Angabe des Zustandsübergangs

Haskell: Zustand = AusdruckÜbergänge: = Reduktionen, d.h. Änderungen der Ausdrücke.

Python: Zustand = UmgebungÜbergänge: = Veränderungen des Speicherinhalts.

operationale Semantik = Spezifikation eines Interpreters

Vorteil: Prinzipiell immer durchführbar

Denotationale Semantik


Zuordnung: Programm 7→ Funktion

Domain D: Menge der möglichen Funktionenund Objekte

Pro Programmkonstrukt: rekursive Angabe der Konstruktion einer

Funktion in D.

Hürden: Mathematisches Vorwissen notwendigDomainkonstruktion kann schwierig seinMeist nur für kleines Fragment einer Programmiersprache

Transformations-Semantik


Vorgehen zur Definition der Semantik eines Programms P ,

wenn die Semantik bereits für eine Untermenge der Programme erklärt

• Transformiere P → . . . → P ′• Nehme die Semantik von P ′.

Verwendung:

Semantik einer vollen Programmiersprache erklärt durch:• Semantik der Kernsprache• Transformation: volle Sprache −→ Kernsprache.

Semantik von Haskell ist teilweise eine Transformationssemantik

Vorteile: Vereinfacht Semantik-DefinitionAnalog zur Arbeitsweise von Compilern

Axiomatische Semantik


Beschreibung der Programmkonstrukte und Eigenschaften von Pro-

grammen mittels logischer Axiome

Herleiten von Programmeigenschaften durch logisches Schließen

Z.B. in Prädikatenlogik:

Für alle Eingaben n von natürlichen Zahlen

liefert quadrat n das Ergebnis n2. Als Formel:

∀n : quadrat(n) = n2

Axiomatische Semantik


Hoare-Logik:

{x > 2} x := x+1 {x > 3}

Vorbedingung

Programmbefehl

Nachbedingung

Auswertung von einfachen Haskell-Programmen:


Ziel: operationale Semantik von Haskell

• formal saubere Definition der Auswertung

• auch für Funktionen höherer Ordnung

• Unabhängigkeit von Compilern

• Unabhängigkeit vom Rechnertyp (Portabilität)

Einfache Haskell-Programme


Definition: Basiswert ist entweder eine Zahl,ein Zeichen oder True,False.

Einfache Haskell-Programme: dürfen benutzen:

• Basiswerte und entsprechende vordefinierte Operatoren• Funktionsdefinitionen• if-then-else• Anwendung von Funktionen auf Argumente

Einfache Haskell-Programme (2)


Definition:

Ein (einfaches) Haskell-Programm besteht aus:• Menge von Funktionsdefinitionen; entsprechend obiger Beschränkungen• Ausdruck (main) vom Typ eines Basiswertes.

Wert des Programms = Wert von main

Beispiel

quadrat x = x * x

kubik x = x * x * x

w = 2

main = if w >= 0 then quadrat w else kubik w

Berechnung und Auswertung


Prinzip der Berechnung für einfache Haskell-Programme

Auswertung =Folge von Transformationen

von main

bis ein Basiswert erreicht ist

main → t1 → t2 → . . . → tn → . . .

Es gibt drei Fälle:1. Die Folge endet mit einem Basiswert2. Die Folge endet, aber nicht mit einem Basiswert3. Die Folge endet nicht

Bei 2. und 3.: Wert undefiniert.

Auswertung


Einfache Haskell-Programm haben drei verschiedene

Arten von Auswertungsschritten

1. Definitionseinsetzung (δ-Reduktion)

2. Arithmetische Auswertung

3. Auswertung von Fallunterscheidungen

Satz von Church und Rosser


Satz (Church-Rosser 1) Sei P ein einfaches Haskell-Programm,

R1, R2 zwei verschiedene Reduktionsfolgen für main

mit jeweiligen Resultat-Basiswerten e1 bzw. e2

dann sind diese Basiswerte gleich, d.h. e1 = e2

Werte von Programmen


Definition: Sei P ein einfaches Haskell-Programm und

main von numerischem oder Booleschem Typ.

Der Wert des Programms P ist:

e wenn es eine terminierende Reduktionsfolge, ausgehend

von main gibt, die mit dem Basiswert e endet,

⊥ ( undefiniert ) wenn es keine mit einem Basiswert terminierende Reduk-tionsfolge ausgehend von main gibt.

Aus dem Satz von Church-Rosser-1 folgt:

Ein einfaches Haskell-Programm

hat einen eindeutig definierten Wert

unabhängig von der Art der Auswertung

Satz 2 von Church und Rosser


SATZ (Church-Rosser-2) Sei P ein einfaches Haskell-Programm.

Wenn es irgendeine Reduktionsfolge für main gibt,

die mit einem Basiswert e terminiert,

dann terminiert auch die normale Reihenfolge der Auswertung von main

und liefert als Basiswert (Resultat) genau e.

Die normale Reihenfolge ist ausreichend zur Auswertung

Haskell benutzt normale Reihenfolge der Auswertung

Gegenbeispiel zu C.R. 2 bei applikativ


Church-Rosser-2 gilt nicht für die applikative Reihenfolge:

nt x = nt x

proj x y = x

main = proj 0 (nt 1)

applikative Reihenfolge für main terminiert nicht:

(nt 1) → (nt 1) → (nt 1) → . . . . . .Deshalb:

proj 0 (nt 1) → proj 0 (nt 1) → . . . . . .

Die normale Reihenfolge liefert sofort 0.

Programmtransformationen


Optimierung: Programm P wird zur Compilezeit mittels

Transformationen in ein anderes Programm P ′ umgewandelt,welches weniger Ressourcen benötigt, aber den gleichen Effekt hat.

”gleicher Effekt” (∼) :• ∼ ist mithilfe der operationalen Semantik definierbar• Äquivalenzrelation ∼ auf Programmen

und Funktionen vom gleichen Typ• Verschiedene Zahlen und Boolesche Werte

sind verschieden unter ∼.



Aussage:

Für einfache Haskellprogramme gilt:

Alle bisher betrachteten Reduktionen, auch deren Umkehrung, sind

auch als Compilezeit-Transformationen verwendbar.

D.h. Wenn P → P ′ mit einer Reduktion, dann gilt auch P ∼ P ′.

Begründung: 1. Satz von Church-Rosser:

Wenn P zu e auswertet und P → P ′ ist eine Transformation,dann wertet auch P ′ zu e aus.



Beispiel:[x]++xs

→ x:( [] ++ xs) Reduktion für append→ x:xs Transformation mittels append

=⇒ [x]++xs kann zu x:xs vereinfacht werden



Bei applikativer Reihenfolge der Auswertung

sind diese Transformationen nicht korrekt,

sowie in Programmiersprachen, die appl. Reihenfolge verwenden.

Ein terminierendes Programm kann zu einem nichtterminierenden wer-

den:

meinif b x y = if b then x else y

main = meinf True True bot

Nach der Transformation:

main = if True then True else bot

D.h. auch: ein nichtterminierendes Programm kann zu einem terminie-

renden werden.

Church-Rosser-Sätze auch für Konstruktoren


Verallgemeinerter Wert statt Basiswert; auch Listen sind Werte:

Ein (verallgemeinerter) Wert ist entweder1. ein Basiswert d.h. eine Zahl oder einer der

Wahrheitswerte True, False,

oder2. eine Applikation (c t1 . . . tn), wobei c ein Konstruktor ist

mit der Stelligkeit n

Beispiele: [1,2,3,4]1: (map quadrat [2,3,4])

Beachte: verallgemeinerte Werte können unausgewertete Unteraus-

drücke haben

Church-Rosser-Sätze für Haskell-Programmemit Listen


Satz(Church-Rosser-1) Sei P ein Haskell-Programm,wobei Konstruktoren und case erlaubt sind, undmain den Typ eines verallgemeinerten Basiswertes hat.

Wenn zwei verschiedene Reduktionsfolgen jeweilsverallgemeinerte Werte e1 bzw. e2 ergeben,dann gibt es einen weiteren verallgemeinerten Wert e3,so dass sowohl e1 als auch e2 zu e3 (in keinem, einem oder mehrerenSchritten) reduziert werden können:

P

~~||||

||||

||||

||||

|

BBB

BBBB

BBBB

BBBB

BB

e1

!!BB

BB

BB

BB

Be2

}}||

||

||

||

|

e3

Church-Rosser-Sätze; Beispiele


Beispiel: Der Ausdruck [3+4,5+6] ist schon ein Wert,auf zwei Arten reduzierbar:

[3 + 4,5 + 6]

wwnnnnnn

nnnnnn

nnnnnn

nnnnnn

nnn

((PPPPP

PPPPPP

PPPPPP

PPPPPP

PPPPP

[7,5 + 6]

''PPP

PPPP

PPPP

PPP

[3 + 4,11]

vvn nn n

n nn n

n nn n

n n

[7,11]

Church-Rosser-Sätze; Beispiele


Beachte: Normalform muss nicht existieren

Beispiel

(3 + 4) : ((5 + 6) : [1..]

ttiiiiiiii

iiiiiiii

iiiiiiii

iiiiiiii

iiiiiii

**UUUUUUU

UUUUUUUU

UUUUUUUU

UUUUUUUU

UUUUUUUU

U

7 : ((5 + 6) : [1..]

**UUUUUUU

UUUUUUUU

UUUUUUUU

UUUUUUUU

UUUUUUUU

(3 + 4) : (11 : [1..])

ttiiiiiiii

iiiiiiii

iiiiiiii

iiiiiiii

iiiiiiii

7 : 11 : [1..]

Church-Rosser-Satz 2


Satz (Church-Rosser-2) Sei P ein let-freies Haskell-Programm.

Wenn irgendeine Reduktionsfolge main zu einem verallg. Wert e redu-

ziert,

dann terminiert auch die normale Reihenfolge der Auswertung von main

mit einem verallg. Wert e1,

und e1 ist reduzierbar zu e.

P

e

e

1

Ex: n

orma

le Au

sw.

v. Wert

Church-Rosser-Satz 2. Beispiel


[3+4]++[5+6]

[3+4,5+6]

[3+4,11]

norm

ale A

usw.

Haskell mit rekursivem let


Church-Rosser-Sätze gelten nicht in vollem Haskell

Grund: rekursives let.

Church-Rosser-Sätze sind zu syntaktisch

Church-Rosser-Sätze: Verallgemeinerung


Notwendig: Konzept der Verhaltensgleichheit ∼ von Ausdrücken:

• verschiedene Basiswerte a, b sind nicht verhaltensgleich:a 6= b ⇒ a 6∼ b

• man kann Gleiches durch Gleiches ersetzena ∼ b ⇒ P [a] ∼ P [b]

Nachzuweisen ist dann:• Reduktion erhält Verhaltensgleichheit:

s → t ⇒ s ∼ t

Induktion und Co-Induktion zum Nachweis derGleichheit von Ausdrücken


Induktionsschema für endliche Listen xs:

1. Zeige die Behauptung für xs = [].2. Zeige, dass die Behauptung für x : xs gilt

unter der Annahme, dass sie für xs gilt.

Co-Induktion für Listen


Co-Induktionsschema für endliche und unendliche Listen xs:

1. Zeige die Behauptung für xs = [].2. Zeige die Behauptung für xs = ⊥.3. Zeige, dass die Behauptung für x : xs gilt

unter der Annahme, dass sie für xs gilt.

Induktion für endliche Listen. Beispiel


Zeige: length(xs ++ ys) = length(xs) + length(ys)für alle endlichen Listen xs,ys

Basisfall:

length([] ++ ys ) = length(ys),

und length([]) + length(ys) = length(ys)

Induktion. Beispiel


Zeige: length(xs ++ ys) = length(xs) + length(ys)für alle endlichen Listen xs,ys

Induktionsfall: xs ist eine Liste der Länge n + 1.

Auswertung beider Seiten, wobei xs = x:xs’.

length(xs ++ ys) → length((x:xs’ ++ ys)→ length((x:(xs’ ++ ys)) →1+ length((xs’ ++ ys)) = 1+ length(xs’)+ length(ys)).

length(xs) + length(ys) = length(x:xs’) + length(ys) →1+ length(xs’) + length(ys).

Grundlagen der Programmierung 2 Operationale Semantikprg2/SS2007/...Semantik von Haskell ist...

Documents

Transcript of Grundlagen der Programmierung 2 Operationale Semantikprg2/SS2007/...Semantik von Haskell ist...