1 Vollst andige partielle Ordnungen, stetige Funk- tionen · Dann hat feinen kleinsten Fixpunkt....

TIDS 2, SS13, Kapitel 1, vom 11.4.2013 1

1 Vollstandige partielle Ordnungen, stetige Funk-tionen

Die Betrachtung vollstandiger partieller Ordnungen soll eine einfache undverstandliche Einfuhrung in einen Ansatz zur denotationellen Semantik lie-fern. Die Sprache, die wir dazu betrachten werden, ist PCF, eine Varianteeiner funktionalen Programmiersprache.

Polymorph getypte funktionale Programmiersprachen und deren deno-tationelle Semantik wurden den Rahmen dieser Vorlesung sprengen.

Definition 1.1 Eine partielle Ordnung ≤ auf einer Menge P ist definiertdurch die Eigenschaften:

• reflexiv: ∀x ∈ P : x ≤ x

• transitiv: ∀x, y, z ∈ P : x ≤ y, y ≤ z =⇒ x ≤ z

• antisymmetrisch ∀x, y,∈ P : x ≤ y ∧ y ≤ x =⇒ x = y

Definition 1.2 Sei X ⊆ P .

• Sei p ∈ P . Wenn ∀x ∈ X : x ≤ p dann ist p obere Schranke von X.

• p ∈ P ist eine kleinste obere Schranke (obere Grenze, lub, least upperbound) von X, wenn p obere Schranke von X und fur jede andere obereSchranke q von X gilt p ≤ q. Bezeichnung: p =

⊔X.

• Analog kann man untere Schranken, glb, untere Grenze usw. definieren

Definition 1.3 Eine Folge a1 ≤ a2 ≤ a3 ≤ . . . mit Elementen ai ∈ P heißtKette (ω-Kette).

• Die partielle Ordnung ≤ auf P ist vollstandig, wenn jede aufsteigendeKette a1 ≤ a2 ≤ a3 ≤ . . . eine kleinste obere Schranke in P hat.Bezeichnung:

⊔i ai.

• Wenn die partielle Ordnung P ein kleinstes Element ⊥ hat, dann sagtman, ≤ ist eine Ordnung mit kleinstem Element.

• Als Abkurzung sprechen wir bei einer vollstandig partiellen Ordnungmit kleinstem Element von einer cpo mit ⊥. Wenn die Bezeichnung ⊥nicht eindeutig ist, indizieren wir das ⊥ mit der zugehorigen cpo.

Wir beschaftigen uns im folgenden mit vollstandigen partiellen Ordnun-gen (cpo’s).

Beispiel 1.4


• Die Potenzmenge einer Menge mit ⊆ ist eine cpo mit kleinstem Ele-ment. Fur eine aufsteigende Kette M1 ⊆ M2 ⊆ M3 ⊆ . . . gilt⊔iMi =

⋃iMi.

• Die Menge der partiellen Funktionen: M →M mit der Teilmengenbe-ziehung ist eine cpo mit kleinstem Element.

• Die zweielementige Menge {⊥,>} mit ⊥ ≤ > ist eine cpo.

Eine diskrete (flache) cpo ist eine partielle Ordnung, in der nur x ≤ xfur alle Elemente x gilt.

Definition 1.5

Monotonie Eine Funktion f : D → E, wobei D,E cpo’s sind, ist monoton,gdw. fur alle d1 ≤D d2 gilt, dass auch f(d1) ≤E f(d2).

Stetigkeit Die Funktion f : D → E ist stetig, wenn sie monoton ist undwenn fur alle Ketten d1 ≤D d2 ≤D d3 ≤D . . . gilt, dass f(

⊔i di) =⊔

i f(di).

Bemerkung 1.6 Die Intuition dahinter ist:

stetig = algorithmisch sinnvoll

Bei Anwendung auf eine Programmiersprache wird sich ergeben, dassalle berechenbaren Funktionen eine stetige Denotation haben.

In manchen Semantiken kommt es vor, dass es stetige Funktionen gibt,die nicht Denotation einer Funktion sind.

Im folgenden bezeichnen wir fur eine Funktion f : D → D. die mehrfacheAnwendung f(. . . f︸︷︷︸

n

(d) auch als fn(d).

Beispiel 1.7 Alle Funktionen, die auf einer diskreten cpo definiert sind,sind stetig.

Eine wichtige Beobachtung, die in ahnlicher Form oft verwendet wirdzur Konstruktion kleinster Fixpunkte, ist folgendes:In einer cpo mit ⊥ sei eine monotone Funktion f gegeben. Dann ist f i(⊥)eine Kette. Es gilt ⊥ ≤ f(⊥) ≤ f(f(⊥)) ≤ . . . ≤ fn(⊥) ≤ fn+1(⊥) ≤ . . ..

Aussage 1.8

• Die Identitat auf einer cpo ist stetig

• Die Komposition von stetigen Funktionen ist stetig. D.h. f◦g ist stetig,wenn f, g stetig sind.


Beweis. Die Identitat ist monoton. Da eine Kette unter Id auf sich selbstabgebildet wird, gilt das auch fur den lub der Kette(n).

Der Rest ist eine Ubungsaufgabe. 2

Definition 1.9 Sei f : D → D eine Funktion, wobei D eine cpo ist. Dannist d ∈ D ein

• Fixpunkt von f , wenn f(d) = d ist.

• Prafix-punkt von f , falls f(d) ≤ d

• Postfix-punkt von f , falls d ≤ f(d).

Satz 1.10 (Fixpunktsatz)Sei f : D → D eine stetige Funktion, wobei D eine cpo mit kleinstemElement ⊥ ist. Dann hat f einen Fixpunkt, insbesondere einen kleinstenFixpunkt a. Zudem gilt a =

⊔fn(⊥). a ist auch der kleinste Prafix-punkt

von f . Diesen kleinsten Fixpunkt nennen wir fix(f).

Beweis. Da D eine cpo ist, existiert⊔fn(⊥)). Es gilt:

f(⊔fn(⊥))

=⊔fn+1(⊥)) (Stetigkeit von f und da

⊥ ≤ f(⊥) ≤ ...fn(⊥) . . .aufsteigende Kette ist)

=⊔fn(⊥)) da f(⊥) ≥ ⊥ und es bis auf ⊥ die gleiche Kette ist.

Damit haben wir gezeigt, dass⊔fn(⊥)) ein Fixpunkt von f ist. Jetzt

zeigen wir, dass dies auch der kleinste ist.Sei d irgendein Fixpunkt von f . D.h. f(d) = d.

Dann gilt: ⊥ ≤ d, also auch f(⊥) ≤ d = f(d), da f monoton ist. MitInduktion nach n erhalt man: fn(⊥) ≤ d, also auch

⊔fn(⊥)) ≤ d, da⊔

fn(⊥)) kleinste obere Schranke der aufsteigenden Kette ⊥ ≤ f(⊥) ≤...fn(⊥) . . . ist.

Dieselbe Argumentation zeigt auch dass⊔fn(⊥)) kleinster Prafixpunkt

von f ist. 2

Es gilt folgender allgemeinerer Satz (siehe z.B. Davey und Priestley)

Satz 1.11 Sei f : D → D eine monotone Funktion, wobei D eine cpo ist.Dann hat f einen kleinsten Fixpunkt.

Allerdings ist der kleinste Fixpunkt in diesem allgemeinen Fall i.a. nicht als⊔fn(⊥) konstruierbar, auch wenn es ein kleinstes Element ⊥ gibt.

Beispiel 1.12 Fur eine nicht-monotone Funktion.Gegeben sei die Boolesche cpo: {True, False,⊥} mit ⊥ ≤ True, ⊥ ≤ False.Die Funktion, die Terminierung testet ist:


f : ⊥ → False, True→ True, False→ True.Diese Funktion f ist nicht monoton. Denn: ⊥ ≤ True, aber f ⊥ = False 6≤True = f True.

Beispiel 1.13 Fur eine monotone, aber nicht stetige Funktion.Betrachte unendliche Strings (oder alternativ unendliche Listen).

Wir wollen Eingabestrome modellieren, wobei diese endlich oder unend-lich sein konnen, und nur aus 0, 1, bestehen.Modellierung: Als Menge benutzen wir (endliche und unendliche) Stringsbestehend aus 0, 1 und $, wobei $ nur am Ende sein darf. Endliche Stringsohne $ am Ende betrachtet man als unvollstandige Strings (bzw. Eingabe).

Formal konnte man schreiben S := ({0, 1}∗ + {0, 1}∗$) ∪ { alle unendli-chen Folgen bestehend aus 0,1 }.

ε bezeichne den leeren String. Als Ordnung verwenden wir s ≤ t, wenns Prafix von t.

Maximale Strings in S sind die unendlichen und mit $ beendete Strings.Die Menge S ist eine cpo mit kleinstem Element ε: Vollstandigkeit: interes-sant sind nur die unendlichen (echten) Folgen. Deren lubs sind unendlicheStrings.

Wir betrachten eine Funktion auf S, die durch Durchlesen des Stringsvon links nach rechts feststellt, ob eine 1 in einem String ist oder nicht:

hateins : S → {True, False}

Das Problem ist jetzt, dass diese Funktion zwar leicht ja sagen kann,aber nein nur, wenn sie bis zum $ keine 1 gefunden hat. Sind bis zu einemZeitpunkt nur 0’en aufgetaucht, so gibt es noch keine Antwort. hateins(ε)bedeutet, dass im Moment auf weitere Eingabe gewartet werden muß.

Im schlechtesten Fall gibt diese Funktion keine Antwort: wenn der un-endlich lange String aus 0’en die Eingabe ist. Entweder ist dann unsereFunktion partiell oder wir brauchen einen Wert “unbekannt“. Da wir bereitsfestgestellt haben, dass partielle Funktionen auch als totale Funktionen aufeinem mit ⊥ erweiterten Bereich modelliert werden konnen, nehmen wir diezweite Alternative:{True, False,⊥} mit ⊥ ≤ True und ⊥ ≤ False.Die Anforderungen an hateins sind:hateins(1s) = True

hateins($) = Falsehateins(0s) = hateins(s)hateins(ε) = ⊥

Diese bestimmen den Wert fur den unendlichen String aus Nullen000 . . . = 0ω nicht eindeutig.

Sinnvoll waren False oder ⊥. Der logisch richtige Wert ware False,aber dieser laßt sich algorithmisch erst nach unendlich vielen Uberprufungenbestimmen.


Betrachtet man das Verhalten der Funktionen bzgl. der cpo, dann kor-respondiert das “richtige“ Berechnungsverhalten zur Stetigkeit der Funktionhateins.00 . . . laßt sich approximieren durch die aufsteigende Folge: ε, 0, 00, 000, . . ..

