4 ms·
Could you encode all untyped lambda calculus expressions by just numbering them and writing the number as the string of bits? Maybe this enumeration is the "ex
by amatus 10y ago
Could you encode all untyped lambda calculus expressions by just numbering them and writing the number as the string of bits?
Maybe this enumeration is the "external collaborator" in this case, but it's a very simple one.
- catnaroek 10y agoInside the lambda calculus, the only thing you can do with a lambda abstraction is apply it. And one thing you can't do using your numbering scheme (which is basically a Gödel numbering) is establish whether two syntactically different functions are extensionally equal (under some fixed reduction strategy).
- pron 10y agoYou could, but you'd need to spend even more effort before beginning interpretation to turn the number into a form that LC can interpret.