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

Flavien Breuvart 1, 2 Giulio Manzonetto 3 Andrew Polonsky 4 Domenico Ruoppolo 3
2 FOCUS - Foundations of Component-based Ubiquitous Systems
CRISAM - Inria Sophia Antipolis - Méditerranée , DISI - Dipartimento di Informatica - Scienza e Ingegneria [Bologna]
3 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.
Type de document :
Article dans une revue
Leibniz International Proceedings in Informatics (LIPIcs), 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〉
Liste complète des métadonnées

Littérature citée [24 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01337192
Contributeur : Flavien Breuvart <>
Soumis le : vendredi 24 juin 2016 - 16:03:19
Dernière modification le : samedi 27 janvier 2018 - 01:31:39
Document(s) archivé(s) le : dimanche 25 septembre 2016 - 12:22:36

Fichier

proc-breuvart.pdf
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

Collections

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 (LIPIcs), 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〉

Partager

Métriques

Consultations de la notice

306

Téléchargements de fichiers

83