Comment by tromp

> LC has a great disadvantage: it's difficult to write a LC interpreter in LC.

It's not; here it is quoted from [1]:

    (λ 1 1) (λ λ λ 1 (λ λ λ λ 3 (λ 5 (3 (λ 2 (3 (λ λ 3 (λ 1 2 3))) (4 (λ 4 (λ 3 1 (2 1)))))) (1 (2 (λ 1 2)) (λ 4 (λ 4 (λ 2 (1 4))) 5)))) (3 3) 2) (λ 1 ((λ 1 1) (λ 1 1)))

> LC does not know what a LC expression is.

Again, it's trivial to encode LC terms as bitstrings [1], which are trivially decoded back into lambda terms. That is exactly what the above lambda expression does. Alternatively, you can encode LC terms with Mogensen's encoding, but that one doesn't give you a textual representation like a bitstring.

[1] https://tromp.github.io/cl/Binary_lambda_calculus.html#Lambd...