8 Bedeutung von BSL

In diesem Kapitel werden wir die Bedeutung (fast) aller Sprachkonstrukte von BSL zusammenfassen und formal definieren.

Dies geschieht in zwei Schritten: Wir werden zunächst die Syntax der Sprache definieren. Die Syntax definiert, welche Texte BSL-Programme sind. Die Syntax wird in Form einer Grammatik definiert. Die Grammatik sagt nicht nur, welche Texte BSL-Programme sind, sondern zerlegt ein BSL-Programm in seine Teile, genau so wie eine Grammatik für natürliche Sprache einen Satz in Teile wie Subjekt, Prädikat und Objekt zerlegt.

Im zweiten Schritt definieren wir für die grammatikalisch korrekten BSL-Programme, was diese bedeuten. Die Bedeutung legen wir durch die Definition von Reduktionsschritten fest, mit denen BSL Programme zu Werten ausgewertet werden können (sofern kein Fehler auftritt und sie terminieren).

Wir haben bereits in den Abschnitten Bedeutung von BSL Ausdrücken, Bedeutung von Funktionsdefinitionen, Bedeutung konditionaler Ausdrücke und Bedeutung von Funktions- und Konstantendefinitionen diese Reduktionsschritte für die meisten Sprachkonstrukte definiert. Wir werden hier diese Reduktionsschritte anhand der formalen Syntaxdefinition nochmal präzisieren. Außerdem werden wir nun auch definieren, welche Bedeutung Strukturen haben.

Es gibt verschiedene Möglichkeiten, die Bedeutung eine Programmiersprache zu definieren; die, die wir benutzen, nennt man Reduktionssemantik oder strukturelle operationelle Semantik oder Plotkin Semantik (nach Gordon Plotkin). Für die Formalisierung der Auswertungspositionen, von denen wir in den vorherigen Kapiteln gesprochen haben, verwenden wir sogenannte Auswertungskontexte, die 1989 von Matthias Felleisen und Robert Hieb vorgeschlagen wurde. Das alles hört sich für einen Programmieranfänger vielleicht angsteinflößend an, aber Sie werden sehen, dass es nicht so kompliziert ist wie es sich anhört :-)

8.1 Wieso?

Die meisten Programmierer dieser Welt programmieren, ohne dass sie jeweils eine formale Definition der Bedeutung ihrer Programmiersprache gesehen haben. Insofern ist die Frage berechtigt, wieso wir uns dies "antun".

Hierzu ist zu sagen, dass viele Programmierer die Programmiersprache, die sie verwenden, nicht wirklich verstehen. Dies führt zu einer Methodik, in der statt systematischem Programmentwurf einfach so lange am Programm "herumgedoktort" wird, bis es "läuft". Ein Programm durch Ausführen und Tests zu validieren ist zwar sinnvoll, aber dennoch kann dies nicht den gedanklichen Prozess ersetzen, wie ein Programm ablaufen muss, damit zu jeder Eingabe die korrekte Ausgabe produziert wird. Dazu ist es unumgänglich, dass Sie genau verstehen, was der Code bedeutet, den Sie gerade programmiert haben.

Wir möchten, dass Sie prinzipiell in der Lage sind, ihre Programme auf einem Blatt Papier auszuführen und exakt vorherzusagen, was ihr Code bewirkt. Auch wenn Ihnen der Umgang mit den eher theoretischen Konzepten dieses Kapitels vielleicht am Anfang schwerstellt, glauben wir, dass Ihnen dieses Kapitel helfen kann, ein besserer und effektiverer Programmierer zu werden.

Davon abgesehen werden Sie sehen, dass die theoretischen Konzepte, die sie in diesem Kapitel kennenlernen, eine Eleganz haben, die es allein aus diesem Grund wert macht, sie zu studieren.

8.2 Kontextfreie Grammatiken

Bisher haben wir nur informell beschrieben, wie BSL Programme aussehen. Mit Hilfe einer Grammatik kann man diese informelle Beschreibung präzise und prägnant darstellen. Es gibt viele unterschiedliche Arten von Grammatiken. Im Bereich der Programmiersprachen verwendet man meistens sogenannte kontextfreie Grammatiken. Diese und andere Grammatikformalismen werden in der Vorlesung "Theoretische Informatik" im Detail behandelt; wir werden Grammatiken hier nur soweit besprechen, wie es zum Verständnis der Definitionen erforderlich ist.

Es gibt unterschiedliche Notationen für kontextfreie Grammatiken. Wir verwenden die sogenannte EBNF — die Erweiterte Backus Naur Form.

