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 and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.