Locally boolean domains and universal models for infinitary sequential languages [Elektronische Ressource] / von Tobias Löw

Sujets

• Mathematics

Informations

• Publié par: technischen_universitat_darmstadt
• Publié le: 01 janvier 2007
• Nombre de lectures: 15
• Langue: English

Extrait

Locally Boolean Domains and
Universal Models for
Infinitary Sequential Languages
Vom Fachbereich Mathematik
der Technischen Universit¨at Darmstadt
zur Erlangung des akademischen Grades eines
Doktors der Naturwissenschaften (Dr. rer. nat.)
genehmigte
Dissertation
von
Dipl.-Math. Tobias L¨ow
aus Offenbach am Main
Referent: Prof. Dr. Thomas Streicher
Korreferent: Dr. James David Laird
Tag der Einreichung: 23. Oktober 2006
Tag der mundlic¨ hen Prufung¨ : 1. Dezember 2006
Darmstadt 2007
D 17Abstract
In the first part of this Thesis we develop the theory of locally boolean domains and
bistable maps (as introduced in [Lai05b]) and show that the category of locally boolean
domains and bistable maps is equivalent to the category of Curien-Lamarche games and
observably sequential functions (cf. [CCF94]). Further we show that the category of
locally boolean domains has inverse limits of ω-chains of embedding/projection pairs.
In the second part we consider the category of locally boolean domains and bistable
maps as model for functional programming languages: in [Lai05a] J. Laird has shown
that an infinitary sequential extension of the functional core language PCF has a fully
abstract model in the category of locally boolean domains. We introduce an extension
SPCF of his language by recursive types and show that it is universal for its model in∞
locally boolean domains. Finally we consider an infinitary target language CPS for the∞
CPS translation of [RS98] and show that it is universal for a model in locally boolean
domains which is constructed like Dana Scott’s D where D = O ={⊥,>}.∞
3Zusammenfassung
Im ersten Teil dieser Arbeit wird die Theorie lokal boolescher Bereiche und bistabiler
Abbildungen(siehe[Lai05b])entwickelt. Eswirdgezeigt, dassdieKategorielokalboole-
scher Bereiche und bistabiler Abbildungen zur Kategorie von Curien-Lamarche Spielen
und beobachtbar sequenzieller Funktionen ¨aquivalent ist. Weiterhin zeigen wir, dass
die Kategorie lokal boolescher Bereiche und bistabiler Abbildungen inverse Limiten von
ω-Ketten von Einbettungs-/Projektionspaaren besitzt.
Im zweiten Teil der Arbeit betrachten wir die Kategorie lokal boolescher Bereiche und
bistabilerAbbildungenalsModellfur¨ funktionaleProgrammiersprachen: in[Lai05a]hat
J. Laird gezeigt, dass es in der Kategorie lokal boolescher Bereiche ein voll abstraktes
Modell fur¨ eine infinit¨are, sequentielle Erweiterung der funktionalen Kernsprache PCF
gibt. Wir definieren SPCF , eine Erweiterung von Lairds Sprache um rekursive Typen,∞
und zeigen, dass diese Sprache universell bezuglic¨ h ihres Modells in der Kategorie lokal
¨boolescher Bereiche ist. Schließlich betrachten wir fur¨ die CPS Ubersetzung aus [RS98]
eine infinit¨are Zielsprache CPS und zeigen, dass sie universell bezuglic¨ h ihres Modells∞
in der Kategorie lokal boolescher Bereiche ist, welches wie Dana Scotts D mit D =∞
O ={⊥,>} konstruiert ist.
Erkl¨arung
Hiermit versichere ich, dass ich diese Dissertation selbst¨andig verfasst und nur die
angegebenen Hilfsmittel verwendet habe.
Tobias L¨ow
4Contents
1 Introduction 7
1.1 Sequentiality and Full Abstraction. . . . . . . . . . . . . . . . . . . . . . 7
1.2 Locally boolean domains . . . . . . . . . . . . . . . . . . . . . . . . . . . 9
1.3 Overview of this thesis . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9
2 Locally Boolean Domains 13
2.1 Locally Boolean Orders . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
2.2 Locally Boolean Domains . . . . . . . . . . . . . . . . . . . . . . . . . . 15
2.3 Bistable maps . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
3 Locally boolean domains and Curien-Lamarche games 35
3.1 Curien-Lamarche games as locally boolean domains . . . . . . . . . . . . 35
3.2 Locally boolean domains as Curien-Lamarche games . . . . . . . . . . . . 40
3.3 Observable sequentiality vs. bistability . . . . . . . . . . . . . . . . . . . 46
3.4 Equivalence of the categories LBD and OSA . . . . . . . . . . . . . . . 50
3.5 Exponentials in theries LBD and OSA . . . . . . . . . . . . . . . 52
3.6 Exponentials as function spaces . . . . . . . . . . . . . . . . . . . . . . . 58
4 Properties of the category LBD 63
4.1 Products, biliftings and sums . . . . . . . . . . . . . . . . . . . . . . . . 63
4.2 Embedding/Projection Pairs in LBD . . . . . . . . . . . . . . . . . . . . 65
4.3 Inverse Limits of Projections in LBD . . . . . . . . . . . . . . . . . . . . 68
4.4 Countably based Locally Boolean Domains . . . . . . . . . . . . . . . . . 80
5 A universal model for the language SPCF in LBD 85∞
5.1 Definition of SPCF . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 85∞
5.2 Operational semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . 88
5.3 Interpretation of types . . . . . . . . . . . . . . . . . . . . . . . . . . . . 90
5.4 Denotational semantics of SPCF . . . . . . . . . . . . . . . . . . . . . . 92∞
5.5 Universality of SPCF . . . . . . . . . . . . . . . . . . . . . . . . . . . . 93∞
6 CPS : An infinitary CPS target language 99∞
6.1 The untyped language CPS . . . . . . . . . . . . . . . . . . . . . . . . . 99∞
6.2 Universality of CPS . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 100∞
6.3 Lack of faithfulness of the interpretation . . . . . . . . . . . . . . . . . . 103
7 Conclusion and possible extensions 105
5Contents
Bibliography 107
Acknowledgements
Thefirstpersontothankhereismyscientificadvisor, ThomasStreicher, forhissupport
and for many helpful explanations, comments and discussions. Further, I am grateful
to Jim Laird on the one hand for refereeing this thesis and on the other hand for his
foundations of the theory of locally boolean domains and bistable maps.
AThisthesiswastypesetusingLT Xandalotofmacropackages. IwouldliketothankE
all people involved in developing and providing all this free software.
Finally, very special thanks go to Daniela. Without her love and encouragement this
thesis would not have been possible.
61 Introduction
The aim of this thesis is to show that the category LBD of locally boolean domains
and bistable maps (as introduced by J. Laird in [Lai05b]) is equivalent to the category
OSA of Curien-Lamarche games and observably sequential maps (as introduced by
R. Cartwright, P.L. Curien and M. Felleisen in [CCF94]). Further we introduce the
language SPCF , a sequential extension of PCF by recursive types, error elements and a∞
catch-construct,andshowthatitisuniversalforitsmodelinLBD. Finallyweconsider
an infinitary target language CPS for the CPS translation (of [RS98]) and show that∞
CPS is universal fora model inLBD which is constructed like DanaScott’sD where∞ ∞
D = O ={⊥,>}.
1.1 Sequentiality and Full Abstraction
The investigation of sequential functional programming languages started end of the
1960ieswhenD.ScottintroducedthelanguageLCF(LogicofComputableFunctions)for
reasoningaboutcomputablefunctionalsofhighertype. Thispaperwasfinallypublished
as[Sco93]butcirculatedforalongtimeasanunpublishedbutmostinfluencingtechnical
report. In [Plo77] G. Plotkin first gave a detailed meta-mathematical analysis of PCF
(Programming Computable Functions), the functional kernel language underlying the
logical calculus LCF.
The language PCF is simply typed λ-calculus extended by a base type of natural
numbers, some basic arithmetic operations, a conditional and fixpoint combinators for
expressing general recursion. In [Plo77] Plotkin formulated an operational semantics for
PCFasatermrewritingsystemsconstrainedbyaleftmost-outermostreduction-strategy
0which is sequential in the sense that each PCF term t contains a unique subterm t that
has to be reduced in the next step of evaluation.
Having an operational and denotational semantics for PCF there arises the question
how these two semantics should be related. Obviously, reduction preserves the denota-
tion of terms. In [Plo77] he proved computational adequacy, i.e. that a closed term t of
base type reduces to a numeral n whenever JtK =n. Thus for closed terms of base type
their denotational semantics coincides with their operational semantics. Two (closed)
terms t and t can be used interchangeably iff for all contexts C[−] of base type C[t ]1 2 1
and C[t ] have the same meaning. Such terms are called observationally equivalent.2
Obviously, if two terms have the same denotational semantics then they are also obser-
vationally equivalent. A model is called fully abstract iff denotational equality coincides
with observational equivalence. Already in [Sco93] D. Scott observed that his domain
model lacks full abstraction because of theparallel-or function which is continuous but
71 Introduction
not sequentially computable. In [Plo77] Plotkin showed that Scott’s domain model is
fully abstract for the extension of PCF with parallel-or. (If one further adds a contin-
uous existential quantifier then the denotable elements of the Scott model are precisely
the computable ones as also shown in [Plo77].)
In [Mil77] R. Milner constructed a fully abstract model as the ideal completion of
a quotient by observational equivalence of those PCF-terms which denote finite ele-
ments. Moreover, he showed that all order extensional fully abstract domain (i.e. cpo-
enriched)models