3 ms·

It's pretty, but Mogensen's self-evaluator E = Y(\e m.m (\x.x) (\m n.(e m)(e n)) (\m v.e (m v))) is probably easier to remember :) I thank Ben Lynn for in

It's pretty, but Mogensen's self-evaluator E = Y(\e m.m (\x.x) (\m n.(e m)(e n)) (\m v.e (m v))) is probably easier to remember :) I thank Ben Lynn for introducing me to it on https://crypto.stanford.edu/~blynn/lambda/ https://crypto.stanford.edu/~blynn/lambda/ Just in case people mistakenly assume Lisp is in some way more practical, please checkout https://crypto.stanford.edu/~blynn/compiler/ https://crypto.stanford.edu/~blynn/compiler/

tromp 5y ago
It's not quite comparable though, as mine operates on a simple bit stream (akin to stdin), which it needs to tokenize and parse. Mogensen's one is more like the LISP interpreter that operates on a quoted form of the term it evaluates to.
Joker_vD 5y ago
Now all you need is to remember what Y is: it's pretty much the Russell's paradox in the shape of a function! If you represent a set as indicator function, then the Russell's set R = \x. N (x x), where N is logical negation. Now let's ask it whether it's a member of itself, and you get (\x. N (x x)) (\x. N (x x)), which essentially tries to find a fix-point of logical negation (and tragically, diverges in the process). Now abstract N away, and you have the fully general Y you know and love: \f. (\x. f (x x)) (\x. f (x x)) I've seen this trick just this morning at [0], and I am absolutely enchanted with this observation. [0] http://c9x.me/notes/2015-06-02.html http://c9x.me/notes/2015-06-02.html
- kmill 5y ago
  This cool observation is generalized in Lawvere's fixed point theorem[1]. It basically says that whenever you have an "interpreter" I : A -> (A -> B) that takes elements of A and turns them into functions A -> B, then if every such function is realized by some element of A (i.e., I is surjective) then any given function f : B -> B has a fixed point. The fixed point can be constructed by (1) letting q = \(a:A), f (I a a), which is a function A -> B, (2) letting p:A be something for which I p = q, then (3) letting s = I p p, which is the fixed point of f. For sets, the way Russell's paradox appears is this: letting Set be the class of all sets, then every set x determines a predicate, which is a function Set -> Bool that for each x returns true or false depending on whether or not y is an element of x. Have I : Set -> (Set -> Bool) be the function that takes a set and turns it into a predicate: I x = \y, y ∈ x. An axiom of set theory (extensionality) is that I is injective. What if I were also surjective? (This is the non-axiom "unrestricted comprehension", that every predicate determines a set.) Well, then we could apply the fixed point theorem to negation N : Bool -> Bool, but N obviously doesn't have a fixed point! (Using the above notation, q = \y, N (y ∈ y) is the predicate that checks whether a set doesn't contain itself, p = {y | N (y ∈ y)} is the supposed set of all sets that don't contain themselves, and s = (p ∈ p) is the impossible fixed point for N.) Here's what the theorem says for lambda calculus. Suppose L is the set of all lambda expressions (where equivalent lambda expressions are equal). In lambda calculus, every expression is also a function, in the sense that if E is an expression then \x, E x is equivalent, so we can have an "interpreter" I : E -> (E -> E) be the identity function. The fixed point theorem says that if you have a function f : L -> L, then it has a fixed point. And what is it? Tracing through the construction, we see it's nothing other than \x, (f x x) (f x x)! (The complexity in stating the theorem precisely is to be able to restrict what we mean by functions A -> B. For the lambda calculus example, we need E -> E to mean just the functions realizable as lambda expressions. This does work out because reflexive objects exist[2].) [1] https://ncatlab.org/nlab/show/Lawvere%27s+fixed+point+theorem https://ncatlab.org/nlab/show/Lawvere%27s+fixed+point+theore... [2] https://ncatlab.org/nlab/show/reflexive+object https://ncatlab.org/nlab/show/reflexive+object
  - kmill 5y ago
    (A mistake above: it should be "we see it's nothing other than (\x, f (x x)) (\x, f (x x))") While we're here, another cool application is that quines exist. I'll give a way that misuses the theorem (though in a correctable way) to derive a quine. Consider the meta-function quote : L -> L that takes a lambda expression and produces a representation of it (like the representation used by the self-interpreter two comments up). I say meta-function because this isn't implemented by a lambda expression itself. Applying the fixed-point theorem to the same I : L -> (L -> L) with quote, if it were an actual lambda expression, we'd get a lambda expression s with s = quote s. That is, the expression s would evaluate to its own representation! The fixed point is purportedly (\x, quote (x x)) (\x, quote (x x)), which doesn't make sense since quote is not a function. However, suppose q is a lambda expression that takes representations of lambda expressions and quotes those, so it satisfies the equation q (quote x) = quote (quote x) for all lambda expressions x. Also, let app : L -> L -> L be the constructor for application. Then (\x, q (app x (q x))) (quote (\x, q (app x (q x)))) fixes the problems and is a quine: (\x, q (app x (q x))) (quote (\x, q (app x (q x)))) = q (app (quote (\x, q (app x (q x)))) (q (quote (\x, q (app x (q x)))))) = quote ((\x, q (app x (q x))) (quote (\x, q (app x (q x))))) (A way to do this all above board is to use the self-interpreter and somehow use q in the thing we're trying to find a fixed point of.)

