We covered the basics of PLT Redex without going into programming-language theory. Instead, we used it to model a game of Peg Solitaire. We used terms to represent elements in the game: boards, pegs, spaces and paddings. We used patterns to match those terms as the basis of several definitions:
- Languages: Named patterns that specify which terms represent elements in Peg Solitaire and which do not.
- Metafunctions: Functions in the language of Peg Solitaire elements. They are deterministic: when faced with multiple choices (multiple clauses that match), a metafunction chooses only one path.
- Reduction Relations: Similar to a metafunction, but works nondeterministically: when faced with multiple choices (multiple clauses that match), a judgment form chooses all paths. Can also be understood as a metafunction that returns a set of results.
- Predicate Relations: Similar to a reduction relation that returns a single boolean indicating whether the predicate holds or not.
- Judgment Forms: The most general form of relation, with arbitrarily many inputs and outputs.
With these definitions in place, we used PLT Redex visualization tools to play Peg Solitaire. We then explored other features, including extra conditions for a clause to contribute to the output, unquoting, holes, testing and typesetting. We also discussed some limitations, including debugging, performance, and more advanced pattern matching; the lack of metaparameters, parallel reduction and higher-order metafunctions; how definition extensions do not reinterpret dependent definitions; how it can be difficult to customize typeset figures; and how PLT Redex is not appropriate for mechanized formal proofs.
You now know enough to read the more advanced material on PLT Redex, and understanding the tool will help you read papers in programming-language theory.
Thanks to the following people for providing feedback on a preliminary version of this article: P.C. Shyamshankar, Scott Moore, Allan Vital and Rafael da Silva Almeida.