Document Open Access Logo

Observability for Pair Pattern Calculi

Authors Antonio Bucciarelli, Delia Kesner, Simona Ronchi Della Rocca

PDF

File

Thumbnail PDF
PDF
LIPIcs.TLCA.2015.123.pdf
  • Filesize: 0.51 MB
  • 15 pages

Document Identifiers

Subject Classification

Keywords
  • solvability
  • pattern calculi
  • intersection types
  • inhabitation

Metrics

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

Abstract

Inspired by the notion of solvability in the λ-calculus, we define a notion of observability for a calculus with pattern matching. We give an intersection type system for such a calculus which is based on non-idempotent types. The typing system is shown to characterize the set of terms having canonical form, which properly contains the set of observable terms, so that typability alone is not sufficient to characterize observability. However, the inhabitation problem associated with our typing system turns out to be decidable, a result which — together with typability — allows to obtain a full characterization of observability.

Cite As Get BibTex

Antonio Bucciarelli, Delia Kesner, and Simona Ronchi Della Rocca. Observability for Pair Pattern Calculi. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 123-137, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.TLCA.2015.123

Author Details

Antonio Bucciarelli
Delia Kesner
Simona Ronchi Della Rocca

References

  1. Thibaut Balabonski. On the implementation of dynamic patterns. In Eduardo Bonelli, editor, HOR, volume 49 of EPTCS, pages 16-30, 2010. Google Scholar
  2. Henk Barendregt. The Lambda Calculus: Its Syntax and Semantics, volume 103 of Studies in logic and the foundation of mathematics. North-Holland, Amsterdam, revised edition, 1984. Google Scholar
  3. Henk Barendregt, Mario Coppo, and Mariangiola Dezani-Ciancaglini. A filter lambda model and the completeness of type assignment. The Journal of Symbolic Logic, 48(4):931-940, 1983. Google Scholar
  4. C. Ben-Yelles. Type-assignment in the lambda-calculus; syntax and semantics. PhD thesis, University of Wales Swansea, 1979. Google Scholar
  5. Antonio Bucciarelli, Delia Kesner, and Simona Ronchi Della Rocca. The inhabitation problem for non-idempotent intersection types. In Josep Díaz, Ivan Lanese, and Davide Sangiorgi, editors, TCS, LNCS. Springer, 2014. To appear. Google Scholar
  6. Serenella Cerrito and Delia Kesner. Pattern matching as cut elimination. Theoretical Computer Science, 323(1-3):71-127, 2004. Google Scholar
  7. Horatiu Cirstea, Germain Faure, and Claude Kirchner. A rho-calculus of explicit constraint application. Higher-Order and Symbolic Computation, 20(1-2):37-72, 2007. Google Scholar
  8. Daniel de Carvalho. Execution time of lambda-terms via denotational semantics and intersection types. CoRR, abs/0905.4251, 2009. Google Scholar
  9. J. Roger Hindley. Basic Simple Type Theory. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Amsterdam, 2008. Google Scholar
  10. Barry Jay and Delia Kesner. First-class patterns. Journal of Functional Programming, 19(2):191-225, 2009. Google Scholar
  11. Wolfram Kahl. Basic pattern matching calculi: A fresh view on matching failure. In Yukiyoshi Kameyama and Peter Stuckey, editors, FLOPS, volume 2998 of LNCS, pages 276-290. Springer, 2004. Google Scholar
  12. Jan-Willem Klop, Vincent van Oostrom, and Roel de Vrijer. Lambda calculus with patterns. Theoretical Computer Science, 398(1-3):16-31, 2008. Google Scholar
  13. Jean Louis Krivine. Lambda-Calculus, Types and Models. Masson, Paris, and Ellis Horwood, Hemel Hempstead, 1993. Google Scholar
  14. Luca Paolini, Mauro Piccolo, and Simona Ronchi Della Rocca. Logical relational lambda-models. To appear in Mathematical Structures in Computer Science. Google Scholar
  15. Barbara Petit. A polymorphic type system for the lambda-calculus with constructors. In Pierre-Louis Curien, editor, Typed Lambda Calculi and Applications, 9th International Conference, TLCA 2009, Brasilia, Brazil, July 1-3, 2009. Proceedings, volume 5608 of Lecture Notes in Computer Science, pages 234-248. Springer, 2009. Google Scholar
  16. Simon Peyton-Jones. The Implementation of Functional Programming Languages. Prentice-Hall, Inc., 1987. Google Scholar
  17. Pawel Urzyczyn. The emptiness problem for intersection types. Journal of Symbolic Logic, 64(3):1195-1215, 1999. Google Scholar
  18. Vincent van Oostrom. Confluence by decreasing diagrams. Theoretical Computer Science, 126(2):259–280, 1994. 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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact