# How to show that two vertices in a connected component are in the same set? (bi conditional)

Show that after all edges are processed by CONNECTED-COMPONENTS, two vertices are in the same connected component if and only if they are in the same set.

The CONNECTED-COMPONENTS algorithm is the following:

It seems pretty obvious that when we keep adding the vertices of the direct edges of a connected component to a set, eventually the set formed has all the vertices in the connected component - directly connected as well as indirectly connected. But how do I formally prove that? Also it seems like a biconditional to me. I've thought of things like loop-invariant or a proof by contradiction. But unable to exactly figure out what to do. Any help is appreciated.

• Think about what it means for two nodes to be connected... We already know that if two nodes are adjacent they're in the same set, so what does that tell us about nodes in the same connected component? – Tom van der Zanden Aug 2 '16 at 6:54
• @TomvanderZanden They are reachable or indirectly connected. They are adjacent to a node which is adjacent to a node and so on till a node which is in the set. Am I correct? If so, how to I "formally" present it? – aste123 Aug 2 '16 at 15:01

Below are two approaches to your problem.

# detailed semi-formal proof

Since you've provided a minimal context, I will state my assumptions then provide a solution. Moreover, I will use very basic loops rather than the fancy for-each loop since they are easier to prove correctness with ─more accurately, easier for me with my current knowledge.

1. We are assuming simple undirected graphs: ie., pairs (V, E) of a set V of vertices and a symmetric relation E ⊆ V × V.
2. Two vertices are “connected” precisely when there is a path along E between the two: x ~ y ∶≡ (∃ n : ℕ • x Eⁿ y) ─where the bullet serves to separate the bound variable of the quantifier and the body of the quantifier, and exponentiation is iterated relational product.
3. A “connected component” is a subgraph in which any two vertices are connected, and which is connected to no additional vertices in the supergraph. For our needs, we only consider connected components arising from subsets of vertices.

𝒞 connected-component
⇔ (∀ x,y : 𝒞 • x ~ y) ∧ (∀ 𝒟 : ℙ V • 𝒞 ⊆ 𝒟 ∧ (∀ x,y : 𝒟 • x ~ y) ⇒ 𝒞 = 𝒟)
⇔ (∀ 𝒟 : ℙ V • (∀ x,y : 𝒟 • x ~ y) ∧ 𝒞 ⊆ 𝒟 ⇔ 𝒟 ⊆ 𝒞)
⇔ 𝒞 is an ~-equivalence class


Note that ∧ means “and”.

4. Make-set assigns the emptyset ∅ to each vertex, in some look-up table. We assume this to be the case at the very beginning and so need not worry about it.

Find-set looks up the set that is associated to a vertex, in the aforementioned look-up table.

Union(x,y) alters the set associated to x by unioning it what the set associated to y, and does so as well for y. In particular, after this command we have Find-set x = old-Find-set x ∪ old-Find-set y.

1. The post-condition of the program is

∀ x : V •
Find-set x = {y : V ❙ (∃ x₀,…,xₙ : V • x = x₀ ∧ xₙ = y ∧ (∀ i • xᵢ E xᵢ₊₁))}


i.e.,

∀ x : V • connected-component (Find-set x)


That is, the algorithm assigns the connected components to the associated sets of the vertices. Alternatively, it is: Find-set x = the ~-equivalence class of x.

2. From the post-condition,

  ∀ x : V •
Find-set x = {y : V ❙ (∃ x₀,…,xₙ : V • x = x₀ ∧ xₙ = y ∧ (∀ i • xᵢ E xᵢ₊₁))}


The simplest thing to do is to replace a constant, say E, with a new variable, and relate it to the constant to obtain an invariant.

P ∷ 𝓔 ⊆ E  ∧
(∀ x : V •
Find-set x
= {y : V ❙ (∃ x₀,…,xₙ : V • x = x₀ ∧ xₙ = y ∧ (∀ i • xᵢ 𝓔 xᵢ₊₁))})


So it is obvious that the post-condition is obtained once we've arrived at the conclusion E ⊆ 𝓔. So a good idea is to increase 𝓔 until this condition is true. Moreover, the invaraint needs to hold before the loop and we can do this by setting 𝓔 ≔ ∅: indeed ∅ ⊆ E and intially every vertex is assigned the emptyset which is what is needed since,

  {y : V ❙ (∃ x₀,…,xₙ : V • x = x₀ ∧ xₙ = y ∧ (∀ i • xᵢ 𝓔 xᵢ₊₁)))}
=⟨ initial value of 𝓔 ⟩
{y : V ❙ (∃ x₀,…,xₙ : V • x = x₀ ∧ xₙ = y ∧ (∀ i • xᵢ ∅ xᵢ₊₁)))}
=⟨ definition of empty set ⟩
{y : V ❙ (∃ x₀,…,xₙ : V • x = x₀ ∧ xₙ = y ∧ (∀ i • false))}
=⟨ “for all i, we have false  ≡ false” ⟩
{y : V ❙ (∃ x₀,…,xₙ : V • x = x₀ ∧ xₙ = y ∧ false)}
=⟨ “false ∧ stuff ≡ false” ⟩
{y : V ❙ (∃ x₀,…,xₙ : V • false)}
=⟨ “there is some stuff yielding false ≡ false” ⟩
{y : V ❙ false }
=⟨ there are no y that make false true ⟩
∅
=⟨ initial value of Find-set ⟩
Find-set x


