# An explanation for Barendregt use of Y combinator in an equation

I am going through the following lecture notes on lambda calculus by Barendregt and Barendsen :

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

Here at page 12 , after introducing fixed point theorem a small exercise which is an attempt to prove the following has been posted : $\exists G \forall X$ $GX =SGX$.

It first proceeds to the implication

$Gx$ = $SGx$

which implies : $G$ = $\lambda x .SGx$

which implies : $G$ = $(\lambda gx.Sgx)G$

and then it concludes that :

$G$ = $Y$ $( \lambda g x.Sgx)$ where $Y$ is the fixed point combinator .

I am unable to figure out how was G found out to be $Y$ $( \lambda g x.Sgx)$ in the last step ? How was this conclusion reached up to ?

• Y satisfies the equation $Y f = f (Y f)$ for all $f$, and so $g=Yf$ solves $g = fg$ for all $f$. Commented Mar 4, 2018 at 2:13
• @YuvalFilmus : And f here would be $( \lambda gx.Sgx)$ ? Commented Mar 4, 2018 at 7:02
• Right, pattern matching would suggest that. Commented Mar 4, 2018 at 10:37
• The direction of implication is wrong: taking $G=YF$ implies $G=FG$, not the other way around. So, taking $G=Y\ldots$ is only one way to solve the requirement on $G$ (other solutions exist), but that's enough for the goal. All your uses of "implies" should instead be "is implied by".
– chi
Commented Mar 7, 2018 at 13:54
• @Chi : Yes , sorry for my mistake Commented Mar 10, 2018 at 18:40

The Y combinator satisfies the equation $Y f = f(Y f)$. Hence $g = Yf$ solves the equation $g = f g$. In your case, the function $f$ is $\lambda g x.Sgx$.
\begin{align} & G=Y(\lambda gx.Sgx) & (*)\\ & G=(\lambda gx.Sgx) Y (\lambda gx.Sgx) & \text{(by FPT (ii))} \\ & G=(\lambda gx.Sgx)G & \text{(by *)} \end{align} Therefore $$G=Y(\lambda gx.Sgx) \implies G=(\lambda gx.Sgx)G$$