This page works through an extended version of
λv. It goes at a faster pace than
tutorial, highlighting a few key parts of Redex.
The extended language starts with the language in
the Why PLT Redex? page, but
adds numbers, addition, a conditional
expression, multi-arity procedures, and treats
+ as a value. The complete version, with added test cases, is
To follow along, start up DrRacket and enter this code fragment:
Here is the grammar for the language, written as code for PLT Redex:
language. The first part of the line specifies the non-terminal, and the remaining expressions on the line are productions for that non-terminal. Each production is written as a pattern, where non-terminals written in the pattern refer to the non-terminals in this grammar, and other symbols in the grammar are treated as literals (eg
λ). The pattern
(variable-except λ + if0)matches any symbol except those listed (in this case,
The reduction rules also translate literally into a use of the
-->matches expressions where a syntactic term of the form
(+ number number)is the next step to be performed. It also binds the pattern metavariables
number_2to the context and
+'s operands, respectively. In general, pattern variables with underscores must match the non-terminal before the underscore and bind variables to be used in the consequence of the rule.
The second argument to
--> is a new
in-hole pattern that appears
on the left-hand side of the rule is dual to
in-hole term constructor used on the
right-hand side. The former decomposes an expression into a
context and a hole, and the latter composes an expression
from a context and its hole's new content. The addition
operation is replaced by the sum of the operands; the comma
is used to escape to Racket and use its
operator (numeric constants in S-expressions are identical
to the numbers they represent). The
term form is PLT Redex's general-purpose tool for building
S-expressions. Here we use it only to dereference pattern variables.
"+" gives a name to this reduction rule; the names
are used in the GUI.
The second and third rules specify how
behaves. If its first argument is
if-expression reduces to its first alternative. The third
rule uses a side-condition to ensure that it only applies
when the test position of the
if0 expression is
non-zero. This side-condition is required, since the cases
in a reduction relation are applied in an un-ordered
fashion. If multiple rules match, the system just produces
The final rule specifies that function application rewrites
via substitution. In general,
... means to
duplicate the expression before it as many times (including
zero) as is necessary. In this case, the subscript on the
ellipses mean that the number of duplications must match. In
other words, the number of formal parameters must match the number of actual parameters.
Although substitution functions are
generally omitted when writing a paper, PLT Redex requires
you to write it out.
The substitution function
accepts an arbitrary number of variables and recursively
subst, which performs the substitution.
subst function is where the real work
of substitution happens.
Here is its definition.
e, it makes no assumptions about the structure of its input, using Redex's
anypattern (a built-in pattern that matches any term).
The first case avoids substituting
x_1 into the
body of a λ-expression when it binds
The second case is a general purpose capture-avoiding step. It avoids
capture by renaming the variable
x_new in body of the
λ-expression being substituted into. The where clause chooses the
particular name bound to the meta-variable
x_new. The unquote
beginning the clause's right-hand side escapes back to Scheme to use
variables-not-in function, which accepts an expression and a list
of variables. It returns a list of variables that do not occur in its
first argument, preferring to return the corresponding variable from
its second argument, if possible. If not, it returns a symbol whose
printed form begins with the printed form of the corresponding symbol
in the second argument.
subst recurs in the body, it uses
subst-vars helper function, rather than
subst-varsdoes a capturing substitution. It blindly replace all occurrences of the variables in its first argument that appear anywhere in its third argument. It is safe in this case because we know that the new variables are freshly generated and thus cannot capture or be captured.
subst function did not
subst-var to recur in the second case, then
it would be correct but would take exponential time, in the
worst case. In particular, if the input is a series of
nested λ-expressions that bind variables that are all in
the expression that is to be substituted, each λ-expression
will generate two recursive calls, each of which will also
generate two recursive calls, etc, leading to an exponential
number of recursive calls.
The third and fourth cases of
handle variables, first when the variable being substituted
matches the variable being substituted for and second when
it does not.
The remaining rules recur into the structure of the term,
but treating it as an arbitrary S-expression. Accordingly,
if you were to add new, non-binding forms to
this substitution function would not need to change.
traces, we can visualize reduction
sequences in λv. Evaluating the expression:
traces. The nodes are free form, and have been rearranged vertically; in addition the mouse was over the last term, causing the edges into and out of that term to be a darker blue.
Once we've explored the reduction system a little bit,
we might formulate a conjecture about it. For example, one
might believe that each non-value expression reduces.
To test that conjecture using
we can define two functions, one that tests valueness
and one that tests if an expression reduces: