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>)
...)
```

`<language>`

: A language as defined previously.`#:domain`

: A contract pattern for the inputs and outputs of the reduction relation. The contract is verified and an error may be raised if the reduction relation is applied to an invalid input or produces an invalid output.`(--> <pattern> <template> <name>)`

: A reduction relation clause.`<pattern>`

: A pattern for the input.`<template>`

: A template for the output.`<name>`

: A name for the clause.

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:

`(row_1 ... [position_1 ... ● ● ○ position_2 ...] row_2 ...)`

: The pattern to match against the input board. The pattern matches if the board includes a sequence`● ● ○`

surrounded by any other`position`

s and`row`

s, to which we assign the names`position_<n>`

and`row_<n>`

so that we can reconstruct the board in the template.`(row_1 ... [position_1 ... ○ ○ ● position_2 ...] row_2 ...)`

: The template to build the board after the move. It changes the sequence`● ● ○`

into`○ ○ ●`

, and reconstructs the surroundings with the names`position_<n>`

and`row_<n>`

.`"→"`

: The name of the clause.

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 `position`

s 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.