# Defining a calculation-reversing function in the lambda calculus

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?