21–30 of 51 posts
One of my favorite programming videos: Jim Weirich on the Y Combinator https://www.youtube.com/watch?v=FITJMJjASUs
Thanks for letting me discover the work of that man. Its approach to learning about something by actually doing it really shines in the video you linked.
tl;dr A fixed point p for a function f, is a value so that f(p)=p. A semi-recursive function f is a like a recursive function, except that instead of invoking itself, it invokes some other function provided as an argument to f. The y-combinator (aka fixed-point-combinator) is a function, that for a function f, finds a fixed point for f. We can turn a semi-recursive function f into the corresponding recursive function…
This came as a shock to Church when he invented it as he wanted to use LC as a language for mathematical logic and fixed point combinators spell out doom for logical purposes. He thus invented the simply typed lambda calculus to banish such constructions.
Has the Y combinator been useful to anything? Has it been used in any software in a role other than pedagogic? It's a beautiful way to make a recursive call without binding the function to an identifier, but has it actually proven useful? It would seem that languages that allow that make it easy to use the Y combinator also typically make it easy to use named recursion with a permanent or a temporary name.
The Y-combinator was discovered originally as a flaw in the LC. It meant that you couldn't use LC as a logical language because you could form infinite loops which are not just not efficiently computable (in a sense, har har) but also correspond to vacuous logical statements like "If A proves A then A is true" which, in the context of rules like reflexivity "If A then A" (provable in LC as λ x . x) is logical nonsense.
To be more clear, here's the Y combinator
λ f . (λ x . f (x x)) (λ x . f (x x))
(λ x . (x x)) (λ x . (x x))
Anyway, Church worked for the next 4 years to invent the Simply Typed Lambda Calculus which imposes a Russell-like typing discipline on the LC in order to outlaw the Y-combinator. This made LC more useful for logic (and indeed STLC models Gentzen's Natural Deduction logical system) but it threw away its ability to compute any "recursively enumerable" function. That latter thing was what eventually came to be the definition of "efficiently computable" (after corroboration between Church's LC, Turing's Turing Machines invented the next year).
And now we happen to care about writing programs which, in general, may be r.e. and so we use either untyped LC or typed LC which has logically unsound recursion principles.
My page on lambda diagrams at http://www.cwi.nl/~tromp/cl/diagrams.html has a nice picture of the Y-combinator at the top, and this note at the bottom: The diagram in the title, produced by the postscript code below, is a slightly deformed alternative Y diagram made to look like a Y. %!PS-Adobe-2.0 EPSF-2.0 %%BoundingBox:0 0 118 110 /m{moveto}def/l{lineto}def/c{concat 6 m 0 6 l 7 8 m 0 8 l l l 3 6 l 2 6 m 7 6 l 3 4 m…
From The Little Schemer - http://www.ccs.neu.edu/home/matthias/BTLS/sample.pdf That chapter made me grok the Y Combinator.
Has the Y combinator been useful to anything? Has it been used in any software in a role other than pedagogic? It's a beautiful way to make a recursive call without binding the function to an identifier, but has it actually proven useful? It would seem that languages that allow that make it easy to use the Y combinator also typically make it easy to use named recursion with a permanent or a temporary name.
Well, in 1936 Church invented the LC in order to serve as a foundational logic for mathematics. This was around the time that Hilbert's Program was attempting to totally mechanize reasoning through rich logical languages and Church wanted to use LC to define the notion of "efficiently computable" which was part of Hilbert's specification. The Y-combinator was discovered originally as a flaw in the LC. It meant that y…
The line
6 * (if 3 == 0 then 1 else 1 * (YF)(1–1))
The previous line is 6 * (λx.(if x == 0 then 1 else x * (YF)(x–1)) 1) When replacing the x s with 1s, it replaces one of the x s with 1, but replaces the first one with 3.
My guess was that this was copied from the first version, and they just forgot to change one of the threes to a 1.
(that is, unless I misunderstood something, which is of course possible)
I think the line should be
6 * (if 1 == 0 then 1 else 1 * (YF)(1–1))
Has the Y combinator been useful to anything? Has it been used in any software in a role other than pedagogic? It's a beautiful way to make a recursive call without binding the function to an identifier, but has it actually proven useful? It would seem that languages that allow that make it easy to use the Y combinator also typically make it easy to use named recursion with a permanent or a temporary name.
Hey. You're completely missing it. The Y combinator shows that full general computation, including recursion and iteration, derives automatically and inevitably from just basic rewrite rules. Obviously it is too raw to be used directly. But if you design/implement any system with rewrite rules, you have provided indefinite power for recursions, and you have opened the Pandora box of undecidable-termination. This mean…
Sorry, I don't understand what that means.
Also, (lambda x: x(x))(lambda x: x(x)) already gives you an infinite loop, so why do you need a Y combinator to show non-termination? Once you have functions as first-class citizens that you can copy around, you've lost control of termination. Seems pretty intuitive. What's the specific contribution of the Y combinator?
Earlier quoted context omitted.
Hey. You're completely missing it. The Y combinator shows that full general computation, including recursion and iteration, derives automatically and inevitably from just basic rewrite rules. Obviously it is too raw to be used directly. But if you design/implement any system with rewrite rules, you have provided indefinite power for recursions, and you have opened the Pandora box of undecidable-termination. This mean…
I do use it directly. For example in Fexl I define the append function for lists as: \append=(@\append\x\y x y \h\t [h; append t y]) Where '@' is the Y-combinator. Note that there's no direct self-reference with the symbol "append" there. I could define it equivalently as: \append=(@\loop\x\y x y \h\t [h; loop t y])