Algebraic foundations of the unifying theories of programming [Elektronische Ressource] / Walter Guttmann

Walter Guttmann

Sujets

• Informatik

Informations

• Publié par: universitat_ulm
• Publié le: 01 janvier 2007
• Nombre de lectures: 3
• Langue: English

Extrait

Algebraic Foundations of the
Unifying Theories of Programming
Dissertation
zur Erlangung des Doktorgrades Dr. rer. nat.
der Fakultat fur Ingenieurwissenschaften und Informatik
der Universitat Ulm
Walter Guttmann
aus Gro wardein
Universitat Ulm
Fakultat fur Ingenieurwissenschaften und Informatik
Institut fur Programmiermethodik und Compilerbau
Direktor: Prof. Dr. Helmuth A. Partsch
2007Amtierender Dekan: Prof. Dr. Helmuth A. Partsch
Erster Gutachter: Prof. Dr. Helmuth A. Partsch
Zweiter Gutachter: Prof. Dr. Friedrich W. von Henke
Dritter Gutachter: Prof. Dr. Bernhard Moller
Tag der Promotion: 5. Dezember 2007Abstract
Hoare and He’s Unifying Theories of Programming take a relational view on semantics. The
meaning of a non-deterministic, imperative program is described by ‘designs’ composed of
two relations. They represent terminating states and relate the initial and nal values of
the observable variables, respectively. Several ‘healthiness conditions’ are imposed by the
theory to obtain properties found in practice.
This work determines the structure of designs and modi es the theory to support non-
strict computations. It achieves these goals by identifying healthiness conditions and related
axioms that involve unnecessary restrictions and subsequently removing them. The outcome
provides a clear account of the algebraic foundations of the Unifying Theories of Program-
ming.
One of the results is a generalisation of designs by constructing them on semirings with
ideals, structures having fewer axioms than relations. This clari es the essential algebraic
structure of designs, allows the reuse of existing mathematical theory and connects to further
semantical approaches. The framework is extended by algebraic formulations of nite and
in nite iteration, domain, pre-image, determinacy, invariants and convergence. Calculations
and reasoning become simpler by the new, more abstract representation as is shown by
applying the theory to investigate linear recursions.
Another result is an extension of the Unifying Theories of Programming to deal with
unde ned values irrespective of non-termination. Besides being closer to practice, it forms
the basis of a new theory of relations representing non-strict computations. They satisfy
additional healthiness conditions that model dependence in computations in an elegant al-
gebraic form. Programs can then be executed according to the principle of lazy evaluation,
otherwise known from functional programming languages.
Acknowledgements
Several individuals played various roles in the creation of this work. Here they are, in
chronological order. I thank Wolfram Schulte and Ton Vullinghs who attracted me to (and
then unfortunately left from) the department ‘Programmiermethodik und Compilerbau’, the
place where this work has been produced. I thank Prof. Dr. Helmuth Partsch who supported
my work by providing a very unconstrained environment at that place, and who brought me
into contact with the next person. I thank Bernhard M oller whose delightful collaboration
resulted in key works [GM06a, GM06b] for Chapter 2 that cannot be imagined without his
and his collaborators’ prior research. I thank Prof. Dr. Friedrich von Henke who agreed to
act as the second referee of this work. I thank Marc Meister and Christian Ehrhardt for
helpful remarks on the text.
Walter Guttmannp f
p f
f
?2422SSSK<G??(?K-42?4-@2->-?Q???Contents
1 Introduction 7
1.1 Unifying theories of programming . . . . . . . . . . . . . . . . . . . . . . . . . 8
1.2 Designs and healthiness conditions . . . . . . . . . . . . . . . . . . . . . . . . 9
2 The structure of designs 11
2.1 Star and omega designs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12
2.1.1 Axioms for conditions . . . . . . . . . . . . . . . . . . . . . . . . . . . 12
2.1.2 Designs and normal designs as matrices . . . . . . . . . . . . . . . . . 15
2.1.3 Star designs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18
2.1.4 Omega designs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19
2.1.5 UTP algebras . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21
2.1.6 Fixpoints and designs . . . . . . . . . . . . . . . . . . . . . . . . . . . 21
2.1.6.1 The greatest xpoint . . . . . . . . . . . . . . . . . . . . . . 22
2.1.6.2 The least xpoint . . . . . . . . . . . . . . . . . . . . . . . . 24
2.2 Relating recursive de nitions . . . . . . . . . . . . . . . . . . . . . . . . . . . 24
2.2.1 Tail-recursion and tests . . . . . . . . . . . . . . . . . . . . . . . . . . 25
2.2.2 Linear recursion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26
2.2.3 Relating tail-recursion and linear recursion . . . . . . . . . . . . . . . 27
2.3 Symmetric linear recursion . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
2.3.1 Domain, modal operators, determinacy and invariants . . . . . . . . . 29
2.3.2 The nite part . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
2.3.3 Convergence and divergence . . . . . . . . . . . . . . . . . . . . . . . . 33
2.3.4 The in nite part . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
2.3.5 Putting the nite and in nite parts together . . . . . . . . . . . . . . 36
2.4 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 386 Contents
3 Representing non-strictness 39
3.1 Prolegomena . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
3.1.1 Designs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
3.1.2 Relations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
3.1.2.1 Modelling computations . . . . . . . . . . . . . . . . . . . . . 42
3.1.2.2 Relation algebra . . . . . . . . . . . . . . . . . . . . . . . . . 42
3.1.2.3 Further conventions . . . . . . . . . . . . . . . . . . . . . . . 43
3.2 Compendium . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
3.2.1 Relational operations . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
3.2.2 Expressions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
3.2.3 Local variables . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
3.2.4 Isotony and neutrality . . . . . . . . . . . . . . . . . . . . . . . . . . . 50
3.3 Finite branching . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51
3.3.1 Minimal elements . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52
3.3.2 Boundedness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55
3.3.3 Continuity . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57
3.3.4 Totality . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59
3.4 Dependence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 60
3.4.1 Non-strict parts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61
3.4.1.1 Inductive derivation . . . . . . . . . . . . . . . . . . . . . . . 61
3.4.1.2 Order formulation . . . . . . . . . . . . . . . . . . . . . . . . 64
3.4.1.3 Closure . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 66
3.4.2 Absent strict parts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 68
3.4.2.1 Inductive derivation . . . . . . . . . . . . . . . . . . . . . . . 68
3.4.2.2 Order formulation . . . . . . . . . . . . . . . . . . . . . . . . 70
3.4.2.3 Closure . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 73
3.5 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 75
3.5.1 Adequacy . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 75
3.5.2 Related work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77
3.6 Appendix . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77
3.6.1 Fixpoint theorems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77
3.6.2 Isotony of expressions . . . . . . . . . . . . . . . . . . . . . . . . . . . 78
3.6.3 Parallel composition . . . . . . . . . . . . . . . . . . . . . . . . . . . . 80
3.6.4 Unde nedness and non-termination . . . . . . . . . . . . . . . . . . . . 81
4 Conclusion 85
References 87
Zusammenfassung 93Chapter 1
Introduction
The Unifying Theories of Programming (UTP) developed in [HH98] provide a framework
to describe and compare the semantics of speci cations and programs of various paradigms
using a common formalism. Its core is a relational, state-based model of non-deterministic,
imperative programs. They are represented as special relations, so-called ‘designs’, combin-
ing transition and termination information. Although designs serve as a solid foundation
for further theories, they impose unnecessary constraints and thus restrict the range of ap-
plication. The topic of this work is to investigate what happens if these limits are removed.
We study two kinds of restrictions. Both have to do with the internal and external struc-
ture of designs. The internal structure is given by the components of designs, namely two
relations modelling the terminating states and the transition behaviour of a computation.
The external structure is given by the so-called ‘healthiness conditions’, laws that models of
computations should satisfy to be useful.
Our rst contribution generalises the component relations by re