4 Judgments in Redex

The final piece of my model will be the judgments. Judgments encode all the properties I care about for my expressions and evaluation function. These include judgments like program equivalence and well typedness. Redex gives me the same inference rule notation I use on paper, and a spectrum of automagic computability for judgments.

Redex uses the American spelling of judgment.

4.1 Judgment TLDR

I define judgments using define-judgment-form. This form allows me to specify the judgment in a relation presentation, and use all of Redex’s pattern language in the process. Once I define a judgment, I can query whether the judgment holds, and even generate terms that satisfy the judgment.

If I #:mode and give output positions in the judgment, Redex will automatically compute the terms in output position from the terms I provide in input positions. I use judgment-holds to ask Redex whether a judgment holds, and to compute the output of judgments. I use build-derivations to have Redex automatically build derivations for moded judgments. For modeless judgments, I can manually build derivations using derivation and ask whether the derivation is valid using judgment-holds. This can be extremely useful for teaching, checking intuition, and debugging judgments.

For testing, I can use test-judgment-holds to test a judgment. Usually, I want to test meta-theoretic properties of judgments by using redex-check.

A common pitfall is to use the wrong language name when defining a judgment. The result is the judgment silently failing to hold, even when you think it ought to. This causes me to avoid using define-extended-language as much as possible to reduce the number of language names I need to keep track of.

There are two important caveats to keep in mind while using judgments. First, they can be frustrating to debug, since Redex only gives you a boolean value: whether the judgment holds or not. I normally resort to printf debugging. The recent addition of modeless judgments provides a new avenue for debugging that seems promising, although I haven’t used this approach in practice. Second, ellipses and Racket escapes are a double-edged sword. While they make defining judgments much easier, they also prevent Redex from generating terms that satisfy the judgment.

4.2 βη-equality Judgment

The first judgment I usually define is an equivalence judgment for expressions. I will usually extend the normalization relation to an equivalence relation, sometimes including η-equivalence.

Below, I define βη-equivalence for BoxyL.

The form define-judgment-form takes a language identifier and a sequence of rules, written in the traditional inference rule notation. The horizontal line can be followed by an optional name for the rule. The length of the horizontal line must be greater than 2 hyphens.

The judgment definition also takes an optional contract delcaration and optional mode declaration. I also use a contract to help catch bugs, including some syntax pitfalls mentioned earlier. The mode lines requires either I for an input or O for an output position. The more output positions you have, the more Redex can compute for you, but the more algorithmic you must make your rules.

You can use the full Redex pattern language in any input and the Redex term language, including metafunctions, in any output. (Recall that input and output flips in premises; inputs become term positions and outputs become pattern positions.) You can use any other judgment directly as a premise. For non-judgment side-conditions, I frequently use where clauses and use side-condition sparingly. Note that side-conditions in judgment forms are Redex terms, and unquote to use Racket expressions. This is unlike side-conditions in grammar, which are Racket expressions and must quote using term to use Redex terms.

We use the Racket function judgment-holds to ask whether a well-moded judgment holds for particular inputs. Redex will search through the judgment rules, and return either #t or #f

Judgments which are exclusively in input mode can be used as metafunctions. I never do this, because (1) I rarely have input-only judgments and (2) typos can easily lead to the symbols-interpreted-as-variables problem, but judgment-holds will report some errors when given bad inputs.

4.3 Typing Judgment

The next judgments I define are the typing judgments. This usually requires an extension to the language to define environments, syntactically.

I usually write my environments as snoc-lists, as we do on paper. Shadowing is structural, as on paper; I don’t need to worry about freshness or anything, since Redex "Does The Right Thing™" when deconstructing a binder and putting it in the context.

To define the type system, I usually give a well-moded algorithmic presentation that computes the type from the environment and the term. This means I usually need my syntax to be full annotated; conveniently, that is already the case. Sometimes I need to go back and modify my syntax with some extra annotations.

Below is the type system for BoxyL. I first define a helper for distinguishing variables. Redex has a special pattern for non-matching patterns, called bang pattern, but frankly they’re hard to use and read.

Once I have a type system, I can ask Redex to infer the types of expressions.

Redex will either return the set of valid types, including the empty set if I asked for an output, or #f if the judgment doesn’t hold and I did not ask for any output.

You can also ask Redex for the entire derivation, rather than just a "yes" or "no".

build-derivations will return the set of valid derivations.

4.4 Testing Judgments

test-judgment-holds has two different interfaces: one for moded judgments, and one for modeless judgments.

Unfortunately, there is no built-in way to check judgments for moded judgments. Thankfully, we can quickly create test-derivation.

4.5 Meta-theory Random-testing

Redex will report how many successful attempts it made, and how many failed generations. Redex can fail to find a good derivation a lot of the time, due annoying internal details. This usually doesn’t indicate a problem, and you should just increase the number of attempts. You can also use #:prepare to try to fix up generated examples.

4.6 Pitfall: Using the Wrong Language Name

While using define-extended-language is nice for modularizing syntax and for pedagogical presentations, I rarely use it in practice. It’s very easy to use the wrong language identifier when defining judgments, and the result can be quite mysterious errors. The errors are easier to spot when you use contracts—typically, some nonterminal in the contract will be undefined, so the judgment will report a useful error message.

If you don’t use the nonterminal in a contract, then the judgment will just assume you meant that nonterminal as a symbol, and silently fail to hold.

4.7 Caveat: Debugging Judgments

When a judgment doesn’t hold, Redex does not give you any help. It merely fails and returns #f or '(). When it appears that a judgment ought to hold, this can be extremely frustrating to debug.

We can use the parameter current-traced-metafunctions to ask Redex’s to print its trace of the search through the judgment. This is essentially a fancy version of printf debugging, but works well for small derivations.

Now we know that the sub-derivation that failed is in the premise for + with the sub-expressions (car (cons 5 1)).

For large judgments and derivations, this method does not work well. Instead, you may want to only observe certain rules. The best method I’ve found for doing this is inserting printfs as side-conditions.

Recall that side-conditions in judgment forms must unquote to use Racket expressions.

4.8 Caveat: Ellipses and Racket Escapes

The Redex pattern language supports ellipses matching on sequences of patterns. This is extremely convenient and matches common on-paper vector notation. Unfortunately, it also completely defeats Redex term generation, so you cannot use that judgment to generate derivations (and thus, e.g., generate well-typed terms). This is a severe and unfortunate limitation.

My usual solution is to avoid any ellipses in my syntax, and instead rely on nesting and currying. This reduces the need for ellipses in judgments. It is easy to define additional metafunctions to provide nicer surface syntax and still get good term generation. For example, we can define n-ary surface syntax for BoxyL as below, and still have good well-typed term generation.

Other features also defeat derivation generation, notably escaping into Racket. This one can be harder to fix. If we’re only escaping to Racket for natual number or booleans, we can encode the computation as an inductive data type in Redex.

When I cannot avoid ellipses or escaping, I will make due with generating terms from grammars and try to fix them up, for example, by initializing mutual variables or by replacing ill-typed subexpressions with obviously well-typed ones. This doesn’t scale particularly well.

When all else fails, there’s Quickcheck.

← Reduction and Evaluation in Redex