2026-08-11T15:20:35Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:5992 2024-03-06T10:37:25Z ddc:004 open_access

New Results on Morris's Observational Theory: The Benefits of Separating the Inseparable Breuvart, Flavien Manzonetto, Giulio Polonsky, Andrew Ruoppolo, Domenico Lambda calculus relational models fully abstract Böhm-out omega-rule Working in the untyped lambda calculus, we study Morris's lambda-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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Flavien Breuvart and Giulio Manzonetto and Andrew Polonsky and Domenico Ruoppolo 2016 Is Part Of LIPIcs, Volume 52, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2016.15 urn:nbn:de:0030-drops-59924 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.15 eng https://creativecommons.org/licenses/by/3.0/legalcode