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 racket-expression) | | | | | | | (where tl-pat term) | | | | | | | (side-condition/hidden racket-expression) | | | | | | | (where/hidden 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.
All side-conditions provided with side-condition and
hidden-side-condition 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 form is the same as
side-condition, except that the side 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. The bindings are the same as bindings in a
term-let expression. A where/hidden clause is the
same as a where clause, but the clause is not
rendered when typesetting via redex/pict.
As an example, this
defines a reduction relation for the lambda-calculus above.
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
defines reductions for the lambda calculus with numbers,
where the ==> relation is defined by reducing in the context
c.
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 all of the reduction relation’s clauses
(or false if there is no name for a given clause).
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.
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.
Returns #t if its argument is a reduction-relation, and
#f otherwise.
This accepts reduction relation, a term, and returns a
list of terms that the term reduces to.
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).