3 ms·

I think this binary lambda calculus self-interpreter might be more beautiful: ┬─┬ ────────────────────────────────────────────────────┬─┬── └─┤ ───────

• Y_Y 5y ago
  I thought the same thing, and was going to link to that same article. The paper giving the BLC self-interpreter is one of my favourite ever. For anyone interested in the graphical representation of terms like this I recommend To Dissect a Mockingbird: https://dkeenan.com/Lambda/ https://dkeenan.com/Lambda/
• FullyFunctional 5y ago
  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