DROPS

Document

DOI: 10.4230/LIPIcs.FSCD.2017.20

Refutation of Sallé's Longstanding Conjecture

Authors: Benedetto Intrigila, Giulio Manzonetto, and Andrew Polonsky

Published in: LIPIcs, Volume 84, 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)

Abstract

The lambda-calculus possesses a strong notion of extensionality, called "the omega-rule", which has been the subject of many investigations. It is a longstanding open problem whether the equivalence obtained by closing the theory of Böhm trees under the omega-rule is strictly included in Morris's original observational theory, as conjectured by Sallé in the seventies. In a recent work, Breuvart et al. have shown that Morris's theory satisfies the omega-rule. In this paper we demonstrate that the two aforementioned theories actually coincide, thus disproving Sallé's conjecture.

Cite as

Benedetto Intrigila, Giulio Manzonetto, and Andrew Polonsky. Refutation of Sallé's Longstanding Conjecture. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 20:1-20:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{intrigila_et_al:LIPIcs.FSCD.2017.20,
  author =	{Intrigila, Benedetto and Manzonetto, Giulio and Polonsky, Andrew},
  title =	{{Refutation of Sall\'{e}'s Longstanding Conjecture}},
  booktitle =	{2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)},
  pages =	{20:1--20:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-047-7},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{84},
  editor =	{Miller, Dale},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.20},
  URN =		{urn:nbn:de:0030-drops-77236},
  doi =		{10.4230/LIPIcs.FSCD.2017.20},
  annote =	{Keywords: lambda calculus, observational equivalence, B\"{o}hm trees, omega-rule}
}

Search Results

Documents authored by Intrigila, Benedetto

Refutation of Sallé's Longstanding Conjecture

Abstract

Cite as

Thanks for your feedback!

Could not send message