Programmiersprachen Vorlesung im WS 94/95

Harald Ganzinger 27. Oktober 1994

Inhaltsverzeichnis

1 Die Vorlesung 3

2 Einleitung 5 2.1 Die Rolle von Struktur in der Programmierung . . . . . . . . . . . . . . 5 2.2 Die von-Neumann-Maschine . . . . . . . . . . . . . . . . . . . . . . . . . 5 2.3 Frühe Erfahrungen . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6

2.3.1 Dominanz der Laufzeiteffizienz . . . . . . . . . . . . . . . . . . . 6 2.3.2 Vorteile der Hochsprachen . . . . . . . . . . . . . . . . . . . . . . 6 2.3.3 Nochmals zur Effizienz . . . . . . . . . . . . . . . . . . . . . . . . 6

2.4 Programmiersprachen als Maschinenerweiterungen . . . . . . . . . . . . 7 2.5 Wie soll man ein Programm strukturieren? . . . . . . . . . . . . . . . . 7 2.6 Sprachbeschreibungen . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 2.7 Historisches . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8

3 Funktionale Programmiersprachen 9 3.1 Übersicht . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 3.2 Einführung in ML . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9

3.2.1 Sprachübersicht . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 3.2.2 Primitive Ausdrücke, Werte und Typen . . . . . . . . . . . . . . 10 3.2.3 Funktionsdefinitionen . . . . . . . . . . . . . . . . . . . . . . . . 13 3.2.4 Deklarationen . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 3.2.5 Muster . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17

3.3 Grundbegriffe der Termersetzung . . . . . . . . . . . . . . . . . . . . . . 19 3.4 Funktionsauswertung als Termersetzung . . . . . . . . . . . . . . . . . . 20 3.5 Typdefinitionen . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 3.6 Strukturelle Induktion . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24

1 Die Vorlesung

Allgemeines

Die Vorlesung (4V+2Ü) ist eine neue Stammvorlesung im Bereich “Praktische Informatik”, die ab diesem Semester (WS 94/95) regelmäßig (in der Regel einmal pro Jahr) angeboten werden wird. Sie richtet sich an Informatikstudenten nach dem Vordiplom. Weitere Voraussetzungen gibt es nicht. Leistungsnachweise werden in Form von Übungsscheinen ausgestellt, die die erfolgreiche Bearbeitung eines gewissen Prozentsatzes an Übungsaufgaben voraussetzen.

Zeit und Ort: Di + Do 14–16, Geb. 27, HS II; Übungen nach Vereinbarung

Beschreibung

Die Vorlesung bespricht die grundlegenden Konzepte heutiger Programmiersprachen aus der Sicht der praktischen Anwendung zur Lösung von Softwareproblemen.

Programmierung bedeutet nicht nur die Entwicklung und das Testen (oder, besser, Verifizieren) irgendeines korrekten und effizienten Programms zur Lösung eines bestimmten Anwendungsproblems. Es ist auch wichtig, daß das Programm gute Wartungseigenschaften besitzt. Ein Programm soll daher möglichst viele, in anderen Kontexten wiederverwendbare Teile besitzten, es soll leicht modifizierbar sein, wenn sich das ursprünglich gestellte Problem ändert, es soll von Leuten verstanden werden können, die an seiner Entwicklung nicht beteiligt waren, und vieles mehr.

In der Vorlesung untersuchen wir die Konzepte heutiger Sprachen hinsichtlich der Art und Weise, wie sie diese Anforderungen an die Programmierung unterstützen. Folgende Fragen werden deshalb typischerweise gestellt:

• Wie helfen Sprachkonzepte, bestimmte Programmentwicklungstechniken umzusetzen?

• Welches Rechenmodell steht hinter einem Sprachkonzept?

• Wie unterstützen Sprachkonzepte die Verifikation von Programmen?

• Wie wird Abstraktion von der konkreten Problemstellung ermöglicht?

• Wie wird Abstraktion von der konkreten Implementierungstechnik ermöglicht?

• Wie wird Strukturierung großer Programmsysteme unterstützt?

• Für welche Softwareprobleme bietet ein Konzept keine Unterstützung?

• Ist ein Konzept leicht und/oder effizient implementierbar, d.h. in Maschinensprache (welcher Maschinen?) übersetzbar?

Diese Fragen werden nicht theoretisch oder technisch detailiert behandelt, sondern anhand ausgewählter, nichttrivialer Programmierbeispiele erläutert. Verweise auf die theoretische oder technisch detailiertere Behandlung, die man in angrenzenden Vorlesungen (z.B. Übersetzerbau, Semantik von Programmiersprachen, Spezifikation und Verifikation, Logische Programmierung, λ-Kalkül und Typentheorie) lernen kann, werden gegeben.

Die Vorlesung orientiert sich an sprachübergreifenden Konzepten (Kontrollstrukturen, Datentypen, Berechnungsmodellen, Abstraktionsmechanismen), eine Sichtweise, die oft parallel, aber manchmal auch orthogonal zu den großen Programmierparadigmen (imperativ, funktional, logisch, objektorientiert) liegt. Die Vorlesung verwendet konkrete Programmiersprachen als Anschaungsmaterial, insbesondere Modula, C(++), Smalltalk, ML, Haskell und Prolog. Die begleitenden Übungen sind teils theoretisch, aber zum größeren Teil praktisches Programmieren in einigen der genannten Sprachen.

Lernziele

• Beherrschen von grundlegenden Techniken des Programmierens in imperativen, funktionalen, logischen und objektorientierten Programmiersprachen

• Multilinguales Programmieren

• Erwerben von Wissen über die Art und Weise, wie einzelne Sprachkonzepte bei der Lösung gewisser Softwareprobleme helfen oder auch nicht helfen

• Erwerben von Verständnis für theoretische und praktische Problemstellungen bei der semantischen Erklärung oder bei der Implementierung von Programmiersprachen

Stichworte zum Inhalt

Wir gehen davon aus, daß aus dem Grundstudium bekannt ist:

1. Imperatives Programmieren (Pascal, C): Kontrollstrukturen und Verifikationstechniken (Zusicherungen, Invarianten)

2. Prozeduren, Module, abstrakte Datentypen, Zusammenhang zwischen Abstraktion und Implementierung (C++, Modula 2)

Wir konzentrieren uns daher auf:

1. Funktionale Programmierung: Termtypen, Typpolymorphismus und Typinferenz, parametrische Module, Typklassen, Auswertungsstrategien (ML und Haskell)

2. Logische Programmierung: relationales Programmieren, Deduktion durch Resolution (Prolog), Constraints

3. Vererbung und objekt-orientierte Programmierung (Smalltalk-80, C++)

4. Programmierung verteilter kommunizierender Prozesse: Occam, Nebenläufiges logisches Programmieren mit Constraints

Literatur

Lehrbücher:

1. R. Sethi: Programming languages: concepts and constructs, Addison-Wesley 1989.

2. D.A. Watt: Programming Language Concepts and Paradigms, Prentice-Hall 1989.

