Leandro Facchinetti

Playing the Game with PLT Redex

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. We can define relations in PLT Redex with define-judgment-form:

(define-judgment-form <language>
  #:mode (<judgment-form> <I/O> ...)
  #:contract (<judgment-form> <pattern> ...)

  [(<judgment-form> <pattern/template> ...)]
  ...)

We can recreate the reduction relation and the winning-board? predicate relation in terms of judgment forms:

judgment-forms.rkt

#lang racket
(require redex "terms.rkt" "languages.rkt")

(define-judgment-form peg-solitaire
  #:mode (⇨/judgment-form I O)
  #:contract (⇨/judgment-form board board)

  [(⇨/judgment-form (row_1
                     ...
                     [position_1 ...    position_2 ...]
                     row_2
                     ...)
                    (row_1
                     ...
                     [position_1 ...    position_2 ...]
                     row_2
                     ...))
   "→"]

  [(⇨/judgment-form (row_1
                     ...
                     [position_1 ...    position_2 ...]
                     row_2
                     ...)
                    (row_1
                     ...
                     [position_1 ...    position_2 ...]
                     row_2
                     ...))
   "←"]

  [(⇨/judgment-form (row_1
                     ...
                     [position_1 ..._n  position_2 ...]
                     [position_3 ..._n  position_4 ...]
                     [position_5 ..._n  position_6 ...]
                     row_2
                     ...)
                    (row_1
                     ...
                     [position_1 ...    position_2 ...]
                     [position_3 ...    position_4 ...]
                     [position_5 ...    position_6 ...]
                     row_2
                     ...))
   "↓"]

  [(⇨/judgment-form (row_1
                     ...
                     [position_1 ..._n  position_2 ...]
                     [position_3 ..._n  position_4 ...]
                     [position_5 ..._n  position_6 ...]
                     row_2
                     ...)
                    (row_1
                     ...
                     [position_1 ...    position_2 ...]
                     [position_3 ...    position_4 ...]
                     [position_5 ...    position_6 ...]
                     row_2
                     ...))
   "↑"])

(define-judgment-form peg-solitaire
  #:mode (winning-board?/judgment-form I)
  #:contract (winning-board?/judgment-form board)
  [(winning-board?/judgment-form ([· ...  ... · ...]
                                  ...
                                  [· ...  ...   ... · ...]
                                  [· ...  ... · ...]
                                  ...))])

We can test whether a judgment holds with the test-judgment-holds form:

(test-judgment-holds
 (⇨/judgment-form initial-board ([· ·    · ·]
                                 [· ·    · ·]
                                 [      ]
                                 [      ]
                                 [      ]
                                 [· ·    · ·]
                                 [· ·    · ·])))

(test-judgment-holds
 (⇨/judgment-form initial-board ([· ·    · ·]
                                 [· ·    · ·]
                                 [      ]
                                 [      ]
                                 [      ]
                                 [· ·    · ·]
                                 [· ·    · ·])))

(test-judgment-holds
 (⇨/judgment-form initial-board ([· ·    · ·]
                                 [· ·    · ·]
                                 [      ]
                                 [      ]
                                 [      ]
                                 [· ·    · ·]
                                 [· ·    · ·])))

(test-judgment-holds
 (⇨/judgment-form initial-board ([· ·    · ·]
                                 [· ·    · ·]
                                 [      ]
                                 [      ]
                                 [      ]
                                 [· ·    · ·]
                                 [· ·    · ·])))

We can also query a judgment form with the judgment-holds form. The following listing includes tests for both ⇨/judgment-form and winning-board?/judgment-form:

(test-equal
 (judgment-holds
  (⇨/judgment-form initial-board ([· ·    · ·]
                                  [· ·    · ·]
                                  [      ]
                                  [      ]
                                  [      ]
                                  [· ·    · ·]
                                  [· ·    · ·])))
 #t)

(test-equal
 (judgment-holds
  (⇨/judgment-form initial-board ([· ·    · ·]
                                  [· ·    · ·]
                                  [      ]
                                  [      ]
                                  [      ]
                                  [· ·    · ·]
                                  [· ·    · ·])))
 #t)

(test-equal
 (judgment-holds
  (⇨/judgment-form initial-board ([· ·    · ·]
                                  [· ·    · ·]
                                  [      ]
                                  [      ]
                                  [      ]
                                  [· ·    · ·]
                                  [· ·    · ·])))
 #t)

(test-equal
 (judgment-holds
  (⇨/judgment-form initial-board ([· ·    · ·]
                                  [· ·    · ·]
                                  [      ]
                                  [      ]
                                  [      ]
                                  [· ·    · ·]
                                  [· ·    · ·])))
 #t)

(test-equal
 (judgment-holds (winning-board?/judgment-form example-board-1))
 #f)
(test-equal
 (judgment-holds (winning-board?/judgment-form example-board-2))
 #f)
(test-equal
 (judgment-holds (winning-board?/judgment-form initial-board))
 #f)
(test-equal
 (judgment-holds (winning-board?/judgment-form example-winning-board))
 #t)

If we provide a pattern in an output position of the judgment form, then judgment-holds 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 apply-reduction-relation:

(test-equal
 (list->set (judgment-holds (⇨/judgment-form initial-board board) board))
 (set
  (term
   ([· ·    · ·]
    [· ·    · ·]
    [      ]
    [      ]
    [      ]
    [· ·    · ·]
    [· ·    · ·]))

  (term
   ([· ·    · ·]
    [· ·    · ·]
    [      ]
    [      ]
    [      ]
    [· ·    · ·]
    [· ·    · ·]))

  (term
   ([· ·    · ·]
    [· ·    · ·]
    [      ]
    [      ]
    [      ]
    [· ·    · ·]
    [· ·    · ·]))

  (term
   ([· ·    · ·]
    [· ·    · ·]
    [      ]
    [      ]
    [      ]
    [· ·    · ·]
    [· ·    · ·]))))

Because ⇨/judgment-form has mode I O, it behaves like a reduction relation, and we can query it with apply-reduction-relation and apply-reduction-relation* as well:

(test-equal
 (list->set (apply-reduction-relation ⇨/judgment-form (term initial-board)))
 (set
  (term
   ([· ·    · ·]
    [· ·    · ·]
    [      ]
    [      ]
    [      ]
    [· ·    · ·]
    [· ·    · ·]))

  (term
   ([· ·    · ·]
    [· ·    · ·]
    [      ]
    [      ]
    [      ]
    [· ·    · ·]
    [· ·    · ·]))

  (term
   ([· ·    · ·]
    [· ·    · ·]
    [      ]
    [      ]
    [      ]
    [· ·    · ·]
    [· ·    · ·]))

  (term
   ([· ·    · ·]
    [· ·    · ·]
    [      ]
    [      ]
    [      ]
    [· ·    · ·]
    [· ·    · ·]))))

(test-equal
 (list->set
  (apply-reduction-relation* ⇨/judgment-form (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:

(define-metafunction L
  [(m <some-kind-of-term>) ___]
  [(m _) ___])

(define r
  (reduction-relation
   (--> <some-kind-of-term> ___)
   (--> <any-other-term> ___)))

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 <some-kind-of-term>. When defining r as a reduction relation version of m, we have to write mutually exclusive clauses and be explicit about what constitutes <any-other-term> that is not <some-kind-of-term>. If we had used _ instead of <any-other-term>, then the second clause in r would always match, even for <some-kind-of-term>.

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, and programming-language 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 define-judgment-form instead of reduction-relation 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 ⇨/judgment-form winning-board?/judgment-form)