Generalized filter models

摘要

In this paper, starting fi om filters which are a natural generalization of intersection filters (Barendregt et al., J. Symbolic Logic 48 (1983) 931-940), the existence of filter models and filter semimodels for the lambda-calculus is investigated. The construction of filters is based on a Z-semilattice of types in which the subsets having infimum are given by a collection Z, called subset system. The set of representable functions is characterized in the obtained domain. In the case where the properties of the subset system Z guarantee the existence of a filter model, the proof of soundness and completeness of the associated natural Z-type assignment system is routine. (C) 2000 Elsevier Science B.V. All rights reserved. [References: 24]