3. C. Ghezzi, M. Jazayeri: Programming Language Concepts, Wiley 1987.

Spezialliteratur: wird in der Vorlesung angegeben.

2 Einleitung

Literatur: R. Sethi: Programming languages: concepts and constructs, Addison-Wesley 1989, Kapitel 1

• Ein Programm ist die Spezifikation einer Berechnung.

• Eine Programmiersprache ist eine Notation zum Schreiben von Programmen.

• Etwas Geschichte.

• Sprachentwicklung wird geleitet durch die Erkenntnis, daß Komplexität durch Strukturierung handhabbar wird.

2.1 Die Rolle von Struktur in der Programmierung

Berühmtes Beispiel: Mariner I-Absturz (1962)

if not in radar contact then do not correct flight path

Einsichten: Dijkstra (1972)

“The art of programming is the art of organising complexity.”

Anforderungen an Programmiersprachen: Leichte • Lesbarkeit

• Verstehbarkeit

• Modifizierbarkeit von Programmen

Problem: Skalierbarkeit von Techniken

Aus der Psychologie: Miller (1967): Menschen können nur mit bis zu sieben Dingen gleichzeitig operieren. Wichtig, daß in möglichst wenige Symbole möglichst viel Information gepackt wird.

Lösung: Abstraktion und Modularisierung

2.2 Die von-Neumann-Maschine

• Am Anfang waren die Maschinen.

• vNM-Entwicklung: späte 40er Jahre in Princeton unter John von Neumann

• Kontrolle—Arithmetik—I/O—Speicher

• kein Unterschied zwischen Daten und Befehlen bzgl. Speicherung

• Sprünge als Mittel, Iterationen zu programmieren

• Maschinensprache (einschl. Assembler) ist unverständlich; zählen wir nicht zu den Programmiersprachen

2.3 Frühe Erfahrungen

2.3.1 Dominanz der Laufzeiteffizienz

FORTRAN als Alternative zur M.-Programmierung (Backus et al. 1957); für numerische Anwendungen; konzise, mathematische^{1} Sprache; effiziente, automatische Übersetzung; Reduktion des Programmieraufwands auf 20%.

• B*B - 4*A*C sehr ähnlich zu b^{2} − 4ac

• Beginn des Faches Übersetzerbau

• Effizienzeinbußen: Zeit zum Übersetzen; nicht optimierter Zielcode (Speicher und Zeit), selbst ein Faktor 2 gegenüber handgeschriebenen Programmen erschien nicht akzeptierbar

• Der Bau des Übersetzers war das dominierende Problem im FORTRAN-Projekt.

• wurde schnell die wichtigste Basis für die wissenschaftliche (numerische) Programmierung

Das Problem wird immer wieder genannt, wenn argumentiert wird, warum eine der moderneren funktionalen oder logischen Programmiersprachen nicht verwendet werden soll.

2.3.2 Vorteile der Hochsprachen

• Lesbarkeit

• schnellere, problemorientiertere Programmentwicklung

• Maschinenunabhängigkeit, Portabilität

• Frühes Fallbeispiel: Reimplementierung von Unix in C (Ritchie 1978)

– neue Benutzer und Erweiterungen des Systems

– Portabilität: ein maschinenunabhängiges Betriebssystem

– Restrukturierung durch verbesserte Lesbarkeit

– Ritchies Resumée: ”Ganz egal wie viel mehr Zeit und Speicher verbraucht wird, wir würden niemals mehr in Assembler programmieren.“

2.3.3 Nochmals zur Effizienz

• Lesbarkeit und verbesserte Struktur tragen zur Effizienzverbesserung bei; Effizienz wird auf allen Entwurfsebenen beeinflußt, falsche Entscheidungen sind in einer Hochsprache leichter revidierbar

• Knuth 1971: Lange Geschichte der Optimierung der falschen Dinge; weniger als 4% des Codes sei verantwortlich für mehr als 50% der Laufzeit

• Verwendung von profilers

1Formula Translation

2.4 Programmiersprachen als Maschinenerweiterungen

• Maschinen haben keine problemorientierte Struktur im Vergleich zu Formeln in FORTRAN

• Programmiersprachen erweitern die Maschine um grundlegende (mathematische) Struktur und um die Fähigkeit zum Bilden von problemorientierter Struktur

– Berechnungsmodell: die reale Maschine scheint durch oder aber auch gerade nicht; Beispiel: Multiprocessing auf einer Maschine

– Datentypen und Operationen: Typisierung von Daten, strukturierte Daten – Abstraktionsmittel: Typdefinitionen und Funktionsdefinitionen erweitern die

Grundbegriffe der Sprache in problemorientierter Weise;

– Problemlösung = Finden einer geeigneten Notation

– Hat eine Sprache Mittel zur Abstraktion, sind Spezialsprachen unnötig. Beispiel: sqrt aus +, −; queues aus arrays

– Erkennung von Fehlern zur Übersetzungszeit

– Schutz vor unerlaubten Zugriffen auf interne Strukturen

2.5 Wie soll man ein Programm strukturieren?

Programmstruktur ist nicht inhärent sondern die Folge von Entwurfsentscheidungen

Beispiel: Auffinden von Duplikaten in Listen

Lösung 1:

sort | find_adjacent_duplicates

• top-down Reduktion des Problems auf zwei einfachere Teilprobleme

• Transformation elementarer Datenstrukturen

• Teilprobleme sind unabhängig, können in verschiedenen Sprachen implementiert werden

• vgl. FP oder pipes in Unix

Lösung 2:

for each element x in the list do
 if find(x) then write(x) else insert(x)

• Strukturierung beruht auf Verwendung eines abstrakten Datentyps mit dessen Hilfe die Begriffswelt problemorientiert erweitert wird

• bottom-up

• Verwendung einer Tabelle ohne daß man wissen muß, wie sie implementiert ist

• interagierende Objekte

2.6 Sprachbeschreibungen

• Syntax; Metasprachen klar (BNF, Syntaxdiagramme)

• Semantik

– nur wenige Sprachen haben eine präzise oder sogar formale Semantikdefinition;

– welche Metasprache? (ML ist das Acronym für Meta-Language.)

– wozu?

• Pragmatik

2.7 Historisches

• Programmierung gab es schon vor der Erfindung des Computers.

Beispiel: lochkartengesteuerter Webstuhl von Jacquard (1801); bis zu 25000 Karten mit bis zu 1050 Löchern für ein seidengewebtes Portrait von 0.5 Quadratmetern mit Auflösung 1000dpi. Beispiel: Turing-Maschine (um 1935)

• Historische Computer:

mechanische Rechenmaschinen seit der Renaissance;

erste Maschine mit Speicher, CPU (“mill”) und Programmierung: Analytical Engine (Babbage 1864)

• siehe Sethi-Buch für Referenzen auf Arbeiten zur Geschichte der Computer und der Programmierung; Artikel im Informatik-Spektrum von F.L. Bauer

• Strukturierte Prorgammierung (Dijkstra 1972)

• Grundprinzipien der Datenabstraktion (Hoare 1972)

