TU Darmstadt / ULB / TUbiblio

A Universal Realizability Model for Sequential Functional Computation

Rohr, Alexander (2003)
A Universal Realizability Model for Sequential Functional Computation.
Technische Universität Darmstadt
Dissertation, Erstveröffentlichung

Kurzbeschreibung (Abstract)

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.

Typ des Eintrags: Dissertation
Erschienen: 2003
Autor(en): Rohr, Alexander
Art des Eintrags: Erstveröffentlichung
Titel: A Universal Realizability Model for Sequential Functional Computation
Sprache: Englisch
Referenten: Streicher, Prof. Dr. Thomas ; Longley, PhD John
Berater: Streicher, Prof. Dr. Thomas
Publikationsjahr: 23 Juli 2003
Ort: Darmstadt
Verlag: Technische Universität
Datum der mündlichen Prüfung: 5 Juli 2002
URL / URN: urn:nbn:de:tuda-tuprints-3515
Kurzbeschreibung (Abstract):

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.

Alternatives oder übersetztes Abstract:
Alternatives AbstractSprache

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.

Deutsch
Freie Schlagworte: Longley-Phoa Vermutung, konstruktiv logisch voll abstraktes Modell, volle Abstraktheit,PCF,FPC,Sequentialität,kombinatorische Algebra, rekursiver Typ, universeller Typ, rekursive Bereichsgleichung, beobachtbare Gleichheit, Retraktion, applikative Äquivalenz, Realisierbarkeitstopos, Bereichstheorie, semantischer Bereich, getypte Programmiersprache, ungetypte Programmiersprache, minimale Invariante, Fixpunktkombinator
Schlagworte:
Einzelne SchlagworteSprache
Longley-Phoa Conjecture, constructively logically fully abstract model, full abstraction,PCF,FPC,sequentiality,modest set,assembly,combinatory algebra, recursive type, universal type, recursive domain equation,observational equivalence, retraction,applicative equivalence,dominance,divergence,game model,realizability topos,domain theory,semantic domain,typed programming language, untyped programming language, lifting, minimal invariant, fixed point combinatorEnglisch
Sachgruppe der Dewey Dezimalklassifikatin (DDC): 500 Naturwissenschaften und Mathematik > 510 Mathematik
Fachbereich(e)/-gebiet(e): 04 Fachbereich Mathematik
Hinterlegungsdatum: 17 Okt 2008 09:21
Letzte Änderung: 05 Mär 2013 09:25
PPN:
Referenten: Streicher, Prof. Dr. Thomas ; Longley, PhD John
Datum der mündlichen Prüfung / Verteidigung / mdl. Prüfung: 5 Juli 2002
Schlagworte:
Einzelne SchlagworteSprache
Longley-Phoa Conjecture, constructively logically fully abstract model, full abstraction,PCF,FPC,sequentiality,modest set,assembly,combinatory algebra, recursive type, universal type, recursive domain equation,observational equivalence, retraction,applicative equivalence,dominance,divergence,game model,realizability topos,domain theory,semantic domain,typed programming language, untyped programming language, lifting, minimal invariant, fixed point combinatorEnglisch
Export:
Suche nach Titel in: TUfind oder in Google
Frage zum Eintrag Frage zum Eintrag

Optionen (nur für Redakteure)
Redaktionelle Details anzeigen Redaktionelle Details anzeigen