|
|
|
|
|
|
by youzicha
853 days 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.... |
|
|
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.