Bx Examples Repository
Title: TrainCrossroads
Version: 0.1
Type: Sketch
Overview
An accessible illustration of a BX that is not history-ignorant.
A train runs on a figure-of-eight track with a crossroads in the middle. In order to determine the state of the train, it is not in general sufficient to specify its position; only also needs to specify the history of its previous positions. In particular, the train may be “at the crossroads” in two different states (or even four, if you're allowed to pick it up and put it back on the track facing the opposite direction).
Models
The source model space consists of the position of (the centre of the locomotive of) the train together with the direction in which it is facing; the direction is tangent to the track at that position, and (let's say) facing anticlockwise round the left-hand loop of the figure-of-eight and clockwise round the right-hand loop.
The view model space consists solely of the position.
Consistency
Models are consistent when their positions agree.
Consistency Restoration
The state of the view is completely determined by the source. For most views (positions), the source (direction) is also determined; but when the position is the centre of the crossroads, there are two possible directions. One might specify that the train should take the shortest route along the track to the required position, and disambiguate at the extremities (say, move forwards when there is a tie).
Properties
Correct and hippocratic. But not history-ignorant: with the shortest-route consistency restoration as above, a series of short moves may take the train to the crossroads facing the opposite direction to where the composition of those moves would.
Discussion
This example was used in the introductory lecture at the Summer School on BX and Shonan Meeting Seminar 091 on BX.
References
Author(s)
Jeremy Gibbons
Reviewer(s)
Comments
Artefacts
