On confluence and semantic full abstraction of lambda calculus languages

Abstract

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.