On this page:
reduction-relation
extend-reduction-relation
union-reduction-relations
reduction-relation->rule-names
compatible-closure
context-closure
reduction-relation?
apply-reduction-relation
apply-reduction-relation/  tag-with-names
apply-reduction-relation*
current-cache-all?
-->
fresh
with
8.14

4.4 Reduction Relations🔗ℹ

syntax

(reduction-relation language domain codomain base-arrow
                    reduction-case ...
                    shortcuts)
 
domain = 
  | #:domain pattern
     
codomain = 
  | #:codomain pattern
     
base-arrow = 
  | #:arrow base-arrow-name
     
reduction-case = (arrow-name pattern term red-extras ...)
     
red-extras = rule-name
  | (fresh fresh-clause ...)
  | (side-condition racket-expression)
  | (where pattern term)
  | (where/hidden pattern term)
  | (where/error pattern term)
  | (bind pattern term)
  | (bind/hidden pattern term)
  | (judgment-holds (judgment-form-id pat/term ...))
  | (judgment-holds (relation-id term ...))
  | (side-condition/hidden racket-expression)
     
shortcuts = 
  | with shortcut ...
     
shortcut = 
[(old-arrow-name pattern term)
 (new-arrow-name identifier identifier)]
     
rule-name = identifier
  | string
  | (computed-name racket-expression)
     
fresh-clause = var
  | ((var1 ...) (var2 ...))
     
pat/term = pattern
  | term
Defines a reduction relation case-wise, one case for each of the reduction-case clauses.

The optional domain and codomain clauses provide contracts for the relation. If the codomain is not present, but the domain is, then the codomain is expected to be the same as the domain.

The arrow-name in each reduction-case clause is either base-arrow-name (default -->) or an arrow name defined by shortcuts (described below). In either case, the pattern refers to language and binds variables in the corresponding term. Following the pattern and term can be the name of the reduction rule and declarations of fresh variables and side-conditions.

For example, the expression

(reduction-relation
 lc-lang
 (--> (in-hole c_1 ((λ (variable_i ...) e_body) v_i ...))
      (in-hole c_1 ,(foldl lc-subst
                           (term e_body)
                           (term (v_i ...))
                           (term (variable_i ...))))
      beta-v))

defines a reduction relation for the lc-lang grammar.

A rule’s name (used in typesetting, the stepper, traces, and apply-reduction-relation/tag-with-names) can be given as a literal (an identifier or a string) or as an expression that computes a name using the values of the bound pattern variables (much like the rule’s right-hand side). Some operations require literal names, so a rule definition may provide both a literal name and a computed name. In particular, only rules that include a literal name may be replaced using extend-reduction-relation, used as breakpoints in the stepper, and selected using render-reduction-relation-rules. The output of apply-reduction-relation/tag-with-names, traces, and the stepper prefers the computed name, if it exists. Typesetting a rule with a computed name shows the expression that computes the name only when the rule has no literal name or when it would not typeset in pink due to with-unquote-rewriters in the context; otherwise, the literal name (or nothing) is shown.

Fresh variable clauses generate variables that do not occur in the term being reduced. If the fresh-clause is a variable, that variable is used both as a binding in the term and as the prefix for the freshly generated variable. (The variable does not have to be a non-terminal in the language of the reduction relation.)

The second form of fresh-clauses generates a sequence of variables. In that case, the ellipses are literal ellipses; that is, you must actually write ellipses in your rule. The variable var1 is like the variable in first case of a fresh-clause; namely it is used to determine the prefix of the generated variables and it is bound in the right-hand side of the reduction rule, but unlike the single-variable fresh clause, it is bound to a sequence of variables. The variable var2 is used to determine the number of variables generated and var2 must be bound by the left-hand side of the rule.

The expressions within side-condition clauses and side-condition/hidden clauses are collected with and and used as guards on the case being matched. The argument to each side-condition should be a Racket expression, and the pattern variables in the pattern are bound in that expression. A side-condition/hidden clause is the same as a side-condition clause, except that the condition is not rendered when typesetting via redex/pict.

Each where clause acts as a side condition requiring a successful pattern match, and it can bind pattern variables in the side-conditions (and where clauses) that follow and in the metafunction result.

A where/hidden clause is the same as a where clause, but the clause is not rendered when typesetting via redex/pict.

The where/error clause clause is like where, except that a failure to match is an error and, if multiple matches are possible, the right-hand side must produce the same result for each of the different matches (in the sense of alpha-equivalent? using the language that this reduction relation is defined with).

Each judgment-holds clause acts like a where clause, where the left-hand side pattern incorporates each of the patterns used in the judgment form’s output positions.

Each shortcut clause defines arrow names in terms of base-arrow-name and earlier shortcut definitions. The left- and right-hand sides of a shortcut definition are identifiers, not patterns and terms. These identifiers need not correspond to non-terminals in language and if they do, that correspondence is ignored (more precisely, the shortcut is not restricted only to terms matching the non-terminal).

For example, this expression

(reduction-relation
 lc-num-lang
 (==> ((λ (variable_i ...) e_body) v_i ...)
      ,(foldl lc-subst
              (term e_body)
              (term (v_i ...))
              (term (variable_i ...))))
 (==> (+ number_1 ...)
      ,(apply + (term (number_1 ...))))
 
 with
 [(--> (in-hole c_1 a) (in-hole c_1 b))
  (==> a b)])

defines reductions for the λ-calculus with numbers, where the ==> shortcut is defined by reducing in the context c.

A fresh clause in reduction-case defined by shortcut refers to the entire term, not just the portion matched by the left-hand side of shortcut’s use.

