Recent work on infinitary versions of the lambda calculus has shown that the infinite lambda calculus can be a useful tool to study the unsolvable terms of the classical lambda calculus. Working in the framework of the intersection type disciplines, we devise a type assignment system such that two terms are equal in the infinite lambda calculus iff they can be assigned the same types in any basis. A novel feature of the system is the presence of a type constant to denote the set of all terms of order zero, and the possibility of applying a type to another type. We prove a completeness and an approximation theorem for our system. Our results can be considered as a first step towards the goal of giving a denotational semantics for the lambda calculus which is suited for the study of the unsolvable terms. However, some noncontinuity phenomena of the infinite lambda calculus make a full realization construction of a filter model) a quite difficult task.
|Autori:||BERARDUCCI A; DEZANI-CIANCAGLINI M|
|Titolo:||INFINITE LAMBDA CALCULUS AND TYPES|
|Anno del prodotto:||1999|
|Digital Object Identifier (DOI):||10.1016/S0304-3975(98)00135-2|
|Appare nelle tipologie:||1.1 Articolo in rivista|