Infinitary Intersection Types as Sequences: a New Answer to Klop's Question
Logic in Computer Science
2016-10-21 v1
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.
Keywords
Cite
@article{arxiv.1610.06409,
title = {Infinitary Intersection Types as Sequences: a New Answer to Klop's Question},
author = {Pierre Vial},
journal= {arXiv preprint arXiv:1610.06409},
year = {2016}
}
Comments
32 pages