Changed in version 1.14 of package redex-lib: Added the #:codomain clause.

syntax

(extend-reduction-relation reduction-relation language more ...)

This form extends the reduction relation in its first argument with the rules specified in more. They should have the same shape as the rules (including the with clause) in an ordinary reduction-relation.

If the original reduction-relation has a rule with the same name as one of the rules specified in the extension, the old rule is removed.

In addition to adding the rules specified to the existing relation, this form also reinterprets the rules in the original reduction, using the new language.
Combines all of the argument reduction relations into a single reduction relation that steps when any of the arguments would have stepped.

Returns the names of the reduction relation’s named clauses.

Added in version 1.20 of package redex-lib.

syntax

(compatible-closure reduction-relation lang non-terminal)

This accepts a reduction, a language, the name of a non-terminal in the language and returns the compatible closure of the reduction for the specified non-terminal.

In the below example, r is intended to calculate a boolean or. Since r does not recursively break apart its input, it will not reduce subexpressions within a larger non-matching expression t.

(define-language unary-arith
  [e ::= Z (S e) (+ e e)])

 

(define addition-without-context
  (reduction-relation
   unary-arith
   #:domain e
   (--> (+ (S e_1) e_2)
        (+ e_1 (S e_2)))
   (--> (+ Z e)
        e)))

 

(define nested-example (term (+ (+ (S Z) (S Z))
                                (+ (S Z) (S Z)))))

 

> (apply-reduction-relation addition-without-context
                            nested-example)

'()

The compatible-closure operator allows us to close addition-without-context over all nested e contexts and then we can use it to find the sum.

(define addition-compat-closure
  (compatible-closure addition-without-context unary-arith e))

 

> (apply-reduction-relation* addition-compat-closure
                             nested-example)

'((S (S (S (S Z)))))

syntax

(context-closure reduction-relation lang pattern)

This accepts a reduction, a language, a pattern representing a context (i.e., that can be used as the first argument to in-hole; often just a non-terminal) in the language and returns the closure of the reduction in that context.

Continuing the example in the documentation for compatible-closure, one might find that there are too many reductions that can take place. The original example, in fact, reduces to two different terms in a single step.

> (apply-reduction-relation addition-compat-closure
                            nested-example)

'((+ (+ (S Z) (S Z)) (+ Z (S (S Z)))) (+ (+ Z (S (S Z))) (+ (S Z) (S Z))))

If we wanted to force an order of evaluation, requiring that we evaluate the left side of the addition before moving on to the right, we can do that by limiting the context where the addition is performed. Here is one definition of a context that does that limitation.

(define-extended-language unary-arith-E unary-arith
  (E ::= hole (+ n E) (+ E e))
  (n ::= Z (S n)))
Now we can use the more general compatible-closure to close only over the places where E allows us to reduce
> (apply-reduction-relation
   (context-closure addition-without-context
                    unary-arith-E
                    E)
   nested-example)

'((+ (+ Z (S (S Z))) (+ (S Z) (S Z))))

procedure

(reduction-relation? v)  boolean?

  v : any/c
Returns #t if its argument is a reduction-relation, and #f otherwise.

procedure

(apply-reduction-relation r t)  (listof any/c)

  r : (or/c reduction-relation? IO-judgment-form?)
  t : any/c
This accepts reduction relation, a term, and returns a list of terms that the term reduces to.

Like apply-reduction-relation, but the result indicates the names of the reductions that were used.

procedure

(apply-reduction-relation* 
  r 
  t 
  [#:all? all 
  #:cache-all? cache-all? 
  #:stop-when stop-when] 
  #:error-on-multiple? error-on-multiple?) 
  (listof any/c)
  r : (or/c reduction-relation? IO-judgment-form?)
  t : any/c
  all : boolean? = #f
  cache-all? : boolean? = (or all? (current-cache-all?))
  stop-when : (-> any/c any) = (λ (x) #f)
  error-on-multiple? : boolean?
Accepts a reduction relation and a term. Starting from t, it follows every reduction path and returns either all of the terms that do not reduce further or all of the terms, if all? is #t. If there are infinite reduction sequences that do not repeat, this function will not terminate (it does terminate if the only infinite reduction paths are cyclic).

If the cache-all? argument is #t, then apply-reduction-relation* keeps a cache of all visited terms when traversing the graph and does not revisit any of them. This cache can, in some cases, use a lot of memory, so it is off by default and the cycle checking happens by keeping track only of the current path it is traversing through the reduction graph.

The stop-when argument controls the stopping criterion. Specifically, it is called with each term that apply-reduction-relation* encounters. If it ever returns a true value (anything except #f), then apply-reduction-relation* considers the term to be irreducible (and so returns it and does not try to reduce it further).

If error-on-multiple? is #t, then an error is signalled if any of the terms reduce to more than one other term.

Changed in version 1.18 of package redex-lib: Added error-on-multiple?.

parameter

(current-cache-all?)  boolean?

(current-cache-all? cache-all?)  void?
  cache-all? : boolean?
Controls the behavior of apply-reduction-relation* and test-->>’s cycle checking. See apply-reduction-relation* for more details.

Examples:
> (define-language empty-lang)
> (define R
    (reduction-relation
     empty-lang
     (--> 0 1)
     (--> 0 2)
     (--> 2 3)
     (--> 3 3)))
> (apply-reduction-relation R 0)

'(2 1)

> (apply-reduction-relation* R 0)

'(1)

syntax

-->

Recognized specially within reduction-relation. A --> form is an error elsewhere.

syntax

fresh

Recognized specially within reduction-relation. A fresh form is an error elsewhere.

syntax

with

Recognized specially within reduction-relation. A with form is an error elsewhere.