So, to be very explicit, we assume that before the algorithm is run, we have

∀ x : V • find-set x = ∅.

3. Anyhow, the previous paragraph informs us that the algorithm we are looking for has the shape

{Pre: (∀ x : V • find-set x = ∅) }
𝓔 ≔ ∅
; {Invariant: 𝓔 ⊆ E  ∧
(∀ x : V • Find-set x = {y : V ❙ (∃ x₀,…,xₙ : V • x = x₀ ∧ xₙ = y           ∧ (∀ i • xᵢ 𝓔 xᵢ₊₁))}) }
while ¬ E ⊆ 𝓔 : do-stuff
{Post: (∀ x : V • Find-set x = {y : V ❙ (∃ x₀,…,xₙ : V • x = x₀ ∧ xₙ = y ∧ (∀ i • xᵢ E xᵢ₊₁))}


Note that it is common to place “assert” statements within curly braces. C♯ for example documents them in the form Contract.Assert.IsTrue(...).

4. It seems the only thing left to do is find an implementation of do-stuff. Well, the loop terminates if we make the loop guard ¬ E ⊆ 𝓔 false.

By the invariant, we know ♯𝓔 ≤ ♯E and so increasing 𝓔 will do the job. We can choose an edge of E, it doesn't matter which one as long as it's one we haven't considered it, and add that to 𝓔. What, are there even such edges!? Well, by the invariant, we have 𝓔 ⊆ E ∧ E ⊈ 𝓔 within the loop, which implies E - 𝓔 ≠ ∅, whence there are such edges.

Hence, one possible candidate for do-stuff is

 (u,v) ≔ choose an edge from E - 𝓔
; 𝓔 ≔ 𝓔 ∪ {(u,v)}


The candidate is enough and we are done deriving our algorithm, “provided” that this choice of do-stuff does not ruin the invariant. It clearly does ruin the invariant since we have not altered the find-set for these two vertices.

The final result is

 {Pre: (∀ x : V • find-set x = ∅) }
𝓔 ≔ ∅
; {Invariant: 𝓔 ⊆ E  ∧
(∀ x : V • Find-set x = {y : V ❙ (∃ x₀,…,xₙ : V • x = x₀ ∧ xₙ = y ∧ (∀ i • xᵢ 𝓔 xᵢ₊₁))}) }
while ¬ E ⊆ 𝓔 :
(u,v) ≔ choose an edge from E - 𝓔
; if find-set u ≠ find set u then union(u,v)
; 𝓔 ≔ 𝓔 ∪ {(u,v)}
{Post: (∀ x : V • Find-set x = {y : V ❙ (∃ x₀,…,xₙ : V • x = x₀ ∧ xₙ = y ∧ (∀ i • xᵢ E xᵢ₊₁))}

5. To relate this to your initial code, consider the following.

 for each i in S : do-stuff
≈
visited ≔ ∅
; while visited ≠ S:
i ≔ pick an element of S - visited
; do-stuff
; visited ≔ visited ∪ {i}


Our loop had ¬ E ⊆ 𝓔 and this is tantamount to E ≠ 𝓔:

  E ≠ 𝓔
=⟨ bi-containment ⟩
¬(E ⊆ 𝓔 ∧ 𝓔 ⊆ E)
=⟨ invariant ⟩
¬(E ⊆ 𝓔 ∧ true)
=⟨ “stuff ∧ true ≡ true” ⟩
¬ E ⊆ 𝓔


We use basic while loops since they are easier to work with is all. I've never really learned to write correctness proofs for for-each loops.

Hope this helps!

# Bi-implication informal argument

The algorithm's post-condition is find-set x = {y : V ❙ (∃ x₀,…,xₙ : V • x = x₀ ∧ xₙ = y ∧ (∀ i • xᵢ E xᵢ₊₁))}.

We show the equality using a bi-implication.

(⊆) ∷

By the construction of find-set, i.e., the way we add elements to the set associated to x, we know that any added element is connected to x and so find-set x ⊆ {y : V ❙ (∃ x₀,…,xₙ : V • x = x₀ ∧ xₙ = y ∧ (∀ i • xᵢ E xᵢ₊₁))}.

(⊇) ∷

We will show by induction that any vertex y at-least n : ℕ edges away from x must be within find-set x.

Base case: n = 0. Then x = x₀ = xₙ = y and clearly y ∈ find-set x.

Inductive step: if x E x₁ E x₂ E ⋯ E xₙ E xₙ₊₁ = y then by the inductive hypothesis xₙ ∈ find-set x; moreover, the algorithm ensures find-set x = find-set xₙ. Now since (xₙ, xₙ+1) is an edge ─a given─, the algorithm ensures find-set xₙ₊₁ = find-set xₙ but by the previous equalities we then have y ∈ find-set y = find-set xₙ₊₁ = find-set xₙ = find-set x.

:-)