• BNF (Backus 1960; Naur 1963)

• Grundlagen für denotationale Semantik (Scott 1969)

3 Funktionale Programmiersprachen

• Auswertung von Ausdrücken

• Werte hängen nur von den Werten der Teilausdrücke ab

• meistens keine Seiteneffekte

• strukturierte Daten mit impliziter Speicherverwaltung

• Funktionen als Bürger erster Klasse

Geschichte: Lisp (McCarthy 1958) war die erste Sprache, die Rekursion, Funktionen höherer Ordnung, Listen mit Speicherbereinigung und eine (in Lisp verfaßte) formale Sprachdefinition (Reflexivität!) anbot. FP (Backus 1978) hebt die Kombinatorprogrammierung hervor. Miranda (Turner 1986) hat verzörgerte Operandenauswertung, ebenso wie Haskell (Hudak, Wadler 1990). Letztere Sprache hat Typklassen, die Vererbungsmechanismen zu definieren gestatten. Funktionale Programmierung war immer stark mit rechnergestütztem Beweisen verbunden.

3.1 Übersicht

• Einführung in ML

• Programmiertechniken

• Verifikationstechniken, insbesondere strukturelle Induktion

• Rechenmodell Termersetzung

• Typinferenz in ML

3.2 Einführung in ML

Literatur: R. Harper: Introduction to Standard ML, Carnegie Mellon University 1986–1993; siehe WWW-Seite L.C. Paulson: ML for the Working Programmer, Cambridge University Press 1991.

3.2.1 Sprachübersicht

• Funktionen sind Daten erster Klasse. Insbesondere können sie Argumente und Ergebnisse von Funktionsaufrufen sein oder in Variablen gespeichert werden. Die Anwendung (rekursiver) Funktionen auf ein Argument ist der hauptsächliche Kontrollmechanismus der ML-Programmierung.

• Interaktivität

• starke Typisierung: Typinferenz durch den Übersetzer, garantiert kein Typfehler zur Laufzeit

• polymorphes Typsystem mit automatisch inferierbaren allgemeinsten Typen

• parametrisierte, abstrakte Datentypen • statische Bindung von Variablen

• typsichere Ausnahmebehandlung

Geschichte: Erste Versionen um 1975 von Gordon, Milner, Wadsworth im Zusammenhang mit Semantik und Verifikation von Programmiersprachen (LCF). Standard ML, welches in dieser Vorlesung behandelt wird, beinhaltet Ideen von HOPE und von Cardellis ML-Dialekt. Das Modulsystem stammt von MacQueen, vgl. Literaturangaben in Harpers Buch.

3.2.2 Primitive Ausdrücke, Werte und Typen

Interaktion

hg@mpii02039(88)% sml
Standard ML of New Jersey, Version 0.93, February 15, 1993
val it = () : unit
- 3+2;
val it = 5 : int
- 3+it;
val it = 8 : int
- it+cos(3.0);
std_in:4.1-4.11 Error: operator and operand don't agree (tycon mismatch)
  operator domain: int * int
  operand:         int * real
  in expression:
    + : overloaded (it,cos (3.0))
- real(it)+cos(3.0);
val it = 7.01000750339955 : real
-

Einheitstyp Der Type unit hat den einzigen Wert (). Wird gebraucht, wenn Wert uninteressant oder für parameterlose Funktionen.

Booleans

- if not true then true andalso false else true;
val it = true : bool

• then-Typ = else-Type

• else zwingend notwendig

• vordefinierte Funktionen not, andalso, orelse

Ganze Zahlen

- 75;
val it = 75 : int
- ~13;
val it = ~13 : int

• vordefinierte Funktionen +, -, *, div, mod

• vordefinierte Relationen <, <=, >, >=, =, <>,

Zeichenreihen

- "Programmiersprachen WS94/95";
val it = "Programmiersprachen WS94/95" : string
- "Programmiersprachen " ^"WS94/95";
val it = "Programmiersprachen WS94/95" : string
- size it;
val it = 27 : int
- "\"Programmiersprachen\" WS94/95";
val it = "\"Programmiersprachen\" WS94/95" : string
- size it;
val it = 29 : int

Reelle Zahlen

- 3.14
= ;
val it = 3.14 : real
- 3.14;
val it = 3.14 : real
- 3E2;
val it = 300.0 : real
- 3.14E3;
val it = 3140.0 : real

• vordefinierte Funktionen +, -, , *, /, sin, sqrt, exp, usw.

• vordefinierte Relationen <, <=, >, >=, =, <>,

• keine implizite Anpassung zwischen int und real; keine gemischten Operandentypen in binären Funktionen und Relationen; explizite Anpassung durch real bzw.

     floor.

Tupel

- (true, ());
val it = (true,()) : bool * unit
- (1,false,"WS94/95",(true,12));
val it = (1,false,"WS94/95",(true,12)) : int * bool * string * (bool * int)
- (14 mod 3, not false) = (1+1, not (not true));
val it = true : bool
- (true, 7) = (true, 8);
val it = false : bool
- (true, 7) = (true, ());
std_in:0.0-0.0 Error: operator and operand don't agree (tycon mismatch)
  operator domain: (bool * int) * (bool * int)

  operand:         (bool * int) * (bool * unit)
  in expression:
    = ((true,7),(true,()))

• geordnete Tupel beliebiger Länge n ≥ 2

• Gleichheit komponentenweise

• Typausdrücke von der Form τ_{1} ∗ τ_{2} ∗ … ∗ τ_{n}

Listen

- nil;
val it = [] : 'a list
- 3 :: 4 :: nil;
val it = [3,4] : int list
- [3,4];
val it = [3,4] : int list
- (3 :: nil) :: (3 :: 4 :: nil) :: nil;
val it = [[3],[3,4]] : int list list
- ["Das", "ist", "eine", "Liste"];
val it = ["Das","ist","eine","Liste"] : string list

Listen werden konstruiert über nil (leere Liste) und :: (ausgesprochen ”cons“), womit ein neues Element an eine bestehende Liste vorne angehängt wird. Man spricht von einem rekursiven Datentyp.

Listen mit Elementen e_{1}, …, e_{n}, n ≥ 0, haben die Form e_{1} :: ... :: e_{n} :: nil, wofür auch [e_{1} :: ... :: e_{n}] geschrieben werden darf.

Die Elemente einer Liste müssen alle vom selben Typ τ sein, in welchem Fall dann τ list der Typ der Liste ist.

Der Typ von nil enthält die Typvariable 'a, da nil Element eines jeden Listentyps ist. nil ist ein polymorphes Objekt, welches aber nur in Listentypen enthalten ist. Ein Typ, der eine Typvariable enthält, heißt ein polymorpher Typ. Instanzen eines polymophen Typs erhält man, indem man Typvariablen durch Typen substituiert. Monomorphe Typen (Monotypen) sind Typen, die keine Typvariablen enthalten.

Man beachte den Unterschied zwischen (parametrischem) Polymorphismus und Überladung von Bezeichnern, auch ad hoc Polymorphismus genannt, wie er z.B. bei + oder >= auftritt.

