2 Syntax in Redex

The first part of my language model is defining the collection expressions in my language. This includes the expressions of my language, the types, and the data. Sometimes I encode the meta structures—environments, machine configurations, etc—as syntax. I will also usually encode simple properties of interest in syntax, such as whether a term is a value or not. This is exactly what we do on paper in programming languages research.

2.1 Syntax TLDR

In short, Redex makes defining and working with syntax damn simple. I use define-language to create BNF grammars. With #:binding-forms (binding forms), I get capture-avoiding substitution (substitute), and α-equivalence (alpha-equivalent?), for free while retaining named identifiers rather than annoying representations such as de Bruijn. Using define-extended-language, I can easily extend existing languages, which can make it easy to modularize grammars; although, I usually avoid it because then I have to remember too many language identifiers. I use redex-match?, redex-match, and redex-let to query whether expressions match nonterminals and to let Redex decompose syntax for me. I use the test functions test-predicate, test-equal, test-results, and the parameter default-equiv, for writing test suites about syntax, and redex-check to do random testing of syntactic properties.

One caveat to be aware of is that grammars with side conditions prevent redex-check from working over the grammar.

There are two common pitfalls to avoid when working with syntax in Redex.

First, be careful about using untagged, arbitrary variables, such as by using variable or variable-not-otherwise-mentioned in your syntax definition. This makes it really easy to create arbitrary variable names, but also easy to make to get typos interpreted as variables. This can cause very unexpected failures. Apparently valid matches will not fail to match and metafunctions can have undefined behavior. One way to help avoid this problem is to tag variables, either in the grammar or with a symbolic prefix using variable-prefix.

Second, avoid unicode subscripts, and be careful with TeX input mode. Unicode subscripts are different than a nonterminal followed by an underscore, i.e., any₁ is a symbol while any_1 is a pattern variable matching an any pattern. This is made worse since TeX input mode will transparently replace the second expression with the first. DrRacket has better LaTeX input that avoids this problem by default.

2.2 Defining Syntax

I usually start my models by requiring redex/reduction-semantics instead of redex. The latter loads GUI stuff I rarely use, and sometimes don’t even install.

The define-language form takes a language identifier, which is used by some functions to specify which grammar and binding specification to use, and BNF-esque grammar, in s-expression notation. After the grammar, I give a binding specification, from which Redex infers definitions of substitution and α-equivalence.

This language defines expression using meta-variable e, which includes variables x, natural numbers, cons pairs, λ, application, the box introduction form, and a pattern matching form for box elimination. It also defines their types, as meta-variables A and B. Note that while productions need to be s-expressions, they need not be in prefix notation. Variables, x and y, are any symbol not used as a keyword or literal elsewhere in the grammar, variable-not-otherwise-mentioned.

This essentially equivalent to the grammar from the Coq model in Preface—Why Redex, but also fixes a representation of variables, and defines the metafunction substitute and the Racket alpha-equivalent? for BoxyL.

2.3 Pattern Matching

Redex has a sophisticated formal pattern language, but in essense any symbols not recognized as a BNF symbol is treated as a keyword. When I write (car e) in the grammar, this is understood to mean the literal symbol car followed by some expression e is also an expression. The pattern language also has some built-in nonterminals, such as natural which indicates a natural number literals such as 5.

This is helpful particularly with large complex languages, or low-level languages with detailed machine configurations. In these kinds of languages, its common to restrict syntax to achieve various properties, and may be non-obvious whether a term is valid.

Note that keywords and literal symbols from the grammar are not variables, but anything else is.

The any pattern can be useful for defining generic metafunctions, grammars, and judgments, or to partially specify contracts on Redex definitions. In large developments, I sometimes create a base language with generic operations on syntax, using any.

When in Racket, we use term to inject syntax into Redex. term acts like quasiquote, and even supports unquote, so we can write use Racket to compute terms through templating. Most quoted s-expressions are also valid Redex terms, which can be useful if we want to move between s-expressions in Racket and terms in Redex.

The structure returned by redex-match is a little annoying to look at. Redex supports non-deterministic matching, so we get back the set of all possible ways to match. The elements of the set are matches, which contain lists of bindings of the pattern variable to the term.

I don’t often use redex-match directly for decomposing terms, because redex-let has a much better interface. But redex-let requires a deterministic single match.

2.4 Extending Syntax and Syntax with Holes (Contexts)

define-extended-language allows extending a base language with new nonterminals, or extending existing nonterminals from the base language with new productions. For example, I could extend expressions with booleans literals as follows.

