3 ms·
Tromp's binary lambda calculus, which is what Justine is using, is based on de Bruijn indices. It works, but it's very fiddly. My favourite way of solving the
by chalst 5y ago
Tromp's binary lambda calculus, which is what Justine is using, is based on de Bruijn indices.
It works, but it's very fiddly. My favourite way of solving the problem of names in the lambda calculus is to use Pitts-Gabbay nominal syntax. Wikipedia has a weak article on them, which I mean someday to fix up: https://en.wikipedia.org/wiki/Nominal_terms_(computer_science) https://en.wikipedia.org/wiki/Nominal_terms_(computer_scienc...
- User23 5y agoInteresting! I hadn’t come across this. Thank you!
- chriswarbo 5y agoI really like de Bruijn indexes, but whenever alternatives are suggested I always like to mention the paper "I am not a number, I am a free variable", if only for the title ;) https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.365.2479&rep=rep1&type=pdf https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.36...