Yu-Han Lyu and I were studying some paper from the algorithm community, and we noticed a peculiar kind of argument. For a much simplified version, let X and D be two relations of type A → B, denoting two alternative approaches to non-deterministically compute possible solution candidates to a problem. Also let ≤ be a transitive relation on B, and ≥ its converse. The relation min ≤ : {B} → B, given a set, returns one of its elements that is no larger (under ≤) than any elements in the set, if such a minimum exists.
We would like find solution as small as possible under ≤.
When arguing for the correctness of its algorithm, the paper we are studying claims that the method X is no worse than D in the following sense: if every solution returned by D is no better than some solution returned by X, which we translate to:
D ⊆ ≥ . Xthen the best (smallest) solution by X must be no worse than (one of the) best solutions returned by D:
min ≤ . ΛX ⊆ ≤ . min ≤ . ΛDwhere Λ converts a relation A → B to a function A → {B} by collecting its results to a set. Note that, awkwardly, X and D are swapped to different sides of relational inclusion.
“What? How could this be true?” was my first reaction. I bombarded Yu-Han with lots of emails, making sure that we didn’t misinterpret the paper. An informal way to see it is that since every result of D is outperformed by something returned by X, collectively, the best result among the latter must is “lower-bounded” by the optimal result of D. But this sounds unconvincing to me. Something is missing.
Totality and Well-Boundedness
It turns out that the reasoning can be correct, but we need some more constraints on D and ≤. Firstly, D must yield some result whenever X does. Otherwise it could be that D ⊆ ≥ . X is true but ΛD returns an empty set, while ΛX still returns something. This is bad because X is no more a safe alternative of D — it could sometimes do too much. One way to prevent it from happening so is to demand that ΛD = dom ∈ . ΛD, where ∈ is the membership relation, and dom ∈, the domain of ∈, consists only of non-empty sets. It will be proved later that this is equivalent to demanding that D be total.
Secondly, we need to be sure that every non-empty set has a minimum, or min ≤ always yields something for non-empty sets. Therefore min ≤ . ΛD would not fall back to the empty relation. Formally, it can be expressed as dom ∈ = dom (min ≤). Bird and de Moor called this property well-boundedness of ≤.
Recall that min ≤ = ∈ ∩ ≤/∋. The part ∈ guarantees that min ≤ returns something that is in the given set, while ≤/∋ guarantees that the returned value is a lower-bound of the given set. Since ΛD (as well as ΛX) is a function, we also have min ≤ . ΛD = D ∩ ≤/D°, following from the laws of division.
Later we will prove an auxiliary lemma stating that if ≤ is well-bounded, we have:
≤/∋ . dom ∈ ⊆ ≤ . min ≤ . dom ∈The right-hand side, given a non-empty list, takes its minimum and returns something possibly smaller. The left-hand side merely returns some lower-bound of the given set. It sounds weaker because it does not demand that the set has a minimum. Nevertheless, the inclusion holds if ≤ is well-bounded.
An algebraic proof of the auxiliary lemma was given by Akimasa Morihata. The proof, to be discussed later, is quite interesting to me because it makes an unusual use of indirect equality. With the lemma, proof of the main result becomes rather routine:
min ≤ . ΛX ⊆ ≤ . min ≤ . ΛD
≣ { since ΛD = dom ∈ . ΛD }
min ≤ . ΛX ⊆ ≤ . min ≤ . dom ∈ . ΛD
⇐ { ≤/∋ . dom ∈ ⊆ ≤ . min ≤ . dom ∈, see below }
min ≤ . ΛX ⊆ ≤/∋ . dom ∈ . ΛD
≣ { since ΛD = dom ∈ . ΛD }
min ≤ . ΛX ⊆ ≤/∋ . ΛD
≣ { since ΛD is a function, R/S . f = R/(f° . S) }
min ≤ . ΛX ⊆ ≤/D°
≣ { Galois connection }
min ≤ . ΛX . D° ⊆ ≤
⇐ { min ≤ . ΛX ⊆ ≤/X° }
≤/X°. D° ⊆ ≤
⇐ { since D ⊆ ≥ . X }
≤/X°. X° . ≤ ⊆ ≤
⇐ { division }
≤ . ≤ ⊆ ≤
≣ { ≤ transitive }
true
Proof Using Enriched Indirect Equality
Now we have got to prove that ≤/∋ . dom ∈ ⊆ ≤ . min ≤ . dom ∈ provided that ≤ is well-bounded. To prove this lemma I had to resort to first-order logic. I passed the problem to Akimasa Morihata and he quickly came up with a proof. We start with some preparation:
≤/∋ . dom ∈ ⊆ ≤ . min ≤ . dom ∈
⇐ { since min ≤ ⊆ ∈ }
≤/(min ≤)° . dom ∈ ⊆ ≤ . min ≤ . dom ∈
And then we use proof by indirect (in)equality. The proof, however, is unusual in two ways. Firstly, we need the enriched indirect equality proposed by Dijkstra in
EWD 1315: Indirect equality enriched (and a proof by Netty). Typically, proof by indirect equality exploits the property:
x = y ≡ (∀u. u ⊆ x ≡ u ⊆ y)and also:
x ⊆ y ≡ (∀u. u ⊆ x ⇒ u ⊆ y)When we know that both x and y satisfy some predicate P, enriched indirect equality allows us to prove x = y (or x ⊆ y) by proving a weaker premise:
x = y ≡ (∀u. P u ⇒ u ⊆ x ≡ u ⊆ y)Note that both ≤/(min ≤)° . dom ∈ and ≤ . min ≤ . dom ∈ satisfy X = X . dom ∈. Later we will try to prove:
X ⊆ ≤/(min ≤)° . dom ∈ ⇒ X ⊆ ≤ . min ≤ . dom ∈
for X such that X = X . dom ∈.
The second unusual aspect is that rather than starting from one of X ⊆ ≤/(min ≤)° . dom ∈ or X ⊆ ≤ . min ≤ . dom ∈ and ending at another, Morihata’s proof took the goal as a whole and used rules like (P ⇒ Q) ⇒ (P ⇒ P ∧ Q). The proof goes:
(X ⊆ ≤/(min ≤)° . dom ∈ ⇒ X ⊆ ≤ . min ≤ . dom ∈)
⇐ { dom ∈ ⊆ id }
(X ⊆ ≤/(min ≤)° ⇒ X ⊆ ≤ . min ≤ . dom ∈)
≣ { Galois connection }
(X . (min ≤)° ⊆ ≤ ⇒ X ⊆ ≤ . min ≤ . dom ∈)
⇐ { (P ⇒ Q) ⇒ (P ⇒ P ∧ Q) }
(X . (min ≤)° ⊆ ≤ ⇒ X ⊆ X . (min ≤)° . min ≤ . dom ∈)
⇐ { R ∩ S ⊆ R }
(X . (min ≤)° ⊆ ≤ ⇒ X ⊆ X . (((min ≤)° . min ≤) ∩ id) . dom ∈)
≣ { dom R = (R° . R) ∩ id }
(X . (min ≤)° ⊆ ≤ ⇒ X ⊆ X . dom (min ≤) . dom ∈)
≣ { ≤ well-bounded: dom ∈ = dom (min ≤) }
(X . (min ≤)° ⊆ ≤ ⇒ X ⊆ X . dom ∈ . dom ∈)
≣ { dom ∈ . dom ∈ = dom ∈ }
(X . (min ≤)° ⊆ ≤ ⇒ X ⊆ X . dom ∈)
≣ { X = X . dom ∈ }
(X . (min ≤)° ⊆ ≤ ⇒ true)
≣ true
Auxiliary Proofs
Finally, this is a proof that the constraint ΛD = dom ∈ . ΛD is equivalent to D being total, that is id ⊆ D° . D. Recall that dom ∈ = ((∋ . ∈) ∩ id). We simplify dom ∈ . ΛD a bit:
dom ∈ . ΛD
= ((∋ . ∈) ∩ id) . ΛD
= { ΛD a function }
(∋ . ∈ . ΛD) ∩ ΛD
= { ∈ . ΛD = D }
(∋ . D) ∩ ΛD
We reason:
dom ∈ . ΛD = ΛD
≡ { R ∩ S = S iff S ⊆ R }
ΛD ⊆ ∋ . D
≡ { ΛD function, shunting }
id ⊆ (ΛD)° . ∋ . D
≡ id ⊆ D° . D
which is the definition of totality.