Leandro Facchinetti

Playing the Game with PLT Redex

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 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 reduction-relation:

(reduction-relation
  <language>
  #:domain <pattern>

  (--> <pattern> <template> <name>)
  ...)

The shape of the reduction-relation form is similar to that of define-metafunction: 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 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:

(--> (row_1
      ...
      [position_1 ...    position_2 ...]
      row_2
      ...)
     (row_1
      ...
      [position_1 ...    position_2 ...]
      row_2
      ...)
     "→")

In detail:

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 positions in each row. For example, the following is the rule for when a peg jumps over its neighbor on the bottom:

(--> (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
      ...)
     "↓")

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 :

reduction-relations.rkt

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

(define
  
  (reduction-relation
   peg-solitaire
   #:domain board

   (--> (row_1
         ...
         [position_1 ...    position_2 ...]
         row_2
         ...)
        (row_1
         ...
         [position_1 ...    position_2 ...]
         row_2
         ...)
        "→")

   (--> (row_1
         ...
         [position_1 ...    position_2 ...]
         row_2
         ...)
        (row_1
         ...
         [position_1 ...    position_2 ...]
         row_2
         ...)
        "←")

   (--> (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
         ...)
        "↓")

   (--> (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
         ...)
        "↑")))

We can test the reduction relation with the test--> form:

(test-->  (term initial-board)
         (term
          ([· ·    · ·]
           [· ·    · ·]
           [      ]
           [      ]
           [      ]
           [· ·    · ·]
           [· ·    · ·]))

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

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

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

We can also query the reduction relation with the apply-reduction-relation form. The apply-reduction-relation 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 S-expression, 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:

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

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

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

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

If we use apply-reduction-relation repeatedly, feeding one output of an application as the input to the next, then we can use relation to compute all possible Peg Solitaire boards. PLT Redex comes with the apply-reduction-relation* form for this purpose. Unfortunately, there are too many possible boards, so the computation does not terminate in reasonable time:

> (apply-reduction-relation*  (term initial-board))
; Runs for too long

But we can test apply-reduction-relation* on a fragment of the board with a single row, for which the outputs are tractable:

(test-equal
 (list->set
  (apply-reduction-relation* #: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:

(test-equal
 (list->set (apply-reduction-relation*  (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.