4 ms·

There is. Using the Mogensen–Scott encoding, a self-interpreter can be written in lambda calculus as (λf.ff)(λf.λt.t(λx.x)(λm.λn.ffm(ffn))(λm.λv.ff(mv))), wh

There is. Using the Mogensen–Scott encoding, a self-interpreter can be written in lambda calculus as (λf.ff)(λf.λt.t(λx.x)(λm.λn.ffm(ffn))(λm.λv.ff(mv))), which is a direct translation of the equivalent Haskell code data Term t = Var t | App (Term t) (Term t) | Abs (t -> Term t) newtype Function = Function {apply :: Function -> Function} interpret :: Term Function -> Function interpret (Var x) = x interpret (App m n) = apply (interpret m) (interpret n) interpret (Abs m) = Function (\v -> interpret (m v)) https://en.wikipedia.org/wiki/Mogensen%E2%80%93Scott_encoding https://en.wikipedia.org/wiki/Mogensen%E2%80%93Scott_encodin...

kazinator 4y ago
I don't see what in the interpreter converts the lambda calculus into the Morgensen-Scott encoding. The Wikipedia page describes a "mse" function that is in some meta-language which is not lambda calculus. So first wee need a Lambda Calculus based interpreter for the meta-language, which can run this "mse" function. It looks like mse[x] is supposed to match a variable term, and mse[M N] matches a function application and so on. There are no such concepts and representations in lambda calculus, not to mention shape matching on them. The meta language might as well just be a paragraph of English: instructions on how to hand-compile the lambda calculus into a bunch of thunks which the interpreter can just invoke in certain ways to bring about the evaluation.
- tromp 4y ago
  You're claiming that LC cannot implement a quoting operator. Which is quite wrong. What you misunderstand is that a LC quote would not work on arbitrary lambda terms. A Mogensen quote operator would take a Mogensen encoding, and output a Mogensen encoding of that Mogensen encoding. Or a BLC quote operator would take a bitstring like 0010 which encodes the identity function λ 1, and output the blc encoding of the nil-terminated list of 4 booleans that represents that bitstring: 01000101100000110010110000011001011000001001011000001100101100000100000100000000101101110110
  - kazinator 4y ago
    > would take a Mogensen encoding obtained where? > output a Mogensen encoding of that Mogensen encoding That's not what a quote operator does; it does precisely nothing, yielding the argument formula without evaluating it. No encoding-of-encoding. Just the encoding. > output the blc encoding of the nil-terminated list of 4 booleans that represents that bitstring Where/how does that become λ 1 again?
    - tromp 4y ago
      > That's not what a quote operator does; it does precisely nothing, This is what gives Lisp murky semantics; you need something (quote) to do nothing, while having nothing (no quote) does something (evaluate). Lisp lacks referential transparency, even without the use of variables. An evaluated term can be evaluated again, yielding something different. > Where/how does that become λ 1 again? By decoding it, which is what mostly what the LC self-interpreter does, as detailed on pages 6,7 of [1]. [1] https://tromp.github.io/cl/LC.pdf https://tromp.github.io/cl/LC.pdf
      - kazinator 4y ago
        > An evaluated term can be evaluated again, yielding something different. Yes, and a Mogensen-Scott encoding can be Mogensen-Scott-encoded again, requiring two rounds of decoding, and so on. Multiple rounds of encoding and evaluation seem inescapable of you have the entanglement of homoiconicity. The quote operator in Lisp is designed exactly right. In mathematics there are literals like the number 3 or the set {}. These objects stand for themselves and are not understood as requiring any calculation: they just are. Symbols like x do not stand for themselves. If you want to talk about x literally as the symbol object, it is inescapable that there is some quoting operator to indicate that the usual semantics of x denoting something else do not apply. (Oxford's A Dictionary of Computer Science has a definition of literal which acknowledges this very issue.) Literals being constants, it means that when they are concretely implemented in a computer, in the best possible way, they do nothing other than trivially reproduce a canned value that already exists before the program starts.
- anderskaseorg 4y ago
  The situation with Lisp is exactly the same. To run a Lisp self-interpreter, we don’t pass it a Lisp function: (interpret (lambda (x) x)) but rather an encoded version of that Lisp function’s code: (interpret (cons 'lambda (cons (cons 'x nil) (cons 'x nil))) Of course, Lisp gives us a more convenient syntax for the latter, in the form of the quote macro: (interpret (quote (lambda (x) x))) (interpret '(lambda (x) x)) But the quote macro is not a function; it’s just syntax. If it were a function, you’d expect this to be equivalent: (interpret (let ((f (lambda (x) x))) (quote f))) which of course it is not. Although the quote macro is an important part of what makes Lisp Lisp, it’s not a fundamental part of what makes Lisp a programming language. We could write any Lisp program without it (assuming we were still given a way to build a primitive 'symbol).
  - kazinator 4y ago
    > The situation with Lisp is exactly the same. No it isn't, because the Lisp code is already understood to have an encoding. So we don't have to play any Gödel-numbering-like games to get the code to be able to talk about code. That battery is included. > gives us a more convenient syntax for the latter, in the form of the quote macro The ' in (cons 'lambda ...) is an instance of quote! You must write (cons (intern "lambda") ...) to remove quote. Oops, now you're using a different kind of quote: a string literal quote. If you remove that, you will have character literals to otherwise build the symbol name. I agree that quote is not essential: take out quote and you can still do useful symbolic processing. Just doing interactive testing and writing unit tests will be inconvenient, mainly. The requirement for quote has a different effect. If we have quote, we can make the additional step in the documentation that all code has the representation produced by quote, even when quote is not being used. When lambda is seen in code, that is actually the same thing that (quote lambda) produces or that (intern "lambda") produces. The above is almost inescapable if user-defined macros are supported. When code is read, it is not determined at read time what is a macro and what isn't. Therefore it is not known what parts of the form may need to be passed to a user-defined expander function without having been evaluated (and thus in the quote representation). The whole thing is in the quoted encoding, so that quote doesn't have to do anything other than pass through its interior.

kazinator 4y ago

I don't see what in the interpreter converts the lambda calculus into the Morgensen-Scott encoding. The Wikipedia page describes a "mse" function that is in some meta-language which is not lambda calculus. So first wee need a Lambda Calculus based interpreter for the meta-language, which can run this "mse" function. It looks like mse[x] is supposed to match a variable term, and mse[M N] matches a function application and so on. There are no such concepts and representations in lambda calculus, not to mention shape matching on them. The meta language might as well just be a paragraph of English: instructions on how to hand-compile the lambda calculus into a bunch of thunks which the interpreter can just invoke in certain ways to bring about the evaluation.

tromp 4y ago
You're claiming that LC cannot implement a quoting operator. Which is quite wrong. What you misunderstand is that a LC quote would not work on arbitrary lambda terms. A Mogensen quote operator would take a Mogensen encoding, and output a Mogensen encoding of that Mogensen encoding. Or a BLC quote operator would take a bitstring like 0010 which encodes the identity function λ 1, and output the blc encoding of the nil-terminated list of 4 booleans that represents that bitstring: 01000101100000110010110000011001011000001001011000001100101100000100000100000000101101110110
- kazinator 4y ago
  > would take a Mogensen encoding obtained where? > output a Mogensen encoding of that Mogensen encoding That's not what a quote operator does; it does precisely nothing, yielding the argument formula without evaluating it. No encoding-of-encoding. Just the encoding. > output the blc encoding of the nil-terminated list of 4 booleans that represents that bitstring Where/how does that become λ 1 again?
  - tromp 4y ago
    > That's not what a quote operator does; it does precisely nothing, This is what gives Lisp murky semantics; you need something (quote) to do nothing, while having nothing (no quote) does something (evaluate). Lisp lacks referential transparency, even without the use of variables. An evaluated term can be evaluated again, yielding something different. > Where/how does that become λ 1 again? By decoding it, which is what mostly what the LC self-interpreter does, as detailed on pages 6,7 of [1]. [1] https://tromp.github.io/cl/LC.pdf https://tromp.github.io/cl/LC.pdf
    - kazinator 4y ago
      > An evaluated term can be evaluated again, yielding something different. Yes, and a Mogensen-Scott encoding can be Mogensen-Scott-encoded again, requiring two rounds of decoding, and so on. Multiple rounds of encoding and evaluation seem inescapable of you have the entanglement of homoiconicity. The quote operator in Lisp is designed exactly right. In mathematics there are literals like the number 3 or the set {}. These objects stand for themselves and are not understood as requiring any calculation: they just are. Symbols like x do not stand for themselves. If you want to talk about x literally as the symbol object, it is inescapable that there is some quoting operator to indicate that the usual semantics of x denoting something else do not apply. (Oxford's A Dictionary of Computer Science has a definition of literal which acknowledges this very issue.) Literals being constants, it means that when they are concretely implemented in a computer, in the best possible way, they do nothing other than trivially reproduce a canned value that already exists before the program starts.
anderskaseorg 4y ago
The situation with Lisp is exactly the same. To run a Lisp self-interpreter, we don’t pass it a Lisp function: (interpret (lambda (x) x)) but rather an encoded version of that Lisp function’s code: (interpret (cons 'lambda (cons (cons 'x nil) (cons 'x nil))) Of course, Lisp gives us a more convenient syntax for the latter, in the form of the quote macro: (interpret (quote (lambda (x) x))) (interpret '(lambda (x) x)) But the quote macro is not a function; it’s just syntax. If it were a function, you’d expect this to be equivalent: (interpret (let ((f (lambda (x) x))) (quote f))) which of course it is not. Although the quote macro is an important part of what makes Lisp Lisp, it’s not a fundamental part of what makes Lisp a programming language. We could write any Lisp program without it (assuming we were still given a way to build a primitive 'symbol).
- kazinator 4y ago
  > The situation with Lisp is exactly the same. No it isn't, because the Lisp code is already understood to have an encoding. So we don't have to play any Gödel-numbering-like games to get the code to be able to talk about code. That battery is included. > gives us a more convenient syntax for the latter, in the form of the quote macro The ' in (cons 'lambda ...) is an instance of quote! You must write (cons (intern "lambda") ...) to remove quote. Oops, now you're using a different kind of quote: a string literal quote. If you remove that, you will have character literals to otherwise build the symbol name. I agree that quote is not essential: take out quote and you can still do useful symbolic processing. Just doing interactive testing and writing unit tests will be inconvenient, mainly. The requirement for quote has a different effect. If we have quote, we can make the additional step in the documentation that all code has the representation produced by quote, even when quote is not being used. When lambda is seen in code, that is actually the same thing that (quote lambda) produces or that (intern "lambda") produces. The above is almost inescapable if user-defined macros are supported. When code is read, it is not determined at read time what is a macro and what isn't. Therefore it is not known what parts of the form may need to be passed to a user-defined expander function without having been evaluated (and thus in the quote representation). The whole thing is in the quoted encoding, so that quote doesn't have to do anything other than pass through its interior.