-1

How to show that $\underline{Y}f =_{\beta} f(\underline{Y}f)$ where $\underline{Y}$ is the usual Y combinator?

Thanks.

Logan Lee
  • 249
  • 1
    There are many fixed point combinators. Please, give the explicit definition of the $\lambda$-term $Y$, otherwise your question is meaningless. Moreover, what's the difference between $ Y$ and $\underline{Y}$? – Taroccoesbrocco Dec 02 '22 at 05:13
  • 1
    I wouldn't say this question is meaningless. Curry's $Y$ combinator is the first and pretty much the only fixed point combinator covered in undergraduate courses, and I think it's not very ambiguous to call it "the usual $Y$ combinator". Apart from this, I do agree that the $\underline{Y}$ is a bit confusing, and I wonder what they meant by that. – mell_o_tron Dec 02 '22 at 16:04

1 Answers1

0

I'm assuming that by "the usual $Y$ combinator" you mean Curry's fixed point combinator:

$$ Y = \lambda f . (\lambda x . f (x x)) (\lambda x. f(x x)) $$

The property $Y F \equiv_\beta F(Y F)$ can be proven as follows:

$$\begin{aligned} YF &\equiv_\beta^\star (\lambda x . F (x x)) (\lambda x. F(x x)) & (1)\\ &\equiv_\beta^\star F ((\lambda x . F (x x)) (\lambda x. F(x x)))& (2)\\ &\equiv F(YF)& (3) \end{aligned}$$

Where $\equiv_\beta^\star$ is the transitive and reflexive closure of the beta-reduction.

  1. The $Y$ combinator is applied to $F$
  2. The recursion happens; the first $(\lambda x. F(x x))$ is applied to the second, obtaining exactly the expression from (1), but "wrapped" inside an $F$.
  3. Since what we had before was equivalent to $YF$, the result is $F(YF)$.
mell_o_tron
  • 528