INFINITE MULTI-BASES

Abstract. Infinite multi-bases can have infinite and multiple type declarations for the same variable. They can be used as a proof-technique to manipulate only one common basis along the proof. However, no proper definition and precise study of typed lambda calculus with infinite multi-bases appear in the literature. This paper introduces type assignment systems with infinite multi-bases and studies the basic meta-theoretic properties. As an application of our study of multi-bases, we prove that a function on λ-terms satisfies the type semantics property if and only if this function defines a λ structure which coincides with the usual filter structure