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

  • 1
    $\begingroup$ 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? $\endgroup$ Commented Sep 12, 2016 at 16:24
  • $\begingroup$ 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. $\endgroup$ Commented Sep 12, 2016 at 19:36


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.