3 ms·

I don't get it example shows that it's y(g)->g(y(g)), not the opposite...

• toxik 3y ago
  No, it shows that `Y g = g (Y g)`, so both ways.
  • ted_dunning 3y ago
    To clarify for people who are sloppy readers like me, the important difference here is the difference between `=` and `=>`, not the difference in notation between `Y(g)` and `Y g`.
• youzicha 3y ago
  Indeed. I think this something that people are often confused about, e.g. one blogger[0] comments: > The key to understanding the fixpoint theorem, for me anyway, was realizing that when it says FG=G, it does not mean that for every F there is a G such that by calling F with parameter G one can get back G. I mention this in the blog post, above. The equality operator in FG=G is the equivalence relation induced by the calculus rewriting relation: that is, it's the symmetric reflexive transitive closure of the rewriting step relation. When you look at the proof of the theorem, it actually works by constructing an expression G such that evaluating G produces, as an intermediate result, FG. There is no need for F to even be a function, and if F is a function it doesn't matter what, if anything, F would actually do when called, because the proof of the theorem doesn't involve calling F. I think the name "fixpoint combinator" is kindof bad, it it was called e.g. the "recursion combinator" I think people would find it more intuitive. [0] https://fexpr.blogspot.com/2013/07/bypassing-no-go-theorems.html?showComment=1385649732798#c4614180298503254427 https://fexpr.blogspot.com/2013/07/bypassing-no-go-theorems....
  • genezeta 3y ago
    The name, fixed point, is a more generic or general concept in mathematics. Given a function f, we say that an element c in the domain of f is a fixed point for f if it satisfies that f(c) = c. In a different nomenclature, if you consider f a "transformation", then c satisfies that it "remains fixed through the transformation". The fixed-point combinator is called so, because it "produces fixed-points for a function". That is, given a function f, then FPC(f) is a fixed-point for f. So, if we call c = FPC(f), then f(c) = c. Or, more classically f(FPC(f)) = FPC(f) or f(Y(f)) = Y(f). --- Note that when talking about fixed points in general, the domain of the f function is whatever -but usually you may have studied it with numbers-. But when talking about the fixed-point combinator the domain is functions themselves.
    • youzicha 3y ago
      Sure I understand that, but nevertheless I have seen at least 3 people who were confused in the same way. (c.f. https://youzicha.tumblr.com/post/728810860450136065 https://youzicha.tumblr.com/post/728810860450136065). I think the issue is that if you see an equation f(c) = c you think about trying to evaluate the function f at the point c, since that's what you do in almost all other situations involving a function call.
• svat 3y ago
  What do you mean by "the opposite"? In your notation, the example shows that Y(g) = g(Y(g)) which by the definition of the equals sign (A=B and B=A say the same thing), is the same as: g(Y(g)) = Y(g) — so Y(g) is a fixed point of g. What is the confusion?
  • konstantinua00 3y ago
    confusion in that if you treat lambda calculus as computation instead of "mathematical truths", then following the proof in the opposite direction requires conjuring out of thin air a complicated construction that isn't obvious from the state you'd have