Creative Commons Attribution 3.0 Unported license (CC-BY 3.0)when quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2016.15
URN: urn:nbn:de:0030-drops-59924
URL: https://drops.dagstuhl.de/opus/volltexte/2016/5992/
Breuvart, Flavien ; Manzonetto, Giulio ; Polonsky, Andrew ; Ruoppolo, Domenico
New Results on Morris's Observational Theory: The Benefits of Separating the Inseparable
| pdf-format: |
|
Abstract
Working in the untyped lambda calculus, we study Morris'slambda-theory H+. Introduced in 1968, this is the original
extensional theory of contextual equivalence. On the syntactic side,
we show that this lambda-theory validates the omega-rule, thus
settling a long-standing open problem.On the semantic side, we
provide sufficient and necessary conditions for relational graph
models to be fully abstract for H+. We show that a relational graph
model captures Morris's observational preorder exactly when it is
extensional and lambda-Konig. Intuitively, a model is lambda-Konig
when every lambda-definable tree has an infinite path which is
witnessed by some element of the model.
Both results follow from a weak separability property enjoyed by
terms differing only because of some infinite eta-expansion,
which is proved through a refined version of the Böhm-out technique.
BibTeX - Entry
@InProceedings{breuvart_et_al:LIPIcs:2016:5992,
author = {Flavien Breuvart and Giulio Manzonetto and Andrew Polonsky and Domenico Ruoppolo},
title = {{New Results on Morris's Observational Theory: The Benefits of Separating the Inseparable}},
booktitle = {1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
pages = {15:1--15:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-010-1},
ISSN = {1868-8969},
year = {2016},
volume = {52},
editor = {Delia Kesner and Brigitte Pientka},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2016/5992},
URN = {urn:nbn:de:0030-drops-59924},
doi = {10.4230/LIPIcs.FSCD.2016.15},
annote = {Keywords: Lambda calculus, relational models, fully abstract, B{\"o}hm-out, omega-rule}
}
| Keywords: | Lambda calculus, relational models, fully abstract, Böhm-out, omega-rule | |
| Seminar: | 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016) | |
| Issue date: | 2016 | |
| Date of publication: | 17.06.2016 |
