Lambda Calculus in 400 Bytes

Re:Lambda Calculus in 400 Bytes by User23 on Sunday February 27, 2022 @07:28PM (#30494536)

One really interesting development of the Lambda calculus is the De Bruijn index. It does away with variable names altogether. It solves the name collision problem and would be an interesting way to write hygienic macros.

[1] https://en.m.wikipedia.org/wiki/De_Bruijn_index

[ Parent | on HN ]

Re:Lambda Calculus in 400 Bytes by chalst on Sunday February 27, 2022 @07:50PM (#30494705)

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_scienc...

[ Parent | on HN ]

Re:Lambda Calculus in 400 Bytes by chriswarbo on Monday February 28, 2022 @03:38AM (#30497711)

I 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.36...

[ Parent | on HN ]

Re:Lambda Calculus in 400 Bytes by User23 on Sunday February 27, 2022 @09:03PM (#30495389)

Interesting! I hadn’t come across this. Thank you!

[ Parent | on HN ]