Given a full model of the simply typed lambda calculus, it's possible to characterise the lambda definable functions as those that are invariant under every "Kripke logical relation". (See here.)
I was wondering if anyone knows whether it is possible to give a similar characterisation of the functions definable in the $\lambda I$ calculus: the functions definable from $\lambda$ terms without vacuous $\lambda$ abstraction (or equivalently definable from the BCIW combinators).
A natural conjecture is that they are just the functions that are invariant under every "Routley-Meyer logical relation". (A Routley-Meyer frame is the analogue of the Kripke semantics for intuitionistic logic but for relevant logic --- the propositional logic axiomised by the types of the B, C, I and W combinators. World relative logical relations can be defined from them in a completely analogous way.)