Leandro Facchinetti

Playing the Game with PLT Redex

We use PLT Redex visualization tools to play Peg Solitaire. The stepper form runs either the reduction relation or the ⇨/judgment-form judgment form on the initial-board:

visualization.rkt

#lang racket
(require redex "terms.rkt" "reduction-relations.rkt" "judgment-forms.rkt")


> (stepper  (term initial-board))
> (stepper ⇨/judgment-form (term initial-board))

DrRacket opens the window below:

DrRacket showing the stepper. Left: The initial-board. Right: The button to make a move. Bottom: A graph showing the path we took while playing the game with only one node that represents the initial-board.

We click on the button to make the first move:

The stepper shows the four possible initial moves on the main pane and on the graph at the bottom.

We select the second board by clicking on the button next to it:

The stepper highlights the differences between the initial-board and the board we chose. The graph at the bottom shows the path. On the bottom right, the stepper shows the clause we chose, .

We click on the button to make the second move:

The stepper shows the three available moves.

We select the board on the bottom by clicking on the button next to it:

The game proceeds.

We can undo moves and try different paths by click on the nodes on the graph at the bottom:

We return to the beginning of the game and chose a different move by clicking on a node in the graph at the bottom. The stepper highlights the differences between the initial-board and our new current board.

We proceed with the game in this alternate path by clicking on :

The next move in the alternate path. The graph at the bottom includes one node for every board we explored.


We accomplished our goal of playing Peg Solitaire by (ab)using PLT Redex.

Traces

We can explore Peg Solitaire further with the traces form, which accepts the same inputs as stepper and explores all possible moves:

> (traces  (term initial-board))
> (traces ⇨/judgment-form (term initial-board))

DrRacket opens the window below:

The tracer explores all possible moves up to a certain number of boards. Click on Reduce to explore further.

When we click on a board, the tracer highlights the moves leading to it and those coming from it. The edges are labeled with the clause associated with the move.


We only explored a small fraction of PLT Redex, in the next section we cover other features.