24 ms·
I prefer to start with two definitions and an assumption: Yf = f(Yf) for all [combinators] f, defines the desired behavior of Y Mx = xx for all [combinators]
by calcnerd256 17y ago
I prefer to start with two definitions and an assumption:
Yf = f(Yf) for all [combinators] f, defines the desired behavior of Y
Mx = xx for all [combinators] x (note that M then equals SII in SKI combinator calculus)
assume there exists a y such that My = Y
proceeding from there, I can derive Y without having to memorize it
- pkrumins 17y agoCan you show the derivation steps you take?
- calcnerd256 17y agoSure. Myf = f(Myf) yyf = f(yyf) Suppose yxf = f(xxf) for all x. Now y is simply (lambda x f . f(xxf)) Note that this doesn't get you the applicative-order version we want, but it does satisfy the definition of Y My = (lambda x . x x) (lambda x f . f (x x f)) = (lambda x f . f (x x f)) (lambda x f . f (x x f)) = (lambda f . f ((lambda a g . g (a a g)) (lambda a g . g (a a g)) f)) etc.