Using Redex as an interactive lambda-calculus workbench?

Questions & Answers
, ,
1

I’m working through Lambda-Calculus and Combinators: An Introduction (Hindley & Seldin) and I’m looking for a locally installable Racket-based tool that can act as an interactive workbench for untyped lambda calculus and combinatory logic.

Here's what I'd like to be able to do:

  • Enter lambda terms close to textbook notation
  • Perform capture-avoiding substitution
  • Step through single β-reductions ideally with a stepper
  • Work with combinators
  • Preferably script or embed examples. Bonus if Emacs friendly, but not required

As a random simple example of the kind of thing I want to check: there's an exercise on pg 8 asking to evaluate [(u v)/x] (λy. x (λw. v w x)). I'd like to be able to type in something almost verbatim to this and get back correctly substituted terms, with the option to see intermediate steps. I’m reasonably familiar with functional languages (Haskell, ML, Scheme) and with Coq, so I’m comfortable writing small formal models if needed but I’m hoping there’s an established Redex (or other Racket) workflow that people recommend for this purpose.

My uestions:

  • Would PLT Redex be the right tool for this, or is there something lighter-weight that’s commonly used?
  • Are there existing Redex models / examples that people use as a lambda-calculus “calculator” or teaching workbench?
  • Any advice on structuring such a Redex model so it’s convenient for simple exploratory work?
2

Redex is the right tool for this, though the notation of Hindley & Seldon uses too few ()s :slight_smile:

In addition to the Redex book, I'd recommend the Redex web page. It comes with a complete model of Plotkin's by-value lambda calculus (which uses a different base axion, namely ((\x.e) v) = e[x :- v] where v is a value (lambda, variable).)

From a theoretical perspective, Redex is really a cross between Barendregt 1980, Plotkin 1974, and my dissertation (book part I), which uses contexts to reduce the bureaucracy of inference rules to syntactic compatibility.