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

TL;DR

This paper introduces an infinitary type system with a validity condition called approximability, providing a novel characterization of hereditary head-normalizing (HHN) lambda-terms, addressing Klop's HHN-problem.

Contribution

It develops an infinitary type system with approximability to characterize HHN lambda-terms, solving a longstanding open problem in lambda-calculus.

Findings

Infinitary type system characterizes HHN lambda-terms.

The system uses non-idempotent intersections.

It offers a new solution to Klop's HHN-problem.

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.