<p>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 <a href="http://homepages.inf.ed.ac.uk/gdp/publications/logical_relations_1973.pdf"> here</a>.)</p>

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

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

CC BY-SA 3.0
2016-09-12T16:24:59.110Z
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
CC BY-SA 3.0
2016-09-12T19:36:13.230Z
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
<lambda-calculus><combinatory-logic><typed-lambda-calculus><logical-relations>
Characterisation of the BCIW definable functions
Andrew Bacon
# Characterisation of the BCIW definable functions

(Asked by: username_0 on 2016-09-09)

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](http://homepages.inf.ed.ac.uk/gdp/publications/logical_relations_1973.pdf).)

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

**Tags:** lambda-calculus, combinatory-logic, typed-lambda-calculus, logical-relations
> **Comments:**
> **username_1**: 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*?  
> **username_0**: 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.  

---

## 0 answers