Der lub davon ist gerade 0ω. Der jeweilige Wert vonhateins(ε), hateins(0), . . . . . . ist ⊥. Stetigkeit bedeutet dann, dasshateins(0ω) = ⊥.

Die Funktion hateins′ mit hateins′(0ω) = False ware nicht mehr ste-tig, da False nicht der lub der approximierenden Folge ist.

1.0.1 Vollstandige Verbande, Knaster-Tarski Fixpunktsatz

Wir erwahnen noch den Fixpunktsatz fur vollstandige Verbande.

Definition 1.14

• Eine Ordnung ≤ auf D ist ein Verband, gdw, fur beliebige Elementex, y ∈ D sowohl glb(x, y) als auch lub(x, y) in D existieren.

• Eine Ordnung ≤ auf D ist ein vollstandiger Verband gdw. fur beliebigeTeilmengen A ⊆ D sowohl glb(A) als auch lub(A) existiert (eindeutig).

Ein vollstandiger Verband ist insbesondere eine cpo mit ⊥, denn jedervollstandige Verband hat ein kleinstes und ein großtes Element.

Die Potenzmenge P(M) einer Menge M ist immer ein vollstandiger Ver-band bzgl ⊆. lub und glb sind durch

⋃{Mi} bzw. durch

⋂{Mi} definiert.

In einem Verband genugt die Monotonie einer Funktion zur Existenzeines Fixpunktes. Der ist auch einfach zu konstruieren.

Satz 1.15 (Knaster, Tarski) Sei D ein Verband und Φ : D → D einemonotone Abbildung. Dann existiert ein kleinster und großter Fixpunkt vonΦ: der kleinste Fixpunkt ist

∧{x | Φ(x) ≤ x}.

Beweis. Sei H := {x ∈ D | Φ(x) ≤ x} und sei α =∧H. Fur alle x ∈ H

gilt α ≤ x, also gilt Φ(α) ≤ Φ(x) ≤ x (Monotonie). Deshalb ist Φ(α) untereSchranke von H; somit Φ(α) ≤ α.

Aus Φ(α) ≤ α folgt jetzt Φ(Φ(α)) ≤ Φ(α) und damit nach Definiti-on von H auch Φ(α) ∈ H D.h. aber, α ≤ Φ(α) und somit folgt aus derAntisymmetrie: α = Φ(α). D.h. α ist ein Fixpunkt.

Da alle Fixpunkte β per Definition in H sind, muß α kleinster Fixpunktvon Φ sein. 2


1.1 Konstruktion neuer cpo’s

Wir konstruieren neue vollstandige partielle Ordnungen, um aus einfachensemantischen Bereichen, wie z.B. dem der naturlichen Zahlen und der Boo-leschen Werte neue cpos, d.h. neue semantische Bereiche zu konstruieren.Wir werden sehen, dass den Konstruktionsverfahren jeweils bestimmte Pro-grammkonstrukte entsprechen.

Zunachst benotigen wir den Begriff der Isomorphie zweier cpo’s:

Definition 1.16 Seien D,E zwei cpo’s. Eine stetige Funktion f : D → Eist ein Isomorphismus, wenn sie eine Bijektion ist und wenn es eine stetige,bijektive Funktion g : E → D gibt, so dass f ◦ g = IdE und g ◦ f = IdD ist.D und E heißen dann isomorph.

I. a. unterscheiden wir isomorphe cpo’ s nicht, da sie im wesentlichen dasselbeObjekt sind.

Aussage 1.17 Seien D,E zwei cpo’s. Eine Funktion f : D → E ist einIsomorphismus, gdw. f eine Bijektion ist mit x ≤D y gdw. f(x) ≤E f(y).

Beweis. Die eine Richtung ist offensichtlich.Sei f : D → E eine Bijektion mit x ≤D y gdw. f(x) ≤E f(y). Sei g dieinverse Funktion zu f . Aus der Voraussetzung folgt, dass g ebenfalls dieMonotonie-Eigenschaft von f hat. Sei a1 ≤D a2 ≤D . . . eine aufsteigendeKette und sei a die kleinste obere Schranke zu ai. Dann existiert zu f(a1) ≤Ef(a2) ≤E . . . eine kleinste obere Schranke e. Da f(ai) ≤E f(a) fur alle i,gilt e ≤ f(a). Wegen der Voraussetzung ist ai ≤ g(e) fur alle i, d.h. g(e) istobere Schranke der ai mit g(e) ≤ a. Da a obere Grenze ist, gilt g(e) = a unddamit auch e = f(a). D.h. f ist stetig. Die Funktion g ist ebenfalls stetig,da g die Voraussetzung der Proposition erfullt. 2

1.2 Diskrete cpo’s

In diskreten cpo’s gilt nur x ≤ x fur alle x ∈ D. Jede Kette ist konstant: x ≤x ≤ . . .. Diese cpo’s kommen vor bei Booleschen Wahrheitswerten, oder derMenge der Zahlen. Die Zahlen sind bzgl. Informationsgehalt unvergleichbar,da sie jeweils den maximalen Informationsgehalt reprasentieren.

Es gilt: Jede Funktion f : D → E ist stetig, wenn D eine diskrete cpoist.

1.3 Endliche Produkte.

Seien Di, i = 1, . . . , k cpo’s. Wir konnen immer annehmen, dass die Mengendisjunkt sind. D1 × . . . × Dk ist das zugehorige cartesische Produkt (dieMenge der k-Tupel). Die Ordnung darauf ist punktweise definiert:


(d1, . . . , dk) ≤ (d′1, . . . , d′k) gdw. di ≤ d′i fur alle i.

Es gilt fur Ketten von Tupeln (d1j , . . . , dkj), dass⊔j(d1j , . . . , dkj) =

(⊔j d1j , . . . ,

⊔j dkj). (Ubungsaufgabe)

Die Projektionsfunktionen πi sind definiert durch πi(d1, . . . , dk) = di.Diese Projektionsfunktionen sind stetig.

Tupelbildung kann man fur Funktionen ebenfalls verwenden:Seien fi : E → Di, i = 1, . . . , k stetige Funktionen auf den cpo’s E,Di.Dann ist die Funktion 〈f1, . . . , fk〉 : E → (D1, . . . , Dk) definiert durch〈f1, . . . , fk〉 e := (f1(e), . . . , fk(e)). Die Funktion 〈f1, . . . , fk〉 erfullt πi ◦〈f1, . . . , fk〉 = fi. Die Funktion 〈f1, . . . , fk〉 ist offenbar monoton.

Sie ist auch stetig:Sei e0 ≤ e1 ≤ e2 ≤ . . . eine Kette in E.

〈f1, . . . , fk〉(⊔i ei)

= (f1(⊔i ei), . . . , fk(

⊔i ei))

