A non-deterministic call-by-need lambda calculus [Elektronische Ressource] : proving similarity a precongruence by an extension of Howe's method to sharing / von Matthias Mann

Sujets

• Informatik
• Mathematics

Informations

• Publié par: goethe_universitat_frankfurt_am_main
• Publié le: 01 janvier 2006
• Nombre de lectures: 17
• Langue: Deutsch
• Poids de l'ouvrage: 1 Mo

Extrait

A Non-Deterministic Call-by-Need Lambda Calculus:
Proving Similarity a Precongruence by an Extension of
Howe’s Method to Sharing
Dissertation
zur Erlangung des Doktorgrades
der Naturwissenschaften
vorgelegt beim Fachbereich 15
der Johann Wolfgang Goethe{Universitat
in Frankfurt am Main
von
Matthias Mann
aus Frankfurt
Frankfurt 2005
(D F 1)vom Fachbereich Informatik und Mathematik der Johann Wolfgang Goethe{
Universitat als Dissertation angenommen.
Dekan: Prof. Dr.-Ing. Detlef Kromk er
Gutachter: Prof. Dr. Manfred Schmidt-Schau
Johann Wolfgang Goethe-Universitat
Fachbereich Informatik und Mathematik
Robert-Mayer-Str. 11-15
60325 Frankfurt
Prof. David Sands, Ph.D.
Chalmers University of Technology and University of Goteborg
Department of Computing Science
S-412 96 Goteb org
Sweden
Datum der Disputation: 17. August 2005Zusammenfassung
Gegenstand der vorliegenden Arbeit ist ein nicht-deterministischer Lambda-
Kalkul mit call-by-need Auswertung. Lambda-Kalkule spielen im allgemeinen
eine grundlegende Rolle in der theoretischen Informatik, sei es als Basis fur
Theorembeweiser im Bereich der Veri k ation oder beim Entwurf sowie der se-
mantischen Analyse von Programmiersprachen, insbesondere funktionalen.
Im Zuge der weiter zunehmenden Komplexitat von Hard- und Softwaresyste-
men werden funktionalehen eine immer gro ere Bedeutung
erlangen. Der Grund liegt darin, da in der Softwareentwicklung stets eine ge-
wisse Diskrepanz entsteht zwischen dem Konzept, welches ein Programmierer
entwirft, und der Art und Weise, wie er es in einer bestimmten Programmier-
sprache umzusetzen hat.
Um robuste und verla lic he Software zu gewahrleisten, sollte es eines der
Hauptanliegen der Informatik sein, diese Diskrepanz so klein wie moglich zu
halten. Im Vergleich zu imperativen oder objekt-orientierten ist dies bei funk-
tionalen Programmiersprachen der Fall, weil sie aufgrund ihrer Herkunft aus
der Semantik starker am Ergebnis einer Berechnung orientiert sind. Imperati-
ve bzw. objekt-orientierte Programmiersprachen hingegen betonen oft zu stark,
welche Schritte notwendig sind, um das gewunschte Ergebnis zu erhalten.
Lambda-Kalkul und funktionales Programmieren
Obwohl der -Kalkul die konzeptionelle Grundlage der funktionalen Sprachfa-
milie bildet, spiegelt er die Implementierung moderner funktionaler Program-
miersprachen nicht angemessen wider. Dies tri t besonders fur die sogenannten
verzogert auswertenden funktionalen Programmiersprachen zu, d.h. solche, bei
denen Argumente nur dann ausgewertet werden, wenn sie zur Ermittlung des
Ergebnisses beitragen. Denn um eine Mehrfachauswertung bei der Anwendung
ieiner Funktion auf nicht vollstandig ausgewertete Argumente zu vermeiden, ver-
wenden alle heutzutage relevanten Implementierungen Graphreduktion, d.h. sie
operieren nicht auf einem Termbaum sondern auf einem Graphen. Ein Beispiel
mag dies verdeutlichen: Die Ausdrucke x: (x + x) und x: (2x) stellen beide ei-
ne Funktion dar, die ihr Argument x verdoppelt. Eine Anwendung auf z.B. das
noch nicht vollstandig ausgewertete Argument (5 3) wurde bei der ublichen
call-by-name Auswertung, d.h. dietausdrucke werden einfach fur die
Argumentvariablen eingesetzt, aber (5 3) + (5 3) bzw. 2(5 3) liefern.
O ensic htlich wurde dann das Ergebnis des Ausdruckes (5 3) bei der ersten
Variante zwei Mal ermittelt, was uber ussig ist, da das zweimalige Vorkommen
des Ausdruckes (5 3) ein- und denselben Wert bezeichnet. Indem diese Infor-
mation in einem Graphen gespeichert wird, umgeht die Implementierung diese
Mehrfachberechnung. Dies ist aber nur zulassig, weil in funktionalen Program-
miersprachen das Prinzip der referentiellen Transparenz erfullt ist, d.h. ein Aus-
1druck verandert wahrend der Ausfuhrung eines Programmes nicht seinen Wert
sondern wird nur in eine andere, aquivalente Form ub erfuhrt.
Um die operationale Semantik einer solchen Implementierung mittels Gra-
phreduktion entsprechend abzubilden, werden sogenannte call-by-need Kalkule
herangezogen. Bei diesen wird durch eine geschickte Wahl der Kalkulregeln si-
chergestellt, da Ausdruc ke erst kopiert werden konnen, wenn sie in einer be-
stimmten Form vorliegen, die man als Basiswert bezeichnen konnte. Der Charak-
ter der verzogerten Auswertung bleibt hierbei freilich erhalten, d.h. eine Funk-
tionsanwendung vermag sofort ein Ergebnis zu liefern, sobald alle relevanten
Argumentausdrucke ausgewertet sind. Fur das genannte Beispiel bedeutet das,
da die Anwendung von x: (x + x) auf das Argument (5 3) zuerst in einen
Ausdruck der Form let x = (5 3) in (x + x) uberfuhrt wird, wobei das let-
Konstrukt hier die Graphdarstellung, das Sharing, explizit darstellt. Erst wenn
das Ergebnis 2 fur den Term (5 3) ermittelt ist, wird es fur x in den Rumpf
x + x eingesetzt und somit die Mehrfachberechnung vermieden.
Nichtdeterminismus und Gleichheit
Die mitunter wichtigste Frage in einem Lambda-Kalkul, nicht nur call-by-need
betre end, ist wohl, welche Arten von Termen kopiert werden durfen. Wesent-
lich bein u t wird hierdurch auch die Frage, welche Programmtransformationen
zulassig sind bzw. welche Gleichheiten auf Programmen gelten sollen.
1Man beachte, da diese Aussage fur imperative Programmiersprachen nicht zutri t.
iiWie das oben angefuhrte Beispiel bereits verdeutlicht hat, sollten die beiden
Ausdruc ke x: (x+x) und x: (2x) als gleich betrachtet werden. Anderseits kann
die im -Kalkul ublic he ()-Regel nicht mehr uneingeschrankt gelten.
( x:M )N = M[N=x] ()
Hierbei bezeichnet M[N=x] die Einsetzung des Argumentes N im Term M fur
die Variable x, was, wir im obigen Beispiel gesehen haben, zu Mehrfachauswer-
tungen fuhren kann.
Wie aber la t sich nun ein adaquater Gleichheitsbegri nden, wenn doch
auch der Ausdruck (5 3) + (5 3) dasselbe Ergebnis, namlich 4, liefert? Es
genugt also o ensic htlich nicht, nur die Ergebnisse von Auswertungen zu be-
trachten. Einige Arbeiten verfolgen daher den Ansatz, die Anzahl der Auswer-
tungsschritte zu zahlen, was auch erfolgversprechend scheint.
Diese Arbeit jedoch schlagt einen anderen Weg ein: Es wird ein Sprachkon-
strukt pick eingefuhrt, welches nichtdeterministisch eines seiner beiden Argu-
menten auswahlt. Nichtdeterminismus in dieser Form verletzt o ensic htlich die
referentielle Transparenz, hilft aber im Gegenzug zu erkennen, wann Sharing
erhalten bleibt bzw. wann nicht: Die beiden Ausdruc ke pick 5 3+pick 5 3 und
let x = pick 5 3 in (x+x) liefern nun unterschiedliche Mengen von moglic hen
Resultaten, namlic hf 6; 8; 10g gegenub erf 6; 10g fur den let-Ausdruck.
Daruberhinaus gibt es eine Vielzahl von Anwendungsgebieten fur nichtde-
terministische Lambda-Kalkule, u.a. als theoretische Grundlage fur nebenlau ge
Prozesse oder von deklarativer, Seitene ekt-b ehafteter Ein-/Ausgabe. Insbeson-
dere im Bezug auf das letztere sind an der Professur schon einige Arbeiten
durchgefuhrt worden, z.B. die Dissertation von Arne Kutzner oder der tech-
nische Bericht zum Kalkul FUNDIO, zu denen sich diese als eine Erganzung
bzw. Fortfuhrung versteht.
Denn die Kenntnis ub er die in einem Kalkul geltenden Gleichheiten spielt ei-
ne herausragende Rolle fur dessen Verstandnis. Die bisherigen Arbeiten stutzen
sich dabei hauptsac hlich auf den Begri der kontextuellen Gleichheit, durch die
zwei Terme s und t miteinander identi ziert werden, wenn deren Auswertung
in allen moglichen Programmkontexten C[ ] dasselbe Terminierungsverhalten,
gekennzeichnet mit+, zeigt:
s ’ t () (8C : C[s]+() C[t]+)c
Die kontextuelle Gleichheit stellt ein mac htiges Werkzeug fur die Beurteilung
der Korrektheit von Programmtransformationen dar, insbesondere weil sie per
iiiDe nition eine Kongruenz ist, d.h. ihre Gleichheiten wiederum in Kontexte ein-
setzbar sind, also die Implikation s’ t =) (8C : C[s]’ C[t]) erfullt.c c
Mitunter sind Gleichheiten aber schwierig nachzuweisen, weil ja die Terminie-
rung der Auswertung in allen moglichen Kontexten betrachtet werden mu .
Daher ist es oftmals sinnvoll, einen anderen Aquivalenzbegri zu Hilfe zu
nehmen. Die Rede ist von der Methode der Bisimulation, welche einen stark er
stufenweisen Gleichheitstest beschreibt. Hier werden zwei Terme als gleich be-
trachtet, wenn sie auf allen moglichen Stufen dasselbe Verhalten zeigen, solange
man also nicht das Gegenteil nachweisen kann. Die Technik fand zuerst im Be-
reich der Zustandsub ergangssysteme Anwendung, ist mittlerweile aber auf dem
Gebiet der funktionalen Programmierung und Lambda-Kalkule gut etabliert
und existiert in verschiedenen Auspragungen. Der Stil, den Abramsky appli-
cative bisimulation nennt, ist am einfachsten in Form einer Praordn ung. zu
illustrieren.
0 0 0 0
s . t () (s+ x:s =) (t+ x:t ^ 8r : ( x:s ) r . ( x:t ) r))
Dies ist nicht etwa eine zyklische De nition, sondern als Fixpunktgleichung zu
verstehen, uber welcher der gro te Fixpunkt gebildet wird. Dadurch wird das
Beweisprinzip der Co-Induktion anwendbar.
Setzt man =.\& so ist leicht zu sehen, da ’ gefolgert werdenc
kann, vorausgesetzt ist eine Kongruenz. Gilt die Einsetzbarkeit in Kontexte
fur eine Praordn ung, so wird von einer Prakongruenz gesprochen. Es ist also
zu zeigen, da die Relation., genannt similarity, eine Prak ongruenz ist. Nicht
nur dieser Beweis sondern bereits der Entwurf der passenden Relation fur ein