2
$\begingroup$

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 ).

$\endgroup$
3
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ : The last expression will give $ ( \lambda x. GG) X $ , right ? This will result in $GG$ if $x$ is not there in G right ? $\endgroup$ – Agnivesh Singh Mar 11 '18 at 9:08
  • $\begingroup$ @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. $\endgroup$ – chi Mar 11 '18 at 10:05

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.