There 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; w

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