Suppose that $M$ is a full model of the simply typed lambda calculus. Suppose each base type is infinite.

Now suppose that $f$ and $g$ are two functions in $M$ (not necessarily in the same domain) that are not definable by any pure term, and that $\alpha$ is a pure term of the $\lambda$-calculus such that: $$M(\alpha) g = f $$

My question is: when is it possible to find a pure term $\beta$ such that $$g=M(\beta)f$$

Are there easy to state necessary or sufficient conditions? I have been unable to find counterexamples when gs type complexity is higher than fs, so maybe that is a sufficient condition?

A couple of examples:

if $f$ is the converse of $g$: $$f=M(\lambda xyz. xzy)g$$ then we can find such a $\beta$ -- in this case, letting it also be $\lambda xyz. xzy$.

Similarly If $f$ is application to $a$: $$f = M(\lambda xy.yx)a$$ then $a$ is $f$ applied to $\lambda x.x$: $$a = M(\lambda y.y(\lambda x.x))f$$

Lastly, if $x$ is a variable in some base type and $f=M(\lambda xy.x)a$, then I don't think there is any pure term such that $a=M(\beta)f$.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.