15 Bedeutung von ISL+

In diesem Kapitel werden wir die im Vergleich zur letzten formalen Sprachdefinition aus Bedeutung von BSL neu hinzugekommen Sprachfeatures präzise definieren. Unsere Methodik bleibt die gleiche. Wir definieren zunächst die Semantik einer Kern-Sprache, die alle wesentlichen Sprachmerkmale enthält. Dann definieren wir eine Auswertungsregel für Programme und Definitionen sowie eine Reduktionsrelation →, mit der Programme Schritt für Schritt ausgewertet werden können.

15.1 Syntax von Core-ISL+

Die beiden neu hinzugekommenen Sprachfeatures in ISL sind 1) lokale Definitionen und 2) die Möglichkeit, Funktionen als Werte zu betrachten. Um die Definitionen möglichst einfach zu halten, werden wir zunächst mal Sprachfeatures entfernen, die wir bereits in Bedeutung von BSL präzise definiert haben und die durch die Hinzunahme der neuen Features nicht beeinflusst werden: Strukturdefinitionen (define-struct), konditionale Ausdrücke (cond) und logische Operatoren (and).

Desweiteren ergeben sich durch die uniforme Behandlung von Funktionen und Werten noch weitere Vereinfachungsmöglichkeiten. Es ist nicht nötig, Konstantendefinitionen und Funktionsdefinitionen zu unterstützen, denn jede Funktionsdefinition (define (f x) e) kann durch eine Konstantendefinition (define f (lambda (x) e)) ausgedrückt werden. Insgesamt ergibt sich damit folgende Syntax für die Kernsprache:

15.2 Werte und Umgebungen

Auch in ISL findet die Auswertung von Programmen immer in einer Umgebung statt. Da es in der Kernsprache keine Struktur- und Funktionsdefinitionen mehr gibt, ist eine Umgebung nun nur noch eine Sequenz von Konstantendefinitionen.

15.3 Bedeutung von Programmen

Die (PROG) Regel aus Bedeutung von Programmen bleibt für ISL nahezu unverändert erhalten (ohne die Teile für die Auswertung von Struktur- und Funktionsdefinitionen):

(PROG): Ein Programm wird von links nach rechts ausgeführt und startet mit der leeren Umgebung. Ist das nächste Programmelement ein Ausdruck, so wird dieser gemäß der unten stehenden Regeln in der aktuellen Umgebung zu einem Wert ausgewert. Ist das nächste Programmelement eine Konstantendefinition (define x e), so wird, sofern e nicht bereits ein Wert ist, in der aktuellen Umgebung zunächst e zu einem Wert v ausgewertet und dann (define x v) zur aktuellen Umgebung hinzugefügt (indem es an das Ende der Umgebung angehängt wird).

Allerdings gibt es einen wichtigen Unterschied, nämlich den, dass sich durch die unten stehende (LOCAL) Regel der Rest des noch auszuwertenden Programms während der Auswertung ändern kann.

15.4 Auswertungspositionen und die Kongruenzregel

Die Standard Kongruenzregel gilt auch in ISL.

(KONG): Falls e-1 → e-2, dann E[e-1] → E[e-2].

15.5 Bedeutung von Ausdrücken

15.5.1 Bedeutung von Funktionsaufrufen

Die Auswertung von Funktionsaufrufen ändert sich dadurch, dass sich die Funktion, die aufgerufen wird, sich im Allgemeinen erst während der Funktionsauswertung ergibt.

(APP): ( ( lambda ( name-1 ... name-n ) e ) v-1 ... v-n ) → e[name-1 := v-1 ... name-n := v-n]

Die Ersetzung der formalen Argumente durch die tatsächlichen Argumente in dieser Regel ist komplexer als es zunächst den Anschein hat. Insbesondere darf ein Name wie name-1 nicht durch v-1 ersetzt werden, wenn name-1 in einem Kontext vorkommt, in dem es eine lexikalisch nähere andere Bindung (durch lambda oder local) von name-1 gibt. Beispiel: ((lambda (x) (+ x 1)) x)[x := 7] = ((lambda (x) (+ x 1)) 7) und nicht ((lambda (x) (+ 7 1)) 7). Wir werden hierauf in unserer Diskussion zu Scope in Scope zurückkommen.

(PRIM): Falls v eine primitive Funktion f ist und f(v-1,...,v-n)=v,
dann ( v v-1 ... v-n ) → v.

Auch primitive Funktionen können das Resultat von Berechnungen sein; beispielsweise hängt im Ausdruck ((if cond + *) 3 4) die Funktion, die verwendet wird, vom Wahrheitswert des Ausdrucks cond ab.

15.5.2 Bedeutung von lokalen Definitionen

Die komplexeste Regel ist die zur Bedeutung von lokalen Definitionen. Sie verwendet einen wie oben definierten Auswertungskontext E um aus lokalen Definitionen globale Definitionen zu machen. Um Namenskollisionen zu vermeiden, werden lokale Definitionen ggf. umbenannt. Abhängigkeiten von lokalen Definitionen vom lokalen Kontext (zum Beispiel einem Funktionsargument) wurden ggf. durch vorhergehende Substitutionen beseitigt.

