2
$\begingroup$

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 ?

$\endgroup$
5
  • $\begingroup$ Y satisfies the equation $Y f = f (Y f)$ for all $f$, and so $g=Yf$ solves $g = fg$ for all $f$. $\endgroup$ Commented Mar 4, 2018 at 2:13
  • $\begingroup$ @YuvalFilmus : And f here would be $( \lambda gx.Sgx) $ ? $\endgroup$ Commented Mar 4, 2018 at 7:02
  • $\begingroup$ Right, pattern matching would suggest that. $\endgroup$ Commented Mar 4, 2018 at 10:37
  • 1
    $\begingroup$ 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". $\endgroup$
    – chi
    Commented Mar 7, 2018 at 13:54
  • $\begingroup$ @Chi : Yes , sorry for my mistake $\endgroup$ Commented Mar 10, 2018 at 18:40

2 Answers 2

1
$\begingroup$

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

$\endgroup$
0
$\begingroup$

$$ \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$

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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