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

| cite | improve this answer | |
$\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$

| cite | improve this answer | |
$\endgroup$

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.