Please use this identifier to cite or link to this item: http://dx.doi.org/10.14279/depositonce-1771
Main Title: Strikte Verfahren zyklischer Berechnung
Translated Title: Strict Methods of Cyclic Computation
Author(s): Trancón y Widemann, Baltasar
Advisor(s): Pepper, Peter
Granting Institution: Technische Universität Berlin, Fakultät IV - Elektrotechnik und Informatik
Type: Doctoral Thesis
Language: German
Language Code: de
Abstract: Diese Arbeit untersucht Theorie und Techniken der deklarativen, funktionalen Erzeugung und Verarbeitung von zyklischen Daten. Anders als bei nichtfundierten Ansätzen, wie sie den sogenannten lazy Programmiersprachen wie Haskell und Clean zugrunde liegen, und in denen unendlich absteigende Teiltermketten gestattet sind, ersetzen wir die übliche Metatheorie Algebra durch ihre Dualisierung Coalgebra. Dadurch wird es möglich, Zyklizität als eigenständiges Phänomen von echter Unendlichkeit zu unterscheiden. Somit können auf zyklischen Daten, die unendliche fortschreitende Beobachtungen zulassen, aber endlich repräsentiert sind, terminierende Berechnungen mit strikter Semantik ausgeführt werden. Der bisher erfolgreichste coalgebraische Ansatz führte zur Entwicklung der Sprache Charity, die sowohl in denotationeller als auch operationaler Semantik auf kategorientheoretische Konstrukte zurückgreift. Hier wird ein entgegengesetzter Ansatz verfolgt, der die operationale Semantik enger an traditionelle strikt funktionale, imperative oder objektorientierte Sprachen anlehnt. Eine Besonderheit dieses Ansatzes ist, daß nicht nur eine finale Coalgebra als Struktur der semantischen Elemente verwendet wird. Konkrete Repräsentationen im Speicher eines Rechners werden als Elemente von nichtfinalen Coalgebren beschrieben. In diesem Rahmen läßt sich eine primitiv corekursive Funktion als eine Familie von Coalgebren darstellen, von denen jede einen Rekursionsschritt der Funktion auf einem Speicherzustand beschreibt. Es wird ein Algorithmus angegeben, der modulo Bisimilarität dem eindeutigen Homomorphismus in die finale Coalgebra, also der erzeugten corekursiven Funktion entspricht. Dieser Algorithmus terminiert auch bei strikter Auswertung auf allen endlichen Eingabezuständen, also insbesondere auf konkreten Graphdarstellungen von Daten im Speicher. Ebenso wird das Entscheiden von Prädikaten durch Tiefensuche, wie etwa beim Resolutionsverfahren der Sprache Prolog, auf eine coalgebraische Darstellung zurückgeführt. Falls die definierenden Schlußregeln zyklisch sind, existieren potentiell verschiedene Fixpunktsemantiken. Es wird auch hier ein Algorithmus angegeben, der bei geeigneter Parametrisierung die Zugehörigkeit einer Formel zu einem Fixpunktmodell entscheidet. Außerdem wird eine Klasse von Parametern konstruktiv definiert, die die gewöhnlich intendierten Fixpunkte, nämlich stückweise kleinste und größte Fixpunkte, auswählen. Beide algorithmischen Verfahren sind so dargestellt, daß sie sich mit den selben technischen Mitteln der Zyklenerkennung implementieren lassen. Da das Entscheiden zyklischer Prädikate lazy nicht möglich ist, ergibt sich durch Kombination beider Verfahren eine erhebliche Mächtigkeit. Zahlreiche Probleme auf zyklischen Eingaben, die auf diese Weise gelöst werden können, erfordern in herkömmlichen Ansätzen ohne coalgebraische Semantik und Zyklenerkennung eine radikale Umcodierung enschließlich der expliziten Modellierung von Zellenidentitäten, was dem Abstraktionsanspruch eines deklarativen Paradigmas zuwiderläuft. Nach detaillierter Analyse der technischen Randbedingungen wird ein operationales Semantikmodell für die sprachseitige Unterstützung der entwickelten Verfahren in Form einer virtuellen Maschine definiert. Diese ist herkömmlichen Modellen wie der Java-Maschine nachempfunden, trägt aber auch den besonderen Bedürfnissen der funktionalen Programmierung höherer Ordnung einerseits und der Zyklenerkennung und -behandlung andererseits Rechnung. Die existierende Java-Implementierung der virtuellen Maschine wird beschrieben. Sie umfaßt Programmmodell und Interpreter mit grafischer Benutzeroberfläche, eine textuelle Eingabesprache, sowie einen optimierenden Compiler, der zur statischen Erzeugung von C oder im just-in-time-Betrieb eingesetzt werden kann. Die Relevanz der coalgebraischen Sichtweise wird durch drei beispielhafte Anwendungsfelder von aufsteigender Komplexität illustriert, für die jeweils eine Reihe typischer Algorithmen in formaler Form und als Maschinenprogramm (im Beispielverzeichnis der Implementierung) entwickelt werden. Die Arbeit legt also eine Basis für die formale Spezifikation und konkrete Implementierung zyklischer Verfahren. Die angegebene Implementierung kann direkt als Programmiersystem genutzt werden, oder als Referenz für die Integration solcher Verfahren in andere Systeme und Paradigmen dienen.
This present work investigates theory and techniques of declarative and functional construction and processing of cyclical data. Contrary to the non-well-founded approaches forming the foundations of so-called lazy programming languages like Haskell or Clean, in which infinitely descending subterm chains are allowed, we replace the common meta-theory of algebra by its categorial dual coalgebra. This allows to distinguish cylicity as a particular phenomenon from proper infinity. Thus cyclic data that allow infinitly progressing observations, but are represented finitely nonetheless, can be processed with terminating computations under strict semantics. The most successful coalgebraic approach so far lead to the development of the language Charity that employs category-theoretic constructs for both denotational and operational semantics. We pursue a contrary approach, gearing operational semantics more towards traditional strict functional, imperative or object-oriented languages. This approach is not restricted to using just final coalgebra as the structure of semantical elements. Actual representations in machine memory are described as elements of non-final coalgebras, as well. In this framework, any primitively corecursive function can be specified as a family of coalgebras, each describing a recursion step on a single state of memory. An algorithm is given that corresponds up to bisimilarity to the unique morphism into the final coalgebra, namely the induced corecursive function. This algorithm terminates even under strict evaluation rules on all finite input states, subsuming real encodings of data graphs in memory. We also reduce the decision procedure for predicates by depth-first search, like it is used in the resolution strategy of Prolog, to a coalgebraic representation. If deduction rules are cyclic, there are potentially several different fixpoint semantics to this resolution. We give another algorithm that decides the inclusion of formulae in one fixpoint model, given proper parametrization. We also define a class of such parameters constructively, covering all of the commonly intended fixpoints, specifically piecewise least and greatest ones. Both algorithmic methods are presented in a way that allows implementation with the same technical means of cycle detection. Since cyclical predicates cannot be decided lazily, considerable power is gained by combining the two methods. Numerous problems on cyclical input concisely solved in this way require radical transcoding in traditional frameworks without coalgebraic semantics and cycle detection. Specifically, cell identities have to be modeled explicitly, which we consider as contradictory to the attitude of abstraction innate to a declarative paradigma. Following a detailed analysis of the technical constraints, we define a virtual machine as operational semantics for supporting the presented methods in a programming language. This machine is modeled after standard examples like the Java machine. But it also caters for the needs of higher-order functional programming on the one hand and of cycle detection and handling on the other. We describe the existing implementation of the machine and its peripheral tools in Java. This comprises a program model, an interpreter with optional graphical user interface, an assembly language for textual program input, and a compiler suitable for both traditional ahead-of-time production of C code and just-in-time operation. The relevance of the coalgebraic viewpoint is finally illustrated by three exemplary application domains of increasing complexity. For each of these, a collection of typical algorithms is developed both as formal specifications and machine programs, available in the examples directory of the implementation. This work provides exhaustive and self-contained foundations for the formal specification and effective implementation of cyclical computations. The given implementation is fit for usage as a programming system on its own, or as a reference for the integration of similar methods into other systems and paradigms.
URI: urn:nbn:de:kobv:83-opus-17559
http://depositonce.tu-berlin.de/handle/11303/2068
http://dx.doi.org/10.14279/depositonce-1771
Exam Date: 28-Feb-2007
Issue Date: 1-Feb-2008
Date Available: 1-Feb-2008
DDC Class: 004 Datenverarbeitung; Informatik
Subject(s): Coalgebra
Funktionale Programmierung
Rekursion
Zyklen
Coalgebra
Cycles
Functional programming
Recursion
Usage rights: Terms of German Copyright Law
Appears in Collections:Technische Universität Berlin » Fakultäten & Zentralinstitute » Fakultät 4 Elektrotechnik und Informatik » Institut für Softwaretechnik und Theoretische Informatik » Publications

Files in This Item:
File Description SizeFormat 
Dokument_32.pdf1.75 MBAdobe PDFThumbnail
View/Open
Dokument_1.zip2.83 MBZIP ArchiveView/Open


Items in DepositOnce are protected by copyright, with all rights reserved, unless otherwise indicated.