Infinitary Intersection Types as Sequences: a New Answer to Klop's Question

2016/10/20 by Vial, Pierre
#FOS: Computer and information sciences #Logic in Computer Science (cs.LO)

paper · doi:10.48550/arxiv.1610.06409

Abstract

We provide a type-theoretical characterization of weakly-normalizing terms in an infinitary lambda-calculus. We adapt for this purpose the standard quantitative (with non-idempotent intersections) type assignment system of the lambda-calculus to our infinite calculus. Our work provides a new answer to Klop's HHN-problem, namely, finding out if there is a type system characterizing the hereditary head-normalizing (HHN) lambda-terms. Tatsuta showed that HHN could not be characterized by a finite type system. We prove that an infinitary type system endowed with a validity condition called approximability can achieve it.

Related

• Sequence Types and Infinitary Semantics
• Strong normalization through idempotent intersection types: a new syntactical approach
• Strict Ideal Completions of the Lambda Calculus
• All the λ-Terms are Meaningful for the Infinitary Relational Model
• Intersection Types for the Computational lambda-Calculus