tromp 5y ago

It's not quite comparable though, as mine operates on a simple bit stream (akin to stdin), which it needs to tokenize and parse. Mogensen's one is more like the LISP interpreter that operates on a quoted form of the term it evaluates to.

Joker_vD 5y ago

Now all you need is to remember what Y is: it's pretty much the Russell's paradox in the shape of a function! If you represent a set as indicator function, then the Russell's set R = \x. N (x x), where N is logical negation. Now let's ask it whether it's a member of itself, and you get (\x. N (x x)) (\x. N (x x)), which essentially tries to find a fix-point of logical negation (and tragically, diverges in the process). Now abstract N away, and you have the fully general Y you know and love: \f. (\x. f (x x)) (\x. f (x x)) I've seen this trick just this morning at [0], and I am absolutely enchanted with this observation. [0] http://c9x.me/notes/2015-06-02.html http://c9x.me/notes/2015-06-02.html

kmill 5y ago
This cool observation is generalized in Lawvere's fixed point theorem[1]. It basically says that whenever you have an "interpreter" I : A -> (A -> B) that takes elements of A and turns them into functions A -> B, then if every such function is realized by some element of A (i.e., I is surjective) then any given function f : B -> B has a fixed point. The fixed point can be constructed by (1) letting q = \(a:A), f (I a a), which is a function A -> B, (2) letting p:A be something for which I p = q, then (3) letting s = I p p, which is the fixed point of f. For sets, the way Russell's paradox appears is this: letting Set be the class of all sets, then every set x determines a predicate, which is a function Set -> Bool that for each x returns true or false depending on whether or not y is an element of x. Have I : Set -> (Set -> Bool) be the function that takes a set and turns it into a predicate: I x = \y, y ∈ x. An axiom of set theory (extensionality) is that I is injective. What if I were also surjective? (This is the non-axiom "unrestricted comprehension", that every predicate determines a set.) Well, then we could apply the fixed point theorem to negation N : Bool -> Bool, but N obviously doesn't have a fixed point! (Using the above notation, q = \y, N (y ∈ y) is the predicate that checks whether a set doesn't contain itself, p = {y | N (y ∈ y)} is the supposed set of all sets that don't contain themselves, and s = (p ∈ p) is the impossible fixed point for N.) Here's what the theorem says for lambda calculus. Suppose L is the set of all lambda expressions (where equivalent lambda expressions are equal). In lambda calculus, every expression is also a function, in the sense that if E is an expression then \x, E x is equivalent, so we can have an "interpreter" I : E -> (E -> E) be the identity function. The fixed point theorem says that if you have a function f : L -> L, then it has a fixed point. And what is it? Tracing through the construction, we see it's nothing other than \x, (f x x) (f x x)! (The complexity in stating the theorem precisely is to be able to restrict what we mean by functions A -> B. For the lambda calculus example, we need E -> E to mean just the functions realizable as lambda expressions. This does work out because reflexive objects exist[2].) [1] https://ncatlab.org/nlab/show/Lawvere%27s+fixed+point+theorem https://ncatlab.org/nlab/show/Lawvere%27s+fixed+point+theore... [2] https://ncatlab.org/nlab/show/reflexive+object https://ncatlab.org/nlab/show/reflexive+object
- kmill 5y ago
  (A mistake above: it should be "we see it's nothing other than (\x, f (x x)) (\x, f (x x))") While we're here, another cool application is that quines exist. I'll give a way that misuses the theorem (though in a correctable way) to derive a quine. Consider the meta-function quote : L -> L that takes a lambda expression and produces a representation of it (like the representation used by the self-interpreter two comments up). I say meta-function because this isn't implemented by a lambda expression itself. Applying the fixed-point theorem to the same I : L -> (L -> L) with quote, if it were an actual lambda expression, we'd get a lambda expression s with s = quote s. That is, the expression s would evaluate to its own representation! The fixed point is purportedly (\x, quote (x x)) (\x, quote (x x)), which doesn't make sense since quote is not a function. However, suppose q is a lambda expression that takes representations of lambda expressions and quotes those, so it satisfies the equation q (quote x) = quote (quote x) for all lambda expressions x. Also, let app : L -> L -> L be the constructor for application. Then (\x, q (app x (q x))) (quote (\x, q (app x (q x)))) fixes the problems and is a quine: (\x, q (app x (q x))) (quote (\x, q (app x (q x)))) = q (app (quote (\x, q (app x (q x)))) (q (quote (\x, q (app x (q x)))))) = quote ((\x, q (app x (q x))) (quote (\x, q (app x (q x))))) (A way to do this all above board is to use the self-interpreter and somehow use q in the thing we're trying to find a fixed point of.)