Sequence Types for Hereditary Permutators
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.
hereditary permutators
Böhm trees
intersection types
coinduction
ridigity
sequence types
non-idempotent intersection
Theory of computation~Type theory
33:1-33:15
Regular Paper
This research has been partially funded by the CoqHoTT ERC Grant 637339.
Pierre
Vial
Pierre Vial
Inria, Nantes, France
10.4230/LIPIcs.FSCD.2019.33
Patrick Bahr. Strict Ideal Completions of the Lambda Calculus. In FSCD 2018, July 9-12, Oxford, pages 8:1-8:16, 2018.
Henk Barendregt. The Lambda-Calculus: Its Syntax and Sematics. Ellis Horwood series in computers and their applications. Elsevier, 1985.
Jan A. Bergstra and Jan Willem Klop. Invertible Terms in the Lambda Calculus. Theor. Comput. Sci., 11:19-37, 1980.
Antonio Bucciarelli, Delia Kesner, and Daniel Ventura. Non-Idempotent Intersection Types for the Lambda-Calculus. Mathematical Structures in Computer Science., 2017.
Daniel De Carvalho. Sémantique de la logique linéaire et temps de calcul. PhD thesis, Université Aix-Marseille, November 2007.
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.
Haskell B. Curry and Robert Feys. Combinatory Logic, volume I. North-Holland Co., Amsterdam, 1958. (3rd edn. 1974).
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.
Mariangiola Dezani-Ciancaglini. Characterization of Normal Forms Possessing Inverse in the lambda-beta-eta-Calculus. Theor. Comput. Sci., 2(3):323-337, 1976.
Philippa Gardner. Discovering Needed Reductions Using Type Theory. In TACS, Sendai, 1994.
Richard Kennaway, Jan Willem Klop, M. Ronan Sleep, and Fer-Jan de Vries. Infinitary Lambda Calculus. Theor. Comput. Sci., 175(1):93-125, 1997.
Betti Venneri Mario Coppo, Mariangiola Dezani-Ciancaglini. Functional Characters of Solvable Terms. Mathematical Logic Quarterly, 27:45–58, 1981.
Makoto Tatsuta. Types for Hereditary Head Normalizing Terms. In FLOPS, Ise, Japan, April 14-16, pages 195-209, 2008.
Makoto Tatsuta. Types for Hereditary Permutators. In LICS, 24-27 June, Pittsburgh, pages 83-92, 2008.
Steffen van Bakel. Complete Restrictions of the Intersection Type Discipline. Theor. Comput. Sci., 102(1):135-163, 1992.
Steffen van Bakel. Intersection Type Assignment Systems. Theor. Comput. Sci., 151(2):385-435, 1995.
Pierre Vial. Infinitary intersection types as sequences: a new answer to Klop’s problem. In LICS, Reykjavik, 2017.
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.
http://www.irif.fr/~pvial
Pierre Vial
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode