We construct a universal and even logically fully abstract realizability model for the sequential functional programming language of call-by-name FPC. This model is defined within the category of modest sets over the total combinatory algebra L of observational equivalence classes of closed terms of the untyped programming language lambda+Error. This language is untyped lazy call-by-name lambda-calculus extended by a single constant ERR and a conditional construct which distinguishes this constant from any other syntactic value. Universality and (constructive) logical full abstraction of the model are proved in three steps. Firstly, a canonical universal and logically fully abstract realizability model for FPC over the typed combinatory algebra T of observational equivalence classes of closed FPC-terms is constructed. Then the recursive type U := mu alpha. void + [ alpha --> alpha ] is shown to be universal, i.e. any other type is a definable retract of U. Hence this type gives rise to an untyped combinatory algebra U which is applicatively equivalent to the typed combinatory algebra T. As a consequence, the realizability toposes over T and U are equivalent and hence the realizability model for FPC over U also universal and logically fully abstract. Finally it is shown that every closed FPC-term of type U can be defined in the untyped language lambda+Error. Hence the combinatory algebras l U and L are applicatively equivalent. It follows that the realizability model over L is universal and logically fully abstract. As a consequence we prove a variant of the Longley-Phoa Conjecture.
Item Type:
Ph.D. Thesis
Erschienen:
2003
Creators:
Rohr, Alexander
Title of the item:
A Universal Realizability Model for Sequential Functional Computation
Wir konstruieren ein universelles und sogar logisch voll abstraktes Realisierbarkeitsmodell für die sequentielle funktionale Programmiersprache Call-by-name-FPC. Das Modell existiert in der Kategorie der Modest Sets über einer totalen kombinatorischen Algebra L bestehend aus observationalen Äquivalenzklassen von geschlossenen Termen der ungetypten Programmiersprache lambda+Error. Diese Programmiersprache ist eine Erweiterung des ungetypten Call-by-name-lambda-Kalküls um eine einzelne Konstante ERR und ein Konditionalkonstrukt, welches diese Konstante von jedem anderen syntaktischen Wert zu unterscheiden vermag. Die Universalität und die (konstruktive) logische volle Abstraktheit des Modells werden in drei Schritten gezeigt. Zunächst wird ein kanonisches universelles und logisch voll abstraktes Realisierbarkeitsmodell für FPC über der getypten kombinatorischen Algebra T der Äquivalenzklassen der geschlossenen FPC-Terme modulo beobachtbarer Gleichheit konstruiert. Anschließend wird gezeigt, dass der rekursive Typ U := mu alpha. void + [ alpha --> alpha ] universell ist, dass also jeder andere Typ ein definierbares Retrakt von U ist. Der universelle Typ induziert eine ungetypte kombinatorische Algebra U, welche applikativ äquivalent zur getypten kombinatorischen Algebra T ist. Folglich sind die Realisierbarkeitstopoi über T und U äquivalent und daher ist das Realisierbarkeitsmodell von FPC über U ebenfalls universell und logisch voll abstrakt. Schließlich wird bewiesen, dass jeder geschlossene FPC-Term vom Typ U in der ungetypten Sprache lambda+Error definierbar ist. Daher sind die kombinatorischen Algebren U und L applikativ äquivalent. Es folgt, dass das Realisierbarkeitsmodell über L universell und logisch voll abstrakt ist. Als Folgerung daraus beweisen wir eine Variante der Longley-Phoa-Vermutung.
![[feed]](/style/images/feed-icon-14x14.png){kind=icon}
![[img]](http://tuprints.ulb.tu-darmstadt.de/style/images/fileicons/application_pdf.png)
Drucken
Imprint
Sitemap
Search