Verbunde Verbundtypen sind ähnlich then ”Pascal records“ und ”C structures“.

- {Name="Ganzinger", Alter=44};
val it = {Alter=44,Name="Ganzinger"} : {Alter:int, Name:string}
- {a=1,b=2} = {b=1+1, a=1};
val it = true : bool
- {a=1,b=2} = {b=1+1, c=1};
std_in:30.1-30.24 Error: operator and operand don't agree (tycon mismatch)
  operator domain: {a:int, b:int} * {a:int, b:int}
  operand:         {a:int, b:int} * {b:int, c:int}

  in expression:
    = ({a=1,b=2},{b=+ : overloaded (1,1),c=1})

Verbundtypen sind endliche Mengen von benamten Feldern der Form {l_{1}=v_{1},…,l_{n}=v_{n}}, n ≥ 1.^{2}. Namen müssen eindeutig sein. Die zugehörigen Typausdrücke haben die Form {l_{1}:τ_{1},…,l_{n}:τ_{n}}, wenn τ_{i} der Typ von v_{i} ist. Die Namen der Felder zählen also zur Typinformation. Die Reihenfolge der Felder ist irrelevant.

Tupeltypen τ_{1} ∗ τ_{2} ∗ … τ_{n} sind Kurzschreibweisen für Verbundtypen der Form {1:τ_{1},…,n:τ_{n}}. D.h. die Ausdrücke (2,true) und {1=2,2=true} haben dieselbe Bedeutung. Als Feldnamen sind also Identifikatoren und ganze Zahlen zugelassen.

Bemerkungen Man beachte die Uniformität der Art und Weise, wie in ML Werte der verschiedenen Typen mit Konstruktoren aus Konstanten gebildet werden. Jeder Wert ist also ein Term, an dessen Blättern Konstante atomarer Typen (Zahlen) oder (nullstellige) Konstruktoren (z.B. nil, true) stehen und an deren inneren Knoten (mehrstellige) Konstruktoren (z.B. ::, ( , ), {name= , alter= }) angewendet sind. Obwohl Konstruktoren Daten in eindeutiger Weise konstruieren, sind sie aber keine Funktionen im technischen Sinne von ML.

3.2.3 Funktionsdefinitionen

Funktionsdefinitionen sind spezielle Formen von bindungserzeugenden Konstrukten, die wir in ihrer ganzen Schönheit noch später kennenlernen werden.

Funktionen werden verwendet, indem sie auf Argumente angewendet werden. Funktionen in ML sind allesamt einstellig. Mehrstellige Funktionen können entweder durch tupelwertige Argumente oder durch Funktionen höherer Ordnung realisiert werden. Applikationen haben die Form e1 e2. Eine Applikation ist typmäßig korrekt, wenn e1 einen Typ von der Form σ → τ und e2 dann den Typ σ hat. Ergebnis der Anwendung ist in diesem Fall ein Wert vom Typ τ. Diese Typbedingung garantiert, daß e1 bei seiner Auswertung^{3} eine Funktion liefern wird, die Argumente vom Typ von e2 akzeptiert. σ bzw. τ heißen die Typen des Definitions- bzw. Wertebereichs der Funktion.

- size;
val it = fn : string -> int
- not;
val it = fn : bool -> bool
- not 3 ;
std_in:4.1-4.5 Error: operator and operand don't agree (tycon mismatch)
  operator domain: bool
  operand:         int
  in expression:
    not 3
- size "abc";
val it = 3 : int

2Der leere Verbund {} ist eine andere Notation für () und hat den Typ unit

3Terminierung wird bei Aussagen dieser Form immer unterstellt. Natürlich kann kein statisches Typkonzept Terminierung garantieren.

Es folgen einfache Beispiele für Funktionsdefinitionen.

- fun twice x = 2*x;
val twice = fn : int -> int
- twice 4;
val it = 8 : int
- fun fact x = if x=0 then 1 else x*fact(x-1);
val fact = fn : int -> int
- fact 5;
val it = 120 : int
- fun plus(x,y) = x+y;
std_in:10.18 Error: overloaded variable cannot be resolved: +
- fun plus(x,y):int = x+y;
val plus = fn : int * int -> int
- plus (3,6);
val it = 9 : int

Folgendes sind die Bestandteile solcher Definitionen:

• Name der zu definierenden Funktion, z.B. plus,

• Parametermuster, z.B. (x,y),

• optionale Ergebnistypbeschränkung, z.B. :int, die vornehmlich zur Auflösung von Typmehrdeutigkeiten, die aus Überladung entstehen, verwendet werden,

• Ausdruck, der das Funktionsergebnis zum jeweiligen Parametermuster spezifiziert, z.B. x+y.

Die Parametermuster liefern Bindungen an die in ihnen enthaltenen Variablen, wenn das Muster auf den jeweiligen aktuellen Parameterwert gelegt wird. Wesentlich ist, daß mehr als eine Regel (oder Klausel) der Form

        <Funktionsname> <Muster> = <Ergebnisausdruck>

angegeben werden darf. Im allgemeinen sind es soviele, daß die Vereinigung der Muster alle möglichen Parameterwerte überdeckt. Die Klauseln werden durch | getrennt. Paßt mehr als eine Regel, wird die erste passende verwendet. Dafür jetzt ein Beispiel.^{4}

- fun isNil   nil  = true
=   | isNil (_::_) = false;
val isNil = fn : 'a list -> bool
- isNil nil;
val it = true : bool
- isNil [2,3];
val it = false : bool
- isNil ["aa","ab"];
val it = false : bool
- fun append (nil,l) = l

4Die =-Zeichen am Anfang von (Folge-)Zeilen ist Ausgabe des Interpreters wenn Eingaben über eine Zeile hinausgehen, nicht Eingabesyntax!

=   | append (hd::tl,l) = hd :: append(tl,l);
val append = fn : 'a list * 'a list -> 'a list
- append([],[1,2,3]);
val it = [1,2,3] : int list
- append(["auch", "eine"],["Liste"]);
val it = ["auch","eine","Liste"] : string list

Bemerkungen:

• Beide Funktionen sind polymorph. Man bemerke aber bei append, daß diese Funktion zwar Listen von beliebigem Elementyp akzeptiert, daß aber die Elementtypen beider Argumentlisten gleich sein müssen (Typ αlist ∗ αlist → αlist). Der ML-Übersetzer findet den allgemeinsten Typ selbst heraus.

• append is rekursiv. Auf der rechten Seite der Regeln sind also alle links eingeführten Bindungen, einschließlich der zu definierenden Funktion, sichtbar.

• Ist eine Teilstruktur eines Wertes irrelevant beim Mustertest, so verwendet man den Joker , siehe zweite Regel für isNil.

• Die Verwendung von Mustern und Mustertest ist die einzige Möglichkeit, um auf Komponenten von Konstruktortermen zuzugreifen. Es gibt in ML keine expliziten Destruktoren.

