# Trying to verify the solution to a lambda calculus equation

I am going through the following introduction to lambda calculus :

http://www.cse.chalmers.se/research/group/logic/TypesSS05/Extra/geuvers.pdf

At page 12 , the following has been asked to prove

$\exists$ $G$ $\forall X$ such that

$GX$ = $GG$

This means to find a function which takes a function as an argument and returns the same expression irrespective of the function .

The book posits the solution to be $G$ = $Y$ $( \lambda gx. gg)$

On trying to verify this I first evaluated the L.H.S to be

$GX$ = $Y ( \lambda gx.gg )$ $X$.

Now $X$ being the argument will be picked up by the first bound variable so .

$L.H.S$ = $Y ( \lambda x . XX)$ = $( \lambda x . XX)$ $Y ( \lambda x . XX)$ = $Y ( \lambda x .$ $Y ( \lambda x . XX)$ $Y ( \lambda x . XX)$)

Here due to the presence of the form $YF$ , I can carry on the reduction continuously by replacinf $YF$ with $FYF$

$R.H.S$ = $Y$ $( \lambda gx. gg)$ $Y$ $( \lambda gx. gg)$ = $Y$$\lambda x. ( Y( \lambda gx. gg) Y( \lambda gx. gg)) Now similarly the reduction can be carried on further by again consuming the first g that comes in the expression with Y( \lambda gx. gg)) and this can on perpetually and it will look like Y ( \lambda x . Y ( \lambda x . XX) Y ( \lambda x . XX))..... So I couldn't completely ascertain that they ( L.H.S and R.H.S) will turn out to be equal but I can see that L.H.S and R.H.S are going to be infinitely long and will resemble each other more and more as the number of reductions go on since the g 's in the R.H.S will continually get replaced . Is this logic correct ? If not , where did I err ? P.S. : On a general and on a lighter note , how are this lambda calculus equations solved ? (They look analogous to differential equations ). ## 1 Answer On trying to verify this I first evaluated the L.H.S to be GX = Y ( \lambda gx.gg ) X. Now X being the argument will be picked up by the first bound variable so . L.H.S = Y ( \lambda x . XX) This is where you went wrong, and the reason is that you've got the association the wrong way round. Y ( \lambda gx.gg ) X means (Y ( \lambda gx.gg )) X. Taking that into account, the only evaluation step possible is to apply Y, giving$$( \lambda gx.gg )(Y ( \lambda gx.gg )) X$$which is$( \lambda gx.gg )GX$, from which the desired conclusion is immediate. • : The last expression will give$ ( \lambda x. GG) X $, right ? This will result in$GG$if$x$is not there in G right ? Mar 11 '18 at 9:08 • @AgniveshSingh Correct. There is no need to require "if$x$is not there in$G$" since we know that$x$is not free in$G\$, which is a closed term by definition.
– chi
Mar 11 '18 at 10:05