The Y Combinator
mvanier.livejournal.com
mvanier.livejournal.com
How did the fixed point combinator come to be known as the Y combinator?
It's like the question: why do we use "x" to denote the unknown value in mathematics, most of the time?
[1] https://www.johndcook.com/blog/2014/02/06/schonfinkel-combin...
> Y because the letter Y has one stem which splits in two, just like what the function does. That’s probably the reason, or at least that’s how I look at it.
Then they resemble a λ.
factorial' self n =
if n == 0
then 1
else n * self self (n - 1)
factorial n = factorial' factorial' n
This technique is straightforwardly extended to the case of mutual recursion:
even' even odd n =
if n == 0
then True
else odd even odd (n - 1)
odd' even odd n =
if n == 0
then False
else even even odd (n - 1)
even n = even' even' odd' n
odd n = odd' even' odd' n fix f = f f
almost_factorial f n =
if n == 0
then 1
else n * f f (n - 1)
factorial = fix almost_factorial
fix f = (\x. x x) (\x. f (\y. x x y))
almost_factorial f n =
if n == 0
then 1
else n * f (n - 1)
factorial = fix almost_factorial
The only real problem is that in my approach the recursive calls look like "f closed_over_functions... new_args..." instead of "f new_args..." but that's what the compilers are for: this transformation is called "closure conversion" and is pretty straightforward. Sure, if you have to encode those things manually, then perhaps using Y is clearer and may even be the only option if you can't mess with the original definitions.
The neat thing about the Y-combinator is that it allows recursion to be defined in systems, such as the lambda calculus, which don't have naming and therefore a function can't refer to itself by name.
It's just that it seems there are not that many such systems used in practice except for "advanced type systems".
I agree that it's rarely justifiable to actually run a translated version of this code, but sometimes it gives you an easy proof of non-termination for some kind of formal system, which often gives you an easy proof of undecidability, which can save you a lot of time trying to figure out how to compute the uncomputable. Or it may persuade you that adding some feature to your design is a bad idea because it eliminates termination guarantees.
because the definition is not strongly typed.
Instead recursion must be added as an additional primitive to
the lambda calculus.
Could you use your Java code to define Factorial?
private static interface FuncToTFunc<T> {
Func<T> apply(FuncToTFunc<T> x);
}
Also is Func defined mutually recursively with FuncToFunc in excerpt below?
public static <T> Func<T> Y(final Func<Func<T>> r) {
return ((FuncToTFunc<T>) f -> f.apply(f))
.apply(
f -> r.apply(
x -> f.apply(f).apply(x)));
}FuncToFunc are defined recursively.
Interface Func doesn't refer to FuncToFunc in its declaration, and interface FuncToFunc doesn't refer to Func. The method Y does refer to those two interfaces, but it's declared later than those are, and they don't (and can't, acvtually) refer to it.
(Haskell)
anyType :: a
anyType = anyType
(Rust)
fn any_type<T>() -> T {
any_type()
}Extensions with a letrec-like construct are common, and are sometimes inaccurately called 'System F', but those languages do not have the properties of System F.
let fact' = ref (fun x -> x) in
let fact = fun n -> if n = 0 then 1 else n * !fact' (n-1) in
fact' := fact; fact 3