models

Wang tiles [@wang1961proving] are square tiles with a colour on each side. For instance: $W = \left\{\scalebox{0.3}{
    \wang{yellow}{red}{blue}{yellow}
    \wang{green}{green}{blue}{red}
}\right\}$. We are interested in the possible tilings made by putting copies of the tiles side by side such that two adjacent sides have the same colour. Our setting naturally generalises the structure and behaviour of Wang tiles in $\nat^2$.

Let $t^i = (c^i_w, c^i_e, c^i_s, c^i_n)$, $i=1,\dots,k$, be a set of Wang tile characterised by west, east, south and north colours. We encode each Wang tile in $\nat^2$ by the star $$(t^i)^\bigstar = \gstar{-h(c^i_w(x), x, y), -v(c^i_s(y), x, y), +h(c^i_e(s(x)), x, y), +v(c^i_n(s(y)), x, y)}.$$

This supposes the signature to contain a unary function symbol for each colour used in the Wang tiles set considered. We use two additional ternary colours $h$ (for *horizontal axis*) and $v$ (for *vertical axis*) for the rays. The terms $s^n(x), s^n(y)$ for $n \leq 0$ represent coordinates on the horizontal and vertical axis encoded as natural numbers, and forbids geometric patterns that would be impossible in the original Wang tile framework (e.g. a tile connected to itself). A (possibly cyclic) diagram will correspond to a finite tiling.

Wang tilings are a Turing-complete model 