(LOCAL): E[( local [ ( define name-1 e-1 ) ... ( define name-n e-n ) ] e )] → ( define name-1' e-1' ) ... ( define name-n' e-n' ) E[e'] wobei name-1',...,name-n' "frische" Namen sind die sonst nirgendwo im Programm vorkommen und e',e-1',...,e-n' Kopien von e, e-1,...,e-n' sind, in denen alle Vorkommen von name-1,...,name-n durch name-1',...,name-n' ersetzt werden.

Die grammatikalisch nicht ganz korrekte Notation ( define name-1' e-1' ) ... ( define name-n' e-n' ) E[e'] soll hierbei bedeuten, dass E[( local ... e )] ersetzt wird durch E[e] und gleichzeitig die Definitionen ( define name-1' e-1' ) ... ( define name-n' e-n' ) als nächste mittels (PROG) auszuwertende Definition in das Programm aufgenommen werden.

Beispiel:

(define f (lambda (x)

(+ 2

(local

[(define y (+ x 1))]

(* y 2)))))

(f 2)

Dann

(f 2)

→

(+ 2

(local

[(define y (+ 2 1))]

(* y 2)))

→

(define y_0 (+ 2 1))

(+ 2 (* y_0 2))

In diesem zweiten Schritt wurde die (LOCAL) verwendet, um aus der lokalen Definition eine globale Definition zu machen. Die Abhängkeit vom lokalen Kontext (nämlich dem Funktionsargument x) wurde zuvor im ersten Schritt durch eine Verwendung der (APP) Regel beseitigt. Die Auswertung setzt sich nun durch Verwendung der (PROG) fort, also wir werten durch (+ 2 1) → 3 die Konstantendefinition aus, fügen (define y_0 3) zur Umgebung hinzu, und werten nun in dieser Umgebung (+ 2 (* y_0 2)) zum Ergebnis 8 aus.

15.5.3 Bedeutung von Konstanten

Die Definition von Konstanten ist gegenüber BSL unverändert.

(CONST): name → v, falls ( define name v ) die letzte Definition von name in env ist.

15.6 Scope

Wir wollen unter der Berücksichtigung der lokalen Definitionen nochmal die Diskussion über Scope aus Scope lokaler Definitionen aufgreifen und diskutieren, wie die formale Definition lexikalisches Scoping garantiert. Lexikalisches Scoping ist in zwei der Regeln oben sichtbar: (APP) und (LOCAL).

In (LOCAL) findet eine Umbenennung statt: Der Name von lokalen Konstanten wird umbenannt und alle Verwendungen des Namens in den Unterausdrücken des local Ausdrucks werden ebenfalls umbenannt. Dadurch, dass diese Umbenennung genau in den Unterausdrücken vollzogen wird, wird lexikalisches Scoping sichergestellt. Dadurch, dass ein "frischer" Name verwendet wird, kann keine Benutzung des Namens ausserhalb dieser Unterausdrücke an die umbenannte Definition gebunden werden.

Das gleiche Verhalten findet sich in (APP): Dadurch, dass die formalen Parameter nur im Body der Funktion durch die aktuellen Argumente ersetzt werden, wird lexikalisches Scoping sichergestellt. Gleichzeitig wird hierdurch definiert, wie Closures repräsentiert werden, nämlich als Funktionsdefinitionen, in denen die "weiter aussen" gebundenen Namen bereits durch Werte ersetzt wurden.

Beispiel: Der Ausdruck (f 3) in diesem Programm

(define (f x)

(lambda (y) (+ x y)))

(f 3)

wird reduziert zu (lambda (y) (+ 3 y)); der Wert für x wird also im Closure mit gespeichert.

Ein wichtiger Aspekt von lexikalischem Scoping ist Shadowing. Shadowing ist eine Strategie, mit der Situation umzugehen, dass gleichzeitig mehrere Definitionen eines Namens im Scope sind.

In diesem Beispiel gibt es drei bindende Vorkommen von x und zwei gebundene Vorkommen von x. Das linke Vorkommen von x in der letzten Zeile des Beispiels ist im lexikalischen Scope von zwei der drei Definitionen; das rechte Vorkommen von x ist sogar im lexikalischen Scope aller drei Definitionen.

Shadowing besagt, dass in solchen Situationen stets die lexikalisch "nächste" Definition "gewinnt". Mit "nächste" ist die Definition gemeint, die man als erstes antrifft, wenn man in der grammatikalischen Struktur des Programmtextes von dem Namen nach außen geht. Die weiter innen stehenden Definitionen überdecken also die weiter außen stehenden Definitionen: Sie werfen einen Schatten ("shadow"), in dem die aussen stehende Definition nicht sichtbar ist. Daher wird in dem Beispiel oben beispielsweise der Ausdruck (f 3) zu 6 ausgewertet.

Shadowing rechtfertigt sich aus einer Modularitätsüberlegung: Die Bedeutung eines Ausdrucks sollte möglichst lokal ablesbar sein. Insbesondere sollte ein Ausdruck, der keine ungebundenen Namen enthält (ein sogenannter "geschlossener" Term), überall die gleiche Bedeutung haben, egal wo man ihn einsetzt. Beispielsweise sollte der Ausdruck (lambda (x) x) immer die Identitätsfunktion sein und nicht beispielsweise die konstante 3 Funktion nur weil weiter außen irgendwo (define x 3) steht. Dieses erwünschte Verhalten kann nur durch lexikalisches Scoping mit Shadowing garantiert werden.

Programmiersprachen, die es erlauben, lokal Namen zu definieren und lexikalisches Scoping mit Shadowing verwenden, nennt man auch Programmiersprachen mit Blockstruktur. Blockstruktur war eine der großen Innovationen in der Programmiersprache ALGOL 60. Die meisten modernen Programmiersprachen heute haben Blockstruktur.