Bevor wir zu interessanteren Beispielen kommen, wollen wir in Abschnitt 3.2.4 allgemeiner auf Identifikatoren, Bindungen und Deklarationen sowie Muster und Mustertest eingehen.

Abschließend sei noch angemerkt, daß Funktionen in SML nicht notwendig einen Namen haben müssen. Sogennante λ-Ausdrücke der Form

    fn <Muster> => <Ausdruck>

definieren namenlose Funktionen, die Argumentmuster Muster auf Ergebnisse Ausdruck abbilden. Diese kann man direkt in Applikationen verwenden oder in Deklarationsausdrücken. Dann sind auch Funktionsdefinitionen spezielle Form von Wertedefinitionen.

fn x => x;
- val it = fn : 'a -> 'a
- it(1);
val it = 1 : int
- val id = fn x => x;
val id = fn : 'a -> 'a
- val plus = fn (x,y):int*int => x+y;
val plus = fn : int * int -> int
- plus(1,3);
val it = 4 : int

3.2.4 Deklarationen

Alle Identifikatoren müssen vor ihrer Verwendung deklariert werden. Bei ihrer Deklaration werden sie zu einem Wert gebunden. Wesentlich ist, daß im Gültigkeitsbereich einer Deklaration dieser Wert fest ist und nicht,, wie etwa in imperativen Sprachen, durch eine Wertzuweisung verändert werden kann. Die ML-Variablen sind also eher vergleichbar den Konstanten (vgl. const-Deklarationen in Pascal) imperativer Sprachen.

- val x = 4*5;
val x = 20 : int
- val s = "abc"^"def";
val s = "abcdef" : string
- val p = ( x, s );
val p = (20,"abcdef") : int * string

Phrasen der Form

        val <Identifikator> = <Ausdruck>

heißen Wertedefinitionen. Ihr Effekt ist die Bindung des Identifikators an den Wert der rechten Seite.

Die Redefinition eines Identifikators verdeckt die bereits bestehende Bindung in demselben Sinne, wie in einer inneren Prozedurdefinition in Pascal durch Redeklaration eine äußere Bindung verdeckt wird. Was der Unterschied zwischen einer Redefinition und einer Pascal-Wertzuweisung ist, werden wir später noch sehen,

- val x = 17;
val x = 17 : int
- val y = x;
val y = 17 : int
- val x = true;
val x = true : bool
- val z = x;
val z = true : bool
- val x = 17;
val x = 17 : int
- val x = true and y = x;
val x = true : bool
val y = 17 : int

Folgene Regeln und Terminologie definieren die Semantik dieser Konstrukte:

• Deklarationen erzeugen Bindungen und Mengen von Bindungen bilden eine Umgebung. Es gibt verschiedene Arten von Deklarationen, z.B. für Werte val oder Funktionen fun; später sehen wir noch andere Arten.

• Die Auswertung eines jeden Ausdrucks erfolgt in einer bestimmten Umgebung, die dann die Werte für die Variablen des Ausdrucks festlegt.

• Die rechte Seite einer Wertdeklaration wird in der alten, bisherigen Umgebung ausgewertet (der Wert des letzten y ist 17 und nicht true). Bei Funktionsdefinitionen

            fun f m_{1} = e_{1} | ...  | f m_{n} = e_{n}

ist dies anders. Hier können die Definitionen rekursiv sein und die neuen Bindungen für f und für die Variablen in den Mustern m_{i} sind bereits in e_{i} sichtbar. Letztere sind nur lokal in den e_{i} sichtbar.

• Deklarationen können durch bestimmte Kombinatoren zusammengesetzt werden. So bedeutet d1 ; d2 die sequentielle Komposition^{5} von Deklarationen d1 und d2. d1 wird in der gegebenen Umgebung E ausgewertet. Der Effekt ist, daß die neuen Bindungen gemäß d1 zu E hinzugefügt werden und alte Bindungen in E für redefinierte Identifikatoren verdeckt werden. In dieser neuen Umgebung erfolgt die Auswertung von d2, die dann in gleicher Weise die Umgebung modifiziert. Auf Interpreter-Eingabeebene sind also nacheinanderfolgende, durch ”;“ getrennte Deklarationen als in diesem Sinn sequentiell zusammengesetzt zu betrachten.

• and trennt parallele Deklarationen von mehreren verschiedenen Identifikatoren. Die Definitionsrümpfe werden alle in der alten Umgebung ausgewertet.

Der Gültigkeitsbereich von Deklarationen kann lokal beschränkt werden.

- local val x = 10
= in
=       val u = x*x + x*x
=       val v = 2*x + (x div 5)
= end;
val u = 200 : int
val v = 22 : int

local erzeugt lokale Deklarationen für eine (zusammengesetzte) Deklaration zwischen

in und end.
- let val x = 10
= in
=     x*x + 2*x +1
= end;
val it = 121 : int

let erzeugt lokale Deklarationen für die Auswertung eines Ausdrucks zwischen in und

end.

3.2.5 Muster

Wir haben schon bei den Funktionsdefinitionen gesehen, daß die Verwendung von Mustern die einzige Möglichkeit ist, um auf Substrukturen von Konstruktortermen zuzugreifen. Muster sind Konstruktorterme, die Variablen enthalten. Es ist nur natürlich, Muster auch in Wertdeklarationen zuzulassen. D.h. Wertdeklarationen haben die allgemeinere Form

        val <Muster> = <Ausdruck>,

bei der der Asudruck in der gegebenen Umgebung ausgewertet wird, das Muster des entstehenden Wertes gestestet wird und im Erfolgsfall die Variablen des Musters an die entsprechenden Subterme gebunden werden.

5Das Semikolon ist optional. Man kann auch einfach d1 und d2 hintereinanderschreiben.

- val x = (17,true);
val x = (17,true) : int * bool
- val (left,right) = x;
val left = 17 : int
val right = true : bool
- val (left,false) = x;
std_in:48.1-48.20 Warning: binding not exhaustive
          (left,false) = ...
uncaught Bind exception std_in:48.1-48.20

• Warnung, wenn Muster nicht alle Möglichkeiten (diese sind nach der Typinferenz bekannt) abdeckt;

• Ausnahmebehandlung wird angestoßen, wenn Muster nicht paßt.

• Alle Muster müssen linear sein, d.h. Mehrfachvorkommen von Variablen sind nicht erlaubt.

Weitere Beispiele:

- val l = [1,2,3];
val l = [1,2,3] : int list
- val [x,y,z] = l;
std_in:49.1-49.15 Warning: binding not exhaustive
          x :: y :: z :: nil = ...
val x = 1 : int
val y = 2 : int
val z = 3 : int
- val r = {name="hugo", used = true};
val r = {name="hugo",used=true} : {name:string, used:bool}
- val {used=u, name=n} = r;
val n = "hugo" : string
val u = true : bool
- val {used=u, ...}=r;
val u = true : bool
- val u = #used r;
val u = true : bool
- fun uu {used = u, ...} = u;
std_in:55.1-55.26 Error: unresolved flex record in let pattern
  type: {used:'Y, '...Z}

• ... ist der Joker, der auf eine beliebige Anzahl von Verbundfeldern paßt.

