4
$\begingroup$

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?

$\endgroup$

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.