This defines a new language, BoxyBoolL, which extends BoxyL with an extra production in the nonterminal e. To extend a nonterminal, I use ...., which means "all the current productions of this nonterminal", followed by the new productions.

We can also add new nonterminals by extending a language.

This defines a new language, BoxyEvalL, which extends BoxyL with a call-by-value evaluation context. Redex syntax also support contexts, that is, programs with a hole. I use this for evaluation and program contexts. In this language, we define the context E by listing the usual evaluation contexts for call-by-value. For operators with many arguments, we can easily specify left-to-right evaluation order using non-deterministic ellipses patterns.

After specifying a context, we can easily decompose a term into its evaluation context and its redex.

2.5 Binding, Substitution, and α-equivalence

In this tutorial, I give only the simplest possible use of binding forms: a single, lexical name. But Redex’s support for binding is extremely sophisticated. It can support n-ary lexical binding with shadowing, pattern-matching style binding, module-style binding. See binding forms in the Redex docs to the many examples of complex binding support.

2.6 Random Generation of Syntax

generate-term takes a language name, a generation specification, and a size. It can generate terms based on lots of Redex definitions, although I almost always generate terms from grammars and judgments.

2.7 Testing Syntax

Once we’re done querying, we can move to testing. Redex features a unit testing library. Tests are great for detecting breakages as you start tinkering with your model, and can also report more information that the mostly-boolean query functions.

When generating syntax, redex-check takes a language identifier, a pattern, a predicate, and (optionally), the number of attempts.

2.8 Caveat: Syntax with Side Conditions

The side-condition takes a pattern and a Racket predicate which can refer to the pattern variables. You can use a side-condition pattern anywhere in a pattern.

Unfortunately, using side-conditions in patterns does not work with redex-check. You can still use generate-term, though.

2.9 Pitfall: All Symbols are Variables

In a couple of the examples above, I rely on an anti-pattern. I pun between a real expression and an expression schema, by punning between variables and meta-variables. For example, consider the Redex term ((λ (x : Nat) e_body) e_arg). This is only valid because I used variable-not-otherwise-mentioned, which makes all symbols valid variables. In BoxyL, this expression is valid, but in an unintuitive way. The subterms e_body and e_arg are actually variables, although we are pretending they are meta-variables.

This can let us treat an expression as an expression schema. It is a very tempting way to create examples. Instead of being very precise about the entire term, you can create readable meta-examples only specifying parts of the term and pretending this applies to all terms of this pattern. But relying on this behavior can really cause problems if you’re not careful.

For example, consider the very similar term ((λ (x : A) e_body) e_arg). Ah, surely this meta-example represents any valid application... but it isn’t even a valid expression.

The problem is that A, isn’t a valid type, and we did not allow types to have variables in the grammar.

Worse, when a term doesn’t match a language nonterminal, metafunctions such as substitute can exhibit undefined behavior.

One should avoid this pattern, and be aware of it because you can do it accidently. For example, if we use the wrong letter or wrong case, we can easily create an invalid term, or a valid term that isn’t what we expected.

The root of the problem is that we used variable-not-otherwise-mentioned and didn’t tag variables, so any symbol is a valid expression. This is hard to avoid in Redex unless you exclusively use variable-prefix. Be careful when using the variable specifications that give you infinite unstructured variables. It’s handy, but like in any scripting language, that usefulness comes at a cost. It will cause you problems. It has caused me problems. It bit me twice while writing this tutorial.

Even when you manage to avoid this, term simply quotes any symbol, so typos can result in valid terms, although the term may not match a nonterminal. If you use contracts, which I strongly encourage and will use in the rest of this tutorial, this is less of a problem since the invalid quoted term will hopefully not match a nonterminal.

2.10 Pitfall: Subscripts and Unicode

Redex makes it very easy to mix unicode into your formal syntax. This is handy, since the code looks closer to the paper presentation. Unfortunatley, it can cause problems if you’re using unicode subscripts or TeX input mode in emacs.

The underscore, _, has a special meaning when attached to a nonterminal in a Redex pattern: it creates a distinct pattern variable matching the preceeding nonterminal. You might be tempted to use a unicode subscript instead, but that doesn’t work.

This can be a particular problem if you’re using TeX input mode in emacs. When in TeX input mode, typing _ causes the input mode to being typing a subscript unicode symbol, creating a literal symbol rather than a pattern variable. This result will be a mysterious failure.

I’m not sure if unicode subscripts should be treated the same by Redex or not, but for now, I recommend never ever using unicode subscripts in Redex. I usually use TeX input mode, and have a hotkey for turning it on and off, so I can type underscores.

← Preface—Why RedexReduction and Evaluation in Redex →