TU Darmstadt / ULB / tuprints

A Universal Realizability Model for Sequential Functional Computation

Rohr, Alexander :
A Universal Realizability Model for Sequential Functional Computation.
[Online-Edition]
TU Darmstadt
[Ph.D. Thesis], (2003)

[img]
Preview
Text
diss.pdf
Available under Creative Commons Attribution Non-commercial No Derivatives.

Download (655Kb) | Preview
Item Type: Ph.D. Thesis
Title: A Universal Realizability Model for Sequential Functional Computation
Language: English
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.

Alternative Abstract:
Alternative AbstractLanguage
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.German
Uncontrolled Keywords: 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
Alternative keywords:
Alternative keywordsLanguage
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, FixpunktkombinatorGerman
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 combinatorEnglish
Classification DDC: 500 Naturwissenschaften und Mathematik > 510 Mathematik
Divisions: Fachbereich Mathematik
Date Deposited: 17 Oct 2008 09:21
Last Modified: 10 Dec 2012 10:00
Official URL: http://elib.tu-darmstadt.de/diss/000351
URN: urn:nbn:de:tuda-tuprints-3515
License: Simple publication rights for ULB
Referees: Streicher, Prof. Dr. Thomas and Longley, PhD John
Advisors: Streicher, Prof. Dr. Thomas
Refereed: 5 July 2002
URI: http://tuprints.ulb.tu-darmstadt.de/id/eprint/351
Export:

Actions (login required)

View Item View Item