# 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$. – Yuval Filmus Mar 4 '18 at 2:13
• @YuvalFilmus : And f here would be $( \lambda gx.Sgx)$ ? – Agnivesh Singh Mar 4 '18 at 7:02
• Right, pattern matching would suggest that. – Yuval Filmus Mar 4 '18 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 Mar 7 '18 at 13:54
• @Chi : Yes , sorry for my mistake – Agnivesh Singh Mar 10 '18 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$.