Playing the Game with PLT Redex
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:
otherfeatures.rkt
#lang racket
(require redex "terms.rkt" "languages.rkt"
"reductionrelations.rkt" "judgmentforms.rkt")
(definerelation pegsolitaire
equallengthrows? ⊆ board
[(equallengthrows? board)
(sidecondition
(andmap (λ (row) (equal? (length row)
(length (first (term board)))))
(term board)))])
(testequal (term (equallengthrows? initialboard))
#t)
(testequal (term (equallengthrows? ([●]
[●])))
#t)
(testequal (term (equallengthrows? ([●]
[● ●])))
#f)
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:
(testequal (term (1 2 ,(+ 1 2)))
'(1 2 3))
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:
define 
Racket  terms  unquote 
,peg 

defineterm 
terms  Racket  term 
(term space) 

Names defined with  ______ are available in  _______ but can be accessed in  _______ with  ________, for example,  _______ 
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. 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
:
(define
⇨/hole
(extendreductionrelation
⇨
PegSolitaire
#:domain board
(> (inhole Board [position_1 ... ● ● ○ position_2 ...])
(inhole Board [position_1 ... ○ ○ ● position_2 ...])
"→")))
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 ...)
. 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.