3 ms·
> In terms of implementation, though, it is far from simple. Lambda calculus has variables, which introduce huge complexity into the interpreter Lambda calculu
by tromp 6y ago
> In terms of implementation, though, it is far from simple. Lambda calculus has variables, which introduce huge complexity into the interpreter
Lambda calculus allows for a surprisingly simple self-interpreter [1]. Here is one, written with De Bruijn indices:
(λ 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)))
This includes a tokenizer/parser of (binary encoded) lambda calculus terms.
[1] https://tromp.github.io/cl/Binary_lambda_calculus.html https://tromp.github.io/cl/Binary_lambda_calculus.html
- chriswarbo 6y agoThere are tricky aspects, and I've tripped up a few times over the years. Most annoying is trying to make a 'step' function from lambda terms to lambda terms; we either need to produce a separate closure type instead, or encode those closures to lambda terms (which may defeat the point of "reducing"), or perform explicit substitution a la call-by-name (duplicating work). I don't think I've ever got all the details of capture-avoiding substitution right (I get part way there, then just copy/paste someone else's code ;) ). Of course, de Bruijn indices can help with this, and I'm a big fan. They get a lot of hate though, e.g. there seems to be an entire CS sub-discipline dedicated to ever-more-elaborate ways to avoid/hide de Bruijn indices ;) (e.g. https://en.wikipedia.org/wiki/Higher-order_abstract_syntax https://en.wikipedia.org/wiki/Higher-order_abstract_syntax https://arxiv.org/pdf/1807.04085.pdf https://arxiv.org/pdf/1807.04085.pdf https://arxiv.org/pdf/1111.0085.pdf https://arxiv.org/pdf/1111.0085.pdf http://lambda-the-ultimate.org/node/544 http://lambda-the-ultimate.org/node/544 etc.)