Leandro Facchinetti

Playing the Game with PLT Redex

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>
  [(<relation> <pattern> ...)])

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? ([· ...  ... · ...]
                    [· ...  ...   ... · ...]
                    [· ...  ... · ...]

The contract 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:

We query the predicate relation by applying it, similar to a metafunction:

(test-equal (term (winning-board? example-board-1))
(test-equal (term (winning-board? example-board-2))
(test-equal (term (winning-board? initial-board))
(test-equal (term (winning-board? example-winning-board))

The predicate relation only holds for the example-winning-board.

We will use the predicate relation winning-board? in a later section when trying to use our model to win Peg Solitaire:

(provide winning-board?)

Next, we cover the most general form of relations that may not be functions: judgment forms.