A toy interpreter for recreational λ-calculus

This entry is a follow-up of A toy parser for recreational λ-calculus.

Until this commit, I have finished implementing a minimalist λ-calculus interpreter.

What I did since I last wrote:

  1. I refactored the λ term representation so that it now tracks the bound of a bound variable, instead of level of the bound as its ancestor. This gives us the benefit to not need to edit the level when doing β-reduction.
  2. I implemented a mechanism to use weak pointers, which wasn’t a problem before I referenced the bound in the bound variable, where circular references came into play.
  3. I implemented a VariantPtr that can store anything (mostly!). This is useful when we’re walking the tree of a λ-term, which gives us the opportunity to store some extra information on-the-fly, without having to create a separate copy or maintaining a dictionary (in most cases).
  4. I fixed a bug in smart pointer assignment. The old lesson teaches. You cannot destroy a pointer to be assigned and move/copy the new value, even if the two aren’t equal. What might happen is that if the new value happens to be a reference to a smart pointer inside the object pointed to by the assignee, destroying the assignee might as well destroy the new value. Best practices are the best indeed. The easiest way to fix this is to pass by value (instead of constant reference and rvalue reference), destroy the assignee and move from the value.
  5. I refactored the toy code to be better reused.
  6. I implemented the reducer and the interactive interpreter.

Let’s talk about the reducer. I read several tutorials on λ-calculus and some discussions on the Internet to get my mind clear on how to do β-reductions. Basically, you need to do it in normal order (the leftmost outermost redex is reduced). To improve efficiency, you have to call-by-need. That means when doing β-reduction, you substitute the bound variables with the same reference. And when you later do β-reductions on the replaced term, you simultaneously reduce all the references to it. Well, though doing it itself is not hard, it’s quite brain-twisting to manage all the references (especially with multiple value/reference/pointer semantics in C++) to ensure that each β-reduction benefit all possible places, and not accidentally make a mess on the tree. The methodology is basically a quite straighforward three-step one:

  1. To substitute a term, replace subterm member pointing to the bound variable to the same reference.
  2. To substitute into some term, you have to deep clone it. This is important because the term being replaced might share the reference with the substitution value, caused by previous β-reductions, or look-up values from a constant table.
  3. To ensure reference sharing, when a deep clone is done, replace all references (outside the clone result) to the old clone with the new clone.

Having finished the interpreter, I wrote several classic terms to amuse myself a bit.

So much for recreational λ-calculus.

Please enable JavaScript to view the comments powered by Disqus.