Proofs: Doubly connected edge list

The doubly connected edge list represents a connected plane graph and its faces full

This proof shows: correctness, termination.

We use the pseudocode of the page. A half-edge is live if it has not been freed. For a live half-edge $h$, write $\mathrm{tgt}(h) = origin[twin(h)]$. For a vertex $v$ with at least one edge, let $\sigma_v$ be the map on the half-edges out of $v$ given by $\sigma_v(h) = twin(prev[h])$; this is the rotation that line L8 reads. The structure is valid if:

• (I1) $next$ and $prev$ restricted to the live half-edges are permutations, and $prev[next[h]] = h$ for each live $h$.
• (I2) $origin[next[h]] = \mathrm{tgt}(h)$ for each live $h$.
• (I3) $face[h] = face[h']$ exactly when $h$ and $h'$ lie on the same cycle of $next$, and $face\_edge[f]$ lies on the cycle with label $f$, for each face $f$ that exists.
• (I4) $vertex\_edge[v]$ is a live half-edge with origin $v$, or nil if $v$ has no edge.
• (I5) The graph is connected, and there is a drawing of it in the plane whose rotation at each vertex $v$ (the counterclockwise order of its edges) is $\sigma_v$ and whose faces are, one for one, the cycles of $next$, the face of a cycle being the face that lies to the left of its half-edges.

Lemma 1 (face tracing). Let $rot$ be a rotation system of a graph, and let $\phi$ map the dart $(u, v)$ to $(v, w)$, where $w$ is the neighbour just before $u$ in $rot[v]$. Then $\phi$ is a permutation of the darts, and the inverse sends $(v, w)$ to $(u, v)$ where $u$ is the neighbour just after $w$ in $rot[v]$. If $rot$ is the rotation system of a drawing of a connected plane graph, the cycles of $\phi$ are exactly the boundary walks of the faces, each traversed with its face on the left.

Proof. Given $(v, w)$, the dart $(u, v)$ with $\phi(u, v) = (v, w)$ must have $w$ just before $u$ in $rot[v]$, so $u$ is the unique neighbour just after $w$. So $\phi$ is one-to-one on a finite set, hence a permutation. The second part is the face tracing theorem for rotation systems (Mohar and Thomassen, Chapter 3; see rotation system). $\square$

Lemma 2 (BUILD). If $rot$ is the rotation system of a drawing of a connected plane graph with $n$ vertices and $m$ edges, BUILD stops after $O(n + m)$ dictionary operations and returns a valid structure.

Proof. Lines L1 and L2 create one pair of half-edges for each edge, since a pair is created only when $(u, v)$ has none, and each edge $uv$ appears as $v \in rot[u]$. Line L4 sets $next[h] = \phi(h)$ and $prev[\phi(h)] = h$, so (I1) holds by Lemma 1, and (I2) holds since $\phi(u, v)$ starts at $v$. Lines L5 and L6 label each cycle of $next$: the walk of line L6 stops when it reaches $h$ again, which it does because $next$ is a permutation, and each step labels one half-edge that had no label, so the number of unlabeled half-edges drops by 1 at each step and lines L5 and L6 take $2m$ steps in all. This gives (I3). The code sets $vertex\_edge[u]$ to a half-edge out of $u$, so (I4) holds. For (I5), take the drawing of $rot$. For a half-edge $h = (v, u)$, $prev[h] = \phi^{-1}(h) = (x, v)$ where $x$ is just after $u$ in $rot[v]$ by Lemma 1, so $\sigma_v(h) = (v, x)$ is the next half-edge out of $v$ counterclockwise, and $\sigma_v$ is the rotation of the drawing. The faces are the cycles of $next = \phi$ by Lemma 1. $\square$

Lemma 3 (walks). In a valid structure, NEIGHBOURS($v$) outputs the neighbours of $v$ in counterclockwise order, each once, and stops after $\deg(v)$ steps; FACE-BOUNDARY($f$) outputs the cycle of $f$ and stops after $|f|$ steps.

Proof. By (I5), $\sigma_v$ is a cyclic order of the $\deg(v)$ half-edges out of $v$, one cycle of length $\deg(v)$. Line L8 applies $\sigma_v$ from $vertex\_edge[v]$, which starts at $v$ by (I4), and stops on its return, so it lists each half-edge out of $v$ once, and their targets in counterclockwise order. Line L9 follows $next$ from $face\_edge[f]$, which lies on the cycle of $f$ by (I3), and stops on its return, after one round of that cycle. $\square$

Lemma 4 (SPLIT-FACE). Let the structure be valid, $a \ne b$ with $face[a] = face[b] = f$, $u = origin[a] \ne v = origin[b]$, and $u, v$ not adjacent. After SPLIT-FACE($a$, $b$), the structure is valid, with one more edge and one more face.

Proof. Let the cycle of $f$ be $a = c_0, c_1, \ldots, c_k = prev[b], c_{k+1} = b, \ldots, c_r = prev[a]$, so $0 \le k < r$ and $b$ follows $c_k$. Line L11 changes $next$ only at $prev[a]$, $prev[b]$, $h$ and $t$, and sets $next[c_r] = h$, $next[h] = b$, $next[c_k] = t$, $next[t] = a$. So the new cycles through these half-edges are $h, c_{k+1}, \ldots, c_r$ and $t, c_0, \ldots, c_k$. They partition the old cycle plus $h$ and $t$, and all other cycles are unchanged. Line L11 sets $prev$ at the same four places, so (I1) holds. For (I2): $origin[b] = v = \mathrm{tgt}(h)$, $origin[a] = u = \mathrm{tgt}(t)$, $origin[h] = u = \mathrm{tgt}(c_r)$ because $next[c_r]$ was $a$, and $origin[t] = v = \mathrm{tgt}(c_k)$ because $next[c_k]$ was $b$. Line L12 gives the cycle of $h$ the new label $g$ and $t$ the label $f$; the other half-edges of the cycle of $t$ keep $f$, so (I3) holds. Vertex records are unchanged, so (I4) holds.

For (I5): by (I5) before the split, the face $F$ of the drawing that belongs to the cycle of $f$ has both $u$ and $v$ on its boundary. Since $F$ is an open connected set, there is a simple arc from $u$ to $v$ through $F$ that leaves $u$ in the angle of $F$ between the edge of $c_r$ and the edge of $a$, and enters $v$ in the angle between the edge of $c_k$ and the edge of $b$. Add it as the new edge. The value $\sigma_u(y) = twin(prev[y])$ changes only for half-edges $y$ out of $u$ whose $prev$ changed. These are $a$, with $prev[a] = t$ and so $\sigma_u(a) = h$, and the new $h$, with $prev[h] = c_r$ and so $\sigma_u(h) = twin(c_r)$, the old value of $\sigma_u(a)$. So the new rotation at $u$ is the old one with $h$ inserted right after $a$, in the angle between $a$ and $twin(c_r)$, which is the corner of $F$ where the arc leaves $u$. In the same way, $\sigma_v(b) = twin(h) = t$ and $\sigma_v(t) = twin(c_k)$, so $t$ is inserted right after $b$ at $v$. So the new drawing has rotation $\sigma$. The arc splits $F$ into two faces, by the Jordan curve theorem applied to the closed curve made of the arc and a boundary path of $F$ from $v$ back to $u$, and the faces to the left of $h$ and of $t$ are bounded by the two new cycles. All other faces are unchanged. The graph stays connected. $\square$

Lemma 5 (ADD-LEAF). In a valid structure, after ADD-LEAF($a$) the structure is valid, with one more vertex, one more edge and the same number of faces.

Proof. Let $p = prev[a]$. Line L13 sets $next[p] = h$, $next[h] = t$, $next[t] = a$, so the cycle of $a$ gains $h, t$ between $p$ and $a$ and no other cycle changes; (I1) holds. (I2): $origin[h] = origin[a] = \mathrm{tgt}(p)$, $origin[t] = w = \mathrm{tgt}(h)$, $origin[a] = \mathrm{tgt}(t)$. Both new half-edges get the face of $a$, so (I3) holds, and the code sets $vertex\_edge$ of $origin[a]$ to $h$ and of $w$ to $t$, so (I4) holds. In the drawing, put $w$ in the face of $a$ near $origin[a]$ and join them by a short arc in the angle between the edge of $p$ and the edge of $a$; as in Lemma 4, the rotation at $origin[a]$ gains $h$ next to $a$, the rotation at $w$ is the single half-edge $t$, and the face keeps one boundary walk, now with $h, t$ in it. The empty case ($a$ nil, one vertex and no edge) makes the cycle $h, t$, the drawing of one edge, with one face. $\square$

Lemma 6 (JOIN-FACES). Let the structure be valid and $face[h] \ne face[t]$ for $t = twin(h)$. After JOIN-FACES($h$), the structure is valid, with one edge and one face fewer.

Proof. The cycles of $h$ and $t$ are different, so neither $next[h]$ nor $prev[h]$ is $t$ or $h$, and the same for $t$. Write the cycles as $h, x_1, \ldots, x_p$ and $t, y_1, \ldots, y_q$ with $p, q \ge 1$, where $x_1 = next[h]$, $x_p = prev[h]$, and likewise for $y$. Line L15 sets $next[x_p] = y_1$ and $next[y_q] = x_1$, so the two cycles become the one cycle $x_1, \ldots, x_p, y_1, \ldots, y_q$, and (I1) holds on the live half-edges. (I2): $\mathrm{tgt}(x_p) = origin[h] = \mathrm{tgt}(t) = origin[y_1]$ and $\mathrm{tgt}(y_q) = origin[t] = origin[x_1]$. Line L14 gives all of $x_1, \ldots, x_p$ the label of $t$, and $face\_edge$ of that face becomes $y_1$, so (I3) holds. If $vertex\_edge[origin[h]] = h$, it becomes $twin(x_p)$, which starts at $origin[h]$ and is live because $x_p \ne t$; the same for $t$, so (I4) holds.

For (I5), erase the edge of $h$ from the drawing. Its two sides are the faces of the two cycles, which are different, so the open arc of the edge joins two different faces into one, and the boundary walk of the union is the merged cycle. The rotation at $u = origin[h]$ loses $h$. Before the deletion, $\sigma_u(y_1) = twin(prev[y_1]) = twin(t) = h$ and $\sigma_u(h) = twin(x_p)$. After it, $prev[y_1] = x_p$, so $\sigma_u(y_1) = twin(x_p)$, and $h$ is cut out of the cycle of $\sigma_u$. In the same way, $\sigma(x_1)$ changes from $t$ to $twin(y_q)$ at $origin[t]$, so $t$ is cut out there. These are the rotations of the drawing without the edge. It remains to see that the graph stays connected. Let $G$ have $n$ vertices, $m$ edges and $f$ faces, so $n - m + f = 2$. The drawing of $G - e$ has $m - 1$ edges and $f - 1$ faces, and if it has $c$ components, Euler's formula for several components gives $n - (m - 1) + (f - 1) = 1 + c$, so $c = 1$. $\square$

Theorem. Starting from BUILD on the rotation system of a connected plane graph, or from the empty structure with one vertex, every sequence of operations whose preconditions hold keeps the structure valid, every walk outputs what its specification says, and every operation terminates. In particular $n - m + f = 2$ after each operation.

Proof. The empty structure (one vertex, no half-edge, one face with no half-edge) is valid. By Lemmas 2, 4, 5 and 6, each operation keeps validity, and by Lemma 3 the walks are correct. Each loop walks along a cycle of a permutation of a finite set and stops at its start, so each loop runs at most once around that cycle. Euler's formula holds for the drawing of (I5), and its faces are the cycles of $next$ by (I5). $\blacksquare$