Obviously, lambda calculus functions are not in general invertible. That is, there is no lambda function $V$ (for inVerse) such that $$ (V\; A)\; (A\; B) \to B $$ for every $A$ and $B$ such that $(A\; B)$ can be reduced to normal form. (The arrow means that when the left- and right-hand expressions are reduced to normal form, they are $\alpha$-equivalent.)

However, I'm interested in defining a function $R$ (for Reverse) such that $$ (R\; A\; B)\; (A\; B) \to B. \tag{1} $$ Intuitively, $R$ is a function that reverses the application of $A$ to $B$; unlike the inverse function, $R$ is told what $B$ is, and just has to return it. By itself this is trivial of course; $(\lambda x.(\lambda y.(\lambda z.y)))$ does the job.

However, I would also like $R$ to have another property. It follows from $(1)$ that $$ R\; (R\; A\; B)\; (A\; B)\; B \to (A\; B). $$ I would like to strengthen this to $$ R\; (R\; A\; B)\; (A\; B) \to A. \tag{2} $$ That is, I want the reverse of a reverse calculation to be the original function $A$, rather than just something that gives the same result when applied to $B$.

Is there a function $R$ that has both properties $(1)$ and $(2)$, whenever the reduction to normal form of $(A\;B)$ is possible? If so, what is it - and if not, how can this be shown?


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.