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. 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
define-relation form to define predicate relations:
(define-relation <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:
#lang racket (require redex "terms.rkt" "languages.rkt") (define-relation peg-solitaire winning-board? ⊆ board [(winning-board? ([· ... ○ ... · ...] ... [· ... ○ ... ● ○ ... · ...] [· ... ○ ... · ...] ...))])
winning-board? ⊆ board says that the
winning-board? 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:
(test-equal (term (winning-board? example-board-1)) #f) (test-equal (term (winning-board? example-board-2)) #f) (test-equal (term (winning-board? initial-board)) #f) (test-equal (term (winning-board? example-winning-board)) #t)
The predicate relation only holds for the
We will use the predicate relation
winning-board? in a later section when trying to use our model to win Peg Solitaire:
Next, we cover the most general form of relations that may not be functions: judgment forms.