Hacker News new | past | comments | ask | show | jobs | submit login

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.




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


You could, but you'd need to spend even more effort before beginning interpretation to turn the number into a form that LC can interpret.




Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | Legal | Apply to YC | Contact

Search: