Playing the Game with PLT Redex
Prerequisites: Functional programming with pattern matching, and the basics of Racket.
Download the code and follow along in DrRacket.
Table of Contents
 Abstract
 Introduction
 Terms
 Pattern Matching
 Languages
 Metafunctions
 Reduction Relations
 Predicate Relations
 Judgment Forms
 Visualization
 Other Features
 Limitations
 Related Work
 Conclusion
 Acknowledgments
Abstract
PLT Redex is a tool for modeling programming languages, operational semantics, type systems, program analyses, and so forth. It is designed after the notation established by research papers, and the existing educational material for PLT Redex targets experienced programminglanguage researchers. But when I started to learn PLT Redex, I was new to the field, so I struggled both with the research papers and with the education material. Through the struggle, I noticed that this was a twoway street: reading papers helped me to understand PLT Redex, but perhaps more importantly, understanding PLT Redex helped me to read papers. I became more fluent in the notation, and could implement the theory in the papers more easily. PLT Redex was lowering the cost of experimenting, and supporting the most effective kind of reading: active reading.
With time, I realized that there is no magic in PLT Redex—it is just functional programming with pattern matching. I wish someone had told me that without bringing up Greek letters and jargon, and this is what I want to do to fellow programmers who are trying to break into programminglanguage theory. I write this article from the other side of the bump hoping to smooth the path for those that follow.
We will (ab)use PLT Redex to play a game of Peg Solitaire. Through this simple board game we will explore functional programming, pattern matching, contract verification, nondeterministic computation, visualization, typesetting, test generation, and so forth. This is a fun exercise of repurposing a tool for a task beyond its intended design, and it is a first step toward the virtuous cycle between knowing PLT Redex and reading papers.
We begin with the minimum to go from nothing to playing the game as quickly as possible. We then start over and redo everything, going into more detail. We model Peg Solitaire elements (for example, pegs and boards) as terms and match them against patterns. We formalize the notion of which terms represent Peg Solitaire elements with a language and define metafunctions on this language. We model moves and the winning condition in Peg Solitaire with forms capable of nondeterministic computation: reduction relations, predicate relations, and judgment forms. We play the game with the visualization tools. We glance at other features, including test generation and typesetting. Finally, we discuss limitations and related work, and conclude.
Introduction
Peg Solitaire is a singleplayer board game that starts with the following board (in the most common American version, which is the version we’ll use in this article):
With each move, a peg can jump over one of its four immediate neighbors and land on a space. The neighbor peg that was jumped over is removed from the board. For example, the following are the four possible starting moves:
The following are examples of invalid moves:

