Some Math about Minesweeper
Desires
A complete algorithm for solving minesweeper. By ‘complete’ I mean one which can solve any game which is in principle solvable without guessing.
An implementation of a minesweeper app that guarantees only presenting solvable games, as proven by the above algorithm
The game, traditionally
Traditionally, the game Minesweeper consists of a finite-size grid of cells, some of which are said to contain a bomb. At the start of the game, the player has no knowledge of which cells contain a bomb. The game proceeds in a sequence of turns; on each turn, the player must choose one cell to reveal. Revealing a cell has one of two effects. If the cell contains a bomb, then the game ends immediately and is considered a loss. If the cell does not contain a bomb, then that fact is revealed to the user, and additionally the user is granted knowledge of how many bombs are present in the 3x3 neighorhood around the revealed cell. (Usually this information is presented by displaying a number in the place of the revealed cell.) Typically boms are placed randomly around the game board. This means that at the start of the game, from the player’s persective, all cells are equally likely to contain a bomb, and hence whether the first move is a loss or not is pure luck. For this reason, some Minesweeper implementations choose to defer the placement of bombs until after the first reveal in order to guarantee that the first reveal is a non-bomb. Others go further and guarantee that the first cell revealed and all surrounding cells in the 3x3 neighborhood around that cell are non-bombs. This gives a rough characterization of “the” traditional Minesweeper game. Implementations may vary on details, such as:
Whether or not cells on opposing sides of the game board are considered neighbors; ie, whether the game board is a rectangle or a torus
Behaviour on first reveal, as discussed above.
Size of the game board, and number of bombs
Placement of bombs
Behaviour on reveal of a cell with no bomb neighbors (a “zero-valued” cell): some implementations, upon such an action, will reveal all contiguous zero-valued cells
Note that in this characterization we do away with the concept of flagging a cell, which most Minsweeper implementations include. The ability to flag a cell can be seen as pure user convenience and does not affect the game, but removing it makes analysis simpler.
The game, for us
A game state consists of the following data:
A finite set of cells, typically denoted Cell % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} \text{Cell}
A valuation function ΣP(Cell)×N % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} \Sigma \subseteq \cl P(\text{Cell}) \times \bb N taking a set of cells (often called a neighborhood) to the number of bombs we know to be present between them. Note that the domain of Σ % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} \Sigma is not necessarily all of P(Cell) % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} \cl P(\text{Cell}), since we won’t know the valuation of all sets of cells (unless the game is complete). We could equivalently consider this function to have signature Σ:P(Cell){?}N % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} \Sigma : \cl P(\text{Cell}) \to \{ ? \} \cup \bb N, where ?N % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} ? \notin \bb N denotes that the valuation of a neighborhood is unkown.
A bomb function B:Cell{0,1} % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} B : \text{Cell} \to \{ 0, 1 \} giving whether or not each cell is actually a bomb or not. The value 1 % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} 1 denotes that it is a bomb, and 0 % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} 0 denotes that it is not
A cell c % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} c is considered to be revealed if {c}dom(Σ) % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} \{c\} \in \text{dom}(\Sigma). If this is the case, then one also knows B(c) % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} B(c). A turn consists of choosing a cell c % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} c to reveal. The result of revealing a cell is that the valuation function Σ % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} \Sigma is updated to at least include the singleton set {c} % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} \{c\} in its domain. If Σ({c})=1 % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} \Sigma(\{c\}) = 1, then we know B(c)=1 % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} B(c) = 1 and the game is an immediate loss. If Σ({c})=0 % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} \Sigma(\{c\}) = 0, the game continues. Note that {c} % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} \{c\} need not be the only neighborhood included; other neighborhoods may also be revaled. For instance, in the case of traditional minesweeper, the valuation function is also updated with the 3x3 neighborhood around the revealed cell. Note that this abstraction makes no assumptions about the shape of the game board (besides finiteness).
Completeness: the goal
One goal is to present a ‘complete’ algorithm for solving a game of minesweeper, where ‘complete’ is meant in the sense that the algorithm will beat the game in all cases where no guessing is required. To make that concrete, we introduce the following notions. A bomb function B % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} B and valuation function Σ % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} \Sigma are said to be compatible if they do not disagree; that is, if for every neighborhood Cdom(Σ) % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} C \in \text{dom}(\Sigma) we have that Σ(C) % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} \Sigma(C) is indeed the number of bombs assigned by B % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} B. In other words, (Cdom(Σ))(Σ(C)=cCB(c)) % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} \Bigg( \forall C \in \t{dom}(\Sigma) \Bigg)\left( \Sigma(C) = \sum_{c \in C} B(c) \right) This can also be interpreted as saying that B % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} B ‘respects’ or ‘realizesΣ % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} \Sigma Say that a cell c % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} c is determined relative to a valuation function Σ % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} \Sigma if every bomb function B % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} B compatible with Σ % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} \Sigma agrees on c % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} c; that is, if (b0{0,1})(bomb-function B)(B compatible with Σ    B(c)=b0) % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} ( \exists b_0 \in \{0,1\} )( \forall \t{bomb-function } B )( B \text{ compatible with } \Sigma \implies B(c) = b_0 ) If a turn is spent revealing a determined cell, call that a progression. Say that a game is progressable if there exists a progression. Call a game solvable if there exists a sequence of progressions resulting in a win.
Prompts
A prompt consists of a set Cell % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} \text{Cell} and a valuation function Σ % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} \Sigma. A prompt is the same as a game state but without the bomb function. The name prompt comes from thinking of it as a ‘puzzle to be solved’. Given two prompts P1=(C1,Σ1) % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} P_1 = (C_1, \Sigma_1) and P2=(C2,Σ2) % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} P_2 = (C_2, \Sigma_2), denote by P1P2 % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} P_1 \cup P_2 their union, formed by unioning their cells and valuation functions. This is only well-defined if the valuation functions agree on C1C2 % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} C_1 \cap C_2. Given two prompts P1=(C1,Σ1) % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} P_1 = (C_1, \Sigma_1) and P2=(C2,Σ2) % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} P_2 = (C_2, \Sigma_2), denote by P1+P2 % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} P_1 + P_2 their coproduct, consisting of the cell set C1+C2 % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} C_1 + C_2 and the valuation function constructed from Σ1,Σ2 % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} \Sigma_1, \Sigma_2 in the natural way. Given a prompt P=(C,Σ) % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} P = (C, \Sigma) and cells x,yC % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} x, y \in C, denote by P/x=y % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} P / x = y the prompt (C{z},Σ{({x,z},1),({y,z},1)}) % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} (C \cup \{z\}, \Sigma \cup \{ (\{x, z\}, 1), (\{y, z\}, 1) \}) for some zC % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} z \notin C. This adds a new cell z % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} z to P % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} P along with assertions that Σ(x,z)=Σ(y,z)=1 % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} \Sigma(x, z) = \Sigma(y, z) = 1, which states that x¬zy % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} x \leftrightarrow \neg z \leftrightarrow y and therefore xy % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} x \leftrightarrow y; ie, x % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} x and y % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} y evaluate equivalently. Relative to a prompt (C,Σ) % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} (C, \Sigma), for a vector c % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} \ol c of cells denote by span(c) % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} \text{span}(\ol c) the set of valuations for those cells compatible with Σ % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} \Sigma. For instance, if C={a,b} % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} C = \{a,b\} and Σ % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} \Sigma demands that a+b=1 % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} a + b = 1 and nothing else, then we get span(a,b)={0,1,1,0} % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} \text{span}(\tup{a,b}) = \{ \tup{0,1}, \tup{1,0} \}. Let P=P1+P2 % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} P = P_1 + P_2 and take a vector of variables vC % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} \ol v \in C. Assume that this vector decomposes as the concatenation v=v1v2 % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} \ol v = \ol v_1 \ol v_2, where v1C1 % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} \ol v_1 \in C_1 and v2C2 % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} \ol v_2 \in C_2. Then spanP(v)=spanP1(v1)×spanP2(v2) % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} \text{span}_P(\ol v) = \text{span}_{P_1}(\ol v_1) \times \text{span}_{P_2}(\ol v_2) (where × % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} \times is not plain cartesian product but a “zipping” cartesian product which combines pairs by concatenation) Now need case for spanP(v) % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} \text{span}_P(\ol v) in P=P/x=y % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} P = P^\star / x=y Conjecture: any prompt can be decomposed into a sequence of coproducts followed by quotients; the span of cell-vectors is the same in the original prompt as in its decomposition. The goal here is to first show some property of the span of cell-vectors, such as that (for instance) all spans are of odd cardinality. Then we use that to show that conjunction cannot be encoded as a prompt, for instance because if we had cells a,b,x % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} a, b, x such that xab % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} x \leftrightarrow a \land b then we’d have that span(a,b,x)=4 % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} \text{span}(\tup{a, b, x}) = 4 is even, which contradicts that all spans are odd.
Completeness: an attempt
One attempt at a complete set of rules for solving a game of minesweeper are the following: Σ(A)=A; aAB(a)=1(bomb-intro)B(a)=1Σ({a})=1(bomb-elim)Σ(A)=0; aAB(a)=0(safe-intro)B(a)=0Σ({a})=0(safe-elim)Σ(U)=n; Σ(A)=k; AUΣ(UA)=nk(split) % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} \begin{gather*} \frac{\Sigma(A) = \norm A;\ a \in A}{B(a) = 1} \hspace{10pt} \t{(bomb-intro)} \\ \\ \frac{B(a) = 1}{\Sigma(\{a\}) = 1} \hspace{10pt} \t{(bomb-elim)} \\ \\ \frac{\Sigma(A) = 0;\ a \in A}{B(a) = 0} \hspace{10pt} \t{(safe-intro)} \\ \\ \frac{B(a) = 0}{\Sigma(\{a\}) = 0} \hspace{10pt} \t{(safe-elim)} \\ \\ \frac{ \Sigma(U) = n;\ \Sigma(A) = k;\ A \subseteq U }{ \Sigma(U\setminus A) = n - k } \hspace{10pt} \t{(split)} \end{gather*} Unfortunately, this rule set is not complete. One counter-example is as follows: – – – – – 1 2 – a b c d – – – – Here a number denotes the valuation of a revealed cell, and letters and hyphens denote un-revealed cells. This valuation determines that B(d)=1 % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} B(d) = 1. However, none of the proposed rules are applicable. Hence, the ruleset is incomplete.
Relation to Boolean Satisfiability
One tempting re-interpretation of the game is as a phrasing for the boolean satisfiability problem. Given a game state, we may consider each cell to be a variable. Then a valuation Σ(C)=n % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} \Sigma(C) = n corresponds to the statement that exactly n % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} n of the variables in C % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} C are true, which is expressible as a finite sentence. For instance, Σ({a,b,c})=2 % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} \Sigma(\{a, b, c\}) = 2 becomes (ab¬c)(a¬bc)(¬abc) % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} (a \land b \land \neg c) \lor (a \land \neg b \land c) \lor (\neg a \land b \land c) It is unclear to me at this moment whether the problem of solving minesweeper is equivalent to boolean satisfiability. While each minesweeper game can be interpreted as a boolean expression, I am unsure if the reverse is also true. Are there boolean sentences which cannot be encoded as minesweeper games? Any sentence which conists only of conjunctions and negations (under the conjunctons), and with no repeated variables, is easy to express. Let C % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} C be the set of variables, and let TC % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} T \subseteq C be the set of non-negated variables. Let Σ={(T,T)} % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} \Sigma = \{ (T, \norm T) \}. Then by split and bomb-intro we can deduce that B(c)=1    cT % shorthands \newcommand{\cl}[1]{ \mathcal{#1} } \newcommand{\sc}[1]{ \mathscr{#1} } \newcommand{\bb}[1]{ \mathbb{#1} } \newcommand{\fk}[1]{ \mathfrak{#1} } \renewcommand{\bf}[1]{ \mathbf{#1} } \renewcommand{\sf}[1]{ \mathsf{#1} } % category names \newcommand{\cat}[1]{{ \sf{#1} }} % more shorthands \newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}[1]{ { \lceil {#1} \rceil } } \newcommand{\ol}[1]{ \overline{#1} } \newcommand{\t}[1]{ \text{#1} } \newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$ \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}[1]{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } % good enough definition of yoneda \newcommand{\yo}{よ} B(c) = 1 \iff c \in T.