New Results on Morris's Observational Theory: the benefits of separating the inseparable

Flavien Breuvart 1 Giulio Manzonetto 2 Andrew Polonsky 3 Domenico Ruoppolo 2
1 FOCUS - Foundations of Component-based Ubiquitous Systems
CRISAM - Inria Sophia Antipolis - Méditerranée , DISI - Dipartimento di Informatica - Scienza e Ingegneria [Bologna]
2 LCR - Logic, Computation and Reasoning [Villetaneuse]
LIPN - Laboratoire d'Informatique de Paris-Nord
Abstract : Working in the untyped lambda calculus, we study Morris's λ-theory H +. Introduced in 1968, this is the original extensional theory of contextual equivalence. On the syntactic side, we show that this λ-theory validates the ω-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 λ-König. Intuitively, a model is λ-König when every λ-definable tree has an infinite path which is witnessed by some element of the model. Both results follows from a weak separability property enjoyed by terms differing only because of some infinite η-expansion, which is proved through a refined version of the Böhm-out technique.
Document type :
Journal articles
Complete list of metadatas

Cited literature [24 references]  Display  Hide  Download

https://hal.inria.fr/hal-01337192
Contributor : Flavien Breuvart <>
Submitted on : Friday, June 24, 2016 - 4:03:19 PM
Last modification on : Thursday, February 7, 2019 - 5:48:15 PM
Long-term archiving on : Sunday, September 25, 2016 - 12:22:36 PM

File

proc-breuvart.pdf
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Citation

Flavien Breuvart, Giulio Manzonetto, Andrew Polonsky, Domenico Ruoppolo. New Results on Morris's Observational Theory: the benefits of separating the inseparable. Leibniz International Proceedings in Informatics , Leibniz-Zentrum für Informatik, 2016, 1st International Conference on Formal Structures for Computation and Deduction, pp.560. ⟨http://fscd2016.dcc.fc.up.pt/⟩. ⟨10.4230/LIPIcs.FSCD.2016.70⟩. ⟨hal-01337192⟩

Share

Metrics

Record views

382

Files downloads

110