• Bei Verbundtypen müssen alle Felder und deren Typen aus dem Kontext hervorgehen, eventuell müssen Typeinschränkungen verwendet werden. Den Polymorphismus, der in der objektorientierten Programmierung durch Verbunderweiterung erfolgt (Vererbung von Instanzvariablen), hat man in SML leider nicht. In einer ML-Variante von Cardelli gab es ihn einmal.

• #name r ist eine abkürzende Schreibweise für den Zugriff auf das Feld name eines Verbundes r.

Muster brauchen nicht flach zu sein, sondern können beliebig geschachtelte Terme sein.

- val l = [(1,["H","G"]),(2,["U","W"])];
val l = [(1,["H","G"]),(2,["U","W"])] : (int * string list) list
- val _::(key,_::second)::tl = l;
val key = 2 : int
val second = ["W"] : string list
val tl = [] : (int * string list) list

3.3 Grundbegriffe der Termersetzung

Unter einem Baum oder auch Termstruktur verstehen wir hier eine präfixabgeschlosse, endliche Teilmenge B von N^{∗}. D.h., ist n_{1}.n_{2}. . . . .n_{k} in B mit k ≥ 1, so ist auch n_{1}.n_{2}. . . . .n_{k−1} in B sowie alle n_{1}.n_{2}. . . . .n_{k−1}.j mit j < n_{k}. Ein Term t über F, wobei F eine Menge von Funktionssymbolen, ist eine Abbildung t : B → F, wobei B ein Baum. Die Knoten in B nennen wir auch die Positionen in t. Wir sagen, daß f an Position p in t vorkommt, wenn t(p) = f gilt. Ist p eine Position in t, so bezeichnet t/p den Subterm von t an p, d.h. den Term t′ mit der Struktur bestehend aus den Positionen q in N^{∗}, für die p.q eine Position in t ist, mit der Markierung t′(q) = t(p.q). Sind s und t Terme und ist p eine Position in t, so bezeichne t[s]_{p} den Baum, der durch Ersetzung des Subterms an p in t durch s entsteht. Als lineare Notation für Terme verwenden wir die Präfixnotation, d.h. schreiben f(t_{1}, …, t_{n}) für einen Term, bei dem f an der Wurzel ϵ vorkommt, und der die Subterme t_{1}, …, t_{m} (an ϵ) besitzt. Oft verwenden wir auch Infix oder Postfixnotation für Funktionssymbole, für die dies die übliche Schreibweise darstellt. Wir schreiben also beispielsweise a + b für den Term +(a, b).

Terme, in denen nur Funktionssymbole vorkommen, heißen auch Grundterme oder variablenfreie Terme. Zusätzlich zu diesen betrachten wir auch Terme mit (getypten) Variablen. Sei also X eine Menge von getypten Variablen der Form x : τ, die disjunkt zu F ist. Dann ist ein Term über X und F einfach ein Tern über X ∪ F, in dem Variablen nur an Blattpositionen vorkommen dürfen.

Wohlgetypte Terme ergeben sich aus folgendem Typinferenzsystem:

\overline{x : τ}  falls x : τ in X

\frac{t_{1} : τ_{1} … t_{n} : τ_{n}}{f(t_{1}, …, t_{n}) : τ_{0}} falls f : τ_{1} ∗ … ∗ τ_{n} → τ_{0} in F, n ≥ 0

Ein Term t heißt daher wohlgetypt, wenn t : τ für einen Typ τ in obigem Inferenzsystem ableitbar ist. In diesem Fall heißt τ ein Typ von t. Im Kontext von Typpolymorphismus braucht es zur Typinferenz weitere Regeln, auf die wir später noch zurückkommen werden.

Nachfolgend bezeichnte T_{F,X} bzw. T_{F} die Menge der Terme mit bzw. ohne Variablen über F und X. Eine Substitution ist eine Abbildung σ : X → T_{F,X}. Die Anwendung einer Substitution σ auf einen Term t, bezeichnet mit σ(t) oder mit tσ, liefert den Term t[s_{1}]_{p_{1}}[s_{2}]_{p_{2}} … [s_{k}]_{p_{k}}, wenn die p_{i} genau die Variablenpositionen in t sind, und wenn t(p_{i}) = X_{i} mit σ(X_{i}) = s_{i} gilt. Die Anwendung ersetzt also alle Auftreten von Variablen durch die gemäß σ zugeordneten Terme.

Substitutionen sind Grundlage für die Formalisierung von Mustertest auf Termen und von Termersetzung. Sind s und t Terme und ist p eine Position in t, so sagen wir, daß das Muster s auf t an p paßt, wenn es eine Anpaßsubstitution σ gibt, so daß t/p = sσ. Paßt s, so ist die Anpaßsubstitution auf den Variablen in t/p eindeutig festgelegt.

Eine Termersetzungsregel ist ein Paar von Termen l und r, geschrieben l → r. Die Regel paßt auf t an p, wenn ihre linke Seite l auf t an p paßt. Ist σ die zugehörige Anpaßsubstitution, so nennen wir t′ = t[rσ]_{p} das Resultat der Anwendung der Regel. In diesem Fall schreiben wir auch t →_{p,l→r,σ} t′. Wir sprechen auch von der Reduktion von t zu t′, und t/p heißt der Redex dieses Redunktionsschrittes. Wir lassen den Subskript weg, wenn die jeweiligen Größen irrelevant oder aus dem Kontext bekannt sind. Ein Termersetzungssystem R ist eine Menge von Termersetzungsregeln. Wir schreiben t →_{R} t′, wenn t′ aus t durch Anwendung einer Regel aus R auf t entsteht. Mit →_{R}^{+} bzw. →_{R}^{∗} bezeichnen wir die transitive bzw. transitive und reflexive Hülle dieser durch R definierten Ersetzungsrelation →_{R}. Wir sagen, daß ein Term irreduzibel ist bzgl. R, wenn für keinen Term t′ →_{R} t′ gilt. t′ heißt eine Normalform von t bzgl. R, wenn t →_{R}^{∗} t′ und wenn t′ irredizibel ist.

3.4 Funktionsauswertung als Termersetzung

Wir betrachten die Funktion

fun append(nil,l) = l
   | append(hd::tl,l) = hd :: append(tl,l)

von oben. Wir können sie uns als zwei Termersetzungsregeln

append(nil,l)    -> l
append(hd::tl,l) -> hd :: append(tl,l)

vorstellen. In F haben wir hierbei alle Konstanten von den Typen int, real, string, und bool, die Konstruktoren für Listen und Verbunde, alle vordefinierten Funktionen sowie append Variablen sind l, hd und tl. Folgende Reduktionsfolge ist beispielsweise möglich:

   append(1::nil,2::3::nil)
-> 1::append(nil,2::3::nil)
-> 1::2::3::nil

Im ersten Schritt wurde die erste Regel, im zweiten schritt die zweite Regel angewendet, und zwar jeweils an der Wurzel des Terms. Folgendes Beispiel ist etwas komplizierter, indem die definierte Funktion append mehrfach vorkommt.

   append(1::nil,append(2::nil,2::3::nil))
