Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen: doi:10.22028/D291-26678
Titel: On confluence and semantic full abstraction of lambda calculus languages
Sonstige Titel: Über Konfluenz und semantische vollständige Abstraktion von Lambda-Kalkül-Sprachen
Verfasser: Müller, Fritz
Sprache: Englisch
Erscheinungsjahr: 2016
SWD-Schlagwörter: Lambda-Kalkül
Funktionale Programmiersprache
Semantischer Bereich
Freie Schlagwörter: lambda calculus languages
confluence
semantic full abstraction
PCF
DDC-Sachgruppe: 004 Informatik
Dokumentart : Dissertation
Kurzfassung: This thesis joins my four articles: (1) Confluence of the lambda calculus with left-linear algebraic rewriting, where we show that a lambda calculus with additional algebraic term rewrite rules that are confluent, left-linear and not-variable-applying, is again confluent, (2) Full abstraction for a recursively typed lambda calculus with parallel conditional, where we apply the theorem (1) to show that a recursively typed lambda calculus with a parallel conditional operator is confluent and has a fully abstract Scott-like (denotational) semantics, (3) On Berry’s conjectures about the stable order in PCF, where we refute Berry’s conjectures (a) that the fully abstract model of PCF together with the stable order forms bidomains, and (b) that the stable order has the syntactic order as its image, (4) From Sazonov’s non-dcpo natural domains to closed directed-lub partial orders, where we explore Sazonov’s notion of natural domains and derive the canonical subclass of closed directed-lub partial orders, which can be realized by dcpos with a restricted subset of their elements.The common background of (2-4) is the semantic full abstraction problem.
Diese Arbeit vereint meine vier Artikel (die englischen Titel sind übersetzt): (1) Konfluenz des Lambda-Kalküls mit links-linearer algebraischer Termersetzung, in dem wir zeigen, dass ein Lambda-Kalkül mit zusätzlichen algebraischen Termersetzungsregeln, die konfluent, links-linear und nicht-Variable-anwendend sind, wieder konfluent ist, (2) Vollständige Abstraktion f¨ur einen rekursiv getypten Lambda-Kalkül mit parallelem Konditional, in dem wir das Theorem (1) anwenden, um einen rekursiv getypten Lambda Kalkül mit einem parallelen Konditional als konfluent zu beweisen, und zu zeigen, dass er eine vollständig abstrakte Scott-artige (denotationale) Semantik hat, (3) Über Berrys Vermutungen über die stabile Ordnung in PCF, in dem wir Berrys Vermutungen widerlegen, (a) dass das vollständig abstrakte Modell von PCF mit der stabilen Ordnung Bidomains bildet, und (b) dass die stabile Ordnung die syntaktische Ordnung als Bild hat, (4) Von Sazonovs nicht-dcpo natürlichen Bereichen zu geschlossenen gerichtet-sup partiellen Ordnungen, in dem wir Sazonovs Begriff der natürlichen Bereiche erforschen und die kanonische Teilklasse von geschlossenen gerichtet-sup partiellen Ordnungen ableiten, die durch Dcpos mit einer eingeschränkten Teilmenge ihrer Elemente realisiert werden können.
Link zu diesem Datensatz: urn:nbn:de:bsz:291-scidok-67145
hdl:20.500.11880/26734
http://dx.doi.org/10.22028/D291-26678
Erstgutachter: Wilhelm, Reinhard
Tag der mündlichen Prüfung: 14-Nov-2016
SciDok-Publikation: 15-Dez-2016
Fakultät: Fakultät 6 - Naturwissenschaftlich-Technische Fakultät I
Fachrichtung: MI - Informatik
Fakultät / Institution:MI - Fakultät für Mathematik und Informatik

Dateien zu dieser Ressource:
Datei Beschreibung GrößeFormat 
T.pdf1,01 MBAdobe PDFÖffnen/Anzeigen


Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.