Approximation Theorems for intersection Type Systems

摘要

In this paper we prove that many intersection type theories of interest (including those which induce as filter models, Scott's and Park's D_∞ models, the models studied in Barendregt Coppo Dezani, Abramsky Ong, and Honsell Ronchi) satisfy an Approximation Theorem with respect to a suitable notion of approximant. This theorem implies That a λ-term has a type if an only if there exists an approximant of that term which has that type. We prove this Result uniformly for all the intersection type theories under consideration using a Kripke version of stable sets where Bases correspond to worlds.