4 The Redex Reference

The redex library provides all of the names documented here.

Alternatively, use the redex/reduction-semantics and redex/pict libraries, which provide only non-GUI functionality (i.e., everything except redex/gui), making them suitable for programs that should not depend on racket/gui/base.

4.1 Patterns

This section covers Redex’s pattern language, which is used in many of Redex’s forms. Patterns are matched against terms, which are represented as S-expressions.

Pattern matching uses a cache—including caching the results of side-conditions—so after a pattern has matched a given term, Redex assumes that the pattern will always match the term.

In the following grammar, literal identifiers (such as any) are matched symbolically, as opposed to using the identifier’s lexical binding:

• The any pattern matches any term. This pattern may also be suffixed with an underscore and another identifier, in which case a match binds the full name (as if it were an implicit name pattern) and match the portion before the underscore.

• The _ pattern matches any term, but does not bind _ as a name, nor can it be suffixed to bind a name.

• The number pattern matches any number.

  The number identifier can be suffixed with an underscore and additional characters, in which case the pattern binds the full name (as if it were an implicit name pattern) when matching the portion before the underscore. For example, the pattern

  number_1

  matches the same as number, but it also binds the identifier number_1 to the matching portion of a term.

  When the same underscore suffix is used for multiple instances if number within a larger pattern, then the overall pattern matches only when all of the instances match the same number.

• The natural pattern matches any exact non-negative integer. Like number, this pattern can be suffixed with an underscore and additional characters to create a binding.

• The integer pattern matches any exact integer. Like number, this pattern can be suffixed with an underscore and additional characters to create a binding.

• The real pattern matches any real number. Like number, this pattern can be suffixed with an underscore and additional characters to create a binding.

• The string pattern matches any string. Like number, this pattern can be suffixed with an underscore and additional characters to create a binding.

• The boolean pattern matches #true and #false (which are the same as #t and #f, respectively). Like number, this pattern can be suffixed with an underscore and additional characters to create a binding.

• The variable pattern matches any symbol. Like number, this pattern can be suffixed with an underscore and additional characters to create a binding.

• The variable-except pattern matches any symbol except those listed in its argument. This pattern is useful for ensuring that reserved words in the language are not accidentally captured by variables.

• The variable-prefix pattern matches any symbol that begins with the given prefix.

• The variable-not-otherwise-mentioned pattern matches any symbol except those that are used as literals elsewhere in the language.

• The hole pattern matches anything when inside the first argument to an in-hole pattern. Otherwise, it matches only a hole.

• The symbol pattern stands for a literal symbol that must match exactly, unless it is the name of a non-terminal in a relevant language or contains an underscore.

  If symbol is a non-terminal, it matches any of the right-hand sides of the non-terminal. If the non-terminal appears twice in a single pattern, then the match is constrained to expressions that are the same, unless the pattern is part of a define-language definition or a contract (e.g., in define-metafunction, define-judgment-form, or define-relation) in which case there is no constraint. Also, the non-terminal will be bound in the expression in any surrounding side-condition patterns unless there the pattern is in a define-language definition.

  If symbol is a non-terminal followed by an underscore, for example e_1, it is implicitly the same as a name pattern that matches only the non-terminal, (name e_1 e) for the example. Accordingly, repeated uses of the same name are constrained to match the same expression.

  If the symbol is a non-terminal followed by _!_, for example e_!_1, it is also treated as a pattern, but repeated uses of the same pattern are constrained to be different. For example, this pattern:

  (e_!_1 e_!_1 e_!_1)

  matches lists of three es, but where all three of them are distinct.

  If the _!_ is used under the ellipsis then the ellipsis is effectively ignored while checking to see if the es are different. For example, the pattern (e_!_1 ...) matches any sequence of es, as long as they are all distinct. Also, unlike e_1 patterns, the nesting depth of _!_ patterns do not have to be the same. For example, this pattern:

  (e_!_1 ... e_!_1)

  matches all sequences of es that have at least one element, as long as they are all distinct.

  Unlike a _ pattern, the _!_ patterns do not bind names.

  If _ names and _!_ are mixed, they are treated as separate. That is, this pattern (e_1 e_!_1) matches just the same things as (e e), but the second doesn’t bind any variables.

  If the symbol otherwise has an underscore, it is an error.

