Abstract
Many concrete
notions of function application, suitable for interpreting typed lambda
calculi with recursive types, have been introduced in the literature. These
arise in different fields such as set theory, multiset theory, type theory
and functor theory and are apparently unrelated. In this paper we introduce
the general concept of applicative exponential structure and show that
it subsumes all these notions. Our approach is based on a generalization
of the notion of intersection type. We construe all these structures in
a finitary way, so as to be able to utilize uniformly a general form of
type assignment system for defining the interpretation function. Applicative
exponential structures are just combinatory algebras, in general. Our approach
suggests a wide variety of entirely new concrete notions of function application;
e.g. in connection with boolean sets. Applicative exponential structures
can be used for modeling various forms of non- deterministic operators.