Beispiele für Texte, die der ‹Zahl› Definition dieser Grammatik entsprechen, sind: 0, 420, -87, 3.1416, -2.09900.

Beispiele für Texte, die nicht der ‹Zahl› Definition dieser Grammatik entsprechen, sind: 007, -.65, 13., zwölf, 111Nonsense222.

Die mit spitzen Klammern markierten Bezeichner wie ‹Zahl› heißen Nichtterminale; die farblich markierten Symbole wie 3 oder . heißen Terminalsymbole. Eine Klausel wie die ersten beiden Zeilen der obigen Grammatik heißt Produktion. Eine Produktion besteht aus einem Nichtterminal auf der linken Seite der Definition und auf der rechten Seite aus einer Menge von Alternativen, die durch das Symbol | voneinander getrennt werden. Zu jedem Nichtterminal gibt es genau eine Produktion.

Zu jedem Nichtterminal kann man eine Menge von Ableitungsbäumen bilden. Ein Ableitungsbaum entsteht durch das Ersetzen der Nichtterminale in einer der Alternativen der dazugehörigen Produktion durch Ableitungsbäume für diese Nichtterminale. Die Konstruktion der Ableitungsbäume ist also ein rekursiver Prozess. Der Prozess stoppt dort, wo man eine Alternative wählt, die nur aus Terminalsymbolen bestehen. Falls ein Nichtterminal durch ein Sternchen oder ein Pluszeichen markiert wird, so wie ‹Ziffer›* oder ‹Ziffer›+ oben, so bedeutet dies 0 oder mehr Wiederholungen (für *) bzw. 1 oder mehr Wiederholungen (für +) des Nichtterminals.

Jeder Ableitungsbaum steht für einen Text (häufig Wort oder Satz genannt), nämlich die Sequenz der Terminalsymbole, die in dem Baum vorkommen, von links nach rechts im Baum abgelesen. Die durch eine Grammatik definierte Sprache ist die Menge aller Worte, für die man Ableitungsbäume bilden kann.

Hier einige Beispiele für AbleitungsbäumeWenn Sie mit Grammatiken und Ableitungsbäumen experimentieren möchten, schauen Sie sich mal das Grammatik-Werkzeug unter http://www.cburch.com/proj/grammar/index.html an. Mit diesem Werkzeug können Sie automatisch Ableitungsbäume für Wörter kontextfreier Grammatiken eingeben. Die Notation für kontextfreie Grammatiken in dem Tool ist allerdings etwas anders und sie u nterstützt nicht die + und * Operatoren sowie nur alphanumerische Nichtterminale. Eine Variante der Grammatik oben, die dieses Tool versteht, finden Sie unter der URL https://github.com/ps-mr/KdP2014/blob/master/materials/grammar. des Nichtterminals ‹Zahl› und die Worte, die sie repräsentieren. Wir stellen die Bäume der Einfachheit halber durch Einrückung des Textes dar. Da damit die Bäume um 90 Grad gegenüber der Standarddarstellung gedreht sind, müssen die Terminalsymbole von oben nach unten (statt von links nach rechts) abgelesen werden.

Der Ableitungsbaum für 0 ist:

‹Zahl›
   ‹PositiveZahl›
     ‹GanzeZahl›
       0

Der Ableitungsbaum für 420 ist:

‹Zahl›
   ‹PositiveZahl›
     ‹GanzeZahl›
       ‹ZifferNichtNull›
         4
       ‹Ziffer›
         ‹ZifferNichtNull›
           2
       ‹Ziffer›
        0

8.3 Syntax von BSL