• The pattern (name id pattern) matches pattern and binds using it to the name id.

• The (in-hole pattern pattern) pattern matches the first pattern, looking for a way to decompose the term such that the second pattern matches at some sub-expression where the hole appears while matching the first pattern.

  The first pattern must be a pattern that matches with exactly one hole.

• The (hide-hole pattern) pattern matches what the embedded pattern matches but if the pattern matcher is looking for a decomposition, it ignores any holes found in that pattern.

• The (side-condition pattern guard-expr) pattern matches what the embedded pattern matches, and then guard-expr is evaluated. If guard-expr produces #f, the pattern fails to match, otherwise the pattern matches. Any occurrences of name in the pattern (including those implicitly present via _ patterns) are bound using term-let in guard-expr.

• The (cross id) pattern is used for the compatible closure functions. If the language contains a non-terminal with the same name as id, the pattern (cross id) matches the context that corresponds to the compatible closure of that non-terminal.

• The (pattern-sequence ...) pattern matches a term list, where each pattern-sequence element matches an element of the list. In addition, if a list pattern contains an ellipsis, the ellipsis is not treated as a literal, instead it matches any number of duplicates of the pattern that came before the ellipses (including 0). Furthermore, each (name symbol pattern) in the duplicated pattern binds a list of matches to symbol, instead of a single match. (A nested duplicated pattern creates a list of list matches, etc.) Ellipses may be placed anywhere inside the row of patterns, except in the first position or immediately after another ellipses.

  Multiple ellipses are allowed. For example, this pattern:

  ((name x a) ... (name y a) ...)

  matches this term:

  (term (a a))

  three different ways. One where the first a in the pattern matches nothing, and the second matches both of the occurrences of a, one where each named pattern matches a single a and one where the first matches both and the second matches nothing.

  If the ellipses is named (i.e., has an underscore and a name following it, like a variable may), the pattern matcher records the length of the list and ensures that any other occurrences of the same named ellipses must have the same length.

  As an example, this pattern:

  ((name x a) ..._1 (name y a) ..._1)

  only matches this term:

  (term (a a))

  one way, with each named pattern matching a single a. Unlike the above, the two patterns with mismatched lengths is ruled out, due to the underscores following the ellipses.

  Also, like underscore patterns above, if an underscore pattern begins with ..._!_, then the lengths must be different.

  Thus, with the pattern:

  ((name x a) ..._!_1 (name y a) ..._!_1)

  and the expression

  (term (a a))

  two matches occur, one where x is bound to '() and y is bound to '(a a) and one where x is bound to '(a a) and y is bound to '().

• The other-literal pattern stands for a literal value—such as a number, boolean, or string—that must match exactly.

Changed in version 1.8 of package redex-lib: Non-terminals are syntactically classified as either always producing exactly one hole or may produce some other number of holes, and the first argument to in-hole is allowed to accept only patterns that produce exactly one hole.

If redex-match has only a lang and pattern, the result is a procedure for efficiently testing whether terms match the pattern with respect to the language lang. The procedure accepts a single term and returns #f or a list of match structures describing the matches.

Caching should be disabled when matching a pattern that depends on values other than the in-scope pattern variables or evaluating a metafunction or judgment-form that reads or writes mutable external state.

Changed in version 1.6 of package redex-lib: Extended caching to cover judgment forms.

The default size is 63.

Changed in version 1.9 of package redex-lib: Corrected spelling error, from check-redudancy to check-redundancy

4.2 Terms

Object language expressions in Redex are written using term. It is similar to Racket’s quote (in many cases it is identical) in that it constructs lists as the visible representation of terms.

The grammar of terms is (note that an ellipsis stands for repetition unless otherwise indicated):

