▼ |  | Redex: Practical Semantics Engineering

1 | Patterns
2 | Terms
3 | Languages
4 | Reduction Relations
5 | Metafunctions and Relations
6 | Testing
7 | GUI
8 | Typesetting
| Index

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*
-->
fresh
with

top← prev up next →

### 4`` Reduction Relations

All of the exports in this section are provided both by redex/reduction-semantics (which includes all non-GUI portions of Redex) and also exported by redex (which includes all of Redex).

(reduction-relation language domain main-arrow reduction-case ...)

domain

=

|  | | |  | #:domain pattern

main-arrow

=

|  | | |  | #:arrow arrow
reduction-case |  | = |  | (--> pattern term extras ...)
extras |  | = |  | name
|  | | |  | (fresh fresh-clause ...)
|  | | |  | (side-condition scheme-expression)
|  | | |  | (where tl-pat term)
fresh-clause |  | = |  | var
|  | | |  | ((var1 ...) (var2 ...))
tl-pat |  | = |  | identifier
|  | | |  | (tl-pat-ele ...)
tl-pat-ele |  | = |  | tl-pat
|  | | |  | tl-pat ... ; a literal ellipsis

Defines a reduction relation casewise, one case for each of the clauses beginning with --> (or with arrow, if specified). Each of the patterns refers to the language, and binds variables in the term.

Following the pattern and term can be the name of the reduction rule, declarations of some fresh variables, and/or some side-conditions. The name can either be a literal name (identifier), or a literal string.

The fresh variables clause generates variables that do not occur in the term being matched. If the fresh-clause is a variable, that variable is used both as a binding in the rhs-exp 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 case of a fresh-clause is used when you want to generate 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 side-conditions are expected to all hold, and have the format of the second argument to the side-condition pattern, described above.

Each where clauses binds a variable and the side-conditions (and where clauses) that follow the where declaration are in scope of the where declaration. The bindings are the same as bindings in a term-let expression.

As an example, this

(reduction-relation
lc-lang
(--> (in-hole c_1 ((lambda (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 lambda-calculus above.

(reduction-relation
language
(arrow-var pattern term) ...
with
[(arrow pattern term)
(arrow-var var var)] ...)

Defines a reduction relation with shortcuts. As above, the first section defines clauses of the reduction relation, but instead of using -->, those clauses can use any identifier for an arrow, as long as the identifier is bound after the with clause.

Each of the clauses after the with define new relations in terms of other definitions after the with clause or in terms of the main --> relation.

A fresh variable is always fresh with respect to the entire term, not just with respect to the part that matches the right-hand-side of the newly defined arrow.

As an example, this

(reduction-relation
lc-num-lang
(==> ((lambda (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 lambda calculus with numbers, where the ==> relation is defined by reducing in the context c.

(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.

(union-reduction-relations r ...) → reduction-relation?
r : reduction-relation?

Combines all of the argument reduction relations into a single reduction relation that steps when any of the arguments would have stepped.

(reduction-relation->rule-names r)
→ (listof (union false/c symbol?))
r : reduction-relation?

Returns the names of all of the reduction relation’s clauses (or false if there is no name for a given clause).

(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.

(context-closure reduction-relation lang pattern)

This accepts a reduction, a language, a pattern representing a context (ie, 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.

(reduction-relation? v) → boolean?
v : any/c

Returns #t if its argument is a reduction-relation, and #f otherwise.

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

This accepts reduction relation, a term, and returns a list of terms that the term reduces to.

(apply-reduction-relation/tag-with-names |  | r |
|  | t) |

→ (listof (list/c (union false/c string?) any/c))
r : reduction-relation?
t : any/c

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

(apply-reduction-relation* r t) → (listof any/c)
r : reduction-relation?
t : any/c

The function apply-reduction-relation* accepts a reduction relation and a term. Starting from t, it follows every reduction path and returns all of the terms that do not reduce further. 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).

-->

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

fresh

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

with

Recognized specially within reduction-relation. A with form is an error elsewhere.
top← prev up next →