This page works through an extended version of λ_v. It is based on the langauge in the Why PLT Redex? page, but also includes numbers, addition, a conditional expression, multi-arity procedures, and treats + as a value. The complete version, with added test cases, is here: lam-v.ss.

To follow along, start up DrScheme, put it in the (module ...) programming language (use the Language|Choose Language... menu item to set the language), and start with this code fragment:

Here is the grammar for the language, written as code for PLT Redex:

The traditional mathematical notation translates directly into PLT Redex: each line in a BNF description of λ_v's grammar becomes one line in 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 +, if0, and λ). The pattern (variable-except λ + if0) matches any symbol except those listed (in this case, λ, +, and if0).

The reduction rules also translate literally into a use of the reduction-relation form.

The first reduction rule defines the semantics of addition. The pattern in the first argument to the first --> matches expressions where a syntactic term of the form (+ number number) is the next step to be performed. It also binds the pattern metavariables E_1, number_1, and number_2 to 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 S-expression. The in-hole pattern that appears on the left-hand side of the rule is dual to the 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 Scheme 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. Finally the "+" gives a name to this reduction rule; the names are used in the GUI.

The second and third rules specify how if0 behaves. If its first argument is 0, the 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 multiple outcomes.

The final rule specifies that function application rewrites via substitution. Although substitution functions are generally omitted when writing a paper, PLT Redex requires you to write it out.

The substitution function subst-n accepts an arbitrary number of variables and recursively calls subst, which performs the substitution.

The subst function is where the real work of substitution happens. Here is its definition.

It accepts a variable, an expression to be substituted, and an expression to substitute. It is defined in cases that are based on the structure of the expression being substituted into (the last argument), but rather assuming that the input is an e, it makes no assumptions about the structure of its input, using Redex's any pattern (a built-in pattern that matches any term).

The first case avoids substituting x_1 into the body of a λ-expression when it binds x_1. The second case is a general purpose capture-avoiding step. It avoids capture by renaming the variable x_2 to x_new in body of the λ-expression being substituted into. The unquote escapes back to Scheme to use term-let, a form that binds variables in term expressions. The variable-not-in function accepts an expression and a variable. It returns a variable that does not occur in its first argument, prefering to return its second argument, if possible. If not, it returns a symbol whose printed form begins with the printed form of its second argument.

When subst recurs in the body, it uses the subst-vars helper function, rather than using subst.

The subst-vars does 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.

If the subst function did not use 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 subst 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 e, this substitution function would not need to change.

With traces, we can visualize reduction sequences in λ_v. Evaluating the expression:

produces a window containing a graph of the reduction sequence starting at the term passed to 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.