New Results on Morris's Observational Theory - Archive ouverte HAL Access content directly
Journal Articles Leibniz International Proceedings in Informatics Year : 2016

New Results on Morris's Observational Theory

(1) , (2) , (3) , (2)


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.
Fichier principal
Vignette du fichier
proc-breuvart.pdf (757.65 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-01337192 , version 1 (24-06-2016)


Attribution - CC BY 4.0



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 , 2016, 1st International Conference on Formal Structures for Computation and Deduction, pp.560. ⟨10.4230/LIPIcs.FSCD.2016.70⟩. ⟨hal-01337192⟩
207 View
56 Download



Gmail Facebook Twitter LinkedIn More