A peg cannot jump diagonally:
○ ○ ○ ○ ○ ○ ○ ○ ○ ○ ○ ○ ○ ● ○ ○ ○ ○ ○ ✗ ○ ○ ○ ○ ○ ○ ○ ○ ○
●○ ○ ○ ○ ➡ ○ ○○○ ○ ○ ○ ○ ○ ○ ○ ○ ○ ○ ○ ○ ○ ● ○ ○ ○ ○ ○ ○ ○ ○ ○ ○ ○ ○ ○ ○ ○ 
A peg cannot jump beyond its neighbor:
○ ○ ○ ○ ○ ○ ○ ○ ○ ○ ○ ○ ○ ○ ○ ○ ○ ○ ○ ✗ ○ ○ ○ ○ ○ ○ ○ ○ ●
●○ ○ ○ ○ ➡ ○ ○○○ ● ○ ○ ○ ○ ○ ○ ○ ○ ○ ○ ○ ○ ○ ○ ○ ○ ○ ○ ○ ○ ○ ○ ○ ○ ○ ○ ○ ○ 
A peg cannot jump over multiple neighbors:
○ ○ ○ ○ ○ ○ ○ ○ ○ ○ ○ ○ ○ ○ ○ ○ ○ ○ ○ ✗ ○ ○ ○ ○ ○ ○ ○ ○ ●
●●○ ○ ○ ➡ ○ ○○○● ○ ○ ○ ○ ○ ○ ○ ○ ○ ○ ○ ○ ○ ○ ○ ○ ○ ○ ○ ○ ○ ○ ○ ○ ○ ○ ○ ○
The goal of Peg Solitaire is to leave a single peg on the board, for example:
The following is an example of a lost game in which two pegs remain on the board, but they are not neighbors, so there are no moves left:
Prototype
Our first implementation is the bare minimum to play the game. Over the course of the next sections we revisit the corners we cut and dive deeper into each topic.
We start by requiring PLT Redex:
Most PLT Redex forms work over languages, so we define a language for Peg Solitaire:
(definelanguage pegsolitaire)
The pegsolitaire
language is analog to a programming language, for example, Racket or Ruby. Programs and program fragments in these programming languages are called terms, for example, the following are terms in Racket:
In the pegsolitaire
language, however, terms are not programs and program fragments, but Peg Solitaire entities, for example, pegs and boards. From PLT Redex’s perspective, programs are data structures, and we abuse this notion to represent Peg Solitaire entities. (The idea that programs are data structures isn’t unique to PLT Redex; it’s shared by any program that works on other programs, for example, compilers, interpreters, linters, and so forth.) The definition of the pegsolitaire
language above does not specify the language shape—it does not define which terms represent which Peg Solitaire entities—but it suffices for our prototype (we revisit it in a later section).
Terms in PLT Redex can be any Sexpression, including identifiers (symbols), numbers, strings, lists, and so forth. We represent a Peg Solitaire board with a list of lists of positions, each of which may be symbols representing pegs, spaces, and paddings:
PLT Redex does not check that the initialboard
is in the pegsolitaire
language, so the listing above works despite the definition of the pegsolitaire
language not specifying what constitutes a board.
To model how a player moves pegs on the board, we use a PLT Redex form called reductionrelation
to define the ⇨
reduction relation. A reduction relation is similar to a function, except that it is nondeterministic, possibly returning multiple outputs. We choose to define ⇨
as a reduction relation instead of a regular function because there might be multiple moves for a given input board. We start to define ⇨
as a reduction relation that operates on the pegsolitaire
language:
We then provide one clause for each kind of possible move. For example, for a peg to jump over its right neighbor, we must find a sequence ● ● ○
on the board, and that sequence turns into ○ ○ ●
after the move, while the rest of the board remains the same. We write this as a reductionrelation
as follows:
(> (any_1
...
[any_2 ... ● ● ○ any_3 ...]
any_4
...)
(any_1
...
[any_2 ... ○ ○ ● any_3 ...]
any_4
...)
"→")
In the listing above, the >
form represents one kind of possible move. The first subform is a pattern against which the input board is matched, the second subform is the template with which to generate the output, and the third subform is the name of this kind of move, →
. The several any_<n>
preserve the rest of the board around the moved pegs.
We define the other kinds of moves similarly. The following is the complete definition of ⇨
:
(define
⇨
(reductionrelation
pegsolitaire
(> (any_1
...
[any_2 ... ● ● ○ any_3 ...]
any_4
...)
(any_1
...
[any_2 ... ○ ○ ● any_3 ...]
any_4
...)
"→")
(> (any_1
...
[any_2 ... ○ ● ● any_3 ...]
any_4
...)
(any_1
...
[any_2 ... ● ○ ○ any_3 ...]
any_4
...)
"←")
(> (any_1
...
[any_2 ..._n ● any_3 ...]
[any_4 ..._n ● any_5 ...]
[any_6 ..._n ○ any_7 ...]
any_8
...)
(any_1
...
[any_2 ... ○ any_3 ...]
[any_4 ... ○ any_5 ...]
[any_6 ... ● any_7 ...]
any_8
...)
"↓")
(> (any_1
...
[any_2 ..._n ○ any_3 ...]
[any_4 ..._n ● any_5 ...]
[any_6 ..._n ● any_7 ...]
any_8
...)
(any_1
...
[any_2 ... ● any_3 ...]
[any_4 ... ○ any_5 ...]
[any_6 ... ○ any_7 ...]
any_8
...)
"↑")))
Playing
PLT Redex features visualization tools, including a stepper
, which we use to play Peg Solitaire:
(stepper ⇨ (term initialboard))
On the following sections we revisit each step of modeling Peg Solitaire in PLT Redex in more detail, starting with terms.
Terms
At a high level, PLT Redex is a tool for manipulating and visualizing Sexpressions (identifiers, numbers, strings, lists, and so forth), which PLT Redex calls terms. In programming languages, terms represent programs and program fragments, types, machine states, and so forth. In Peg Solitaire, terms represent pegs, boards, and so forth. We use the term
form to construct terms from Racket values, for example:
We represent pegs with ●
and spaces with ○
:
(testequal (term ●)
'●)
(testequal (term ○)
'○)
We can group pegs and spaces together in lists:
(testequal (term (● ● ○))
'(● ● ○))
We can assign terms to names in PLT Redex with the defineterm
form. We can then refer to these names in other terms:
(defineterm apeg ●)
(testequal (term apeg)
'●)
We represent a Peg Solitaire board as a list of rows; a row as a list of positions; and a position as either a peg (●
), a space (○
) or a padding (·
). We choose this representation because it is visually appealing, but it is not the only possibility. For example, we could represent pegs as 1s and spaces as 0s, in which case the whole board would be a just a (binary) number. The following are examples of boards:
The following is the initial board:
(defineterm initialboard
([· · ● ● ● · ·]
[· · ● ● ● · ·]
[● ● ● ● ● ● ●]
[● ● ● ○ ● ● ●]
[● ● ● ● ● ● ●]
[· · ● ● ● · ·]
[· · ● ● ● · ·]))
And the following is an example of a winning board:
(defineterm examplewinningboard
([· · ○ ○ ○ · ·]
[· · ○ ○ ○ · ·]
[○ ○ ○ ○ ○ ○ ○]
[○ ○ ○ ● ○ ○ ○]
[○ ○ ○ ○ ○ ○ ○]
[· · ○ ○ ○ · ·]
[· · ○ ○ ○ · ·]))
We will use these boards for testing in later sections, so we provide
them here:
(provide exampleboard1 exampleboard2
initialboard examplewinningboard)
Next, we explore the most common operation on terms, pattern matching.
Pattern Matching
Pattern matching is the foundation of all the PLT Redex forms we will explore in the later sections. Pattern matching has two purposes: to verify whether a term matches a pattern, and to assign names to the parts that were matched. To experiment with pattern matching, we must first define a language, but to define a language we must first understand pattern matching. We solve this conundrum the same way we solved it in the Introduction: by defining a dummy empty language, which we will revisit in the next section:
We verify whether a term matches a pattern with the redexmatch?
form:
(redexmatch? <language> <pattern> <term>)
The simplest kind of pattern is a literal term, for example:
(testequal (redexmatch? pegsolitaire ●
(term ●))
#t)
(testequal (redexmatch? pegsolitaire (● ● ○)
(term (● ● ○)))
#t)
For example, the listing above shows that the pattern ●
matches the term (term ●)
.
The Underscore (_
) and the any
Patterns
The underscore pattern (_
) means “anything” (similar to the dot (.
) in regular expressions). For example:
(testequal (redexmatch? pegsolitaire _
(term ●))
#t)
(testequal (redexmatch? pegsolitaire (_ ● ○)
(term (● ● ○)))
#t)
(testequal (redexmatch? pegsolitaire (_ _ ○)
(term (● ● ○)))
#t)
(testequal (redexmatch? pegsolitaire (_ _ _)
(term (● ● ○)))
#t)
(testequal (redexmatch? pegsolitaire _
(term (● ● ○)))
#t)
In the listing above, the underscore pattern (_
) can match either the elements in the list, or the whole list (last example). Another pattern that matches anything is the any
pattern, for example:
(testequal (redexmatch? pegsolitaire (any ● ○)
(term (● ● ○)))
#t)
But the underscore pattern (_
) and the any
pattern are not equivalent, because only the latter introduces names. In the next sections we will explore forms in which patterns not only recognize terms, but also name the fragments that were matched, so we can use them to build other terms. These names are similar to the ones we defined with defineterm
in the previous section, but they are available only within the forms containing the pattern.
We can observe the names a pattern introduces with the redexmatch
form, which is similar to the redexmatch?
form but returns the introduced names instead of just whether the pattern matched or not:
In the first interaction, no names are introduced, as indicated by the empty list '()
, and in the second interaction the name any
is associated with the matched fragment ●
. This is the output in more detail:
(list⁶ (match⁵ (list⁴ (bind³ 'any¹ '●²))))
any
: The name in the pattern.●
: The term that was matched byany
.bind
: The binding data structure representing the association between the name and the term.list
: There might be multiple bindings in a pattern.match
: The matching data structure representing one way to match the term with the pattern.list
: There might be multiple ways to match a term with a pattern.
Both the underscore (_
) and the any
patterns may appear multiple times in a pattern. When introducing the underscore pattern above, we saw that multiple uses of the underscore in the same pattern may match different fragments, for example, the pattern (_ _ _)
matches the term (● ● ○)
, so _
corresponds to ●
and ○
. But the any
pattern assigns a name to the fragment it matches, so if it appears multiple times in a pattern, it must match the same fragment every time, for example:
(testequal (redexmatch? pegsolitaire (any any ○)
(term (● ● ○)))
#t)
(testequal (redexmatch? pegsolitaire (any ● any)
; ≠
(term (● ● ○)))
#f)
The second pattern in the listing above does not match (note the #f
) because the any
name cannot be associated with ●
and ○
at the same time.
A pattern may include multiple any
s that associate with different terms by adding a suffix, any_<suffix>
, for example:
(testequal (redexmatch? pegsolitaire (any_1 any_2 any_3)
(term (● ● ○)))
#t)
> (redexmatch pegsolitaire (any_1 any_2 any_3)
(term (● ● ○)))
(list (match (list (bind 'any_1 '●) (bind 'any_2 '●) (bind 'any_3 '○))))
Each any_<suffix>
was associated with a different term.
We can require that the first and second list elements are the same, but allow the third to differ by using any_1
twice, for example:
(testequal (redexmatch? pegsolitaire (any_1 any_1 any_2)
(term (● ● ○)))
#t)
> (redexmatch pegsolitaire (any_1 any_1 any_2)
(term (● ● ○)))
(list (match (list (bind 'any_1 '●) (bind 'any_2 '○))))
Using different suffixes allows patterns to match different terms, but does not require them to be different, for example:
(testequal (redexmatch? pegsolitaire (any_1 any_1 any_2)
(term (● ● ●)))
#t)
> (redexmatch pegsolitaire (any_1 any_1 any_2)
(term (● ● ●)))
(list (match (list (bind 'any_1 '●) (bind 'any_2 '●))))
The pattern does not match if the two occurrences of any_1
are different, for example:
(testequal (redexmatch? pegsolitaire (any_1 any_1 any_2)
; ≠
(term (● ○ ○)))
#f)
Ellipses
We can match a sequence of terms using ellipsis (...
), which means “zero or more of the previous pattern” (similar to the Kleene star (*
) in regular expressions). For example:
(testequal (redexmatch? pegsolitaire (any ...)
(term (● ● ○)))
#t)
> (redexmatch pegsolitaire (any ...)
(term (● ● ○)))
(list (match (list (bind 'any '(● ● ○)))))
In the listing above the name any
was associated with the sequence ● ● ○
.
A pattern may match a term in multiple ways when it includes multiple ellipses, for example:
(testequal (redexmatch? pegsolitaire (any_1 ... any_2 ...)
(term (● ● ○)))
#t)
> (redexmatch pegsolitaire (any_1 ... any_2 ...)
(term (● ● ○)))
(list
(match (list (bind 'any_1 '()) (bind 'any_2 '(● ● ○))))
(match (list (bind 'any_1 '(●)) (bind 'any_2 '(● ○))))
(match (list (bind 'any_1 '(● ●)) (bind 'any_2 '(○))))
(match (list (bind 'any_1 '(● ● ○)) (bind 'any_2 '()))))
Similar to how we suffixed any
, we can suffix ellipses, ..._<suffix>
, constraining them to match sequences of the same length, for example:
(testequal (redexmatch? pegsolitaire (any_1 ..._n any_2 ..._n)
(term (● ● ○ ●)))
#t)
> (redexmatch pegsolitaire (any_1 ..._n any_2 ..._n)
(term (● ● ○ ●)))
(list (match (list (bind 'any_1 '(● ●)) (bind 'any_2 '(○ ●)))))
(testequal (redexmatch? pegsolitaire (any_1 ..._n any_2 ..._n)
; ≠
(term (● ● ○)))
#f)
In the listing above, the first pattern matches because it can divide the term into two sequences of the same length and satisfy the ..._n
constraint. But the last pattern does not match because there is no way to divide a 3element list into two sequences of the same length. Ellipses with different suffixes may match sequences of different lengths, for example:
(testequal (redexmatch? pegsolitaire (any_1 ..._n any_2 ..._m)
(term (● ● ○)))
#t)
In the listing above ellipses can match sequences of different lengths because they have different suffixes (which in this case is equivalent to not suffixing the ellipses).
Finally, we can nest ellipses, and they still mean “zero or more of the previous pattern,” even if this pattern contains ellipses itself. With this, we can define a pattern that matches the initialboard
from the previous section:
The pattern fragment [· ... ● ... ○ ... ● ... · ...]
means “a sequence of zero or more paddings (·
), followed by a sequence of zero or more pegs (●
), followed by a sequence of zero or more spaces (○
), followed by a sequence of zero or more pegs (●
), followed by a sequence of zero or more paddings (·
).” This matches a single row of the initial board, regardless of whether it is the first row, [· · ● ● ● · ·]
(which includes paddings but no spaces), or the fourth row, [● ● ● ○ ● ● ●]
(which includes a space but no paddings). The pattern fragment ([___] ...)
means “zero or more rows.”
Next, we use pattern matching to define the shape of terms that represent Peg Solitaire elements with a language.
Languages
A language defines patterns for terms and gives them names. In programming languages, a language determines which terms are programs and which are not. A language might also include extra machinery, for example, binding and type environments, stores, machine states, and so forth. This extra machinery is invisible to programmers, but is used by an interpreter or a type checker, for example. In general, if terms are data, then languages are the definitions of data structures. They provide names for the patterns we explored in the previous section.
A language for Peg Solitaire must specify the patterns for terms that represent pegs, boards, and so forth. In the previous section, we defined a placeholder language called pegsolitaire
, using the definelanguage
form. The specification was empty, because we just wanted enough to allow us to explore pattern matching, so we revisit that language definition now to add names for patterns:
Each line [<name> ::= <pattern> ...]
assigns a <name>
to a <pattern>
, and occurrences of other <name>
s in <pattern>
are interpreted accordingly, for example, the name row
appears in the pattern for board
. Patterns in the definelanguage
form are the only ones in which multiple occurrences of a name can match different terms. For example, if a language includes the line [pair ::= (position position)]
then pair
would match the term (● ○)
. To insist on the same term, suffix the names, for example, [pair ::= (position_1 position_1)]
. The following is each line of the definition above in more detail:
[board ::= (row ...)]
: Aboard
is a list of zero or morerow
s.[row ::= [position ...]]
: Arow
is a list of zero or moreposition
s.[position ::= peg space padding]
: Aposition
is either apeg
, or aspace
, or apadding
.[peg ::= ●]
: Apeg
is literally the term●
. Similarly forspace
andpadding
.
We can use the pattern names (also know as nonterminals) when matching terms, for example:
(testequal (redexmatch? pegsolitaire peg
(term ●))
#t)
(testequal (redexmatch? pegsolitaire position
(term ●))
#t)
(testequal (redexmatch? pegsolitaire (peg ● ○)
(term (● ● ○)))
#t)
(testequal (redexmatch? pegsolitaire (position ● ○)
(term (● ● ○)))
#t)
(testequal (redexmatch? pegsolitaire (position position ○)
(term (● ● ○)))
#t)
Multiple occurrences of a name must match the same term, so the following does not match because position
cannot be ●
and ○
at the same time:
(testequal (redexmatch? pegsolitaire (position position position)
; ≠
(term (● ● ○)))
#f)
We can suffix the names to allow them to match to different terms:
(testequal (redexmatch? pegsolitaire (position_1 position_2 position_3)
(term (● ● ○)))
#t)
We can use the pegsolitaire
language to match the board examples:
(testequal (redexmatch? pegsolitaire board (term exampleboard1))
#t)
(testequal (redexmatch? pegsolitaire board (term exampleboard2))
#t)
(testequal (redexmatch? pegsolitaire board (term initialboard))
#t)
(testequal (redexmatch? pegsolitaire board (term examplewinningboard))
#t)
Our language is too permissive, allowing board
to match terms we consider illformed boards, for example:
(testequal (redexmatch? pegsolitaire board (term ([● ○]
[●])))
#t)
The term above does not represent a Peg Solitaire board: it is too small and the rows have different sizes. Yet, the board
pattern in the pegsolitaire
language matches it. We could refine the language definition so that it would match exactly the terms that represent Peg Solitaire elements, but that would be more complicated and would fail to communicate our intent to our readers. The named patterns we introduced in pegsolitaire
will serve well for the definitions in the following sections, so this simpler language specification suffices. We will proceed assuming all boards are wellformed, and in a few cases we will even use illformed boards on purpose to simplify tests. If more rigor was necessary, we could define a predicate relation that only holds for wellformed boards, and test the inputs to the forms we will define in later sections.
We will use the pegsolitaire
language in later sections, so we provide
it here:
(provide pegsolitaire)
Now that we have a language, we can operate on terms. On the next section, we cover the most familiar operation, the metafunction.
Metafunctions
From all the PLT Redex forms for manipulating with terms, we begin with the metafunction because it is the most familiar—it is just a function on terms. We define a metafunction with the definemetafunction
form including patterns that match the input terms, and templates to compute the output terms:
(definemetafunction <language>
<contract>
[(<metafunction> <pattern> ...) <template>]
...)
<language>
: A language as defined in the previous section.<contract>
: A contract with patterns for the inputs and outputs of the metafunction. The contract is verified and an error may be raised if the metafunction is called with invalid inputs or produces an invalid output.[(<metafunction> <pattern> ...) <template>]
: A metafunction clause.<metafunction>
: The metafunction name.<pattern>
: Patterns against which the metafunction inputs are matched. Patterns are tried clause by clause in the order they are defined, and the first clause that matches is executed.<template>
: A term that is the output of the metafunction. Names from the<pattern>
are available in the<template>
.
A metafunction is similar to define/match
in that it compares the inputs to patterns and executes the first clause that matches. More generally, it is similar to forms for multiway conditionals, for example, case
and cond
.
When we introduced patterns, we noted that they are to terms as regular expressions are to strings, and we used the redexmatch?
form to recognize terms the same way we can use regular expressions to match strings. Continuing that analogy, a metafunction is similar to a searchandreplace with regular expressions including capture groups.
In programming languages, metafunctions are the small utilities, for example, substituting variables for their values (a metafunction generally notated as programfragment[variable\value]
), and evaluating primitive operators (a metafunction generally named δ
).
We define a metafunction to invert a position
:
In the listing above, we define the invert/position
metafunction for the pegsolitaire
language. Its input and output are position
s. The invert/position
metafuction compares the input to each of the patterns in turn: peg
, space
, and padding
. The first pattern that matches determines the metafunction output: ○
, ●
, and ·
, respectively. The last clause exemplifies how a name in the pattern (padding
) is available in the template.
We use a metafunction by applying it on terms:
We can call a metafunction from any place in which a term might appear, including the definition of another metafunction. To illustrate this, consider the following metafunction that inverts a whole board by calling invert/position
on each position
:
(definemetafunction pegsolitaire
invert/board : board > board
[(invert/board ([position ...] ...))
([(invert/position position) ...] ...)])
The invert/board
metafunction matches its input to the pattern ([position ...] ...)
, which represents boards. Its output is the result of calling invert/position
on each position
: the ellipses (...
) after the metafunction call mean “map over the position
s with the metafunction invert/position
.” The following is an example of calling the invert/board
metafunction with the initialboard
:
(testequal (term (invert/board initialboard))
(term ((· · ○ ○ ○ · ·)
(· · ○ ○ ○ · ·)
(○ ○ ○ ○ ○ ○ ○)
(○ ○ ○ ● ○ ○ ○)
(○ ○ ○ ○ ○ ○ ○)
(· · ○ ○ ○ · ·)
(· · ○ ○ ○ · ·))))
We defined two metafunctions in this section only for illustration—we do not use them to play the game. But the digression is over, because in the next section we cover reduction relations, which we use to model Peg Solitaire moves.
Reduction Relations
In functions, including metafunctions, each input relates to one output. When we enumerate a function, each input appears only once on the left column, for example:
position (invert/position position) ● ○ ○ ● · ·
A function (or a method, a procedure, a routine, and so forth) is not a natural way to model moves in Peg Solitaire, because there might be multiple moves available for a given board. If functions were all we had, then we could encode our intent with a ⇨/function
that returned a set of output boards, for example:
board (⇨/function board) (term (set ([· · ● ● ● · ·] (term [· · ● ● ● · ·] ([· · ● ● ● · ·] [● ● ● ● ● ● ●] [· · ● ● ● · ·] [● ● ● ○ ● ● ●] [● ● ● ● ● ● ●] [● ● ● ● ● ● ●] [● ○ ○ ● ● ● ●] [· · ● ● ● · ·] [● ● ● ● ● ● ●] [· · ● ● ● · ·])) [· · ● ● ● · ·] [· · ● ● ● · ·])) (term ([· · ● ● ● · ·] [· · ● ● ● · ·] [● ● ● ● ● ● ●] [● ● ● ● ○ ○ ●] [● ● ● ● ● ● ●] [· · ● ● ● · ·] [· · ● ● ● · ·])) (term ([· · ● ● ● · ·] [· · ● ○ ● · ·] [● ● ● ○ ● ● ●] [● ● ● ● ● ● ●] [● ● ● ● ● ● ●] [· · ● ● ● · ·] [· · ● ● ● · ·])) (term ([· · ● ● ● · ·] [· · ● ● ● · ·] [● ● ● ● ● ● ●] [● ● ● ● ● ● ●] [● ● ● ○ ● ● ●] [· · ● ○ ● · ·] [· · ● ● ● · ·]))) ⋮
But a function is just a special case of relation, which may relate one input to multiple outputs. While all functions are relations, not all relations are functions. When we enumerate a relation that may not be a function, each input may appear on the left column multiple times. For example, we can define a relation called ⇨
to model moves in Peg Solitaire:
board (⇨ board) (term (term ([· · ● ● ● · ·] ([· · ● ● ● · ·] [· · ● ● ● · ·] [· · ● ● ● · ·] [● ● ● ● ● ● ●] [● ● ● ● ● ● ●] [● ● ● ○ ● ● ●] [● ○ ○ ● ● ● ●] [● ● ● ● ● ● ●] [● ● ● ● ● ● ●] [· · ● ● ● · ·] [· · ● ● ● · ·] [· · ● ● ● · ·])) [· · ● ● ● · ·])) (term (term ([· · ● ● ● · ·] ([· · ● ● ● · ·] [· · ● ● ● · ·] [· · ● ● ● · ·] [● ● ● ● ● ● ●] [● ● ● ● ● ● ●] [● ● ● ○ ● ● ●] [● ● ● ● ○ ○ ●] [● ● ● ● ● ● ●] [● ● ● ● ● ● ●] [· · ● ● ● · ·] [· · ● ● ● · ·] [· · ● ● ● · ·])) [· · ● ● ● · ·])) (term (term ([· · ● ● ● · ·] ([· · ● ● ● · ·] [· · ● ● ● · ·] [· · ● ○ ● · ·] [● ● ● ● ● ● ●] [● ● ● ○ ● ● ●] [● ● ● ○ ● ● ●] [● ● ● ● ● ● ●] [● ● ● ● ● ● ●] [● ● ● ● ● ● ●] [· · ● ● ● · ·] [· · ● ● ● · ·] [· · ● ● ● · ·])) [· · ● ● ● · ·])) (term (term ([· · ● ● ● · ·] ([· · ● ● ● · ·] [· · ● ● ● · ·] [· · ● ● ● · ·] [● ● ● ● ● ● ●] [● ● ● ● ● ● ●] [● ● ● ○ ● ● ●] [● ● ● ● ● ● ●] [● ● ● ● ● ● ●] [● ● ● ○ ● ● ●] [· · ● ● ● · ·] [· · ● ○ ● · ·] [· · ● ● ● · ·])) [· · ● ● ● · ·])) ⋮
The ⇨
relation models moves in Peg Solitaire more straightforwardly than the ⇨/function
function. The listing above is similar to how we wrote our examples in the game description:
● ● ● ● ● ● ● ● ● ● ○ ● ● ● ●●● ● ● ● ● ●○● ● ● ● ● ● ○ ● ● ● ➡ ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ○●● ● ➡ ● ● ● ●○○ ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ○ ● ● ● ➡ ● ● ● ● ● ● ● ● ● ●●● ● ● ● ● ●○● ● ● ● ● ● ● ○ ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ●●○ ● ● ● ➡ ● ○○● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● jumps over●
Most programming languages only support functions, and when we use them, we have to resort to an encoding similar to ⇨/function
, but PLT Redex supports relations that may not be functions, so we can define the ⇨
relation directly. Among the different PLT Redex forms for defining relations, the first we encounter is reductionrelation
:
(reductionrelation
<language>
#:domain <pattern>
(> <pattern> <template> <name>)
...)
<language>
: A language as defined previously.#:domain
: A contract pattern for the inputs and outputs of the reduction relation. The contract is verified and an error may be raised if the reduction relation is applied to an invalid input or produces an invalid output.(> <pattern> <template> <name>)
: A reduction relation clause.<pattern>
: A pattern for the input.<template>
: A template for the output.<name>
: A name for the clause.
The reductionrelation
form returns the reduction relation as a value, unlike the other forms we discussed so far that assign names, for example, definelanguage
and definemetafunction
. If we want to assign a name to a reduction relation, we need to use define
:
(define <name>
(reductionrelation ___))
The shape of the reductionrelation
form is similar to that of definemetafunction
: it is a series of clauses with patterns for the inputs and templates for the outputs. The difference between the two is in how they proceed when multiple clauses match the input: while a metafunction follows the definition order and chooses the first clause that matches, a relation chooses all clauses. We say metafunctions compute deterministically, because an input determines exactly one output, while relations may compute nondeterministically.
The ⇨
Reduction Relation
The ⇨
reduction relation has four clauses, one for each kind of move. The following is the clause for when a peg jumps over its neighbor on the right:
In detail:
(row_1 ... [position_1 ... ● ● ○ position_2 ...] row_2 ...)
: The pattern to match against the input board. The pattern matches if the board includes a sequence● ● ○
surrounded by any otherposition
s androw
s, to which we assign the namesposition_<n>
androw_<n>
so that we can reconstruct the board in the template.(row_1 ... [position_1 ... ○ ○ ● position_2 ...] row_2 ...)
: The template to build the board after the move. It changes the sequence● ● ○
into○ ○ ●
, and reconstructs the surroundings with the namesposition_<n>
androw_<n>
."→"
: The name of the clause.
The clause for when a peg jumps over its neighbor on the left is similar. The clauses for when a peg jumps over its neighbors on the top or bottom follow the same idea, but we must use named ellipses (..._<suffix>
) to capture the surroundings involving multiple rows. The named ellipses align the sequence of interest (for example, ● ● ○
) in the same column, because it guarantees that the sequence is preceded by the same number of position
s in each row
. For example, the following is the rule for when a peg jumps over its neighbor on the bottom:
The named ellipses (..._n
) only match sequences position_1
, position_3
and position_5
of the same length, so the sequence ● ● ○
must appear in the same column. The clause for when a peg jumps over its neighbor on the top is similar, and with it we conclude the definition of ⇨
:
We can test the ⇨
reduction relation with the test>
form:
(test> ⇨ (term initialboard)
(term
([· · ● ● ● · ·]
[· · ● ● ● · ·]
[● ● ● ● ● ● ●]
[● ○ ○ ● ● ● ●]
[● ● ● ● ● ● ●]
[· · ● ● ● · ·]
[· · ● ● ● · ·]))
(term
([· · ● ● ● · ·]
[· · ● ● ● · ·]
[● ● ● ● ● ● ●]
[● ● ● ● ○ ○ ●]
[● ● ● ● ● ● ●]
[· · ● ● ● · ·]
[· · ● ● ● · ·]))
(term
([· · ● ● ● · ·]
[· · ● ○ ● · ·]
[● ● ● ○ ● ● ●]
[● ● ● ● ● ● ●]
[● ● ● ● ● ● ●]
[· · ● ● ● · ·]
[· · ● ● ● · ·]))
(term
([· · ● ● ● · ·]
[· · ● ● ● · ·]
[● ● ● ● ● ● ●]
[● ● ● ● ● ● ●]
[● ● ● ○ ● ● ●]
[· · ● ○ ● · ·]
[· · ● ● ● · ·])))
We can also query the ⇨
reduction relation with the applyreductionrelation
form. The applyreductionrelation
form returns a list representing a set of outputs, similar to the ⇨/function
encoding we mentioned above. This is a compromise because PLT Redex has to output an Sexpression, which does not include forms for nondeterministic values or sets. We can turn the returned list into a Racket set
with list>set
, so the following test is equivalent to the previous one:
(testequal (list>set (applyreductionrelation ⇨ (term initialboard)))
(set
(term
([· · ● ● ● · ·]
[· · ● ● ● · ·]
[● ● ● ● ● ● ●]
[● ○ ○ ● ● ● ●]
[● ● ● ● ● ● ●]
[· · ● ● ● · ·]
[· · ● ● ● · ·]))
(term
([· · ● ● ● · ·]
[· · ● ● ● · ·]
[● ● ● ● ● ● ●]
[● ● ● ● ○ ○ ●]
[● ● ● ● ● ● ●]
[· · ● ● ● · ·]
[· · ● ● ● · ·]))
(term
([· · ● ● ● · ·]
[· · ● ○ ● · ·]
[● ● ● ○ ● ● ●]
[● ● ● ● ● ● ●]
[● ● ● ● ● ● ●]
[· · ● ● ● · ·]
[· · ● ● ● · ·]))
(term
([· · ● ● ● · ·]
[· · ● ● ● · ·]
[● ● ● ● ● ● ●]
[● ● ● ● ● ● ●]
[● ● ● ○ ● ● ●]
[· · ● ○ ● · ·]
[· · ● ● ● · ·]))))
If we use applyreductionrelation
repeatedly, feeding one output of an application as the input to the next—something called the transitive closure of the reduction relation—then we can use ⇨
relation to compute all possible Peg Solitaire boards. PLT Redex comes with the applyreductionrelation*
form for this purpose. Unfortunately, there are too many possible boards, so the computation does not terminate in reasonable time:
> (applyreductionrelation* ⇨ (term initialboard))
; Runs for too long
But we can test applyreductionrelation*
on a fragment of the board with a single row, for which the outputs are tractable:
(testequal
(list>set
(applyreductionrelation* #:all? #t ⇨ (term ([● ● ● ○ ● ● ●]))))
(set
(term ((● ● ● ● ○ ○ ●)))
(term ((● ● ○ ○ ● ○ ●)))
(term ((○ ○ ● ○ ● ○ ●)))
(term ((● ○ ○ ● ● ● ●)))
(term ((● ○ ● ○ ○ ● ●)))
(term ((● ○ ● ○ ● ○ ○)))))
We can also query just the final boards, from which we cannot move further, by omitting the #:all?
argument:
(testequal
(list>set (applyreductionrelation* ⇨ (term ([● ● ● ○ ● ● ●]))))
(set
(term ((○ ○ ● ○ ● ○ ●)))
(term ((● ○ ● ○ ● ○ ○)))))
The ⇨
relation is enough to play Peg Solitaire using PLT Redex visualization tools, and we will need it in later sections:
(provide ⇨)
But before we return to this and play Peg Solitaire, we explore in the following sections a few other PLT Redex forms for relations that may not be functions, starting with predicate relations.
Predicate Relations
When we looked at reduction relations, we were interested in transforming terms. We defined clauses with patterns to match against inputs, and templates to produce outputs. But in some cases we are only interested in whether the inputs satisfy certain conditions, for example, whether a board is a winning board—that is, whether it contains a single peg. If we were to define that as a reduction relation, then the output templates would be booleans. For this special case, PLT Redex provides the definerelation
form to define predicate relations:
(definerelation <language>
<contract>
[(<relation> <pattern> ...)])
<language>
: A language as defined previously.<contract>
: A contract with a pattern for the inputs of the predicate relation. The contract is verified and an error may be raised if the predicate relation is queried with invalid inputs.[(<relation> <pattern> ...)]
: A predicate relation clause.<relation>
: The predicate relation name.<pattern>
: Pattern against which the predicate relation inputs are compared. If the patterns match, then the predicate relation holds.
Predicate relations typically check whether a program is well formed, whether a type is a subtype of another type, and so forth. We define a predicate relation to check whether a board is a winning board:
The contract winningboard? ⊆ board
says that the winningboard?
predicate relation is only defined over boards—it would not make sense to ask this question about terms that are not boards. We use the symbol for subsetting (⊆
) because only some boards are winning boards.
The pattern in the predicate relation clause in more detail:
[· ... ○ ... · ...] ...
: Any number of rows without a peg.[· ... ○ ... ● ○ ... · ...]
: A row with a single peg.[· ... ○ ... · ...] ...
: More rows without a peg.
We query the predicate relation by applying it, similar to a metafunction:
(testequal (term (winningboard? exampleboard1))
#f)
(testequal (term (winningboard? exampleboard2))
#f)
(testequal (term (winningboard? initialboard))
#f)
(testequal (term (winningboard? examplewinningboard))
#t)
The predicate relation only holds for the examplewinningboard
.
We will use the predicate relation winningboard?
in a later section when trying to use our model to win Peg Solitaire:
(provide winningboard?)
Next, we cover the most general form of relations that may not be functions: judgment forms.
Judgment Forms
Both reduction relations and predicate relations are special forms of relations. A reduction relation has one input term and one output term, and a predicate relation only has inputs terms, but in general a relation may have any number of input terms and output terms.
It would be more mathematically accurate to not think of terms in a relation as inputs or outputs, but we make this compromise to make it easier to compute with out definitions.
We can define relations in PLT Redex with definejudgmentform
:
(definejudgmentform <language>
#:mode (<judgmentform> <I/O> ...)
#:contract (<judgmentform> <pattern> ...)
[(<judgmentform> <pattern/template> ...)]
...)
<language>
: A language as defined previously.#:mode
: A judgment form may have multiple inputs and outputs, and they all appear as arguments to the form. The#:mode
annotation distinguishes inputs (I
) from outputs (O
).#:contract
: A contract with patterns for the arguments of the judgment form. The contract is verified and an error may be raised if the judgment form is queried with invalid inputs or produces invalid outputs.[(<judgmentform> <pattern/template> ...)]
: A judgment form clause.<judgmentform>
: The judgment form name.<pattern/template>
: A pattern for an input or a template for an output.
We can recreate the ⇨
reduction relation and the winningboard?
predicate relation in terms of judgment forms:
We can test whether a judgment holds with the testjudgmentholds
form:
(testjudgmentholds
(⇨/judgmentform initialboard ([· · ● ● ● · ·]
[· · ● ● ● · ·]
[● ● ● ● ● ● ●]
[● ○ ○ ● ● ● ●]
[● ● ● ● ● ● ●]
[· · ● ● ● · ·]
[· · ● ● ● · ·])))
(testjudgmentholds
(⇨/judgmentform initialboard ([· · ● ● ● · ·]
[· · ● ● ● · ·]
[● ● ● ● ● ● ●]
[● ● ● ● ○ ○ ●]
[● ● ● ● ● ● ●]
[· · ● ● ● · ·]
[· · ● ● ● · ·])))
(testjudgmentholds
(⇨/judgmentform initialboard ([· · ● ● ● · ·]
[· · ● ○ ● · ·]
[● ● ● ○ ● ● ●]
[● ● ● ● ● ● ●]
[● ● ● ● ● ● ●]
[· · ● ● ● · ·]
[· · ● ● ● · ·])))
(testjudgmentholds
(⇨/judgmentform initialboard ([· · ● ● ● · ·]
[· · ● ● ● · ·]
[● ● ● ● ● ● ●]
[● ● ● ● ● ● ●]
[● ● ● ○ ● ● ●]
[· · ● ○ ● · ·]
[· · ● ● ● · ·])))
We can also query a judgment form with the judgmentholds
form. The following listing includes tests for both ⇨/judgmentform
and winningboard?/judgmentform
:
(testequal
(judgmentholds
(⇨/judgmentform initialboard ([· · ● ● ● · ·]
[· · ● ● ● · ·]
[● ● ● ● ● ● ●]
[● ○ ○ ● ● ● ●]
[● ● ● ● ● ● ●]
[· · ● ● ● · ·]
[· · ● ● ● · ·])))
#t)
(testequal
(judgmentholds
(⇨/judgmentform initialboard ([· · ● ● ● · ·]
[· · ● ● ● · ·]
[● ● ● ● ● ● ●]
[● ● ● ● ○ ○ ●]
[● ● ● ● ● ● ●]
[· · ● ● ● · ·]
[· · ● ● ● · ·])))
#t)
(testequal
(judgmentholds
(⇨/judgmentform initialboard ([· · ● ● ● · ·]
[· · ● ○ ● · ·]
[● ● ● ○ ● ● ●]
[● ● ● ● ● ● ●]
[● ● ● ● ● ● ●]
[· · ● ● ● · ·]
[· · ● ● ● · ·])))
#t)
(testequal
(judgmentholds
(⇨/judgmentform initialboard ([· · ● ● ● · ·]
[· · ● ● ● · ·]
[● ● ● ● ● ● ●]
[● ● ● ● ● ● ●]
[● ● ● ○ ● ● ●]
[· · ● ○ ● · ·]
[· · ● ● ● · ·])))
#t)
(testequal
(judgmentholds (winningboard?/judgmentform exampleboard1))
#f)
(testequal
(judgmentholds (winningboard?/judgmentform exampleboard2))
#f)
(testequal
(judgmentholds (winningboard?/judgmentform initialboard))
#f)
(testequal
(judgmentholds (winningboard?/judgmentform examplewinningboard))
#t)
If we provide a pattern in an output position of the judgment form, then judgmentholds
makes the names available in a template we provide as the second argument. The result becomes not only whether the relation holds, but the templates built from terms for which it hold. We can convert this resulting list into a set similar to how we did when testing applyreductionrelation
:
(testequal
(list>set (judgmentholds (⇨/judgmentform initialboard board) board))
(set
(term
([· · ● ● ● · ·]
[· · ● ● ● · ·]
[● ● ● ● ● ● ●]
[● ○ ○ ● ● ● ●]
[● ● ● ● ● ● ●]
[· · ● ● ● · ·]
[· · ● ● ● · ·]))
(term
([· · ● ● ● · ·]
[· · ● ● ● · ·]
[● ● ● ● ● ● ●]
[● ● ● ● ○ ○ ●]
[● ● ● ● ● ● ●]
[· · ● ● ● · ·]
[· · ● ● ● · ·]))
(term
([· · ● ● ● · ·]
[· · ● ○ ● · ·]
[● ● ● ○ ● ● ●]
[● ● ● ● ● ● ●]
[● ● ● ● ● ● ●]
[· · ● ● ● · ·]
[· · ● ● ● · ·]))
(term
([· · ● ● ● · ·]
[· · ● ● ● · ·]
[● ● ● ● ● ● ●]
[● ● ● ● ● ● ●]
[● ● ● ○ ● ● ●]
[· · ● ○ ● · ·]
[· · ● ● ● · ·]))))
Because ⇨/judgmentform
has mode I O
, it behaves like a reduction relation, and we can query it with applyreductionrelation
and applyreductionrelation*
as well:
(testequal
(list>set (applyreductionrelation ⇨/judgmentform (term initialboard)))
(set
(term
([· · ● ● ● · ·]
[· · ● ● ● · ·]
[● ● ● ● ● ● ●]
[● ○ ○ ● ● ● ●]
[● ● ● ● ● ● ●]
[· · ● ● ● · ·]
[· · ● ● ● · ·]))
(term
([· · ● ● ● · ·]
[· · ● ● ● · ·]
[● ● ● ● ● ● ●]
[● ● ● ● ○ ○ ●]
[● ● ● ● ● ● ●]
[· · ● ● ● · ·]
[· · ● ● ● · ·]))
(term
([· · ● ● ● · ·]
[· · ● ○ ● · ·]
[● ● ● ○ ● ● ●]
[● ● ● ● ● ● ●]
[● ● ● ● ● ● ●]
[· · ● ● ● · ·]
[· · ● ● ● · ·]))
(term
([· · ● ● ● · ·]
[· · ● ● ● · ·]
[● ● ● ● ● ● ●]
[● ● ● ● ● ● ●]
[● ● ● ○ ● ● ●]
[· · ● ○ ● · ·]
[· · ● ● ● · ·]))))
(testequal
(list>set
(applyreductionrelation* ⇨/judgmentform (term ([● ● ● ○ ● ● ●]))))
(set
(term ((○ ○ ● ○ ● ○ ●)))
(term ((● ○ ● ○ ● ○ ○)))))
When to Use the Different Forms
At this point, we covered four different ways to operate on terms in PLT Redex: metafunctions, reduction relations, predicate relations and judgment forms. We could solve some of the same problems with more than one of these forms, so we need criteria to choose. It is particularly difficult to choose between a metafunction and a reduction relation when the reduction relation is deterministic. We could leverage the clause order and define a metafunction that is terser than its reduction relation counterpart, for example:
(definemetafunction L
[(m <somekindofterm>) ___]
[(m _) ___])
(define r
(reductionrelation
(> <somekindofterm> ___)
(> <anyotherterm> ___)))
In the listing above, we can rely on the clause order and use the underscore pattern (_
) in the second clause of the metafunction m
to only match terms that are not <somekindofterm>
. When defining r
as a reduction relation version of m
, we have to write mutually exclusive clauses and be explicit about what constitutes <anyotherterm>
that is not <somekindofterm>
. If we had used _
instead of <anyotherterm>
, then the second clause in r
would always match, even for <somekindofterm>
.
This case arrises often when defining the semantics of a deterministic language, and we could be tempted by the terser definition to prefer a metafunction, resorting to reduction relations only when we need nondeterminism (for example, in ⇨
in Peg Solitaire). But it is a better practice to use reduction relations when defining semantics. First, because it follows the semantic framework on which PLT Redex is built (something called reduction semantics), and programminglanguage researchers expect semantics in this form. Second, because the clause order may hide ambiguities and leave semantic considerations implicit. Third, because it leaves the foundation ready for when it is necessary to introduce nondeterminism in the semantics.
Usually, metafunctions are the auxiliary utilities, for example, to substitute variables for values, calculate the result of primitive operations, and so forth. Reduction relations are better suited for defining semantics. They should reduce the terms in the language. The notion of a reduced term depends on the language and does not always correspond to a smaller term; in Peg Solitaire, for example, a reduced term is not a smaller board, but one with less pegs. It is also common to use the more general definejudgmentform
instead of reductionrelation
when the only difference would be the notation.
Next, we provide the judgment forms defined in this section and we are ready to play Peg Solitaire using PLT Redex visualization tools.
(provide ⇨/judgmentform winningboard?/judgmentform)
Visualization
We use PLT Redex visualization tools to play Peg Solitaire. The stepper
form runs either the ⇨
reduction relation or the ⇨/judgmentform
judgment form on the initialboard
:
DrRacket opens the window below:
We click on the →
button to make the first move:
We select the second board by clicking on the ↕
button next to it:
We click on the →
button to make the second move:
We select the board on the bottom by clicking on the ↕
button next to it:
We can undo moves and try different paths by click on the nodes on the graph at the bottom:
We proceed with the game in this alternate path by clicking on →
:
We accomplished our goal of playing Peg Solitaire by (ab)using PLT Redex.
Traces
We can explore Peg Solitaire further with the traces
form, which accepts the same inputs as stepper
and explores all possible moves:
> (traces ⇨ (term initialboard))
> (traces ⇨/judgmentform (term initialboard))
DrRacket opens the window below:
We only explored a small fraction of PLT Redex, in the next section we cover other features.
Other Features
In this section we give a high level view of a miscellanea of other PLT Redex features.
Conditions
The forms for manipulating terms can do more than just pattern matching on the input terms to determine whether a clause contributes to the output. They can apply metafunctions and reduction relations, they can query predicate relations and judgment forms, and they can perform arbitrary computations with the sidecondition
form. For example, the following predicate relation uses a sidecondition
form to check that the board
has rows of matching length (ellipses with suffixes (..._<suffix>
) would be a more straightforward way of achieving this same goal):
Unquoting
We can use arbitrary computations to define extra conditions under which a clause contributes to the output, and we can also use arbitrary computations to define that output. We can escape from terms back to Racket with unquote
, which is written with a comma (,
), for example:
In the listing above, the ,(+ 1 2)
form means “escape from the term back to Racket, compute (+ 1 2)
and place the result here.”
Previously, we used defineterm
to name terms, for example:
(defineterm apeg ●)
(testequal (term apeg)
'●)
We can also assign terms to regular Racket names with define
, for example:
(define aspace (term ○))
We access this name outside terms as usual:
(testequal aspace
'○)
In terms, we unquote to escape back to Racket and access the name, for example:
(testequal (term ,aspace)
'○)
The defineterm
form is not a shorthand for (define ___ (term ___))
because names defined with defineterm
are only available in other terms, not directly in Racket. If we try to access in Racket a name defined with defineterm
, for example, apeg
, the result is a syntax error:
> apeg
apeg: illegal use of syntax in: apeg
The converse also holds: names defined with define
are only available directly in Racket, not in terms. Trying to access the name aspace
defined with define
in a term is not a syntax error, but does not produce the result you might expect:
(testequal (term aspace)
'aspace)
In the listing above, the aspace
in term
is interpreted as a symbol, not as a reference to the Racket variable aspace
. This is a common pitfall, so pay attention to the different contexts and do not mix Racket with terms.
With unquote
we can access names defined with define
from within terms and mix them with names defined with defineterm
, for example:
(defineterm apeg ●)
(define aspace (term ○))
(testequal (term (● apeg ,aspace))
'(● ● ○))
We can use the term
form from within unquote
:
(testequal (term (● ,(term apeg) ,aspace))
'(● ● ○))
In the following example, we define a count●
metafunction to count how many pegs there are in a board by unquoting and relying on Racket’s functions for manipulating lists:
(definemetafunction pegsolitaire
count● : board > integer
[(count● ([position ...] ...))
,(count (λ (position) (equal? position (term ●)))
(term (position ... ...)))])
(testequal (term (count● initialboard)) 32)
The listing above matches the input board with the pattern ([position ...] ...)
, so the name position
in the template refers to a list of lists of position
s. We use the template (position ... ...)
to flatten this list of lists. We then unquote and use Racket’s count
to count how many position
s are equal?
to pegs (●
).
In summary:
 Names defined with
define
are available in Racket but can be accessed in terms withunquote
, for example,,peg
.  Names defined with
defineterm
are available in terms but can be accessed in Racket withterm
, for example,(term space)
.
Extensions and Holes
We can define languages, metafunctions, judgment forms and so forth by extending existing definitions. In the following example, we extend the pegsolitaire
language into the PegSolitaire
language:
(defineextendedlanguage PegSolitaire pegsolitaire
[Board ::= (row ... hole row ...)])
The PegSolitaire
language includes all names in pegsolitaire
as well as the new name Board
. It is equivalent to the following:
(definelanguage PegSolitaire
[board ::= (row ...)]
[row ::= [position ...]]
[position ::= peg space padding]
[peg ::= ●]
[space ::= ○]
[padding ::= ·]
[Board ::= (row ... hole row ...)])
The name Board
refers to pattern (row ... hole row ...)
. A hole
is a special pattern built into PLT Redex, similar to how any
is a special pattern built into PLT Redex. A Board
is a board
with a missing row
, the hole
. We can match a board with the inhole
form, for example:
(testequal (redexmatch? PegSolitaire (inhole Board row)
(term ([●]
[○]
[●])))
#t)
The pattern (inhole Board row)
means “the Board
is a board
with a row
missing.” This pattern matches the simplified input board in three ways:
> (redexmatch PegSolitaire (inhole Board row)
(term ([●]
[○]
[●])))
(list
(match (list (bind 'Board '((●) (○) hole)) (bind 'row '(●))))
(match (list (bind 'Board '((●) hole (●))) (bind 'row '(○))))
(match (list (bind 'Board '(hole (○) (●))) (bind 'row '(●)))))
The first match, for example, means the missing row
in the Board
is the last one.
With PegSolitaire
and Board
s with hole
s, we can shorten the definition of the ⇨
reduction relation. We define the ⇨/hole
reduction relation that extends ⇨
and replaces the →
clause with a simpler definition using inhole
:
The (inhole Board [position_1 ... ● ● ○ position_2 ...])
in the input pattern matches a row including the ● ● ○
sequence. This saves us from having to repeat the surroundings by writing (row_1 ... ___ row_2 ...)
. We cannot shorten the definition further by removing the position_<n> ...
parts because a hole
cannot match a sequence of position
s, for example, ● ● ○
. The (inhole Board [position_1 ... ○ ○ ● position_2 ...])
in the template does the opposite, plugging the term [position_1 ... ○ ○ ● position_2 ...]
in the hole
we had left in Board
.
The ⇨/hole
extended reduction relation works the same as the ⇨
original reduction relation:
(testequal (list>set (applyreductionrelation ⇨/hole
(term initialboard)))
(set
(term
([· · ● ● ● · ·]
[· · ● ● ● · ·]
[● ● ● ● ● ● ●]
[● ○ ○ ● ● ● ●]
[● ● ● ● ● ● ●]
[· · ● ● ● · ·]
[· · ● ● ● · ·]))
(term
([· · ● ● ● · ·]
[· · ● ● ● · ·]
[● ● ● ● ● ● ●]
[● ● ● ● ○ ○ ●]
[● ● ● ● ● ● ●]
[· · ● ● ● · ·]
[· · ● ● ● · ·]))
(term
([· · ● ● ● · ·]
[· · ● ○ ● · ·]
[● ● ● ○ ● ● ●]
[● ● ● ● ● ● ●]
[● ● ● ● ● ● ●]
[· · ● ● ● · ·]
[· · ● ● ● · ·]))
(term
([· · ● ● ● · ·]
[· · ● ● ● · ·]
[● ● ● ● ● ● ●]
[● ● ● ● ● ● ●]
[● ● ● ○ ● ● ●]
[· · ● ○ ● · ·]
[· · ● ● ● · ·]))))
PLT Redex provides other more sophisticated forms for extending languages and reduction relations, for example, defineunionlanguage
creates a language by joining together the names for patterns from various languages, and contextclosure
defines a reduction relation based on another in a way that saves us from typing (inhole ___)
repeatedly, as we did in ⇨/hole
.
Checking
All tests we have written thus far depend on examples we have written by hand, for example, initialboard
, exampleboard1
and exampleboard2
. While these tests increase our confidence in our model, they do not suffice to check more sophisticated properties. For example, we may conjecture that boards have less pegs after every move, because we remove the peg that was jumped over. We may want to prove this proposition holds for all boards, but developing a formal proof can be timeconsuming, so before we start we want to use our model to test the proposition on a variety of boards, particularly on boards we did not think of ourselves.
PLT Redex includes a tool to generate terms and check propositions. For example, the following listing checks the proposition above:
(redexcheck
pegsolitaire board
(for/and ([board′ (inlist (applyreductionrelation ⇨ (term board)))])
(> (term (count● board)) (term (count● ,board′)))))
The redexcheck
form is working over the pegsolitaire
language and generating terms that follow the definition of board
. For each term it generates, it runs the predicate (for/and ___)
, which asserts that the board
includes more pegs than the board′
s after one move. By default, PLT Redex will try this a 1000 times:
redexcheck: .../playingthegamewithpltredex/otherfeatures.rkt:131
no counterexamples in 1000 attempts
If we check for an invalid property, for example, the opposite of the one above (using <
instead of >
), then redexcheck
outputs a counterexample:
> (redexcheck
pegsolitaire board
(for/and ([board′ (inlist (applyreductionrelation ⇨ (term board)))])
(< (term (count● board)) (term (count● ,board′)))))
redexcheck: .../playingthegamewithpltredex/otherfeatures.rkt:131
counterexample found after 125 attempts:
((○) (●) (●))
Typesetting
We can typeset the forms we defined thus far for including them in papers. This streamlines the writing process and prevents errors when translating our model to LaTeX. For example, the following is the typeset definition of ⇨/judgmentform
:
(renderjudgmentform ⇨/judgmentform)
This default typesetting may be unsatisfactory, for example, we may wish that ⇨/judgmentform
is infix instead of prefix. PLT Redex offers forms to customize the typesetting.
Next, we cover the limitations in PLT Redex.
Limitations
In this section we explore several ways in which PLT Redex falls short.
Debugging
When things go wrong while you are developing your model, PLT Redex generally has little more to say than “relation does not hold,” or “term does not match pattern.” It does not say why: which clauses it tried to match, why they failed, and so forth. We are left with rudimentary debugging techniques, for example, using the redexmatch?
form to check parts of terms and patterns, and using sidecondition
s to trace the execution of metafunctions and reduction relations.
The following listing exemplifies a typical debugging session investigating why a term is not a board
by reducing terms and patterns:
The term is not a board
because *
is not a position
.
Performance
An executable model is not an implementation. PLT Redex is good for visualizing and understanding a model on relatively small inputs. It can scale to moderately sized inputs if we design patterns and relations carefully, but it can never replace a performancetuned implementation. It has to check contracts, perform nondeterministic computations, and so forth—tasks that are computationally expensive.
As an example of a declarative definition that does not scale for being too naïve, consider the following function to find winning boards:
(define (winningboards startboard)
(filter (λ (board) (judgmentholds (winningboard? ,board)))
(applyreductionrelation* ⇨ startboard)))
The winningboards
function works by applying the ⇨
reduction relation to find all boards reachable by one or more moves starting from startboard
. It then filters the winning boards among them with the winningboard?
predicate relation. This strategy is straightforward and works for small boards, for example:
(testequal (winningboards (term ([● ● ○ ●])))
'(([○ ● ○ ○])))
But it does not scale to the initialboard
:
> (winningboards (term initialboard))
; Runs for too long
Advanced Pattern Matching
All operations we have covered rely on terms matching patterns, but it is often useful to query whether a term does not match a pattern, and PLT Redex does not support it. One workaround is to unquote, escape back to Racket and use the redexmatch?
form. For example, the following listing defines the notpeg?
predicate relation, which holds for position
s other than a peg
:
(definerelation pegsolitaire
notpeg? ⊆ position
[(notpeg? position)
,(not (redexmatch? pegsolitaire peg (term position)))])
(testequal (term (notpeg? ●))
#f)
(testequal (term (notpeg? ○))
#t)
(testequal (term (notpeg? ·))
#t)
Similarly, PLT Redex does not include patterns for data structures other than Sexpressions, for example, hashes and sets. One workaround is the same as before, to unquote
, but models that unquote
too often quickly become unreadable. The best solution is to approximate these data structures using Sexpressions, for example, hashes become association lists (lists of pairs) and sets become lists. The downside of this approach is that the model must provide utilities for manipulating these data structures (adding elements, looking up, and so forth) while guaranteeing the invariants, for example, that set elements are distinct.
Metaparameters
It is common for papers to include a series of definitions which rely on a parameter that remains the same, for example, a parameter that indicates how to allocate addresses. When the context is evident, papers often omit these parameters to improve readability. Because they are parameters in the guest language, we call them metaparameters. PLT Redex has no support for metaparameters: we must clutter the definitions by passing them around explicitly or resort to one of a few other workarounds, but they all have their downsides. Racket includes a feature to solve the issue, parameters, and we can use them with unquote
, but then our definitions are no longer pure, they may output different results when given the same (explicit) inputs, so we must turn off PLT Redex’s cache, aggravating the performance issue.
Parallel Reduction
PLT Redex is unable to reduce on multiple hole
s in a single step. We would have run into this limitation if we had chosen, for example, Conway’s Game of Life instead of Peg Solitaire. In each step of Conway’s Game of Life, all cells on the board change state (alive or dead) in parallel, but we could not model it with multiple hole
s, we would have to opt for a less straightforward representation and serialize the step in a series of substeps.
HigherOrder Metafunctions
Metafunctions in PLT Redex are firstorder: they cannot be passed as arguments, they cannot be a return value, they cannot be store in data structures, and so forth. This issue arises, for example, when trying to model a ContinuationPassing Style converter. If higherorder functions are necessary, then we must unquote
and use regular Racket functions.
Definition Extension Limitations
Let L
be a language, m
a metafunction, r
a reduction relation that uses m
, and L′
, m′
and r′
their respective extensions. The parts of r′
that use m
are not reinterpreted to use m′
and range over L′
. The only possible workarounds are to copy r
into the definition fo r′
and modify uses of m
to m′
or be careful in the definitions so that the issue does not occur. This is the approach taken in a paper that discusses this limitation, An Introduction to Redex with Abstracting Abstract Machines.
Customized Typesetting
PLT Redex includes many features to customize typesetting, but they can be hard to learn and have their shortcomings. For example, there is not way to change the arrangement of antecedents on a predicate relation—they always appear on the same line. Also, the paper size is fixed, and big definitions may not fit. In general, the figures require postprocessing before they can appear on a paper: trimming, rearranging and so forth. I recommend pdfcrop
for simple trimming, Inkscape for more complex manipulation and pdf2svg
for when the figure must appear on a web page.
Formal Proofs
PLT Redex is a lightweight modeling tool, not a theorem prover or a model checker. It can check propositions to increase your confidence in them with little effort, but if you need mechanized formal proofs, use tools like Coq.
At this point in our journey, we know enough to follow more advanced material on PLT Redex. In the next section, we list this related work.
Related Work
 PLT Redex website.
 Reference manual.
 Semantics Engineering with PLT Redex, by Matthias Felleisen, Robert Bruce Findler, and Matthew Flatt. The book is outdated in parts, and does not cover all features, but the first part covers semantics and programminglanguage theory—which never grows old—and is one of the most comprehensive and accessible materials on those subjects.
 Run Your Research: On the Effectiveness of Lightweight Mechanization, by Casey Klein et al. A paper about PLT Redex development.
 PLT Redex FAQ, by Ben Greenman and Sam Caldwell.
 An Introduction to Redex with Abstracting Abstract Machines, by David Van Horn.
 PLT Redex Summer Schools: 2015, 2017 [notes].
 Examples of research using PLT Redex:
λ
_{JS} and Abstracting Abstract Control.
Conclusion
We covered the basics of PLT Redex without going into programminglanguage theory. Instead, we used it to model a game of Peg Solitaire. We used terms to represent elements in the game: boards, pegs, spaces and paddings. We used patterns to match those terms as the basis of several definitions:
 Languages: Named patterns that specify which terms represent elements in Peg Solitaire and which do not.
 Metafunctions: Functions in the language of Peg Solitaire elements. They are deterministic: when faced with multiple choices (multiple clauses that match), a metafunction chooses only one path.
 Reduction Relations: Similar to a metafunction, but works nondeterministically: when faced with multiple choices (multiple clauses that match), a judgment form chooses all paths. Can also be understood as a metafunction that returns a set of results.
 Predicate Relations: Similar to a reduction relation that returns a single boolean indicating whether the predicate holds or not.
 Judgment Forms: The most general form of relation, with arbitrarily many inputs and outputs.
With these definitions in place, we used PLT Redex visualization tools to play Peg Solitaire. We then explored other features, including extra conditions for a clause to contribute to the output, unquoting, holes, testing and typesetting. We also discussed some limitations, including debugging, performance, and more advanced pattern matching; the lack of metaparameters, parallel reduction and higherorder metafunctions; how definition extensions do not reinterpret dependent definitions; how it can be difficult to customize typeset figures; and how PLT Redex is not appropriate for mechanized formal proofs.
You now know enough to read the more advanced material on PLT Redex, and understanding the tool will help you read papers in programminglanguage theory.
Acknowledgments
Thanks to the following people for providing feedback on a preliminary version of this article: P.C. Shyamshankar, Scott Moore, Allan Vital and Rafael da Silva Almeida.