• A term written identifier is equivalent to the corresponding symbol, unless the identifier is bound by term-let, define-term, or a pattern variable or the identifier is hole (as below).

• A term written (term-sequence ...) constructs a list of the terms constructed by the sequence elements.

• A term written ,expr evaluates expr and substitutes its value into the term at that point.

• A term written ,@expr evaluates the expr, which must produce a list. It then splices the contents of the list into the expression at that point in the sequence.

• A term written (in-hole term term) is the dual to the pattern in-hole – it accepts a context and an expression and uses plug to combine them.

• A term written hole produces a hole.

• A term written (mf-apply f arg ...) asserts that f is a metafunction and produces the term (f arg ...).

• A term written as a literal boolean or a string produces the boolean or the string.

The term form behaves similarly to quasiquote, except for a few special forms that are recognized (listed below) and that names bound by term-let are implicitly substituted with the values that those names were bound to, expanding ellipses as in-place sublists (in the same manner as syntax-case patterns).

The optional #:lang keyword must supply an identifier bound by define-language, and adds a check that any symbol containing an underscore in term could have been bound by a pattern in the language referenced by lang-id. In practice, this means that the underscore must be preceded by a non-terminal in that language or a built-in pattern such as number. This form of term is used internally by default, so this check is applied to terms that are constructed by Redex forms such as reduction-relation and define-metafunction.

For example,