-> append(1::nil,2::append(nil,2::3::nil))
-> append(1::nil,2::2::3::nil)
-> 1::append(nil,2::2::3::nil)
-> 1::2::2::3::nil

Im Prinzip wäre auch folgende Reduktionsfolge möglich gewesen:

   append(1::nil,append(2::nil,2::3::nil))
-> 1::append(nil,append(2::nil,2::3::nil))
-> 1::append(nil,2::append(nil,2::3::nil))
-> 1::append(nil,2::2::3::nil)
-> 1::2::2::3::nil

Wir sehen, daß das Ergebnis das Gleiche ist, unabhängig von der Reduktionsstrategie. In SML ist die zweite Reduktionsfolge nicht erlaubt. SML-Reduktion erfolgt nach der Strategie “innerste Redexe zuerst“. Der erste Schritt in der zweiten Reduktionsfolge wäre daher in SML nicht erlaubt, da es ein weiter innen liegendes Auftreten von append gibt, welches ebenfalls reduzierbar ist. Die Argumente einer Funktion müssen daher zuerst zu Konstruktortermen normalisiert werden, bevor irgendeine Regel der jeweiligen Funktionsdefinition angewendet wird. Unter einem Konstuktorterm verstehen wir einen Term, in dem nur Konstruktoren (die Konstanten der Typen int, real, string, und bool sowie die Konstruktoren für Verbunde und Listen) vorkommen dürfen. Wir werden später sehen, daß der ML-Programmierer weitere Konstruktoren deklarieren darf, also nicht notwendig alle rekursiven, strukturierten Daten als Listen kodieren muß.

Halten wir fest: Das Ergebnis value(e) der Auswertung eines SML-Ausdrucks e ist die Normalform, die sich durch Reduktion von e mit der Strategie “innerste Redexe zuerst“ ergibt. Gibt es keine Normalform weil die Reduktion nicht terminiert, so ist die Auswertung undefiniert. Konsequenz dieser Reduktionsstrategie ist die Striktheit aller benutzerdefinierten Funktionen f. Es gilt

value(f(e_{1}, …, e_{n})) = value(f(value(e_{1}), …, value(e_{n})))  (1)

und als Konsequenz ist value(f(e_{1}, …, e_{n})) undefiniert, sofern eines der value(e_{i}) undefiniert ist. Ausdrücke mit funktionalem Typ, if-Ausdrücke, usw. sind speziellen Reduktionsstrategien unterworfen. Erstere werden nicht reduziert. Bei letzteren wird erst die Bedingung reduziert und dann, je nach Ergebnis, der then- oder der else-Ausdruck. Es gilt daher

value(if true then e_{1} else e_{2}) = value(e_{1})  (2)
value(if false then e_{1} else e_{2}) = value(e_{2})  (3)

Es bleibt noch anzumerken, daß die SML-Semantik garantiert, daß Normalformen, sofern sie existieren, immer eindeutig bestimmt sind, die Reduktionsrelation ist konfluent. Dazu gehört, daß die Regeln geordnet sind, so daß, wenn mehr als eine regel anwendbar ist, immer die erste anwendbare Regel verwendet wird. Aus diesem Grunde gilt, wenn l → r eine Regel ist,

value(t[lσ]_{p}) = value(t[rσ]_{p})  (4)

für jeden Term und jede Position p in t, die nach der vorgenannten Reduktionsstrategie mit Regel l → r unter Substitution σ reduziert werden darf.

3.5 Typdefinitionen

Typabkürzungen. Hier werden neue Namen als Abkürzungen für komplexe, evtl. parametrisierte Typausdrücke eingeführt. Hier gibt es keinen speziellen semantischen Gehalt. Diese Typen werden auch transparente Typen genannt. Alle Auftreten des neuen Typnamens sind äquivalent zu seinem definierenden Ausdruck.

- type intpair = int * int;
type  intpair = int * int
- fun f(x:intpair) = let val (l,r)=x in l end;
val f = fn : intpair -> int
- f(3,2);
val it = 3 : int
- type 'a pair = 'a * 'a;
type  'a pair = 'a * 'a
- type boolpair = bool pair;
type  boolpair = bool pair

Neue Datentypen. In Datentypdeklarationen können neue (rekursive, polymorphe) Typen von Konstruktortermen definiert werden. Folgende Definitionen führen 3 nullstellige Konstruktoren für einen neuen Typ color ein bzw. zeigen, wie man den vordefinierten Typ bool selbst definieren könnte.

- datatype color = red | green | blue;
datatype  color
  con blue : color
  con green : color
  con red : color
- red;
val it = red : color
- datatype bool = true | false;
datatype  bool
  con false : bool
  con true : bool
val like = fn : color -> bool
- fun like red = true
=   | like green = false
=   | like blue = true;
val like = fn : color -> bool
- like blue;
val it = true : bool

Wir sehen, daß Typdefinitionen dieser Art den Aufzählungstypen von Pascal entsprechen. Konstruktoren müssen nicht nullstellig sein:

type  rbg_color = color
- datatype cmy_color = cyan | magenta | yellow;
datatype  cmy_color
  con cyan : cmy_color
  con magenta : cmy_color
  con yellow : cmy_color
- datatype color = rbg of rbg_color | cmy of cmy_color;
datatype  color
  con cmy : cmy_color -> color
  con rbg : rbg_color -> color

Hier ist rbg ein Konstruktor vom Typ rbg color -> color und cmy ein Konstruktor vom Typ cmy color -> color. Zusammen bilden sie alle Möglichkeiten, Terme vom (redefinierten) Typ color zu konstrieren.

Wir kommen nun zu rekursiven Typen und definieren als erstes (unmarkierte) Binärbäume.

- datatype btree = empty | leaf | node of btree * btree;
datatype  btree
  con empty : btree
  con leaf : btree
  con node : btree * btree -> btree
- fun countleaves(empty) = 0
    | countleaves( leaf) = 1
    | countleaves(node(subtree1,subtree2)) =
                 countleaves(subtree1)+countleaves(subtree2);
val countleaves = fn : btree -> int
- countleaves(node(node(leaf,leaf),leaf));
val it = 3 : int

Es ist nur natürlich, daß Funktionen auf rekursiven Datentypen selbst rekursiv sind und daß die Rekursionen oft parallel verlaufen. Mathematisch steht hier das Prinzip der strukturellen Induktion im Raum, welches wir im Abschnitt 3.6 rekapitulieren wollen.

Als nächstes Beispiel zeigen wir, wie wir die Listen selbst definieren können.

- datatype 'a list = nil | :: of 'a * 'a list;
datatype  'a list
  con :: : 'a * 'a list -> 'a list
  con nil : 'a list

Da es sich hier um einen polymorphen Typ handelt, müssen wir den Parameter auf der linken Seite der Typdeklaration ebenfalls angeben. list ist also ein Typkonstruktor, der aus Argumenttypen α Listen typen αlist konstruiert. Hier eine Variation der Binärbäume so, daß sie an Blättern Information tragen.