= (⊔i(f1(ei), . . . ,

⊔i fk(ei)) da alle fi stetig sind

=⊔i((f1(ei), . . . , fk(ei)) (Definition des Produktes)

=⊔i 〈f1, . . . , fk〉(ei) Definition von 〈. . .〉

Die Produktbildung kann man fur Funktionen und Kreuzprodukt voncpo’s gemeinsam machen:Seien fi : Di → Ei stetige Funktionen auf cpo’s. Dann istf1 × . . . × fk : D1 × . . . × Dk → E1 × . . . × Ek definiert durch f1 × . . . ×fk(d1, . . . , dk) = (f1(d1), . . . , fk(dk)).

Dies kann man schreiben als f1 × . . .× fk = 〈f1 ◦ π1, . . . , fk ◦ πk〉.Daraus kann man schließen, dass diese Funktion ebenfalls stetig ist.

Lemma 1.18 Sei h : E → D1× . . .×Dk eine Funktion auf cpo’s. Dann isth stetig gdw. πi ◦ h stetig ist fur alle i.

Beweis. “ =⇒ “: Komposition ist stetig.“⇐“: Nehme an, dass πi ◦ h stetig ist fur alle i. Dann kann man h ausstetigen Operationen rekonstruieren: h(x) = (π1 ◦ h(x), . . . , πk ◦ h(x)) =〈(π1 ◦ h, . . . , πk ◦ h〉(x). Diese Funktion ist stetig, da πi ◦ h stetig ist, und〈. . .〉 stetige Funktionen erzeugt. 2

Wir zeigen auch eine analoge Aussage fur eine Funktion h : D1 × . . . ×Dk → E. Diese Aussage ist etwas schwerer zu zeigen.

Dazu benotigen wir ein Lemma uber lubs von aufsteigenden arrays.

Lemma 1.19 Sei ei,j Elemente einer cpo E, so dass ei,j ≤ ei′,j′ wenn i ≤ i′und j ≤ j′. Dann gilt: {ei,j | i, j ∈ IN} hat eine kleinste obere Schranke und⊔

i,j

ei,j =⊔i

(⊔j

ei,j) =⊔j

(⊔i

ei,j) =⊔i

ei,i


Beweis. Es ist eine leichte Ubung, zu zeigen, dass die Mengen{ei,j}, {ei,i}, {

⊔j ei,j}, {

⊔i ei,j} die gleichen oberen Schranken haben.

Zunachst gilt, dass ei,j ≤ ek,k wenn k = max{i, j}. Sei a eine obere Schrankevon {

⊔j ei,j}. Dann ist a auch obere Schranke von {ei,j}. Umgekehrt sei a

obere Schranke von {ei,j}. Dann ist fur jedes i:⊔j ei,j ≤ a, denn das linke

ist eine kleinste obere Schranke einer Teilmenge. Damit ist a auch obereSchranke von {

⊔j ei,j}. 2

Lemma 1.20 Sei f : D1 × . . . × Dk → E eine Funktion auf cpo’s Di, E.Dann ist f stetig gdw. f stetig in jedem Argument ist.

Beweis. “ =⇒ :“ Sei f stetig: Fur feste dj definiere die Funktion fi(x) :=f(d1, . . . , di−1, x, di+1, . . . , dk). Diese ist stetig.“⇐:“ Sei der Einfachheit halber k = 2 und sei (x0, y0) ≤ (x1, y1) ≤ . . . eineaufsteigende Kette. Dann gilt:

f(⊔i(xi, yi))

= f(⊔i xi,

⊔j yj) lubs fur kartesisches Produkt

=⊔i f(xi,

⊔j yj) da f stetig im ersten Argument

=⊔i(⊔j f(xi, yj) da f stetig im zweiten Argument

=⊔i f(xi, yi) wegen obigem Lemma

2

1.4 Funktionenraume

Seien D,E cpo’s.Mit [D → E] bezeichnen wir die Menge der stetigen Funktionen D → E.

Die Ordnung auf [D → E] sei f ≤ g gdw. ∀d ∈ D : f(d) ≤ g(d).Wenn E ein bottom-Element hat, dann hat [D → E] das kleinste Ele-

ment ⊥[D→E], definiert durch: ⊥[D→E] d = ⊥E fur alle d ∈ D.Die Ordnung [D → E] ist eine cpo:Betrachte eine Kette f0 ≤ f1 ≤ f2 ≤ . . . Fur d ∈ D konnen wir f0(d) ≤

f1(d) ≤ . . . bilden. Deshalb existiert⊔i fi(d). D.h die Funktion

⊔i fi ist so

definiert, dass (⊔i fi)(d) :=

⊔i fi(d).

Es bleibt zu zeigen, dass (⊔i fi) stetig ist, d.h. ∈ [D → E] ist.

Sei d0 ≤ d1 ≤ d2 ≤ . . . eine Kette in D. Dann gilt:

(⊔i fi)(

⊔j dj)

= (⊔i fi(

⊔j dj) nach Definition der Funktion(

⊔i fi)

=⊔i

⊔j fi(dj) da fi stetig ist

=⊔j

⊔i fi(dj) nach dem Lemma uber aufsteigende arrays

=⊔j((⊔i fi)(dj)) Definition von lub fur Funktionen


Beispiel 1.21 Wenn I eine Menge mit diskreter Ordnung ist, entsprichtder Funktionenraum [I → D] einem Produkt von zu D isomorphen Ordnun-gen, wobei I die Menge der Indizes ist. Wenn I endlich ist sind das gerade|I|-Tupel.

1.5 Operationen auf Funktionenraumen

Anwendung einer Funktion auf das Argument:apply : [D → E]×D → E wobei D,E cpo’s sind. Die Definition ist:apply (f, d) = f(d).

Die Funktion apply ist stetig: Sie ist stetig in jedem Argument:

1. stetig im ersten Argument:Sei f0 ≤ f1 ≤ f2 ≤ eine Kette von Funktionen. Dann gilt:apply((

⊔i fi), d) = (

⊔i fi)d

=⊔i fi(d) (Definition des lubs von Funktionen)

=⊔i apply(fi, d)

2. Stetig im zweiten Argument:Sei d0 ≤ d1 ≤ d2 ≤ . . . eine Kette.apply(f, (

⊔i di))

= f(⊔i di) =

⊔i f(di) da f stetig

=⊔i apply(f, di)

Beispiel 1.22 Currying macht aus einer Funktionen auf Tupeln eine Funk-tion, die man nacheinander auf die Elemente des Tupels anwenden kann.(Das ist eine Konstruktion, die zeigt, dass man mit einstelligen Funktionenim Prinzip auskommt)

curry : [F ×D → E]→ (F → [D → E])curry(g) : F → [D → E]curry(g) = λv ∈ F.(λd ∈ D.g(v, d))

Wir argumentieren dass folgendes gilt:

1. curry ist korrekt definiert, d.h. das Bild liegt in (F → [D → E])

2. curry (g) ist stetig.

3. curryselbst ist stetig

Jetzt machen wir das mal von Hand. Man kann zeigen, dass alle dieseKonstruktionen automatisch stetig sind.

1. curry(g) ist korrekt definiert:(λd ∈ D.g(v, d)) ist eine stetige Funktion [D → E].Die Behauptung gilt, denn g ist stetig in jedem Argument.


2. curry(g) ist stetig fur alle g: v0 ≤ v1 ≤ v2 ≤ . . . sei Kette in F . Seid ∈ D beliebig. Dann betrachte curry(g)(

⊔i vi)d

= g((⊔i vi), d) =

⊔i g(vi, d) =

=⊔i curry(g) vi d

Also stimmt die Funktion curry(g)(⊔i vi) mit (

⊔i curry(g) vi) ube-

rein. D.h. curry(g) ist stetig.

3. curryist stetig: Sei g1 ≤ g2 ≤ g3 ≤ . . .Dann gilt:

⊔i (curry(gi)) d e =

⊔i gi(d, e)

=⊔i gi(d, e)

= (⊔i gi)(d, e) da gi ∈ [F ×D → E]

= curry(⊔i gi) d e

D.h.⊔i curry(gi) und curry(

⊔i gi) stimmen als Funktionen uberein.

Damit ist curry stetig.

1.6 Lifting

Diese Konstruktion addiert ein neues Bottom-Element zu einer cpo. DerZweck ist i.a., partiell definierte Funktionen handhabbarer zu machen, ins-besondere diese auf bekannte Funktionen zuruckzufuhren. Man kann es auchsehen als Umwandlung einer mathematisch gegebenen Berechnungsmoglich-keit in eine algorithmische, wobei “undefiniert“ und Nicht-terminierung mit-behandelt werden sollen.

Die Konstruktion selbst ist einfach: Sei D eine cpo. Definiere D⊥ =D∪{⊥}, wobei ⊥ von allen Elementen von D verschieden ist. Die Ordnungauf D⊥ ist die Ordnung von D, zusatzlich gilt ⊥ ≤ d fur alle d ∈ D⊥. DieEinbettung ι : D → D⊥ ist die Funktion mit ι(d) = d.

Lemma 1.23 Die Einbettung ist stetig.

Sei E eine cpo mit kleinstem Element. Eine Funktion f : D → E kannauf f : D⊥ → E fortgesetzt werden. Diese Funktion nennen wir f∗.

f∗(d) ={f(d) wenn d 6= ⊥⊥E sonst. d.h. d = ⊥

f∗ ist stetig: Sei d1 ≤ d2: wenn d2 = ⊥, dann ist d1 = ⊥. wenn d2 6= ⊥,dann ist f∗(d1) = f(d1) oder f∗(d1) = ⊥E ≤ f(d2).

Sei d1 ≤ d2 ≤ . . . eine aufsteigende Kette. Wenn ein di 6= ⊥, dann istlub f∗(di) = lub f(di) = f(lub di) = f∗(lub di) da (lub di) 6= ⊥. Wenndi = ⊥, dann ist lub f∗(di) = lub ⊥ = ⊥ = f∗(lub di).

Bemerkung 1.24 Wenn f durch eine Funktion λx.e beschrieben werdenkann, dann schreiben wir statt (λx.e)∗(d) auch (slet x = d in e) (slet soll“striktes let“ andeuten)

! Das “normale“ (let x = d in e) kann als (d e) ubersetzt werden.


Lemma 1.25 Die (Lifting-)Funktion (.)∗ : [D → E]→ [D⊥ → E] ist stetig:

Beweis. Sei f ≤ g. Sei d ∈ D⊥. Wenn d = ⊥, dann ist f∗ ⊥ = ⊥ = g∗⊥.Wenn d 6= ⊥, dann betrachte f d ≤ g d. Wegen f∗(d) = f(d) und g ∗ (d) =g(d) ist (.)∗ monoton.

Sei f0 ≤ f1 ≤ . . . eine Kette in [D → E] und d ein Element aus D⊥.Wenn d = ⊥, dann ist (

⊔i fi)

∗⊥ = ⊥. Die Kette⊔i f∗i ⊥ ist konstant = ⊥,

also ebenfalls = ⊥.Sei d 6= ⊥. Dann gilt:

(⊔i fi)

∗d =⊔i fi)d (denn so war (.)∗definiert)

=⊔i fi(d) =

⊔i f∗i (d) Stetigkeit von fi und Definition von (.)∗

= (⊔i f∗i )(d) Da (

⊔i f∗i ) punktweise definiert ist

2

Mathematische Operationen auf Mengen konnen damit “geliftet wer-den“. Zum Beispiel kann man damit Multiplikation oder andere Funktionenauf Zahlen auch fur Argumente verwenden, die moglicherweise undefiniertsind. Die Zahlen werden dann als geliftete Zahlen betrachtet, d.h. als einflache cpo mit einem kleinstem Element. Diese Methode geht dann davonaus, dass diese neuen Operationen jeweils “undefiniert“ liefern fur undefi-nierte Argumente. D.h. man kann sie gemeinsam mit anderen Funktionenverwenden, die rekursiv definiert und moglicherweise fur bestimmte Werteundefiniert sind.

geliftete Multiplikation:

∗⊥ := λa, b.(slet x = a, y = b in x ∗ y)

Diese Definition liefert auch fur das Produkt 0 ∗⊥ ⊥ = ⊥.geliftete Disjunktion (oder)

∨⊥ := λa, b.(slet x = a, y = b in x ∨ y)

Man sieht: dieses “oder“ muß erst testen, ob die Argumente definiertsind. Z.B. False ∨⊥ ⊥ = ⊥. D.h. es hat eine andere Semantik als das inHaskell definierte oder (||), das nur das erste Argument immer testet.

Fur die Untersuchung der Aquivalenzen im ungetypten (lazy) Lambda-Kalkul wird auch ein Lifting verwendet, das einen Funktionenraum (derbereits ein kleinstes Element hat) nochmals liftet und mit einem extra klein-sten Element versieht. Damit ist es moglich, die Funktionen λx.⊥ und dasElement ⊥ zu unterscheiden.

Definition 1.26 Eine Funktion f : D → E , wobei D,E cpo’s mit ⊥ sind,ist strikt gdw f ⊥ = ⊥


Dies ist eine Definition bzgl. Funktionen auf cpo’s. Bei der Semantikvon funktionalen Programmiersprachen hat dieser Begriff eine operationaleBedeutung: wenn [[f ]] strikt ist, kann man die Optimierung verwenden, sodass f zuerst sein Argument auswertet, und dann weiter reduziert.

Seien D,E cpos mit ⊥. Betrachte die Funktion strict : [D → E] →[D → E], definert durch:

(strict f) d ={f(d) wenn d 6= ⊥⊥E wenn d = ⊥

Operational bedeutet dies, dass eine Funktion f verandert wird, indemzunachst das Argument ausgewertet wird.

Es gilt:

1. (strict f) ist stetig, wenn f stetig ist.

2. strict ist stetig: Der Beweis geht analog zu (*), zusatzlich sind einpaar Fallunterscheidungen zu machen.

1.7 Summen von cpo’s; Fallunterscheidungen

Die Summen-Konstruktion ist die Grundlage der Semantik des case-Konstruktes.

Definition 1.27 Seien D1, . . . , Dk (disjunkte) cpo’s. Die Summe diesercpo’s ist einfach die (disjunkte) Vereinigung

⋃Di, wobei die Ordnung genau

ubertragen wird. Die Elemente aus verschiedenen cpo’s sind unvergleichbar.Die Summe schreiben wir auch als D1 + . . . + Dk. Es gibt (injektive) Ein-bettungen ιi : Di → D1 + . . .+Dk mit ιi(di) = di

Es gilt: Alle Einbettungen sind stetig. (offensichtlich)Oft wird diese Summe explizit mit Konstruktoren konstruiert, da die

Di’s moglicherweise nicht disjunkt sind: Wenn man ci als verschiedene Kon-struktoren hat, dann definiert man D1 + . . .+Dk = {ci(di) | i = 1, . . . , k}.

Man kann stetige Funktionen in eine gemeinsame cpo E auch “summie-ren“:Sei fi : Di → E stetige Funktionen auf cpo’s.Dann definiert man [f1, . . . , fk] : D1 + . . .+Dk → E folgendermaßen:[f1, . . . , fk]ιi(di) = fi(di). D.h. [f1, . . . , fk] ◦ ιi = fi.

Hat man die Summe mit Konstruktoren ci definiert, dann definiert man:[f1, . . . , fk]ci(di) = fi(di).

Es gilt: Die Operation [., . . . , .] : ([D1 → E]× . . .× [Dk → E])→ ((D1 +. . .+Dk)→ E) ist stetig.

Die Summe von cpo’s kann zur Beschreibung des case-Konstruktes die-nen. Das einfachste ist “ if“: Die diskrete cpo T = {True, False} kann manals Summe der cpo’s True und False ansehen.


Seien zwei Funktionen gegeben:λx1.e1 : True→ Eλx2.e2 : False→ E

Dann kann man definieren:

cond0(t, e1, e2) := [λx1.e1, λx2.e2](t)

Wenn t = True ergibt, dann erhalt man (λx1.e1)(True), im anderen Fall(λx2.e2)(False).

Da man i.a. die Situation hat, dass die Bedingung undefiniert sein kann,betrachtet man E mit ⊥, liftet {True, False} zu {True, False}⊥, und defi-niert

cond(t, e1, e2) := (slet t = b in cond0(t, e1, e2))

Dies ist das cond mit folgendem Verhalten:wenn t = ⊥, dann ist cond(t, e1, e2) = ⊥,wenn t = True, dann e1(True)wenn t = False, dann e2(False)

D.h., Die Summenkonstruktion gehort zu einem if. Das kann man ohneProbleme zu einem case verallgemeinern:

D1 + . . .+Dk sei Summe von cpo’s, die mit Konstruktoren ci konstruiertworden ist. Wenn Funktionen λxi.ei : Di → E gegeben sind, dann entspricht[λx1.e1, . . . , λxn.en](d) einer Konstruktion mit case:

case d of (c1(x1)→ e1(x1));. . .(cn(xn)→ en(xn))

Im allgemeinen ist das zu schwach, da dies voraussetzt, dass die Auswertung,die den Konstruktor erkennt, auch terminiert.

Deshalb nimmt man i.a. die geliftete Summe (D1+. . .+Dk)⊥ als Summevon cpo’s, die mit Konstruktoren ci konstruiert worden ist.Wenn Funktionen λxi.ei : Di → E gegeben sind, dann entsprechen sich:

• (slet x = d in [λx1.e1, . . . , λxn.en](d))und

•case d of (c1(x1)→ e1(x1));

. . .cn(xn)→ en(xn);

1.8 Stetigkeit von fix

Sei D eine cpo mit ⊥. Der kleinste-Fixpunkt-Operator fix : [[D → D]→ D]ist definiert als

fix f =⊔n

fn(⊥)


Dies kann man auch schreiben als

fix =⊔n

λf.fn(⊥)

Denn λf.⊥ ≤ λf.f(⊥) ≤ . . . ist eine aufsteigende Kette in [[D → D] →D]. Da wir gezeigt haben, dass [[D → D] → D] eine cpo ist, existiert diekleinste obere Schranke, und diese ist auch in [[D → D]→ D]. Diese kleinsteobere Schranke ist gerade fix: denn

fix f =⊔n

fn(⊥) = (⊔n

λx.xn(⊥))f

Also gilt:fix ∈ [[D → D]→ D].

2 Eine Metasprache und Stetigkeit

Die Idee einer Metasprache ist eine allgemeine Moglichkeit, Funktionen aufcpos als stetig nachzuweisen, solange sie sich mittels Lambda-Ausdruckendarstellen lassen; und zwar ohne jedesmal einen expliziten Beweis fuhren zumussen. Dies soll helfen, fur verschiedene Varianten von Lambda-Notationenbzw. Lambda-Kalkulen die Stetigkeit von Ausdrucken aus allgemeinerenPrinzipien herzuleiten, anstatt diese jeweils extra nachzurechnen. Damitkann man dann etwas leichter eine denotationale Semantik fur eine gege-bene Programmiersprache definieren, da man die Stetigkeit aller Ausdruckenicht gesondert nachweisen muß.

Wir nehmen an, dass es cpo’s gibt, so dass wir auch die neu konstruiertencpo’s verwenden durfen.

E ::= Di | E1 × . . .× En | [E1 → E2] | [E1, . . . , En] | E⊥

2.1 Syntax fur die Lambda-Meta-Sprache

Fur Ausdrucke:

• ci Konstanten fur (alle) Elemente in einer festen cpo.

• Konstruktoren cE fur bestimme cpo’s. Wir nehmen auch an, dass dieSummen-cpo’s aus cpo’s gebildet werden, die mit Konstruktoren ver-kleidet sind.

• Funktionen, die fest an eine bestimmte cpo’s gebunden sind: Projek-tionen, Einbettungen

• Generische Konstanten, wie apply, curry, fix, strict.


•e ::= x | λx.e | (e1 e2) | (slet x = e1 in e2)

| (case e of(cE,1(x1)→ e1); . . . ; (cE,n(xn)→ en))

Analog zum Typcheck fur die einfach getypte Lambda-Notation gilt auchhier, dass nur solche Ausdrucke sinnvoll sind, fur die man eine sinnvolleInterpretation als Funktion auf einer (konstruierten) cpo herleiten kann.Diese ist analog zum hergeleiteten Typ.

Die Bedingungen, die dann gelten mussen, sind:

• Variablen haben im Geltungsbereich stets die gleiche Zuordnung

• Konstanten haben ihre feste Zuordnung zur cpo,

• Jedes Vorkommen einer generische Konstanten hat ebenfalls einezulassige Belegung. D.h. man kann so tun, als gabe es fur jeden (sinn-vollen Typ) eine generische Konstante dieses Typs.

• (e1 e2): e1 : [D → E], e2 : D und (e1e2) gehort zur cpo E

• (slet x = e1 in e2): x gehort zur cpo D, e1 zur cpo D⊥; e2 und(slet x = e1 in e2) gehoren zur gleichen cpo E

• (case e of(cE,1(x1)→ e1); . . . ; cE,n(xn)→ en): Der Ausdruck e gehortzur cpo E, die Variable xi gehort zur Ei, cE,i ist der Konstruktor, derEi versteckt. E = [E1, . . . , En]. Der case-Ausdruck gehort zur cpo E.

Wir gehen davon aus, dass sinnvolle Ausdrucke genau diejenigen sind, furdie man eine Belegung aller Unterausdrucke mit cpo’s angeben kann, so dassobige Bedingungen erfullt sind. Dies ist nicht nur zufallig genauso wie imeinfach getypten Lambdakalkul.

2.2 Stetigkeit von Funktionen in der Metasprache

Hier braucht man wieder die Begriffe wie freie Variablen, gebundene Varia-blen, die wir hier voraussetzen.

Die Konstruktion von syntaktischen Ausdrucken ergibt i.a. Unteraus-drucke, die freie Variablen enthalten. Dies muß in die Betrachtungen ein-fließen. Dazu benotigen wir eine angepaßte Definition der Stetigkeit einesAusdrucks mit freien Variablen.

Definition 2.1

1. Sei e ein Ausdruck, und seien x1, . . . , xn die freien Variablen in e. Seix eine Variable. Dann ist e stetig in der Variablen x, wenn fur allezulassigen Belegungen xi : Di mit di ∈ Di fur xi 6= x gilt, dassλx.e[di/xi | i = 1, . . . , n, xi 6= x] stetig ist.


2. Ein Ausdruck e ist stetig in seinen Variablen, wenn e stetig in allenfreien Variablen ist.

Dies ist unabhangig von der Reihenfolge der gewahlten Variablen in derDefinition, da wir einen Ausdruck e : E als Funktion mit den freien Variablen{x1 : D1, . . . , xn : Dn} als Funktion von D1× . . .×Dn → E ansehen konnen,und bereits gezeigt haben, dass eine Funktion stetig ist, gdw. sie in jedemArgument separat stetig ist.

Wir gehen jetzt die Konstrukte einzeln durch und argumentieren, dassalle gebildeten Ausdrucke stetig sind:

Variablen x ist stetig in x, denn fur jede cpo D, die man x zuordnet, istλx : D.x als Identitat auf D stetig. x ist auch stetig in y fur y 6= x, dakonstante Funktionen stetig sind. d.h ist stetig in seinen Variablen.

Generische Konstanten apply : [[D → E] ×D → E], wobei D,E cpo’ssind (polymorph)fix: [D → D]→ Dcurry: (F ×D → E)→ (F → [D → E])

Diese sind alle stetig, wie bereits gezeigt. Da diese Funktionen keinefreien Variablen enthalten, gilt, dass sie stetig in allen Variablen sind.

Tupelbildung (e1, . . . , en):Wenn alle ei stetig in allen Variablen sind, dann ist (e1, . . . , en) eben-falls stetig in allen Variablen: Sei eine zulassige cpo-Belegung fur dasTupel gegeben. Diese ist auch eine fur jedes ei. Da alle λx.ei[dy/y | x 6=y] stetig sind, gilt das auch fur λx.(e1, . . . , en)[dy/y|x 6= y] (dies folgtaus den Betrachtungen uber Tupelbildung von Funktionen Also ist(e1, . . . , en) stetig in seinen Variablen

Anwendung Sei e ein Ausdruck. Betrachte zunachst (apply(e1, e2)) wobeiapply eine generische Konstante ist. Dann gilt: wenn (e1, e2) stetig ist,dann auch (apply (e1, e2)).Sei eine Belegung von (apply(e1, e2)) gegeben.Dann ist dies auch eine gemeinsame Belegung von apply und (e1, e2).Sei außerdem (e1, e2) stetig in x. Die cpo von (e1, e2) wurde konstruiertals (D → E)×D.Dann ist λx.((e1, e2)[dy/y|y 6= x]) stetig und in [F → (D → E) ×D]Dann ist auch apply ◦ λx.(e1, e2)[dy/y] stetig.Offenbar gilt: apply ◦ λx.(e1, e2)[dy/y] = λx.apply(e1, e2)[dy/y].Denn (apply ◦ λx.(e1, e2)[dy/y](a) = (apply(e1, e2)[dy/y, a/x]= (e1, e2)[dy/y, a/x] = (λx.apply(e1, e2)[dy/y])(a)Damit ist apply(e1, e2) stetig.

Offenbar ist apply(e1, e2) = (e1e2). Also ist Anwendung stetig.


Abstraktion λz.e ist stetig in allen Variablen

Dazu betrachte λx.λz.e[dy/y | y 6= x, z].Diese Funktion ist stetig, wenn x keine freie Variable in λz.e ist. Wennx eine freie Variable in λz.e ist, dann ist e[dy/y | y 6= x, z] als Funktionvon D1×D2 → E stetig, wobei x, z die Variablen sind mit x : D1 undz : D2. Dann konnen wir diese Funktion transformieren mit curry:curry(λ(x, z).e) = λx.λz.e[dy/y|y 6= x, z].Da curry als stetig bereits nachgewiesen ist, ist damit die Funktionλx.λz.e[dy/y|y 6= x, z] stetig.

Dies gilt fur alle x, also ist λz.e stetig in seine Variablen

slet: (slet x = e1 in e2): Bedingung an eine Belegung mit cpo’s ist :e1 : D⊥, x : D, e2 : E. e2 ist stetig in allen Variablen, insbesondere ist(λx.e2) stetig; damit auch die geliftete Funktion (λx.e2)∗. Dies habenwir bereits bei der Betrachtung zu lifting gesehen. Da Anwendungebenfalls eine Konstruktion ist, die zu stetigen Funktionen fuhrt, gilt:(λx.e2)∗(e1) ist stetig in allen Variablen. Denn es gilt:

(slet x = e1 in e2) = (λx.e2)∗(e1)

case: (case e of (cE,1(x1)→ e1); . . . ; (cE,n(xn)→ en))Hier muss die Belegung mit cpo’s so sein, wie oben beschrieben:

(e gehort zur cpo E, die Variable xi gehort zur cpo Ei, cE,i ist derKonstruktor, der Ei versteckt. E = [E1, . . . , En].

Diese Konstruktion ist stetig, da(case e of (cE,1(x1) → e1); . . . ; (cE,n(xn) → en)) als[λx1.e1, . . . , λxn.en] e definiert ist.

Damit sind auch alle syntaktischen Konstruktionen wie(if a then b else c ) stetig.

Fix : ist offenbar auch stetig, wie oben schon gezeigt. In Sprachen kommtdas oft als expliziter Rekursions-Operator vor, manchmal in der Syntaxµx.s

Zusammenfassend gilt, dass alle mittels der Metasprache bildbaren Aus-drucke stetig sind, insbesondere alle geschlossenen Ausdrucke.


3 PCF: Programming Language for ComputableFunctions

Diese Sprache wurde von Dana Scott 1969 (LCF) eingefuhrt, um Grundla-genuntersuchungen an funktionalen Sprachen durchzufuhren. PCF ist eineeinfach getypte funktionale Sprache, fur die wir mit unseren Mitteln einedenotationale Semantik mittels Konstruktionen uber cpo’s angeben konnen.PCF hat als Basisdatentypen naturliche Zahlen und die beiden Wahrheits-werte True, False. Einige wenige Funktionen sind schon vorhanden.

3.1 Syntax

Typen:τ ::= num | Bool | τ → τ

Ausdrucke:E ::= True | False |

0 | 1 | 2 | . . . |pred E | succ E, |zero? E |(if E then E else E ) |x | λx :: τ.E | (E E) |µx :: τ.E

Alle zulassigen Ausdrucke sind einfach (monomorph) getypt. D.h.diese haben einen Typ, der keine Variablen enthalt. Dieser Typ ist zudemeindeutig.In den Konstrukten λ, µ mussen die Variablen mit einem (monomorphen)Typ versehen sein, damit man den Typ der Ausdrucke angeben kann.

Einige Typen von Ausdrucken:0, 1, 2, . . .: numzero?: num→ Boolif−then−else−:: Bool→ α→ α→ α fur alle α.

D.h. das if-then-else kann man als generisches Konstrukt ansehen, dasfur jeden Typ τ zu einem extra if-then-elseτ instanziiert wird.

Der neue Operator µ ist der Fixpunktoperator.Typregel fur µ ist:

λx.E : τ → τ

(µx : τ.E) : τ

3.2 Operationale Semantik von PCF

Die operationale Semantik wird zunachst als “big-step“ Semantik angege-ben. Mit v bezeichnen wir einen Wert und mit w einen Wert, oder einen λ-oder µ-Ausdruck. Die Regeln fur die Reduktion →op sind:


e1 →op True; e2 →op v

if e1 then e2 else e3 →op v

e1 →op False; e3 →op v

if e1 then e2 else e3 →op v

s→op (λx.e) e[a/x]→op w

(λx.e) a→op w

(e[(µx.e)/x])→op w

(µx.e)→op w

t→op pred; e→op n und n > 0t e→op (n− 1)

t→op succ; e→op n

t e→op (n+ 1)

t→op pred; e→op 0t e→op 0

t→op zero?; e→op 0t e→op True

t→op zero?; e→op n und n 6= 0t e→op False

Als Reduktionsrelation (d.h. “small-step Semantik“) kann man das auchfolgendermaßen definieren:

if True then e2 else e3 → e2if False then e2 else e3 → e3pred n → n− 1 falls n > 0pred 0 → 0succ n → n+ 1zero? 0 → Truezero? n → False falls n > 0(λx.e)a → e[a/x](µx.e) → (e[µx.e/x])

Betrachten wir noch Reduktionskontexte in PCF:

R ::= [] | R E | if R then E else E | pred R | succ R | zero? R

, und erlauben nur Reduktionen, die in einem Reduktionskontext stattfin-den: d.h. nur R[s] → R[t] ist zulassig. Diese Reduktion im Reduktionskon-text bezeichnen wir auch als Normalordnungsreduktion. Die transitive Hullevon → bezeichnen wir als ∗−→.

Es gilt, dass →op ⊆ ∗−→.Die Sprache PCF ist zwar einfach und monomorph getypt, aber es ist

leicht zu sehen, dass sie Turing-machtig ist. D.h. man kann alle berechenba-ren Funktionen definieren.

Definition 3.1 Sei t ein PCF-Ausdruck.

• t ist in Normalform gdw. t nicht mehr reduzierbar ist.


• t ist in WHNF (schwache Kopfnormalform): gdw. t ≡ λx.t′ oder t istein Basiswert vom Typ num oder Bool.

Definition 3.2 Sei t ein geschlossener PCF-Ausdruck. Wenn ein t′ exi-stiert mit t ∗−→ t′, wobei t′ eine WHNF ist, dann schreiben wir t′↓.

3.3 Ubersetzung PCF nach Haskell

Bevor wir die Eigenschaften von PCF genauer betrachten, geben wirzunachst eine Ubersetzung nach Haskell an. Wir wollen diese Ubersetzungnicht formal verifizieren. Diese Ubersetzung soll nicht dazu dienen, PCF se-mantisch zu fundieren, sondern soll illustrieren, wie man fur PCF schnelleinen Interpreter bauen kann. Außerdem kann man danach die Ausfuhrungvon PCF-Ausdrucken und die Unterschiede zu Haskell schneller sehen.

Die ubersetzten Funktionen sind zum Teil allgemeiner, d.h. in Haskellhaben sie einen polymorphen Typ statt eines monomorphen in PCF; siekonnten Argumente zulassen, die in PCF verboten waren. Aber es soll fol-gendes erfullt sein:

1. Ubersetzte Ausdrucke sind wohlgetypt in Haskell.

2. Sei t ein Ausdruck in PCF und t∗−→ n und n eine Zahl oder ein Boo-

lescher Wert. Wenn wir die Ubersetzung τ und die Reduktion in Has-kell ebenfalls mit Index H andeuten, dann gilt fur die Ubersetzung:tH

∗−→H nH .

3.3.1 Ubersetzung nach Haskell:

Typen: τ ::= num | Bool | τ → τ

Ausdrucke: Boolesche Werte und Zahlen kann man direkt ubersetzen.if-then-else und pred, succ ebenfalls direkt.zero?H := iszero(λx : τ.E)H := \x→ EH(µx : τ.E)H = fix(\x→ EH)

Folgende Haskell-Definition werden fur diese Ubersetzung benotigt:

pred n = if n > 0 then n-1 else 0succ n = n+1iszero x = x == 0fix f = f (fix f)

Man kann alternativ auch das let(rec)-Konstrukt zur Ubersetzung desµ verwenden:(µx : τ.E)H = let x = EH in x

Die Fixpunktbildung entspricht offenbar der (einfachen) Rekursion.


Beispiel 3.3 Addition mittels succ. Ein Versuch in funktionaler Notation:

add s t := if zero?(s) then t else succ (add (pred s) t)

In PCF sieht diese Funktion so aus:

add := µa.(λs, t.if zero? (s) then t else succ (a(pred s) t)

Die Haskell-Ubersetzung dieser Funktion ist:

1. erste Variante

add = fix (\a -> (\s t -> if iszero s then t else succ (a (pred s) t)))

2. Zweite Variante

add = let a = (\s t -> if iszero s then t else succ (a (pred s) t))in a

Beispiel 3.4 Multiplikation:funktional:

mult s t := if zero?(s) then 0 else add t (mult (pred s) t)

in PCF:

mult := µm.λs, t.if zero?s then 0 else add t (m(pred s)t)

Haskell-Ubersetzung:

1. mult = fix (\m -> (\s t -> if iszero s then 0else add t (m (pred s) t)))

2. mult = let m = (\s t -> if iszero s then 0else add t (m (pred s) t))

in m

4 Eigenschaften von PCF

Definition 4.1 Eine Relation → ist konfluent (bzw. Church-Rosser) gdw.fur alle s, s1, s2: wenn s

∗−→ s1 und s ∗−→ s2, dann existiert ein weiterer Terms3, so dass s1

∗−→ s3 und s2∗−→ s3.

Satz 4.2 Die Reduktionsrelation → ist konfluent.


Beweis. Mit Methoden wie in (Barendregt) 2

Ohne den Fixpunktoperator ist diese Sprache nicht Turingaquivalent:Es gilt, dass ohne Fixpunktoperator alle Reduktionen terminieren. DieseAussage benotigen wir auch spater fur die Adaquatheit der denotationalenSemantik.

Folgende Aussage entspricht einer Variante des Progress-Lemmas.

Lemma 4.3 In PCF gilt: geschlossene Terme, die Normalformen vom TypBool bzw. num sind, konnen nur die Basiswerte selbst sein, d.h. Zahlen oderWahrheitswerte.

Beweis. Wir zeigen dies mit Induktion nach der Große der Terme:Es gilt: Ein Term M in Normalform kann kein µ-Ausdruck enthalten, dennjeder µ-Term ist reduzierbar, also nicht in Normalform.

Wir gehen die Konstruktionsmoglichkeiten durch.

• M ≡ 0, n, True, False: trivial.

• M ≡ pred M ′, succ M ′, zero? M ′: Das gilt mit Induktion, da M ′

ebenfalls von Basistyp, und eine Ein-Schritt Reduktion ausreicht, umden Ausdruck ebenfalls in einen Basiswert zu uberfuhren.

• M ≡ if M0 then M1 else M2 : wenn dieser Term in Normalform ist,dann ist auch M0 in NF, also True oder False. Dann kann man aberreduzieren.

• M ≡ λx.M ′: kann nicht sein, da dies vom falschen Typ ist.

• M ≡ (M1 M2): Dieser Term muß von der Form((. . . (M ′n Mn−1′) . . . ..)M2) sein. Der Term M ′n kann nur eineAbstraktion sein. If-then-else ist nicht moglich, da wegen der Induk-tionshypothese ein inneres if-then-else nicht in NF sein kann. Damitkann man aber β-reduzieren, und der Term ist nicht in Normalform.

2

Wir betrachten jetzt das Fragment PCF−µ: das ist die Sprache PCFohne den µ-Operator.

Definition 4.4 Definiere eine Menge Ttrm von PCF−µ-Termen als kleinsteMenge, die folgendes erfullt:

1. Wenn M geschlossen ist und vom Typ num oder Bool, und alle Reduk-tionen, die von M ausgehen, terminieren, dann ist M ∈ Ttrm.

2. Sei M : τ1 → τ2. Dann ist M ∈ Ttrm, wenn fur alle geschlossenenN : τ1 ∈ Ttrm gilt: (M N) ∈ Ttrm.


Jetzt definiere noch die Menge Ttrm,v folgendermaßen:Wenn M die freien Variablen x1, . . . , xn hat, dann ist M ∈ Ttrm,v, wennσ(M) ∈ Ttrm fur alle σ = {xi → Ni | i = 1, . . . , n} wobei Ni ∈ Ttrm.

Offenbar gilt:

1. Sei M ∈ Ttrm. Dann terminieren alle von M ausgehenden Reduktio-nen.

2. M ∈ Ttrm,v gdw. fur alle σ, die Ttrm- Terme fur freie Varia-blen einsetzen und fur alle geschlossenen N1 . . . Nk ∈ Ttrm, so dassσ(M) N1 . . . Nk von Basistyp ist : σ(M) N1 . . . Nk hat nur terminie-rende Reduktionen.

Satz 4.5 Betrachte das Fragment PCF−µ der Sprache PCF. Fur die Aus-drucke dieser Sprache gilt, dass sie in Ttrm,v enthalten sind. D.h. Man kannjeden geschlossenen Term in PCF−µ nur endlich oft reduzieren.

Beweis. Mit Induktion nach der Große der Terme.

• M ≡ x: trivial

• M ≡ 0, True, False, n: trivial, da alles in Normalform.

• M ≡ pred M ′, succ M ′, zero?(M ′): Betrachte σ(M ′). Nach Induk-tion terminiert σ(M ′). Wegen der operationalen Definitionen vonsucc, pred, zero? gilt dies auch fur σ(M). Also ist M ∈ Ttrm,v.

• M ≡ if M0 then M1 else M2 Nehme an, dass Ni ∈ Ttrm sind und σSubstitution, die nur Terme aus Ttrm einsetzt, so dass (σM) N1 . . . Nn

geschlossener Term vom Basistyp ist.Induktion zeigt, dass (σ M0) terminierend ist, ebenso (σM1) N1 . . . Nn

und (σM2)N1 . . . Nn also ist auch (σM) N N1 . . . Nn terminierend.Dies gilt fur alle terminierenden, geschlossenen Ni. Also gilt M ∈Ttrm,v.

• M ≡ (L N): Da L,N ∈ Ttrm,v nach Induktionshypothese, gilt furalle Substitutionen σ die nur Terme aus Ttrm einsetzen, dass auchσL, σN ∈ Ttrm. Wegen der Definition von Ttrm ist auch (σL (σN))terminierend, also ist (L N) ∈ Ttrm,v .

• M = λx.M ′: Zu zeigen ist: (λx.σM ′)N ∈ Ttrm ist terminierend furgeschlossene N ∈ Ttrm,v und Substitutionen σ, die nur Terme ausTtrm einsetzen.Da M ′ ∈ Ttrm,v nach Induktionshypothese, gilt s[N/x]M ′ ∈ Ttrm. Alsogilt das auch fur σ(M ′[N/x]). Damit ist M = λx.M ′ ∈ Ttrm,v.


2

Korollar 4.6

1. Alle Terme des µ-freien PCF-Fragments haben nur terminierende Re-duktionen.

2. Alle Terme vom Basistyp im µ-freien PCF-Fragment reduzieren zueiner Zahl, oder True, False.

Korollar 4.7 Der µ-Operator ist nicht im µ-freien PCF-Fragment definier-bar. D.h dies ist eine echte Erweiterung.

5 Denotationale Semantik von PCF

Fur jedes Konstrukt mussen wir angeben, wie syntaktische Objekte deno-tiert werden: Da PCF-Unterterme freie Variablen enthalten konnen, benoti-gen wir eine Umgebungsvariable. Diese Umgebung ist eine partielle Funk-tion von Variablen in zugehorige Werte. Wir nehmen an, dass Variablenmit einem Typ markiert sind. Wir nehmen auch an, dass die Ausdruckeentsprechend dem einfach getypten Lambda-Kalkul getypt sind.

Als Domains verwenden wir cpo’s, die wir im Vorlesungsteil zu cpo’seingefuhrt und ausfuhrlich behandelt haben. Die verwendeten Notationensind dort erklart.

Die Denotationen der Typen ergeben sich rekursiv folgendermaßen:[[num]] = IN⊥ geliftete naturliche Zahlen[[bool]] = {True, False}⊥ geliftete zweielementige Menge[[τ1 → τ2]] = [[[τ1]]→ [[τ2]]]⊥ stetige Funktionen, geliftet

Wir benutzen hier geliftete Funktionenraume, d.h. es gibt einen extrahinzugefugten Wert ⊥, der verschieden ist von der Funktion die stets ⊥ lie-fert. Der Funktionenraum vor dem Liften hat bereits ein kleinstes Element:es ist die Denotation von λx.⊥. Die Anwendung von ⊥ als Funktion auf einArgument ergibt in D stets ebenfalls ⊥. Das gleiche gilt fur die Denotationvon λx.⊥, d.h. die Extensionalitat gilt nicht mehr in D: es gibt verschiedeneObjekte, die als Funktionen gleich sind.

Beachte, dass in anderen Artikeln auch stetige Funktionenraume benutztwerden ohne Lifting.

Cartesische Produkte werden nicht benotigt, da es keine Datenkonstruk-toren, insbesondere keine Tupel in PCF gibt. Diese kann man verwenden,wenn man PCF mit Tupeln erweitern will.

Die zugehorigen Denotationen fur geschlossene Terme M :: τ sind dannjeweils aus der Denotation [[τ ]] des Typs τ , d.h. [[M ]] ∈ [[τ ]]. Bei offenen


Termen gilt das ganz ahnlich, nur muß man noch Einsetzungen fur die freienVariablen hinzufugen.

Im folgenden lassen wir die Typisierungsbezeichnungen teilweise weg.Trotzdem nehmen wir an, dass diese vorhanden sind.

Definition 5.1 (denotationale Semantik von PCF)ρ ist eine Umgebung, die Variablen Werte aus der richtigen Menge zuordnet.ρ(x :: τ) ∈ [[τ ]]

Diese Umgebung wird benotigt, damit man Unterausdrucke, die freie Va-riable enthalten, behandeln kann. Ausdrucke ohne freie Variablen (geschlos-sene Ausdrucke) haben eine denotationale Semantik, die unabhangig voneiner Umgebung ist.Die Vorstellung ist: Fur alle globalen Werte (die in ρ) gilt die Definitionbereits. Wir benutzen λ auch auf der Seite der Denotationen, aber notierenes dort als λ

[[x]] ρ = ρ(x)[[n]] ρ = n[[pred M ]] ρ = ([[M ]] ρ)− 1 wenn ([[M ]] ρ) > 0

= 0 wenn ([[M ]] ρ) = 0= ⊥ sonst

[[succ M ]] ρ = ([[M ]] ρ) + 1 wenn ([[M ]] ρ) ≥ 0= ⊥ wenn ([[M ]] ρ) = ⊥

[[if M then L1 else L2 ]] ρ = ⊥ wenn [[M ]] ρ = ⊥= [[L1]] ρ wenn [[M ]] ρ = True= [[L2]] ρ wenn [[M ]] ρ = False

[[(M N)]] ρ = ([[M ]] ρ) ([[N ]] ρ)[[λx.M ]] ρ = λy.([[M ]](ρ[y/x]))[[µx.M ]] ρ = fix(λy.([[M ]](ρ[y/x]))

(hier mussen M und x gleichen Typ haben)

Um zu sehen, dass die Definitionen alle stetig sind, wenden wir die Uber-legungen zur Meta-Notation an. Die einfache Typisierung aller Ausdruckestellt sicher, dass es jeweils zulassige Belegungen mit cpo’s gibt.

• Alle Konstrukte sind stetig: succ, pred und zero? sind auf gelifteten,diskreten cpo’s definiert

• Applikation, Abstraktion, Fixpunktbildung sind ebenfalls stetig als ge-nerische Konstanten.

• if-then-else ist als case - Konstrukt uber der gelifteten Summe eben-falls stetig.

Satz 5.2 Seien M und N PCF-Ausdrucke. Wenn M∗−→ N , dann gilt:

[[M ]] ρ = [[N ]] ρ fur alle ρ .


Beweis. Wir zeigen dies fur die Einschrittrelation→. Dann gilt das auch furdie transitive Hulle. Wir betrachten dabei jeweils den Unterausdruck, derunmittelbar reduziert wird (den Redex).

• pred n→ n− 1:[[pred n]] ρ = ([[n]] ρ)− 1 = n− 1.Analog fur pred 0, succ n, zero? n.

• (if True then L1 else L2 )→ L1:[[if True then L1 else L2 ]] ρ = [[L1]] ρ fur alle ρ.

• Analog: False-Fall

• (λx.M)N →M [N/x]:

[[(λx.M)N ]] ρ = ([[(λx.M)]] ρ)([[N ]] ρ)= (λy.[[M ]] ρ[x→ y])([[N ]] ρ)= [[M ]] ρ[x→ ([[N ]] ρ)]= [[M [N/x]]] ρ( Induktion nach der syntaktischen Struktur von M)

• (µx.M)→ (M [(µx.M)/x];

[[(µx.M)]] ρ= fix(λy.([[M ]](ρ[x→ y])))= (λy.([[M ]](ρ[x→ y]))(fix(λy.([[M ]](ρ[x→ y])))= (λy.([[M ]](ρ[x→ y])))([[(µx.M)]] ρ)= ([[M ]](ρ[x→ ([[(µx.M)]] ρ)])))= [[(M [(µx.M)/x])]] ρ

2

Die andere Richtung, namlich dass der semantische Wert etwas uberdie Reduktion aussagt, ist etwas komplizierter. Die gewunschte Aussage furgeschlossene Ausdrucke M,N ist: Wenn [[M ]] ∅ = [[N ]] ∅ und N eine WHNFist, dann auch M

∗−→ N . Dies ist zuviel verlangt, es gilt fur Konstanten wieZahlen und die Booleschen Konstanten, aber nicht fur Abstraktionen, dennLambda-abstraktionen in WHNF sind nicht notwendig auch in Normalform.

Beachte, dass durch das Liften der Funktioneraume [[λx.⊥]] 6= [[⊥]], wasdazu passt, dass λx.⊥ eine WHNF hat, wahrend ⊥ keine WHNF hat.

Das folgende werden wir nachweisen:Wenn [[M ]] ∅ = m ist, dann gilt M ∗−→ m.

Zunachst zeigen wir, wie wir alle Fixpunktausdrucke approximierenkonnen.

Sei M = µx.M ′ ein µ- Ausdruck, dann definiere:


Semantische Seite:Betrachte d = fix(λy.([[M ′]](ρ[x → y])) Offenbar ist dies ein lub der Kettedn := en⊥ wobei e = (λy.([[M ′]](ρ[x→ y]))

Syntaktische Seite:

M0 := µx.xMk+1 := (λx.M ′)Mk

Lemma 5.3 Es gilt: [[Mk]] ρ = dk

Beweis. Induktion nach k:[[M0]] ρ = ⊥ = d0.Angenommen, es gilt bereits fur k.[[Mk+1]] ρ = [[(λx.M ′)Mk]] ρ = ([[(λx.M ′)]] ρ)([[Mk]] ρ)= ([[(λx.M ′)]] ρ)dk = λy.([[M ′]](ρ[x→ y]))dk = e(ek⊥) = ek+1⊥ = dk+1. 2

Lemma 5.4 Sei N ein geschlossener PCF-Term, so dass [[N ]] = n eine Zahlist und alle µ-Ausdrucke in N von der Form µx.x sind. Dann gilt N ∗−→ n.

Beweis. Angenommen, das ist falsch. Dann gibt es einen Term N :: num mit[[N ]] = n, alle µ-Ausdrucke in N sind von der Form µx.x und die Normal-ordnungsreduktion fur N terminiert nicht. Da alle Reduktionen im µ-freienFragment von PCF terminieren, muß die Normalordnungsreduktion irgend-wann einen der Unterterme µx.x reduzieren. Wir nehmen einen Term, furden das gilt, und der eine kleinste Anzahl von Normalordnungsreduktionbenotigt, bis das erste mal µx.x reduziert wird. Unter diesen wahlen wirden kleinsten Term. Offenbar konnen wir annehmen, dass die erste Normal-ordnungsreduktion bereits einen Term µx.x reduziert. Da der Term µx.x einNormalordnungsredex ist, kann er nur in folgendem Kontext auftauchen:pred(µx.x), succ(µx.x), zero?(µx.x), if (µx.x) then e1 else e2 , ((µx.x)e).In jedem dieser Falle konnen wir den Term verkleinern, indem wir den Redexdurch µx.x ersetzen. Die denotationale Semantik des Terms bleibt gleich, dapred ⊥, succ ⊥, zero? ⊥, if ⊥ then e1 else e2 , (⊥ x) jeweils als Denotationwieder ⊥ haben. Die operationale Semantik bleibt ebenfalls gleich, d.h. dieNormalordnungsreduktion terminiert auch fur den neu konstruierten Termnicht. Der konstruierte Term ist jedoch kleiner geworden. D.h. der Termselbst muß µx.x sein. Dessen Denotation ist aber ⊥, im Widerspruch zurAnnahme. 2

Satz 5.5 Sei N ein geschlossener PCF-Term, so dass [[N ]] = n eine Zahlist. Dann gilt N ∗−→ n.

Beweis. Induktion nach der Anzahl der echten µ-Ausdrucke in N , wobei wirdie Ausdrucke µx.x nicht mitzahlen.


Basis. Wenn N keine echten µ-Ausdrucke enthalt, dann terminiert dieReduktion von N mit einem n′ nach obigem Lemma. Wir haben bereits ge-zeigt, dass dann n = n′ sein muß.Induktionsschritt.Wahle in N einen innersten echten µ-Ausdruck M aus, der selbst keine ech-ten µ-Ausdrucke mehr enthalt und definiere Nk als die Terme, die entstehen,wenn fur N jeweils Mk (wie oben) eingesetzt wird.Wir ubernehmen die Bezeichnungen wie oben. Da

⊔k dk = d (fur alle ρ)

ist, gilt somit auch⊔k [[Nk]] = [[N ]] = n. Hierbei konnen wir die Stetig-

keit verwenden, die wir fur die Metasprache gezeigt haben. Da⊔k [[Nk]] =

[[N ]] = n, muß die Folge [[Nk]] fur k = 1, 2, . . . folgende Form haben:⊥,⊥, . . . ,⊥, n, n . . . . Also gibt es ein k0, so dass [[Nk0 ]] = [[N ]] = n. Nk0

hat einen µ-Ausdruck weniger als N , dann gilt die Induktionshypothese,und wir konnen schließen, dass Nk0

∗−→ n. Somit gibt es auch eine Normal-ordnungsreduktion Nk0

∗−→ n. Da der Term Mk0 im Innern einen nichtter-minierenden Term enthalt, wurde fur diesen die WHNF nicht berechnet.Damit gilt: Man kann den inneren Term ⊥ wieder durch M ersetzen underhalt Nk′

0mit Nk′

0

∗−→ n. Da aber Nk′0

durch Reduktion aus N hergeleitet

werden kann, d.h. N ∗−→ Nk′0

∗−→ n, gilt insgesamt N ∗−→ n. 2

Korollar 5.6 Sei N ein geschlossener PCF-Term vom Typ num. Dann gilt[[N ]] = ⊥ gdw. N keine terminierende Reduktion hat.

Was hier noch zu zeigen ist, ware die Aussage:Wenn N geschlossen ist und [[N ]] 6= ⊥, dann gilt N↓

6 Volle Abstraktion und Gleichheit

Gleichheit von Funktionen kann man jetzt auf zwei Arten definieren:

• Die denotationale Gleichheit:

s =d t gdw. [[s]] = [[t]]

In dieser Semantik gilt:


die Funktion por (paralleles “or“) mit

por True True = TrueTrue False = TrueFalse True = TrueFalse False = False⊥ True = TrueTrue ⊥ = TrueFalse ⊥ = ⊥⊥ False = ⊥⊥ ⊥ = ⊥

ist monoton und stetig, also im Modell enthalten, aber es gibt keinenPCF-Ausdruck, der die Denotation von por hat.

• kontextuelle Gleichheit. Ein Programmkontext ist ein Ausdruck Cmit einem Loch an einer Stelle, an der ein Unterterm stehen darf. Wirschreiben dies als C[].

Wir definieren s =c t gdw. fur alle Programmkontexte C[] gilt: C[s]↓gdw. C[t]↓.Diese kontextuelle Gleichheit vergleicht Terme anhand ihres Terminie-rungsverhaltens in allen Programmen. D.h. wenn sich s, t nicht un-terscheiden lassen durch Einsetzen in einen Programmkontext, dannwerden sie als gleich betrachtet.

Aussage 6.1 Es gilt s =d t =⇒ s =c t (Adaquatheit der denotationalenSemantik)

Beweis. Wenn s =d t, dann gilt fur alle Programmkontexte C[] auch C[s] =d

C[t]. Wenn [[C[s]]] nicht ⊥ ist, dann ist auch [[C[t]]] nicht ⊥. Dann gilt furbeide Terme C[s] und C[t], dass diese konvergieren. Damit ist s =c t. 2

Ubungsaufgabe 6.2 Definiere in PCF die logischen Funktionen wienot, and, or.

Lemma 6.3 In PCF gilt fur alle Funktionen f : τ1 → . . . τn → B (Boolodernum). Die Funktion f ist entweder konstant oder strikt in einem Argument.

Beweis. Annahme: Die Funktion f sei nicht konstant. Dann betrachte eineReduktion in Normal-Ordnung wobei der Term (f t1 . . . tn) reduziert wird.Wenn die Unterausdrucke ti nicht reduziert werden, dann ware f konstant,also wird mindestens ein Term ti zu WHNF reduziert. Da der Index i des


reduzierten ti unabhangig vom Ausdruck ti ist, gibt es einen Index i, so dassti reduziert wird. Die Funktion f ist damit strikt im i-ten Argument. 2

Wir betrachten die Funktion

F = λxλf. if(and (f True ⊥)(f ⊥ True)not (f False False))

then xelse True

Lemma 6.4 Es gilt (F True) =c (F False)

Beweis. Wir nutzen das obige Lemma aus. Wir wenden (F True)und (F False) auf eine Funktion f vom Typ Bool → Bool →Bool an. Wenn diese konstant ist, dann kann der Ausdruck(and (f True ⊥) (f ⊥ True) (not (f False False))) nicht zu True auswer-ten. Damit stimmen (F True f) und (F False f) uberein. Wenn f nichtkonstant ist, dann ist f strikt im ersten oder im zweiten Argument, unddas Ergebnis ist jeweils ⊥. 2

Wenn wir die beiden Funktionen (denotational) semantisch betrachten,dann gilt:

Lemma 6.5 Es gilt (F True) 6=d (F False)

Beweis. Wende die Denotationen auf por an. Dann gilt: (F True por) =True und (F False por) = False. 2

Definition 6.6 Eine denotationale Semantik ist voll abstrakt, wenn diekontextuelle Gleichheit mit der denotationalen Gleichheit ubereinstimmt.

Korollar 6.7 Unsere denotationale Semantik von PCF ist nicht voll ab-strakt.

Begrundung: Die beiden Ausdrucke (F True) und (F False) sind einGegenbeispiel, denn (F True) =c (F False), aber (F True) 6=d (F False).

Abhilfe:

Alternative 1: Um eine voll abstrakte denotationale Semantik zu erhalten,fugt man in der Syntax parallele Operationen hinzu: Es gilt, dass PCF+ por als voll abstrakte Semantik genau die bisherige denotationaleSemantik hat. Allerdings sagt diese Semantik dann nichts mehr ausuber Eigenschaften sequentieller Programme.


Alternative 2 Man verkleinert die Grundmenge, die der denotationalenSemantik zur Verfugung steht. Dies ergibt eine denotationale Seman-tik, die auf der operationalen basiert, und die aus allen Ausdruckenerzeugt wird.Problem hierbei: Gibt es ein effektives Konstruktionsverfahren fur die-se Grundmenge?

Leider gelten selbst bei endlichem Grundbereich negative Aussagen:

• Es gibt kein effektives Konstruktionsverfahren, wenn man nur Boolals Grundmenge nimmt?

Das “Lambda-Definierbarkeits-Problem fur endliches PCFist unentscheidbar“

• Die kontextuelle Gleichheit ist unentscheidbar, auch wenn man nur[[Bool]] als Grundmenge nimmt. D.h. man kann von zwei gegebenenAusdrucken s, t in PCF, die keinen Bezug zu Zahlen haben, d.h. nurBoolesche Konstanten und Typen, aber naturlich auch Funktionstypenverwenden, nicht algorithmisch entscheiden, ob diese kontextuell gleichsind.

7 Satz von Bekic

Man sieht: In PCF fehlen Datenkonstruktoren (Produkttypen, semantisch:Kreuzprodukte.)Programmiertechnisch bewirkt dies unter anderem, dass wir keine Daten-strukturen auf einfache Weise mit Konstruktoren aufbauen konnen: keinePaare, Listen u.a. Außerdem scheint die einfache Moglichkeit zu fehlen, ver-schrankt rekursive Funktionen zu definieren.Wir gehen nochmal zuruck zu cpo’s und wollen jetzt zeigen, dass es dieseMoglichkeit doch gibt, allerdings ist diese etwas versteckt.

Sei D cpo mit ⊥ und F : D → D eine stetige Funktion. Dann existiertein kleinster Fixpunkt fix(F ). Fur diesen gilt:

(fix1) F (d) ≤ d =⇒ fix(F ) ≤ d (fix(F ) ist auch kleinster Prafixpunktvon F )

(fix2) F (fix(F )) = fix(F )

Der Satz von Bekic sagt etwas aus uber die Existenz von Fixpunkten aufKreuzprodukten und wie diese aus koordinatenweisen Fixpunkten berechnetwerden konnen.

Satz 7.1 (Bekic)Seien D,E cpo’s mit ⊥ und F : D × E → D und G : D × E → D stetigeFunktionen. Der kleinste Fixpunkt von 〈F,G〉 : D × E → D × E laßt sichdarstellen als 〈f , g〉 wobei


f = µf.F (f, µg.G(µf.F (f, g), g)) (= µf.F (f, g))

g = µg.G(µf.F (f, g), g)

Beweis.

1. Ist Fixpunkt: f ist Fixpunkt von µf.F (f, g) , also ist f = F (f , g).g = G(µf.F (f, g), g) = G(f , g).Damit ist 〈F,G〉(f , g) = (f , g).

2. Seien (f0, g0) kleinere Fixpunkt von 〈F,G〉. Dann gilt f0 ≤ f undg0 ≤ g.Wir zeigen die umgekehrten Ungleichungen. Da f0 = F (f0, g0), giltauch µf.F (f, g0) ≤ f0.G ist monoton, also gilt: G(µf.F (f, g0), g0) ≤ G(f0, g0) = g0Also gilt g ≤ g0. Denn g ist der kleinste Prafix-Punkt vonλg.G(µf.F (f, g), g).Monotonie von F zeigt jetzt, dass : F (f0, g) ≤ F (f0, g0) = f0. Damitist f0 ein Prafixpunkt von λf.F (f0, g). Also ist f ≤ f0.

2

Da wir den Satz auch fur schwachere Strukturen (partielle Ordnungen,aber keine cpo’s) benutzen wollen, formulieren wir den Satz mit schwacherenVoraussetzungen:

Satz 7.2 (Bekic) (Version 2) Seien D,E partielle Ordnungen mit ⊥ undF : D×E → D und G : D×E → D monotone Funktionen. Wir nehmen an,dass die kleinsten Fixpunkte in folgenden Formeln existieren. Der kleinsteFixpunkt von 〈F,G〉 : D × E → D × E laßt sich darstellen als 〈f , g〉 wobei

f = µf.F (f,mg.G(µf.F (f, g), g)) (= µf.F (f, g))


Es gibt auch eine symmetrische Form dieses Satzes:

f = µf.F (f, µg.G(f, g))


Offenbar ist es kein Problem, den Satz von Bekic auch fur mehrere Va-riablen zu formulieren und zu zeigen.

In der Anwendung haben wir meist F : D → D → D und G : D → D →D. Das erste entspricht einer rekursiv definierten Funktion f , das zweiteArgument der rekursiv definierten Funktion g.

Ein Programmkonstrukt, das sich auf diesen Satz stutzen kann, ist dasletrec:


(letrec x = s, y = t in e) x, y durfen in s, t und e vorkommen undsind dort durch das letrec gebunden.

Die Anwendung ergibt dann folgende Semantik:

y = µy.t[(µx.s)/x]

x = µx.s[y/y]

Somit konnten wir mittels Bekic’s Satz die Sprache PCF auch um einletrec mit mehreren Variablen erweitern. Der Satz von Bekic zeigt: dieseErweiterung fugt keine neue Ausdruckskraft hinzu:

8 Einfach getypte Kombinatorsprache: PCFK

Da Haskell im Prinzip auch ohne die Konstrukte λ, µ, letrec auskommenkann, ist es interessant, die Beziehung von PCF zu einer Kombinatorvariantevon PCF zu untersuchen. Wir nennen dies funktionale Sprache PCFK .

Diese hat die gleichen Typen wie PCF. Ebenso die gleichen Basiskon-stanten und Funktionen. Es gibt aber kein λ und kein µ. Stattdessen gibtes rekursive Definitionen von Kombinatoren. Den Kombinatoren muß einmonomorpher Typ zugewiesen werden.

Definitionen sind von der Form:

(〈name〉 : 〈Typ〉) x1 . . . xn = e

wobei e andere Kombinatornamen enthalten darf. Alle freien Variablen vone sind in {x1, . . . , xn} enthalten.

main: ist der (reservierte) Name des auszuwertenden Ausdrucks.Es gilt: Diese Sprache PCFK ist aquivalent zu PCF.Den Begriff der Aquivalenz mussen wir genauer spezifizieren:

Es gibt eine naturliche Ubersetzung von PCF nach PCFK , so dass folgendesgilt:Die Ubersetzung erhalt den Typ und es gilt:Zu jedem Ausdruck e : num in PCF existiert ein Programm Pe in PCFK , sodass maine eine Normalform n hat, gdw. e die Normalform n hat.

8.1 Ubersetzung

8.1.1 PCF → PCFK

Gegeben ein geschlossener Ausdruck e in PCF. Zunachst mache alle gebun-denen Variablennamen disjunkt, und achte darauf, dass dies im Algorithmuszu jeder Zeit eingehalten wird.

Von unten her verwandle Lambda-Ausdrucke und µ-Ausdrucke inKombinator-Ausdrucke.


Fall: ein innerer Ausdruck ist ein Lambda-Ausdruck. Betrachte einen ma-ximalen Ausdruck t. D.h. einen solchen, der nicht selbst genau der Rumpfeines Lambda-Ausdrucks ist.

• Wenn t keine freien Variablen enthalt, dann erzeuge eine Superkombi-natordefinition: λx1, . . . xn.e wird zu neuerkomb x1 . . . xn = e. Ersetzeden Lambda-Ausdruck durch

• Wenn t freie Variablen enthalt, dann verwende Lambda-Lifting: Sei yeine solche freie Variable in e, dann:

λx1, . . . xn.e[y]→ λz, x1, . . . xn.e[z/y]) y

Fall: ein innerer Ausdruck ist ein µ-Ausdruck.

• Wenn t ≡ µx.e und e keine freien Variablen außer x enthalt,dann erzeuge eine neue Superkombinatordefinition: neuerkomb =e[neuerkomb/x]. und ersetze den µ-Ausdruck in t durch neuerkomb.

• Wenn t ≡ µx.e und µx.e genau die genau freien Variableny1, . . . , yn enthalt, dann erzeuge eine neue Superkombinatordefiniti-on: neuerkomb y1 . . . yn = e[(neuerkomb y1 . . . yn)/x]. und ersetze denµ-Ausdruck in t durch (neuerkomb y1 . . . yn). Der Gesamtausdruck ewird als Definition main = e in die Menge der Definition aufgenommen

8.1.2 PCFK → PCF

Das Ziel dieser Ubersetzung ist es, Namen durch Ausdrucke zu ersetzen.Betrachte alle Definitionen als großes letrec.

letrec name1 = λx1,1, . . . , x1,m1 .d1,. . . ,namen = λxn,1, . . . , xn,mn .dnin main

Die Kombinatoren lassen sich jetzt durch den n-dimensionalen Satz vonBekic als Fixpunktausdrucke darstellen und damit hat man einen einzigenAusdruck, der mit λ und µ-Ausdrucken in PCF dargestellt werden kann.

Bemerkung 8.1 Fur Funktionstypen gilt eine zum Verhalten von Aus-drucken vom Basistyp analoge Aussage:Zu jedem Ausdruck e : τ1 → τ2 → . . . τn → num existiert ein ubersetztes Pro-gramm und ein Ausdruck maine, so dass fur alle Ausdrucke ei : τi und derenUbersetzung gilt: e e1 . . . en hat Normalform m gdw. maine maine,1 . . . maine,ndie Normalform m hat.

Beispiel 8.2 1. PCF→ PCFK :e = µx : num.(µy : num.if zero? x then y else x ) ergibt:


f x = if zero? x then f x else x)g = f g

2. PCFK → PCF: Maximumsfunktion:

max x y = if zero? x then yelse if zero? y then y else succ (max (pred x) (pred y))

max = µm. if zero? x then yelse if zero? y then y else succ(m(pred x)(pred y))

Bemerkung 8.3 Eigenschaften der Ubersetzung: Fur Ausdrucke vom Ba-sistyp num gilt, dass die Ausdrucke vor und nach der Ubersetzung jeweils zudemselben Wert reduziert und auch das gleiche Terminierungsverhalten ha-ben. D.h. Fur Basistypen ist die Ubersetzung operational gleich, die Anzahlder Reduktionsschritte ist gleich bis auf konstante Faktoren, die im wesentli-chen die evtl. unterschiedliche Zahlweise bei Superkombinatorreduktion undβ- bzw. µ-Reduktion ausdrucken.

Fur allgemeinere Typen gilt das nicht: Die Anzahl der Schritte ist etwasweniger korreliert. Z.B. λxλy.x wird ubersetzt in K x y = x.

Aber: der Ausdruck (K 1) ist in WHNF in PCFK , wahrend (λxλy.x) 1in einem Schritt zu λy.1 reduziert. Die Anzahl der zusatzlichen Reduktions-schritte ist aber begrenzt durch die Große des Programms und des Ausdrucks.

Folgerung:Verschrankte Rekursion entspricht der Anwendung des µ-Operator auf

Ausdrucken mit freien Variablen.

1 Vollst andige partielle Ordnungen, stetige Funk- tionen · Dann hat feinen kleinsten Fixpunkt....

Documents

Transcript of 1 Vollst andige partielle Ordnungen, stetige Funk- tionen · Dann hat feinen kleinsten Fixpunkt....