|
|
|
|
|
by tromp
1369 days 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 |
|
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?