(term-let ([body '(+ x 1)]

[(expr ...) '(+ - (values * /))]

[((id ...) ...) '((a) (b) (c d))])

(term (let-values ([(id ...) expr] ...) body)))

evaluates to

'(let-values ([(a) +]

[(b) -]

[(c d) (values * /)])

(+ x 1))

It is an error for a term variable to appear in an expression with an ellipsis-depth different from the depth with which it was bound by term-let. It is also an error for two term-let-bound identifiers bound to lists of different lengths to appear together inside an ellipsis.

Symbols in a term whose names end in guillemets (French quotes) around a number (for example asdf«5000») will be modified to contain a smiley face character (for example asdf«5000☺»). This is to prevent collisions with names generated by the freshening process that binding forms use.

Note that each ellipsis should be the literal symbol consisting of three dots (and the ... elsewhere indicates repetition as usual). If tl-pat is an identifier, it matches any value and binds it to the identifier, for use inside term. If it is a list, it matches only if the value being matched is a list value and only if every subpattern recursively matches the corresponding list element. There may be a single ellipsis in any list pattern; if one is present, the pattern before the ellipses may match multiple adjacent elements in the list value (possibly none).

This form is a lower-level form in Redex, and not really designed to be used directly. For let-like forms that use Redex’s full pattern matching facilities, see redex-let, redex-let*, term-match, term-match/single.

This form raises an exception recognized by exn:fail:redex? if any right-hand side does not match its left-hand side in exactly one way.

In some contexts, it may be more efficient to use term-match/single (lifted out of the context).

When evaluating a term-match expression, the patterns are compiled in an effort to speed up matching. Using the procedural result multiple times to avoid compiling the patterns multiple times.

The term-match/single form raises an exception recognized by exn:fail:redex? if no clauses match or if one of the clauses matches multiple ways.

When evaluating a term-match/single expression, the patterns are compiled in an effort to speed up matching. Using the procedural result multiple times to avoid compiling the patterns multiple times.

The variables-not-in function does not expect the symbols in vars to be distinct, but it does produce a list of distinct symbols.

4.3 Languages

A non-terminal-def comprises one or more non-terminal names (considered aliases) followed by one or more productions.

It has non-terminals: e for the expression language, x and y for variables, v for values, and E for the evaluation contexts.

Non-terminals used in define-language are not bound in side-condition patterns and duplicates are not constrained to be the same unless they have underscores in them.

4.3.1 Binding Forms

Typical languages provide a mechanism for the programmer to introduce new names and give them meaning. The language forms used for this (such as Racket’s let and λ) are called binding forms.

Binding forms require special treatment from the language implementer. In Redex, this treatment consists of declaring the binding forms at the time of language definition. Explicitly declaring binding forms makes safely manipulating terms containing binding simpler and easier, eliminating the need to write operations that (explicitly) respect the binding structure of the language.

When maybe-binding-spec is provided, it declares binding specifications for certain forms in the language. The binding-pattern specification is an extension of Redex’s pattern language, allowing the keywords #:refers-to, #:exports, and #:...binds to appear nested inside a binding pattern.

The language, lc-lang, above does not declare any binding specifications, despite the clear intention of λ as a binding form. To understand the consequences of not specifying any binding forms, consider the behavior of substitution on terms of lc-lang.

Passing the #:lang argument to term allows the substitute metafunction to determine the language of its arguments.

> (term (substitute (x (λ (x) (λ (y) x)))                     x                     (y y)) #:lang lc-lang)

'((y y) (λ ((y y)) (λ (y) (y y))))

This call is intended to replace all free occurrences of x with (y y) in the first argument to substitute. But, because lc-lang is missing a binding forms declaration, substitute replaces all instances of x with (y y) in the term (x (λ (x) (λ (y) x))). Note that even the x that appears in what is normally a binding position has been replaced, resulting in an ill-formed lambda expression.

In order to have substitute behave correctly when substituting over terms that contain bound variables, the language lc-lang must declare its binding specification. Consider the following simplification of the lc-lang definition, this time with a binding form declaration for λ.

(define-language lc-bind

(e ::= (e e)

x

(λ (x) e))

(v ::= (λ (x) e))

(x y ::= variable-not-otherwise-mentioned)

#:binding-forms

(λ (x) e #:refers-to x))

Just like Racket’s λ, in lc-bind all instances of the argument variable in the body of the lambda refer to the argument. In a binding declaration, this is specified using the #:refers-to keyword. Now the previous example has the right behavior.

> (term (substitute (x (λ (x) (λ (y) x)))                     x                     (y y)) #:lang lc-bind)

'((y y) (λ (x«0») (λ (y«1») x«0»)))

Note that sometimes substitute changes the names of the bound identifiers, in this case replacing the x and y with identifiers that have « and » in their names.

The #:refers-to declaration says that, in a λ term, the e subterm has the name from the x subterm in scope.

4.3.2 Multiple Variables in a Single Scope

To generalize to the version of λ in lc-lang, we need to cope with multiple variables at once. And in order to do that, we must handle the situation where some of the names are the same. Redex’s binding support offers only one option for this, namely taking the variables in order. The is captured by the keyword shadow. It also allows us to specify the binding structure for let:

(define-language lc-bind+let

(e ::= x

number

(λ (x ...) e)

(e e)

(let ([x e] ...) e))

(x ::= variable-not-otherwise-mentioned)

#:binding-forms

(λ (x ...) e #:refers-to (shadow x ...))

(let ([x e_x] ...) e_body #:refers-to (shadow x ...)))

This #:binding-forms declaration says that the subterm e of the λ expression refers to all of the binders in λ. Similarly, the e_body refers to all of the binders in the let expression.

> (term (substitute (let ([x 5] [y x]) (y x))                     x                     z) #:lang lc-bind+let)

'(let ((x«2» 5) (y«3» z)) (y«3» x«2»))

The intuition behind the name of the shadow form can be seen in the following example:

> (term (substitute (let ([x 1] [y x] [x 3]) x)                     x                     z) #:lang lc-bind+let)

'(let ((x«4» 1) (y«5» z) (x«6» 3)) x«4»)

Because the lc-bind+let language does not require that all binders in its let form be distinct from one another, the binding forms specification must declare what happens when there is a conflict. The shadow form specifies that duplicate binders will be shadowed by earlier binders in its list of arguments. (Of course, if we were interested in modelling Racket’s let form, we’d want that term to be malformed syntax.)

It is possible to have multiple uses of #:refers-to in a single binding specification. For example, consider a language with a letrec form.

(define-language lc-bind+letrec

(e ::= x

number

(λ (x ...) e)

(e e)

(let ([x e] ...) e)

(letrec ([x e] ...) e))

(x ::= variable-not-otherwise-mentioned)

#:binding-forms

(λ (x ...) e #:refers-to (shadow x ...))

(let ([x e_x] ...) e_body #:refers-to (shadow x ...))

(letrec ([x e_x] ...) #:refers-to (shadow x ...) e_body #:refers-to (shadow x ...)))

In this binding specification the subterms corresponding to both ([x e_x] ...) and e_body refer to the bound variables (shadow x ...).

4.3.3 Ellipses in Binding Forms

Some care must be taken when writing binding specifications that match patterns with ellipses. If a pattern symbol is matched underneath ellipses, it may only be mentioned under the same number of ellipses. Consider, for example, a language with Racket’s let-values binding form.

(define-language lc-bind+values

(e ::= x

number

(λ (x ...) e)

(e e)

(values e ...)

(let-values ([(x ...) e] ...) e))

(x ::= variable-not-otherwise-mentioned)

#:binding-forms

(λ (x ...) e #:refers-to (shadow x ...))

(let-values ([(x ...) e_x0] ...)

e_body #:refers-to (shadow (shadow x ...) ...)))

In the binding specification for the let-values form, the bound variable, x, occurs only under a single ellipsis, thus when it is mentioned in a #:refers-to clause it is restricted to be mentioned only underneath a single ellipsis. Therefore the body of the let-values form must refer to (shadow (shadow x ...) ...) rather than (shadow x ... ...).

4.3.4 Compound Forms with Binders

So far, the nonterminals mentioned in #:refers-to have always stood directly for variables that appear in the terms. But sometimes the variables are down inside some piece of the term, or only some of the variables are relevant. The #:exports clause can be used to handle such situations.

When a binding form with an #:exports clause is mentioned, the names brought into scope are determined by recursively examining everything mentioned by that #:exports clause. Consider the following version of the lc-bind language with lists that allows for pattern matching in binding positions.

(define-language lc-bind+patterns

(e ::= x

number

(λ (p) e)

(e e)

(list e ...))

(x ::= variable-not-otherwise-mentioned)

(p ::= (listp p ...) x)

#:binding-forms

(λ (p) e #:refers-to p)

(listp p ...) #:exports (shadow p ...))

In this language functions accept patterns as arguments, therefore all variables mentioned in a pattern in binding position should be bound in the body of the function. A call to the substitute metafunction shows this behavior.

> (term    (substitute (x (λ ((listp w (listp x y) z)) (list z y x w)))                x                u)    #:lang lc-bind+patterns)

'(u   (λ ((listp w«13» (listp x«14» y«15») z«16»)) (list z«16» y«15» x«14» w«13»)))

The use of the #:exports clause in the binding specification for lc-bind+patterns allows the use of nested binding patterns seen in the example. More precisely, each p may itself be a pattern that mentions any number of bound variables.

4.3.5 Binding Repetitions

In some situations, the #:exports and #:refers-to keywords are not sufficiently expressive to be able to describe the binding structure of different parts of a repeated sequence relate to each other. For example, consider the let* form. Its shape is the same as let, namely (let* ([x e] ...) e), but the binding structure is different.

In a let* form, each variable is accessible to each of the es that follow it, with all of the variables available in the body (the final e). With #:exports, we can build an expression form that has a structure like that, but we must write syntax that nests differently than let*.

(define-language lc-bind+awkward-let*

(e ::= (let*-awk c e) natural x (+ e ...))

(x ::= variable-not-otherwise-mentioned)

(c ::= (clause x e c) ())

#:binding-forms

(let*-awk c e #:refers-to c)

(clause x e c #:refers-to x) #:exports (shadow x c))

The let*-awk form binds like Racket’s let*, with each clause’s variable being active for the subsequent ones, but the syntax is different with extra nesting inside the clauses:

> (term (substitute (let*-awk (clause x y (clause y x ()))                               (+ x y z))                     x                     1)         #:lang lc-bind+awkward-let*)

'(let*-awk (clause x«17» y (clause y«18» x«17» ())) (+ x«17» y«18» z))

> (term (substitute (let*-awk (clause x y (clause y x ()))                               (+ x y z))                     y                     2)         #:lang lc-bind+awkward-let*)

'(let*-awk (clause x«19» 2 (clause y«20» x«19» ())) (+ x«19» y«20» z))

In order to get the same syntax as Racket’s let*, we need to use the #:...bind binding pattern annotation. A #:...bind can appear wherever a ... might appear, and it has the same function, namely indicating a repetition of the preceding pattern. In addition, however it comes with three extra pieces that follow the #:...bind form that describe how the binding structure inside the repetition is handled. The first part is a name that can be used by a #:refers-to outside of the repetition to indicate all of the exported variables of the sequence. The middle piece indicates the variables from a specific repetition of the ellipsis are exported to all subsequent repetitions of the ellipsis. The last piece is a beta that moves backwards through the sequence, indicating what is exported from the last repetition of the sequence to the one before, from the one before to the one before that, and then finally from the first one to the export of the entire sequence (as named by the identifier in the first position).

So, in this example, we use #:...bind to express the scope of let*.

(define-language lc-bind+let*

(e ::= (let* ([x e] ...) e) natural x (+ e ...))

(x ::= variable-not-otherwise-mentioned)

#:binding-forms

(let* ([x e] #:...bind (clauses x (shadow clauses x)))

e_body #:refers-to clauses))

It says that the name of the exported variables from the entire sequence is clauses, which means that all of the variable exported from the sequence in the second position of the let* bind variables in the body (thanks to the last #:refers-to in the example). The x in the second position following the #:...bind says that x is in scope for each of the subsequent [x e] elements of the sequence. The final (shadow clauses x) says that the variables in a subsequent clauses are exported by the current one, as well as x, which then is exported by the entire sequence.

> (term (substitute (let* ([x y] [y x])                       (+ x y z))                     x                     1)         #:lang lc-bind+let*)

'(let* ((x«22» y) (y«21» x«22»)) (+ x«22» y«21» z))

> (term (substitute (let* ([x y] [y x])                       (+ x y z))                     y                     2)         #:lang lc-bind+let*)

'(let* ((x«24» 2) (y«23» x«24»)) (+ x«24» y«23» z))

(define-extended-language lc-num-lang

lc-lang

(e ::= ....     ; extend the previous `e' non-terminal

number

+)

(v ::= ....     ; extend the previous `v' non-terminal

number

+))

extends lc-lang with two new alternatives (+ and number) for the v non-terminal, carries forward the e, E, x, and y non-terminals. Note that the meaning of variable-not-otherwise-mentioned adapts to the language where it is used, so in this case it is equivalent to (variable-except λ +) because λ and + are used as literals in this language.

The four-period ellipses indicates that the new language’s non-terminal has all of the alternatives from the original language’s non-terminal, as well as any new ones. If a non-terminal occurs in both the base language and the extension, the extension’s non-terminal replaces the originals. If a non-terminal only occurs in either the base language, then it is carried forward into the extension. And, of course, extend-language lets you add new non-terminals to the language.

If a language is has a group of multiple non-terminals defined together, extending any one of those non-terminals extends all of them.

If a language has a prefix, then all of the non-terminals from that language have the corresponding prefix in the union language. The prefix helps avoid unintended collisions between the constituent language’s non-terminals.

The default-language parameter is set to the appropriate language inside judgment forms and metafunctions, and by apply-reduction-relation.

If the lang argument is not supplied, it defaults to the value of (default-language), which must not #f.

Note that substitute is merely a convenience metafunction. Any manually-written substitution in the correct language will also be capture-avoiding, provided that the language’s binding forms are correctly defined. However, substitute may be significantly faster.

4.4 Reduction Relations