- datatype 'a tree = empty | leaf of 'a | node of 'a tree * 'a tree;
datatype  'a tree
  con empty : 'a tree
  con leaf : 'a -> 'a tree
  con node : 'a tree * 'a tree -> 'a tree
- fun frontier empty = []
    | frontier (leaf(x)) = [x]
    | frontier (node(t1,t2)) = append (frontier(t1),frontier(t2));
val frontier = fn : 'a tree -> 'a list
- frontier(node(leaf("a"),node(node(leaf("b"),empty),leaf("a"))));
val it = "a" :: "b" :: "a" :: nil : string list

Abstrakte Datentypen Abstrakte Datentypen verstecken die Implementierungsstruktur von Daten. Hierdurch werden Impementierungsaspekte unabhängig von der Verwendung des Typs. Insbesondere kann die Implementierung geändert werden, ohne daß Anwendungen reimplementiert werden müssen, solange die exportierten Funktionen des Typs, genannt die Schnittstelle, sich in ihren beobachtbaren Eigenschaften nicht ändern. Wir machen ein Beispiel, in dem 4-Bit RGB-Farben definiert werden.

abstype color = blend of int*int*int
with val white = blend(0,0,0)
      and   red = blend(15,0,0)
      and green = blend(0,15,0)
      and  blue = blend(0,0,15)
      fun mix(parts:int,blend(r,g,b),parts':int,blend(r',g',b')) =
      if parts<0 orelse parts'<0 then white
      else let val tp=parts+parts'
               val rp = ((parts*r+parts'*r') div tp) mod 16
               and gp = ((parts*g+parts'*g') div tp) mod 16
               and bp = ((parts*b+parts'*b') div tp) mod 16
            in blend(rp,gp,bp)
           end
end;
type color
val white = - : color
val red = - : color
val green = - : color
val blue = - : color
val mix = fn : int * color * int * color -> color
- val black = mix(1,red,1,mix(1,green,1,blue));
val black = - : color

Man beachte:

• Die Typgleichung hinter ”abstype“ hat dieselbe Syntax, wie die, die wir vorher kennengelernt haben. Also können hier auch neue Typkonstruktoren eingeführt werden.

• Die nach außen sichtbare Schnittstelle des abstrakten Datentyps besteht aus dem Namen des Typs und den Namen der zwischen with und end eingeführten Werte und Funktionen.

• Die Implementierung der Schnittstellenobjekte bleibt verborgen. Technisch bedeutet das insbesondere, daß der Typ verschieden ist von allen anderen Typen und daß seine Konstruktoren außen nicht sichtbar sind. Daher kann man insbesondere keine musterorientierten Funktionen auf einem abstrakten Type schreiben. Zudem ist die Gleichheit = nicht definiert für Werte eines abstrakten Datentyps. Soll es eine Gleichheitsfunktion geben, so muß man die implementieren und in der Schnittstelle zur Verfügung stellen.

• Innerhalb der Definition Abstrakten Datentyps sind die Konstruktoren natürlich sichtbar und können zu musterorientierten Definitionen verwendet werden.

Diese Art von abstrakten Datentypen in SML ist historisch bedingt und sollte angesichts der erweiterten Möglichkeiten von Abstraktion mit Hilfe der Konzepte von Strukturen und Funktoren eigentlich nicht mehr verwendet werden.

3.6 Strukturelle Induktion

Gegeben sei eine Menge von Funktionssymbolen F. Strukturelle Induktion erlaubt, Eigenschaften aller Terme in T_{F} zu beweisen, indem folgende Schlußregel verwendet wird.

Theorem 1 (Prinzip der strukturellen Induktion) Sei P (x) eine Eigenschaft über Termen x in T_{F}. Wenn man für alle Funktionssymbole f in F die Implikation

∀t_{1}, …, t_{n} : T_{F} . P (t_{1}) ∧ … ∧ P (t_{n}) ⊃ P (f(t_{1}, …, t_{n}))

zeigen kann, so gilt P (t) für alle t in T_{F}.

Wir geben ein Beispiel für seine Anwendung, welches die zentrale Bedeutung dieses Prinzips zur Verifikation funktionaler Programme zeigt. Betrachte folgende Funktion, die Binärbäume rekursiv spiegelt.

- fun swap empty = empty
=   | swap leaf = leaf
=   | swap(node(t1,t2))  = node(swap(t2),swap(t1));
val swap = fn : btree -> btree
- countleaves(swap(node(node(leaf,leaf),leaf)));
val it = 3 : int

Wir beweisen, daß für alle Konstruktorterme t vom Typ btree

            value(countleaves(swap(t))) = value(countleaves(t)).

In diesem Fall besteht also unser f aus den Funktionen empty, leaf und node. Wir haben also drei Fälle zu untersuchen:

(i) f = empty : Hier ist das n aus dem Induktionsprinzip 0 und es bleibt zu zeigen, daß

        value(countleaves(swap(empty))) = value(countleaves(empty)).

welches sich direkt durch Reduktion von swap(empty) zu empty mit der ersten Regel von swap ergibt.

(ii) f = leaf: Hier ist n ebenfalls 0 und es gilt

         value(countleaves(swap(leaf))) = value(countleaves(leaf)).

durch Reduktion von swap(leaf) zu leaf mit der zweiten Regel von swap.

(iii) f = node : btree * btree -> btree: Hier ist n = 2. Wir nehmen an, um die Implikation zu zeigen, daß

            value(countleaves(swap(t_{i}))) = value(countleaves(t_{i})).

für beliebige t_{i}, i = 1, 2. (Diese Annahme nennt man die Induktionsannahme.) Nun berechnen wir (wobei wir value zu v abkürzen)

 v(countleaves(swap(node(t_{1}, t_{2}))))

= v(countleaves(node(swap(t_{2}), swap(t_{2}))))  (Regel 3 von swap)

 = v(countleaves(swap(t_{2})) + countleaves(swap(t_{1})))  (Regel 3 countleaves)

= v(v(countleaves(swap(t_{2}))) + v(countleaves(swap(t_{1}))))  (Striktheit von +)
= v(v(countleaves(t_{2})) + v(countleaves(swap(t_{1}))))  (Ind.-Annahme für t_{2})
= v(v(countleaves(t_{2})) + v(countleaves(t_{1})))  (Ind.-Annahme für t_{1})
= v(v(countleaves(t_{1})) + v(countleaves(t_{2})))  (+ ist kommutativ)
= v(countleaves(t_{1}) + countleaves(t_{2}))  (+ ist strikt)

 = v(countleaves(node(t_{1}, t_{2})))  (Regel 3 countleaves)

und erhalten die Gleichung, die zu zeigen war. Bzgl. der Striktheit von Funktionen vgl. Gleichung (1). Die Anwendungen der Regeln aus den Funktionsdefinitionen nach Gleichung (4) sind allesamt zulässig. Die t_{i} sind Konstruktorterme, so daß die jeweiligen Positionen mit den genannten Regeln reduzierbar sind.