Document Open Access Logo

Sequence Types for Hereditary Permutators

Author Pierre Vial

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2019.33.pdf
  • Filesize: 0.57 MB
  • 15 pages

Document Identifiers

Author Details

Pierre Vial
  • Inria, Nantes, France

Funding

This research has been partially funded by the CoqHoTT ERC Grant 637339.

Cite AsGet BibTex

Pierre Vial. Sequence Types for Hereditary Permutators. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 33:1-33:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.FSCD.2019.33

Abstract

The invertible terms in Scott’s model D_infty are known as the hereditary permutators. Equivalently, they are terms which are invertible up to beta eta-conversion with respect to the composition of the lambda-terms. Finding a type-theoretic characterization to the set of hereditary permutators was problem # 20 of TLCA list of problems. In 2008, Tatsuta proved that this was not possible with an inductive type system. Building on previous work, we use an infinitary intersection type system based on sequences (i.e., families of types indexed by integers) to characterize hereditary permutators with a unique type. This gives a positive answer to the problem in the coinductive case.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
Keywords
  • hereditary permutators
  • Böhm trees
  • intersection types
  • coinduction
  • ridigity
  • sequence types
  • non-idempotent intersection

Metrics

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

References

  1. Patrick Bahr. Strict Ideal Completions of the Lambda Calculus. In FSCD 2018, July 9-12, Oxford, pages 8:1-8:16, 2018. Google Scholar
  2. Henk Barendregt. The Lambda-Calculus: Its Syntax and Sematics. Ellis Horwood series in computers and their applications. Elsevier, 1985. Google Scholar
  3. Jan A. Bergstra and Jan Willem Klop. Invertible Terms in the Lambda Calculus. Theor. Comput. Sci., 11:19-37, 1980. Google Scholar
  4. Antonio Bucciarelli, Delia Kesner, and Daniel Ventura. Non-Idempotent Intersection Types for the Lambda-Calculus. Mathematical Structures in Computer Science., 2017. Google Scholar
  5. Daniel De Carvalho. Sémantique de la logique linéaire et temps de calcul. PhD thesis, Université Aix-Marseille, November 2007. Google Scholar
  6. Mario Coppo and Mariangiola Dezani-Ciancaglini. An extension of the basic functionality theory for the λ-calculus. Notre Dame Journal of Formal Logic, 4:685-693, 1980. Google Scholar
  7. Haskell B. Curry and Robert Feys. Combinatory Logic, volume I. North-Holland Co., Amsterdam, 1958. (3rd edn. 1974). Google Scholar
  8. Lukasz Czajka. A Coinductive Confluence Proof for Infinitary Lambda-Calculus. In Rewriting and Typed Lambda Calculi - Joint International Conference, RTA-TLCA, Vienna, Austria, July 14-17, pages 164-178, 2014. Google Scholar
  9. Mariangiola Dezani-Ciancaglini. Characterization of Normal Forms Possessing Inverse in the lambda-beta-eta-Calculus. Theor. Comput. Sci., 2(3):323-337, 1976. Google Scholar
  10. Philippa Gardner. Discovering Needed Reductions Using Type Theory. In TACS, Sendai, 1994. Google Scholar
  11. Richard Kennaway, Jan Willem Klop, M. Ronan Sleep, and Fer-Jan de Vries. Infinitary Lambda Calculus. Theor. Comput. Sci., 175(1):93-125, 1997. Google Scholar
  12. Betti Venneri Mario Coppo, Mariangiola Dezani-Ciancaglini. Functional Characters of Solvable Terms. Mathematical Logic Quarterly, 27:45–58, 1981. Google Scholar
  13. Makoto Tatsuta. Types for Hereditary Head Normalizing Terms. In FLOPS, Ise, Japan, April 14-16, pages 195-209, 2008. Google Scholar
  14. Makoto Tatsuta. Types for Hereditary Permutators. In LICS, 24-27 June, Pittsburgh, pages 83-92, 2008. Google Scholar
  15. Steffen van Bakel. Complete Restrictions of the Intersection Type Discipline. Theor. Comput. Sci., 102(1):135-163, 1992. Google Scholar
  16. Steffen van Bakel. Intersection Type Assignment Systems. Theor. Comput. Sci., 151(2):385-435, 1995. Google Scholar
  17. Pierre Vial. Infinitary intersection types as sequences: a new answer to Klop’s problem. In LICS, Reykjavik, 2017. Google Scholar
  18. Pierre Vial. Non-Idempotent Typing Operator, beyond the Lambda-Calculus. Phd thesis, Université Sorbonne Paris-Cité, 2017, available on URL: http://www.irif.fr/~pvial.
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 Imprint Privacy Contact