4 Reduction Relations
All of the exports in this section are provided both by redex/reductionsemantics (which includes all nonGUI portions of Redex) and also exported by redex (which includes all of Redex).
(reductionrelation language domain mainarrow reductioncase ...)  

Following the pattern and term can be the name of the reduction rule, declarations of some fresh variables, and/or some sideconditions.
The rule’s name (used in typesetting, the stepper, traces, and applyreductionrelation/tagwithnames) 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 righthand 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 extendreductionrelation, used as breakpoints in the stepper, and selected using renderreductionrelationrules. The output of applyreductionrelation/tagwithnames, 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 withunquoterewriters in the context; otherwise, the literal name (or nothing) is shown.
The fresh variables clause generates variables that do not occur in the term being matched. If the freshclause is a variable, that variable is used both as a binding in the rhsexp and as the prefix for the freshly generated variable. (The variable does not have to be a nonterminal in the language of the reduction relation.)
The second case of a freshclause 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 freshclause, namely it is used to determine the prefix of the generated variables and it is bound in the righthand side of the reduction rule, but unlike the singlevariable 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 lefthand side of the rule.
The expressions within sidecondition clauses and sidecondition/hidden clauses are collected with and and used as guards on the case being matched. The argument to each sidecondition should be a Racket expression, and the pattern variables in the pattern are bound in that expression. A sidecondition/hidden clause is the same as a sidecondition 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 sideconditions (and where clauses) that follow and in the metafunction result. The bindings are the same as bindings in a termlet 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
(reductionrelation 
lclang 
(> (inhole c_1 ((lambda (variable_i ...) e_body) v_i ...)) 
(inhole c_1 ,(foldl lcsubst 
(term e_body) 
(term (v_i ...)) 
(term (variable_i ...)))) 
betav)) 
defines a reduction relation for the lambdacalculus above.

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 righthandside of the newly defined arrow.
As an example, this
(reductionrelation 
lcnumlang 
(==> ((lambda (variable_i ...) e_body) v_i ...) 
,(foldl lcsubst 
(term e_body) 
(term (v_i ...)) 
(term (variable_i ...)))) 
(==> (+ number_1 ...) 
,(apply + (term (number_1 ...)))) 
with 
[(> (inhole c_1 a) (inhole c_1 b)) 
(==> a b)]) 
defines reductions for the lambda calculus with numbers, where the ==> relation is defined by reducing in the context c.
(extendreductionrelation reductionrelation language more ...) 
If the original reductionrelation has a rule with the same name as one of the rules specified in the extension, the old rule is removed.
(unionreductionrelations r ...) → reductionrelation? 
r : reductionrelation? 
(compatibleclosure reductionrelation lang nonterminal) 
(contextclosure reductionrelation lang pattern) 
(reductionrelation? v) → boolean? 
v : any/c 
(applyreductionrelation r t) → (listof any/c) 
r : reductionrelation? 
t : any/c 
 
→ (listof (list/c (union false/c string?) any/c))  
r : reductionrelation?  
t : any/c 
(applyreductionrelation* r t) → (listof any/c) 
r : reductionrelation? 
t : any/c 
Examples:  
> (definelanguage emptylang)  
 
> (applyreductionrelation R 0)  
'(2 1)  
> (applyreductionrelation* R 0)  
'(1) 