Theoretical Computer Science Stack Exchange is a question and answer site for theoretical computer scientists and researchers in related fields. It only takes a minute to sign up.
Sign up to join this community
I've read in Lemma 2 of the paper 1 that if every square region of the plane admits a tiling, then the whole plain admits a tiling, but the proof is omitted. This sounds like a compactness property, but I don't see how easy can be proven.
I added the tag "automata theory" because there is a correspondence between Wang tilings and finite state transducers.
Yes, this is a compactness property.
Let $X$ be the region you want to tile, and $T$ the finite set of possible tiles. The space $T^X$ of all assignments of tiles to $X$ is compact by Tychonoff’s theorem. For any finite $X_0\subseteq X$, the set $C_{X_0}\subseteq T^X$ of all correct tilings of $X_0$ is closed (in fact, clopen), and since $C_{X_0\cup X_1}\subseteq C_{X_0}\cap C_{X_1}$, they generate a filter. Thus, assuming every finite subset of $X$ can be tiled, the system $\{C_{X_0}:X_0\subseteq X\text{ finite}\}$ has fip, and by compacteness, its intersection is nonempty. This intersection is the set of all correct tilings of $X$.
Instead of all finite $X_0$, it suffices to use any family of finite subsets which is upwards directed and covers $X$, such as, in your case, the set of all finite square subregions of the plane.
Alternatively, you may set up the argument to use the compacteness of classical propositional logic: let $\{p_{x,t}:x\in X,t\in T\}$ be a set of propositional variables, and let $C$ be the theory consisting of the formulas $$\begin{gather*} \bigvee_{t\in T}p_{x,t},\qquad x\in X,\\ \neg(p_{x,t}\land p_{x,t'}),\qquad x\in X,t\ne t'\in T, \end{gather*}$$ and $$\neg(p_{x,t}\land p_{x',t'})$$ for all $x,x'\in X$ that are neighbours, and $t,t'\in T$ that are incompatible when placed on $x$ and $x'$, respectively. If each finite subset of $X$can be tiled, then $C$ is consistent, and any satisfying assignment gives a tiling of $X$.
First, there is an infinite tiling of the plane if and only if there are square tilings $$ T_1 < T_2 < T_3 < \ ... $$ such that $T_i$ is an $i \times i$ square tiling, and $T_i$ is a subtiling of $T_{i+1}$.
Now, for each $T_i$ define $f(T_i)$ to be the size of the largest square tiling that $T_i$ is a subtiling of, where $f(T_i) = \infty$ if for all $n > i$, $T_i$ is a subtiling of some $n\times n$ tiling.
Lemma 1: if for an $i \times i$ tiling $T_i$, $f(T_i) = \infty$, then there is some $(i+1) \times (i+1)$ tiling $T_{i+1}$ with $T_i < T_{i+1}$ and $f(T_{i+1}) = \infty$.
Proof: Suppose not. Then look at the maximum value $n$ of $f(T)$ for $(i+1) \times (i+1)$ tilings containing $T_i$:
$$n = \max_{T > T_i \atop T \mathrm{\ is\ } (i+1) \times (i+1)} f(T). $$
If this is finite, then no tiling containing $T_i$ can be larger than $n \times n$, contradicting $f(T_i) = \infty$. And if it is infinite, one of the $(i +1) \times (i+1)$ tilings $T$ must have $f(T) = \infty$, as otherwise we have $\infty$ is the maximum of a finite number of finite integers (since there are a finite number of $(i+1) \times (i+1)$ tilings).
So at least one of the $(i+1) \times (i+1)$ tilings containing $T$ must have an infinite value for $f$. QED
Now, we can ask whether $f(T_1) = \infty$ for any single $1 \times 1$ tile. If not, then there is a maximum size square that admits a tiling. And if so, then given a tiling $T_1$ with $f(T_1) = \infty$, we can use lemma 1 to find tilings $$ T_1 < T_2 < T_3 < \ ... $$ such that $f(T_i) = \infty$ for all $i$, showing that there is an infinite tiling of the plain.