Nach diesen Vorarbeiten können wir nun präzise die Syntax von BSL durch eine kontextfreie Grammatik definieren. Diese Syntax ist vollständig bis auf folgende Sprachfeatures, die wir noch nicht behandelt haben: Definition von Funktionen durch lambda-Ausdrücke, Quoting, Zeichendaten, Bibliotheksimporte. Außerdem werden in der Grammatik Aspekte, die für die Bedeutung der Sprache irrelevant sind, außer Acht gelassen, zum Beispiel Kommentare, Zeilenumbrüche und Leerzeichen. Aus diesem Grund bezeichnet man Grammatiken wie die folgende für BSL häufig als die abstrakte Syntax einer Programmiersprache, im Unterschied zur konkreten Syntax, die auch Aspekte wie Kommentare und Zeilenumbrüche umfasst. Analog dazu werden Ableitungsbäume, wie sie oben beschrieben wurden, im Kontext abstrakter Syntax häufig als abstrakte Syntaxbäume (abstract syntax trees (AST) bezeichnet.

Das Nichtterminal ‹program› steht für die Syntax ganzer Programme; ‹def-or-expr› für Definitionen oder Ausdrücke, ‹definition› für Funktions-/Konstanten-/Strukturdefinitionen, ‹e› für Ausdrücke und ‹v› für Werte.

Die geschweiften Klammern um Teilsequenzen wie in {[ ‹e› ‹e› ]}+ dienen dazu, um den * oder + Operator auf eine ganze Sequenz von Terminalsymbolen und Nichtterminalen anzuwenden und nicht nur auf ein einzelens Nichtterminal. In diesem Beispiel bedeutet es, dass 1 oder mehr Vorkommen von [ ‹e› ‹e› ] erwartet werden.

Die Produktionen für einige Nichtterminale, deren genaue Form nicht interessant ist, wurden in der Grammatik ausgelassen: ‹name› steht für die zugelassenen Bezeichner für Funktionen, Strukturen und Konstanten. ‹number› steht für die zugelassenen Zahlen. ‹boolean› steht für #true oder #false. ‹string› steht für alle Strings wie "asdf". Das Nichtterminal ‹image› steht für Bilder im Programmtext (Bildliterale) wie .

Die Werte der Form < make-‹name› ‹v›* > dienen dazu, Instanzen von Strukturen zu repräsentieren. Sie dürfen in BSL nicht direkt im Original-Programmtext vorkommen, aber sie werden während der Reduktion erzeugt und in das Programm eingefügt.

8.4 Die BSL Kernsprache

Wenn man die Bedeutung einer Sprache definiert, möchte man normalerweise, dass diese Definition so kurz wie möglich ist, denn nur dann kann ein Benutzer sie leicht verstehen und Schlussfolgerungen ziehen.

Aus diesem Grund identifizieren wir eine Untersprache der BSL, die bereits ausreichend ist, um alle Programme zu schreiben, die man auch in BSL schreiben kann. Der einzige Unterschied ist, dass man an einigen Stellen vielleicht etwas umständlicheres schreiben muss.

Wir haben bereits ein intellektuelles Werkzeug kennengelernt, um Kernsprachenelemente von eher unwichtigem Beiwerk zu unterscheiden, nämlich den syntaktischen Zucker. Im Abschnitt Bedeutung konditionaler Ausdrücke haben wir gesehen, dass es nicht notwendig ist, if Ausdrücke und innerhalb von cond Ausdrücken den else Operator zu unterstützen, weil man diese Sprachfeatures leicht mit dem einfachen cond Ausdruck simulieren kann. Die in Bedeutung konditionaler Ausdrücke angegebenen Transformationen betrachten wir daher als die Definition dieser Sprachfeatures und betrachten daher im folgenden nur noch die Kernsprache, in die diese Transformationen abbilden.

Man könnte versuchen, auch and noch wegzutransformieren und durch einen cond Ausdruck zu ersetzen: (and e-1 e-2) wird transformiert zu (cond [e-1 e-2] [else #false]). Zwar simuliert dies korrekt die Auswertungsreihenfolge, aber diese Transformation ist nicht adäquat für das in DrRacket implementierte Verhalten, wie folgendes Beispiel illustriert:

> (and #true 42)

and: question result is not true or false: 42

> (cond [#true 42] [else #false])

42

Damit sieht die Grammatik unserer Kernsprache wie folgt aus. Die Grammatik für Werte ‹v› bleibt unverändert.

8.5 Werte und Umgebungen

Was bedeuten nun Programme in der Sprache, deren Syntax oben definiert wurde? Die Bedeutung eines Ausdrucks wollen wir modellieren als Sequenz von Reduktionsschritten, die am Ende zu einem Wert führt (oder mit einem Fehler abbricht oder nicht terminiert).

Werte haben wir bereits oben durch die Grammatik definiert. Alle Konstanten wie #true, 42 oder "xyz" sind also Werte. Außerdem sind Instanzen von Strukturen Werte; die Werte aller Felder der Struktur müssen ebenfalls Werte sein. Also ist beispielsweise <make-posn 3 4> ein Wert. Wir modellieren Strukturen so, dass Ausdrücke wie (make-posn 3 (+ 2 2)) zu diesem Wert ausgewertet werden — hier ist also der Ausdruck der make-posn aufruft (mit runden Klammern) von dem Wert <make-posn 3 4> (mit spitzen Klammern) zu unterscheiden.

Sofern in Ausdrücken Funktionen, Konstanten, oder Strukturen benutzt werden, kann die Auswertung eines Ausdrucks nicht im "luftleeren" Raum stattfinden, sondern man muss die Umgebung (Environment, im folgenden als env abgekürzt) kennen, in dem der Ausdruck ausgewertet wird, um Zugriff auf die dazugehörigen Definitionen zu haben. Vom Prinzip her ist die Umgebung einfach der Teil des Programms bis zu dem Ausdruck, der gerade ausgewertet wird. Allerdings werden Konstantenfinitionen ja auch ausgewertet (siehe Bedeutung von Funktions- und Konstantendefinitionen). Dies bringen wir durch folgende Definition zum Ausdruck. Beachten Sie, dass im Unterschied zur Grammatik von BSL Konstantendefinitionen die Form ( define ‹name› ‹v› ) und nicht ( define ‹name› ‹e› ) haben.

Ein Umgebung besteht also aus einer Sequenz von Funktions-, Konstanten- oder Strukturdefinitionen, wobei der Ausdruck in Konstantendefinitionen bereits zu einem Wert ausgewertet wurde.

8.6 Auswertungspositionen und die Kongruenzregel

Im Abschnitt Bedeutung von BSL Ausdrücken haben wir das erste Mal über Auswertungspositionen und die Kongruenzregel gesprochen. Die Auswertungspositionen markieren, welcher Teil eines Programms als nächstes ausgewertet werden soll. Die Kongruenzregel sagt, dass man Unterausdrücke in Auswertungspositionen auswerten und das Ergebnis der Auswertung wieder in den ganzen Ausdruck einbauen darf.

Betrachten wir als Beispiel den Ausdruck (* (+ 1 2) (+ 3 4)). Der Unterausdruck (+ 1 2) befindet sich in Auswertungsposition und kann zu 3 ausgewertet werden. Gemäß der Kongruenzregel kann ich den Gesamtausdruck also zu (* 3 (+ 3 4)) reduzieren.

Wir werden Auswertungspositionen und die Kongruenzregel durch einen Auswertungskontext formalisieren. Ein Auswertungskontext ist eine Grammatik für Programme, die ein "Loch", [], enthalten. In Bezug auf den DrRacket Stepper kann man den Auswertungskontext als den während einer Reduktion nicht farblich markierten Teil des Ausdrucks verstehen. Die Grammatik ist so strukturiert, dass jedes Element der definierten Sprache genau ein "Loch" enthält.

Hier einige Beispiele für Auswertungskontexte:

(* [] (+ 3 4))

(posn-x (make-posn 14 []))

(and #true (and [] x))

Dies sind alles keine Auswertungskontexte:

(* (+ 3 4) [])

(posn-x (make-posn 14 17))

(and #true (and x []))

Das "Loch" in diesen Ausdrücken steht genau für die Unterausdrücke in einem Programm, die in Auswertungsposition sind. Wir verwenden die Definition für Werte, ‹v›, von oben, um zu steuern, dass die Auswertung der Argumente in Funktionsaufrufen von links nach rechts erfolgt.

Bisher (in Abschnitt Bedeutung von BSL Ausdrücken und Bedeutung von Funktionsdefinitionen) hatten wir die Auswertungspositionen so definiert, dass man bei Funktionsaufrufen die Argumente in beliebiger Reihenfolge auswerten kann. Die Auswertungskontexte wie oben definiert legen diese Reihenfolge fest, nämlich von links nach rechts. Wir werden später mehr zu diesem Unterschied sagen.

Sei E ein Auswertungskontext. Wir verwenden die Schreibweise E[e], um das "Loch" in dem Auswertungskontext durch einen Ausdruck e zu ersetzen.

Beispiel: Wenn E = (* [] (+ 3 4)), dann ist E[(+ 1 2)] = (* (+ 1 2) (+ 3 4)).

Mit Hilfe dieser Schreibweise können wir nun die Kongruenzregel so definieren:

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

Wir schreiben die Auswertungsregeln generell so auf, dass wir jeder Regel einen Namen geben. Diese Regel heißt (KONG).

Beispiel: Betrachten wir den Ausdruck e = (* (+ 1 2) (+ 3 4)). Diesen können wir zerlegen in einen Auswertungskontext E = (* [] (+ 3 4)) und einen Ausdruck e-1 = (+ 1 2), so dass e = E[e-1]. Da wir e-1 reduzieren können, (+ 1 2) → 3, können wir auch dank (KONG) e reduzieren zu E[3] = (* 3 (+ 3 4)).

8.7 Nichtterminale und Metavariablen - Keine Panik!

In der Kongruenzregel von oben stehen Namen wie e-1 und e-2 für beliebige Ausdrücke und E für einen beliebigen Auswertungskontext.

Im Allgemeinen verwenden wir die Konvention, dass der Name x und Varianten wie x-1 und x-2 für beliebige Worte des Nichtterminals ‹x› steht (zum Beispiel für ‹x› = ‹e› oder ‹x› = ‹v›). Derart verwendete Bezeichner wie v-1 oder e-2 nennt man auch Metavariablen, weil sie nicht Variablen von BSL sind, sondern Variablen sind, die für Teile von BSL Programmen stehen.

Wenn wir Nonterminale als Mengen interpretieren (nämlich die Menge der Worte für die es Ableitungsbäume gibt), so könnten wir die Regel von oben auch so aufschreiben:

Für alle e-1∈‹e› und alle e-2∈‹e› und alle E∈‹E› : Falls e-1 → e-2, dann E[e-1] → E[e-2].

Da dies die Regeln aber viel länger macht, verwenden wir die hier beschriebene Konvention.

8.8 Bedeutung von Programmen

Gemäß unserer Grammatik besteht ein Programm aus einer Sequenz von Definitionen und Ausdrücken. Die Auswertungsregel für Programme nennen wir (PROG):

(PROG): Ein Programm wird von links nach rechts ausgeführt und startet mit der leeren Umgebung. Ist das nächste Programmelement eine Funktions- oder Strukturdefinition, so wird diese Definition in die Umgebung aufgenommen und die Ausführung mit dem nächsten Programmelement in der erweiterten Umgebung fortgesetzt. 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 in der aktuellen Umgebung zunächst e zu einem Wert v ausgewertet und dann (define x v) zur aktuellen Umgebung hinzugefügt.

Beispiel: Das Programm ist:

(define (f x) (+ x 1))

(define c (f 5))

(+ c 3)

8.9 Bedeutung von Ausdrücken

Jeder Ausdruck wird in einer Umgebung env ausgewertet, wie sie im vorherigen Abschnitt definiert wurde. Um die Notation nicht zu überladen, werden wir env nicht explizit zu jeder Reduktionsregel dazuschreiben sondern als implizit gegeben annehmen. Die Auswertung wird, wie aus Abschnitt Bedeutung von BSL Ausdrücken bekannt, in Form von Reduktionsregeln der Form e-1 → e-2 definiert. Ein Ausdruck e wird ausgewertet, indem er solange reduziert wird, bis ein Wert herauskommt: e → e-1 → ... → v.

Ein Fehler während der Auswertung äußert sich darin, dass die Reduktion "steckenbleibt", also wir bei einem Ausdruck ankommen, der kein Wert ist und der nicht weiter reduziert werden kann.

8.9.1 Bedeutung von Funktionsaufrufen

Funktionen werden unterschiedlich ausgeführt je nachdem ob der Funktionsname eine primitive Funktion oder eine in der Umgebung definierte Funktion ist. Im ersten Fall wird die primitive Funktion auf den Argumenten ausgewertet. Ist dies erfolgreich, so kann auf das Result reduziert werden. Ist dies nicht erfolgreich, so kann der Ausdruck nicht reduziert werden.

Ist die Funktion hingegen in der Umgebung definiert, so wird der Aufruf zum Body der Funktionsdefintion reduziert, wobei vorher alle Parameternamen durch die aktuellen Parameterwerte ersetzt werden. Dies ist die Bedeutung der Notation e[name-1 := v-1 ... name-n := v-n].

Die Reduktionsregeln sind also:

(FUN): Falls ( define ( name name-1 ... name-n ) e ) in der Umgebung,
dann ( name v-1 ... v-n ) → e[name-1 := v-1 ... name-n := v-n]

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

8.9.2 Bedeutung von Konstanten

Konstanten werden ausgewertet, indem sie in der Umgebung nachgeschlagen werden:

(CONST): Falls ( define name v ) in der Umgebung, dann name → v.

8.9.3 Bedeutung konditionaler Ausdrücke

Konditionale Ausdrücke werden ausgewertet, wie schon in Bedeutung konditionaler Ausdrücke beschrieben. Gemäß der Definition des Auswertungskontextes wird stets nur der erste Bedingungsausdruck ausgewertet. Je nachdem ob dieser #true oder #false ergibt, wird auf den Ergebnisausdruck oder den um die fehlgeschlagene Bedingung gekürzten cond Ausdruck reduziert:

(COND-True): ( cond [ #true e ] ... ) → e

(COND-False): ( cond [ #false e-1 ] [ e-2 e-3 ] ... ) → ( cond [ e-2 e-3 ] ... )

8.9.4 Bedeutung boolscher Ausdrücke

Die Definition der Auswertung boolscher Ausdrücke wertet die Bedingungen nur soweit wie nötig aus. Insbesondere wird die Auswertung abgebrochen, sobald einer der Ausdrücke #false ergibt.

Die ersten beiden Reduktionsregeln sind erforderlich, um zu überprüfen, dass alle Argumente boolsche Werte sind; andernfalls hätten die beiden Regeln zu ( and #true v ) → v zusammengefasst werden können. Insgesamt benötigen wir für boolsche Ausdrücke die folgenden vier Regeln:

(AND-1): ( and #true #true ) → #true

(AND-2): ( and #true #false ) → #false

(AND-3): ( and #false ... ) → #false

(AND-4): ( and #true e-1 e-2 ... ) → ( and e-1 e-2 ... )

8.9.5 Bedeutung von Strukturkonstruktoren und Selektoren

Strukturdefinitionen definieren drei Arten von Funktionen: Konstruktoren wie make-posn, Selektoren wie posn-x und Prädikate wie posn?. Zu jeder dieser drei Arten benötigen wir eine Reduktionsregel.

Konstruktoren erzeugen Instanzen einer Struktur. Dies gelingt, wenn eine Struktur des gleichen Namens in der Umgebung zu finden ist, und diese so viele Felder wie der Konstruktor Parameter hat. Dies bringt uns zu folgender Regel:

(STRUCT-make): Falls ( define-struct name ( name-1 ... name-n ) ) in der Umgebung, dann ( make-name v-1 ... v-n ) → < make-name v-1 ... v-n >.

Selektoraufrufe werden reduziert, indem in der Umgebung die Strukturdefinition nachgeschlagen wird, um den Namen des Feldes auf die Argumentposition des Konstruktoraufrufs abzubilden. Dann wird der entsprechende Wert des Feldes zurückgegeben:

(STRUCT-select): Falls ( define-struct name ( name-1 ... name-n ) ) in der Umgebung, dann ( name-name-i < make-name v-1 ... v-n > ) → v-i

Bei Prädikaten wird geschaut, ob es sich beim Argument des Prädikats um eine Strukturinstanz der in Frage stehenden Struktur handelt oder nicht, und je nachdem #true bzw. #false zurückgegeben:

(STRUCT-predtrue): ( name? < make-name ... > ) → true

(STRUCT-predfalse): Falls v nicht < make-name ... >, dann ( name? v ) → #false

8.10 Reduktion am Beispiel

Betrachten Sie folgendes Programm, dessen Bedeutung wir Schritt für Schritt mit Hilfe der Auswertungsregeln ermitteln werden:

(define-struct s (x y))

(define (f x) (cond [(< x 1) (/ x 0)]

[#true (+ x 1)]

[#true x]))

(define c (make-s 5 (+ (* 2 3) 4)))

(f (s-x c))

• Gemäß (PROG) starten wir mit der leeren Umgebung env = leer. Das erste Programmelement ist eine Strukturdefinition, daher ist gemäß (PROG) die Umgebung im nächsten Schritt env = (define-struct s (x y)).

• Das nächste Programmelement ist eine Funktionsdefinition, daher ist gemäß (PROG) die Umgebung im nächsten Schritt env =

  (define-struct s (x y))

  (define (f x) (cond [(< x 1) (/ x 0)]

  [#true (+ x 1)]

  [#true x]))

• Das nächste Programmelement ist eine Konstantendefinition. Gemäß (PROG) müssen wir also zunächst (make-s 5 (+ (* 2 3) 4)) auswerten:

  • e = (make-s 5 (+ (* 2 3) 4)) zerfällt in E = (make-s 5 (+ [] 4)) und e-1 = (* 2 3). Gemäß (PRIM) gilt e-1 → 6; gemäß (KONG) gilt daher e → (make-s 5 (+ 6 4)).

  • e = (make-s 5 (+ 6 4)) zerfällt in E = (make-s 5 []) und e-1 = (+ 6 4). Gemäß (PRIM) gilt e-1 → 10; gemäß (KONG) gilt daher e → (make-s 5 10).

  • (make-s 5 10) → <make-s 5 10> gemäß (STRUCT-make).

  Gemäß (PROG) ist unsere neue Umgebung daher nun env =

  (define-struct s (x y))

  (define (f x) (cond [(< x 1) (/ x 0)]

  [#true (+ x 1)]

  [#true x]))

  (define c <make-s 5 10>)

• Das letzte Programmelement ist ein Ausdruck, den wir gemäß (PROG) in der aktuellen Umgebung auswerten:

  • e = (f (s-x c)) zerfällt in E = (f (s-x [])) und e-1 = c. Gemäß (CONST) gilt c → <make-s 5 10>; gemäß (KONG) gilt daher e → (f (s-x <make-s 5 10>)).

  • e = (f (s-x <make-s 5 10>)) zerfällt in E = (f []) und e-1 = (s-x <make-s 5 10>). Gemäß (STRUCT-select) gilt e-1 → 5; gemäß (KONG) gilt daher e → (f 5).

  • (f 5) → (cond [(< 5 1) (/ 5 0)] [#true (+ 5 1)] [#true 5]) gemäß (FUN).

  • e = (cond [(< 5 1) (/ 5 0)] [#true (+ 5 1)] [#true 5]) zerfällt in E = (cond [[] (/ 5 0)] [#true (+ 5 1)] [#true 5]) und e-1 = (< 5 1). Gemäß (PRIM) gilt e-1 → #false; gemäß (KONG) gilt daher e → (cond [#false (/ 5 0)] [#true (+ 5 1)] [#true 5]).

  • (cond [#false (/ 5 0)] [#true (+ 5 1)] [#true 5]) → (cond [#true (+ 5 1)] [#true 5]) gemäß (COND-False).

  • (cond [#true (+ 5 1)] [#true 5]) → (+ 5 1) gemäß (COND-True).

  • (+ 5 1) → 6 gemäß (PRIM).

8.11 Bedeutung von Daten und Datendefinitionen

Datendefinitionen haben auf das Programmverhalten keinen Einfluss, da sie in Form eines Kommentars definiert werden. Dennoch können wir ihnen eine präzise Bedeutung geben, die hilft, ihre Rolle zu verstehen.

Hierzu ist es wichtig, das Datenuniversum eines Programms zu verstehen. Das Datenuniversum umfasst alle Daten, die in einem gegebenen Programm potentiell vorkommen können. Welche Werte das sind, wird durch unsere Grammatik für Werte, ‹v›, oben beschrieben. Allerdings können nicht alle Werte, die durch ‹v› beschrieben werden, in einem Programm vorkommen, sondern nur diese, für die die benutzen Strukturen auch wirklich im Programm definiert sind.

Beispiel: Ein Programm enthält die Strukturdefinitionen

(define-struct circle (center radius))

(define-struct rectangle (corner-ul corner-dr))

Das Datenuniversum für dieses Programm umfasst alle Werte der Basistypen, aber auch alle Strukturinstanzen, die sich auf Basis dieser Strukturdefinitionen bilden lassen, also zum Beispiel <make-circle 5 6> aber auch:

<make-circle <make-circle <make-rectangle 5 <make-rectangle #true "asdf">> 77> 88>

Das Datenuniversum sind also alle Werte, die sich durch die Grammatik von ‹v› bilden lassen, eingeschränkt auf die Strukturen, die in dem Programm definiert sind.

Eine Strukturdefinition erweitert also das Datenuniversum um neue Werte, nämlich alle Werte, in denen mindestens einmal diese Struktur verwendet wird.

Eine Datendefinition, auf der anderen Seite, erweitert nicht das Datenuniversum. Eine Datendefinition definiert eine Teilmenge des Datenuniversums.

Beispiel:

; a Posn is a structure: (make-posn Number Number)

<make-posn 3 4 > ist ein Element der definierten Teilmenge, aber <make-posn #true "x" > oder <make-posn <make-posn 3 4> 5> sind es nicht.

Eine Datendefinition beschreibt im Allgemeinen eine kohärente Teilmenge des Datenuniversums. Funktionen können durch ihre Signatur deutlich machen, welche Werte des Datenuniversums sie als Argumente akzeptieren und welche Ergebnisse sie produzieren.

8.12 Refactoring von Ausdrücken und Schliessen durch Gleichungen

Wir hatten in Abschnitt Bedeutung von BSL Ausdrücken vorgestellt, wie man auf Basis der Reduktionsregeln eine Äquivalenzrelation auf Ausdrücken definieren kann. Diese Äquivalenzen können zum Refactoring von Programmen verwendet werden - also Programmänderungen, die nicht die Bedeutung verändern aber die Struktur des Programms verbessern. Außerdem können sie verwendet werden, um Eigenschaften seines Programmes herzuleiten, zum Beispiel dass die Funktion overlaps-circle aus dem vorherigen Kapitel kommutativ ist, also (overlaps-circle c1 c2) ≡ (overlaps-circle c2 c1).

Die Äquivalenzrelation aus Abschnitt Bedeutung von BSL Ausdrücken war allerdings zu klein für viele praktische Zwecke, denn sie erfordert beispielsweise, dass wir Funktionsaufrufe nur dann auflösen können, wenn alle Argumente Werte sind.

BSL hat jedoch eine bemerkenswerte Eigenschaft, die es uns erlaubt, eine viel mächtigere Äquivalenzrelation zu definieren: Es ist für das Ergebnis eines Programms nicht von Bedeutung, in welcher Reihenfolge Ausdrücke ausgewertet werden. Insbesondere ist es nicht notwendig, vor einem Funktionsaufruf die Argumente auszuwerten; man kann auch einfach die Argumentausdrücke verwenden.

Die Idee wird durch folgenden, allgemeineren Auswertungskontext ausgedrückt:

(EKONG): Falls e-1 ≡ e-2, dann E[e-1] ≡ E[e-2].

Eine Äquivalenzsrelation sollte möglichst groß sein, damit wir so viele Äquivalenzen wie möglich zeigen können. Gleichzeitig sollte sie korrekt sein. Dies bedeutet, dass äquivalente Programme das gleiche Verhalten haben, also insbesondere – sofern sie terminieren – bei Auswertung den gleichen Wert ergeben.

Wir definieren nun nach und nach die Regeln, die für die Äquivalenzrelation gelten sollen. Zunächst einmal sollte es tatsächlich eine Äquivalenzrelation — also reflexiv, kommutativ und transitiv — sein:

(EREFL): e ≡ e.

(EKOMM): Falls e1 ≡ e2, dann e2 ≡ e1.

(ETRANS): Falls e-1 ≡ e-2 und e-2 ≡ e-3, dann e-1 ≡ e-3.

Die Verknüpfung zur Auswertungsrelation wird durch diese Regel geschaffen: Reduktion erhält Äquivalenz.

(ERED): Falls e-1 → e-2 dann e-1 ≡ e-2.

Damit wir auch "symbolisch" Funktionen auswerten können, erweitern wir die Regel für Funktionsaufrufe, so dass es für die Bestimmung von Äquivalenzen nicht notwendig ist, die Argumente auszuwerten.

(EFUN): Falls ( define ( name name-1 ... name-n ) e ) in der Umgebung,
dann ( name e-1 ... e-n ) ≡ e[name-1 := e-1 ... name-n := e-n]

Bei der Konjunktion wissen wir, dass der Gesamtausdruck zu #false auswertet (oder nicht terminiert), wenn mindestens eines der Argumente äquivalent zu #false ist.

(EAND): ( and ... #false ... ) ≡ #false

Außerdem können wir Wissen, das wir über die eingebauten Funktionen haben, beim Schliessen mit Äquivalenzen nutzen. Beispielsweise wissen wir, dass (+ a b) ≡ (+ b a). Wir fassen die Menge der Äquivalenzen, die für die eingebauten Funktionen gelten unter dem Namen (EPRIM) zusammen.

Einen kleinen Hakenfuss gibt es allerdings doch noch. Man würde sich von einer Äquivalenzrelation für Programme wünschen, dass folgende Eigenschaft gilt: Falls e-1 ≡ e-2 und e-1 →* v, dann auch e-2 →* v. Diese Eigenschaft gilt jedoch nicht, weil es sein kann, dass e-1 terminiert aber e-2 nicht.

Beispiel: Betrachten Sie folgendes Programm:

(define (f x) (f x))

(define (g x) 42)

(g (f 1))

Da (f 1) → (f 1), terminiert die Berechnung des Arguments für g nicht, und gemäß der Kongruenzregel gilt damit (g (f 1)) → (g (f 1)), daher terminiert die Berechnung des Ausdrucks (g (f 1)) → (g (f 1)) nicht. Auf der anderen Seite gilt jedoch gemäß (EFUN) (g (f 1)) ≡ 42. Man muss daher bei der Verwendung der Äquivalenzregeln berücksichtigen, dass die Äquivalenz nur unter der Voraussetzung gilt, dass die Terme auf beiden Seiten terminieren..

Es gilt jedoch folgende etwas schwächere Eigenschaft, die wir ohne Beweis aufführen:

Falls e-1 ≡ e-2 und e-1 →* v-1 und e-2 →* v-2, dann v1 = v2.

Wenn also e-1 und e-2 gleich sind und beide terminieren, dann ist der Wert, der herauskommt, gleich.