Document Open Access Logo

Refutation of Sallé's Longstanding Conjecture

Authors Benedetto Intrigila, Giulio Manzonetto, Andrew Polonsky

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2017.20.pdf
  • Filesize: 1.08 MB
  • 18 pages

Document Identifiers

Author Details

Benedetto Intrigila
Giulio Manzonetto
Andrew Polonsky

Cite As Get BibTex

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) https://doi.org/10.4230/LIPIcs.FSCD.2017.20

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.

Subject Classification

Keywords
  • lambda calculus
  • observational equivalence
  • Böhm trees
  • omega-rule

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Hendrik P. Barendregt. Some extensional term models for combinatory logics and λ-calculi. Ph.D. thesis, Utrecht Universiteit, the Netherlands, 1971. Google Scholar
  2. Hendrik P. Barendregt. The lambda calculus, its syntax and semantics. Number 103 in Studies in Logic and the Foundations of Mathematics. North-Holland, second edition, 1984. Google Scholar
  3. Hendrik P. Barendregt, Jan A. Bergstra, Jan Willem Klop, and Henri Volken. Degrees of sensible lambda theories. Journal of Symbolic Logic, 43(1):45-55, 1978. Google Scholar
  4. Flavien Breuvart. On the characterization of models of ℋ^*. In Tom Henzinger and Dale Miller, editors, CSL-LICS'14, pages 24:1-24:10. ACM, 2014. Google Scholar
  5. Flavien Breuvart, Giulio Manzonetto, Andrew Polonsky, and Domenico Ruoppolo. New results on Morris’s observational theory. In Delia Kesner and Brigitte Pientka, editors, Formal Structures for Computation and Deduction, volume 52 of LIPIcs, pages 15:1-15:18. Schloss Dagstuhl, 2016. Google Scholar
  6. Matt Brown and Jens Palsberg. Breaking through the normalization barrier: a self-interpreter for F-omega. In Rastislav Bodík and Rupak Majumdar, editors, Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, pages 5-17. ACM, 2016. Google Scholar
  7. Mario Coppo, Mariangiola Dezani-Ciancaglini, and Patrick Sallé. Functional characterization of some semantic equalities inside lambda-calculus. In Hermann A. Maurer, editor, Automata, Languages and Programming, volume 71 of Lecture Notes in Computer Science, pages 133-146. Springer, 1979. Google Scholar
  8. Mario Coppo, Mariangiola Dezani-Ciancaglini, and Maddalena Zacchi. Type theories, normal forms and 𝒟_∞-lambda-models. Information and Computation, 72(2):85-116, 1987. Google Scholar
  9. Pietro Di Gianantonio, Gianluca Franco, and Furio Honsell. Game semantics for untyped λβη-calculus. In Typed Lambda Calculi and Applications, volume 1581 of Lecture Notes in Computer Science, pages 114-128. Springer, 1999. Google Scholar
  10. Thomas Given-Wilson and Barry Jay. A combinatory account of internal structure. J. Symb. Log., 76(3):807-826, 2011. Google Scholar
  11. Xavier Gouy. Étude des théories équationnelles et des propriétés algébriques des modèles stables du λ-calcul. Thèse de doctorat, Université de Paris 7, 1995. Google Scholar
  12. Martin Hyland. A survey of some useful partial order relations on terms of the λ-calculus. In Lambda-Calculus and Computer Science Theory, volume 37 of Lecture Notes in Computer Science, pages 83-95. Springer, 1975. Google Scholar
  13. Martin Hyland. A syntactic characterization of the equality in some models for the λ-calculus. Journal London Mathematical Society (2), 12(3):361-370, 1975/76. Google Scholar
  14. Benedetto Intrigila and Monica Nesi. On structural properties of η-expansions of identity. Inf. Proc. Lett., 87(6):327-333, 2003. Google Scholar
  15. Benedetto Intrigila and Richard Statman. The omega rule is Π₂⁰-hard in the λβ-calculus. In Symposium on Logic in Computer Science (LICS 2004), pages 202-210. IEEE Computer Society, 2004. Google Scholar
  16. Benedetto Intrigila and Richard Statman. The omega rule is Π¹₁-complete in the λβ-calculus. Logical Methods in Computer Science, 5(2), 2009. Google Scholar
  17. Jean-Jacques Lévy. Approximations et arbres de Böhm dans le lambda-calcul. In Bernard Robinet, editor, Lambda Calcul et Sémantique formelle des langages de programmation, Actes de la 6ème École de printemps d'Informatique théorique, La Châtre, LITP-ENSTA, pages 239-257, 1978. (In French). Google Scholar
  18. Stefania Lusin and Antonino Salibra. The lattice of λ-theories. Journal of Logic and Computation, 14(3):373-394, 2004. Google Scholar
  19. Giulio Manzonetto. A general class of models of ℋ^*. In Rastislav Královic and Damian Niwinski, editors, Mathematical Foundations of Computer Science 2009, volume 5734 of Lecture Notes in Computer Science, pages 574-586. Springer, 2009. Google Scholar
  20. Giulio Manzonetto and Domenico Ruoppolo. Relational graph models, Taylor expansion and extensionality. Electronic Notes in Theoretical Computer Science, 308:245-272, 2014. Google Scholar
  21. Torben Æ. Mogensen. Efficient self-interpretations in lambda calculus. J. Funct. Program., 2(3):345-363, 1992. Google Scholar
  22. James H. Morris. Lambda calculus models of programming languages. PhD thesis, Massachusetts Institute of Technology, 1968. Google Scholar
  23. Gordon D. Plotkin. The lambda-calculus is ω-incomplete. Journal of Symbolic Logic, 39(2):313-317, 1974. Google Scholar
  24. Andrew Polonsky. Axiomatizing the Quote. In Marc Bezem, editor, Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL, volume 12 of Leibniz International Proceedings in Informatics (LIPIcs), pages 458-469, Dagstuhl, Germany, 2011. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. Google Scholar
  25. Simona Ronchi Della Rocca and Luca Paolini. The Parametric λ-Calculus: a Metamodel for Computation. EATCS Series. Springer, Berlin, 2004. Google Scholar
  26. Patrick Sallé. Une extension de la théorie des types en λ-calcul. In Giorgio Ausiello and Corrado Böhm, editors, Automata, Languages and Programming: Fifth Colloquium, Udine, Italy, July 17-21, 1978, pages 398-410. Springer Berlin Heidelberg, 1978. Google Scholar
  27. Dana S. Scott. Continuous lattices. In Lawvere, editor, Toposes, Algebraic Geometry and Logic, volume 274 of Lecture Notes in Mathematics, pages 97-136. Springer, 1972. Google Scholar
  28. Paula Severi and Fer-Jan de Vries. An extensional Böhm model. In Sophie Tison, editor, Rewriting Techniques and Applications: 13th International Conference, RTA 2002, pages 159-173. Springer Berlin Heidelberg, 2002. Google Scholar
  29. Paula Severi and Fer-Jan de Vries. The infinitary lambda calculus of the infinite η-Böhm trees. Mathematical Structures in Computer Science, 27(5):681-733, 2017. Google Scholar
  30. Christopher P. Wadsworth. The relation between computational and denotational properties for Scott’s 𝒟_∞-models of the lambda-calculus. SIAM Journal of Computing, 5(3):488-521, 1976. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact