# Characterisation of the BCIW definable functions

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.)

• I'm pretty sure no one has looked at this particular question. However, in game semantics there has been quite a bit of work on full abstraction for systems related to linear logic (ie, the BCK combinators), which typically proceeds by a definability result followed by a quotienting (extensional collapse). Maybe see Abramsky, Jagadeesan and Malacaria's Full Abstraction for PCF, or Hyland and Ong's On Full Abstraction for PCF? – Neel Krishnaswami Sep 12 '16 at 16:24
• Thanks, I'll look into this. Linear logic corresponds to the BCI combinators, I believe, which is pretty close to the thing I'm looking for. – Andrew Bacon Sep 12 '16 at 19:36