[kazinator]

> 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]

> 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

[kazinator]

> 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.

[Y_Y]

What's so special about "literals"? They must be symbols in the sense that they can be evaluated. The fact that you've defined them so that they evaluate to something indistinguishable from the unevaluated form is neat, but it doesn't seem to me fundamental. We could have a lisp where you aren't allowed to evaluate a raw number, it would just be a little more awkward.

[lisper]

One could also have symbols that evaluate to themselves rather than some bound value. In fact, Common Lisp has exactly that: keywords.