Skip to Main content Skip to Navigation
Journal articles

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 metadata

Cited literature [24 references]  Display  Hide  Download
Contributor : Flavien Breuvart Connect in order to contact the contributor
Submitted on : Friday, June 24, 2016 - 4:03:19 PM
Last modification on : Friday, October 30, 2020 - 12:04:03 PM
Long-term archiving on: : Sunday, September 25, 2016 - 12:22:36 PM


Files produced by the author(s)


Distributed under a Creative Commons Attribution 4.0 International License



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. ⟨10.4230/LIPIcs.FSCD.2016.70⟩. ⟨hal-01337192⟩



Les métriques sont temporairement indisponibles