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 Abstract | Sprache |
---|
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 Schlagworte | Sprache |
---|
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 combinator | Englisch |
|
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 Schlagworte | Sprache |
---|
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 combinator | Englisch |
|
Export: |
|
Suche nach Titel in: |
TUfind oder in Google |
|
Redaktionelle Details anzeigen |