BeltAndShoes

# Title: BeltAndShoes

## Overview

An accessible illustration of a BX that is not undoable/history-ignorant/very-well-behaved.

My wife saves me from making a faux pas by breaking the Laws of Fashion, in particular that thou shalt not wear a brown belt with black shoes, or a black belt with brown shoes. Before I leave the house, she corrects any inconsistencies in my outfit. One morning, I put on a brown belt and brown shoes; then I decide that the brown shoes are too scruffy for today's meetings, so I change to black shoes; then my wife notices, and changes my belt to black to match; finally, I decide that the shoes are not comfortable enough for the walk to work, so I change into my red trainers; my wife doesn't care what belt I wear with red trainers, so I leave for work with black belt and red trainers. The next morning, a similar story unfolds, except that my wife does not notice me with black shoes and brown belt, so doesn't change my belt; again I change into my red trainers; now my wife checks my outfit, doesn't care what belt I wear with red trainers, and I leave for work with brown belt and red trainers.

## Models

$\mathit{Shoes} = \{ \mathit{none}, \mathit{brown}, \mathit{black}, \mathit{red} \}$

$\mathit{Belt} = \{ \mathit{none}, \mathit{brown}, \mathit{black} \}$

## Consistency

Brown and black should not be worn together; anything else is fine.

$R(s,b) \equiv (s = \mathit{brown} \Rightarrow b \ne \mathit{black}) \land (s = \mathit{black} \Rightarrow b \ne \mathit{brown})$

## Consistency Restoration

There is some freedom when fixing a fashion faux pas of brown belt with black shoes or black belt with brown shoes; here, we make sure the shoes are the same colour as the belt.

$\begin{array}{lcl} \overrightarrow{R}(\mathit{brown},\mathit{black}) &=& \mathit{brown} \\ \overrightarrow{R}(\mathit{brown},b) &=& b \quad\mbox{when$b \ne \mathit{black}$} \\ \overrightarrow{R}(\mathit{black},\mathit{brown}) &=& \mathit{black} \\ \overrightarrow{R}(\mathit{black},b) &=& b \quad\mbox{when$b \ne \mathit{brown}$} \\ \overrightarrow{R}(s,b) &=& s \quad\mbox{when$s \notin \{\mathit{brown},\mathit{black}\}$} \end{array}$

Backwards consistency restoration $\overleftarrow{R}$ is not relevant for this illustration, but could be defined similarly to forwards.

## Properties

• correct (shoes and belt are consistent afterwards)
• hippocratic (when shoes and belt are consistent, no change is made)
• neither undoable or history ignorant (let $s = \mathit{black}, s' = \mathit{red}, b = \mathit{brown}, b' = \mathit{black}$; then $\overrightarrow{R}(s',\overrightarrow{R}(s,b)) = b'$ but $\overrightarrow{R}(s',b) = b$)

## Variants

Mike Johnson observes that it is arguable that this illustration does not break PutPut, provided you think of it from an ordered perspective — that is, it satisfies Monotonic PutPut. Specifically, the belt states are ordered with $\mathit{none} < \mathit{brown}$ and $\mathit{none} < \mathit{black}$, and similarly the shoe states are ordered with $\mathit{none}$ below any colour of shoes. Then the only monotonic sequences of changes to my shoes are trivial — all but one of them must be the identity — and so putting a composition of steps coincides with putting each of them in turn.

## Discussion

This example was used in the introductory lecture at the Summer School on BX and Shonan Meeting Seminar 091 on BX.

## Author(s)

Jeremy Gibbons and Sue Gibbons