The Pruning Theorem: Thinning Based on a Loose Notion of Monotonicity

The reason I studied the thinning theorem again is because I need a slightly generalised variation. The following seems to be what I need. The general idea and the term “pruning” emerged from discussion with Sharon Curtis. The term “lax preorder” is invented by myself. I am not good at naming, and welcome suggestions for better names.

The notation below are mostly taken from the book Algebra of Programming. Not many people, even among functional programmers, are familiar with these notations involving relational intersection, division, etc. One starts to appreciate their benefits once he/she gets used to using their calculation rules. Most of the time when I was doing the proof, I was merely manipulating the symbols. I could not have managed the complexity if I had to fall back to the semantics and think about what they “mean” all the time.

A relation Q :: PA ← A between a set of A and an element is called a lax preorder if it is

1. reflexive in the sense that ∋ ⊆ Q, and
2. transitive in the sense that (Q/∋) . Q ⊆ Q.

A relation S :: A ← FA is monotonic on lax preorder Q if S . FQ˘ ⊆ Q˘. Λ(S . F∈).

Given a lax preorder, we define:

$prune\; Q\; =\; \in \backslash \in \; \cap \; Q/\ni$

The definition induces the universal property:

$X\; \subseteq \; prune\; Q\; .\; \Lambda S \equiv \; \in \; .\; X\; \subseteq \; S\; \bigwedge \; X\; .\; S˘\subseteq \; Q$

Any preorder R induces a lax preorder ∋ . R. If a relation S is monotonic on R˘, it is monotonic on lax preorder ∋ . R. Furthermore, prune (∋ . R) = thin R. Therefore, pruning is a generalisation of thinning. We need the notion of lax preorders because, for some problems, the generating relation S is monotonic on a lax preorder, but not a preorder.

Theorem: if S is monotonic on lax preorder Q, we have:

$fold\; (prune\; Q\; .\; \Lambda (S\; .\; F\in ))\; \subseteq \; prune\; Q\; .\; \Lambda (fold\; S)$

Proof. Since Λ(fold S) = fold (Λ(S . F∈)), by fold fusion, the theorem holds if

$prune\; Q\; .\; \Lambda (S\; .\; F\in )\; .\; F(prune\; Q)\; \subseteq \; prune\; Q\; .\; \Lambda (S\; .\; F\in )$

By the universal property of prune, the above is equivalent to:

$\in \; .\; prune\; Q\; .\; \Lambda (S\; .\; F\in )\; .\; F(prune\; Q)\; \subseteq \; S\; .\; F\in \; \bigwedge \; prune\; Q\; .\; \Lambda (S\; .\; F\in )\; .\; F(prune\; Q)\; .\; (S\; .\; F\in )˘\; \subseteq \; Q$

The first inclusion is proved by:

$\; \in \; .\; prune\; Q\; .\; \Lambda (S\; .\; F\in )\; .\; F(prune\; Q)\; \subseteq \{\; since\; prune\; Q\; \subseteq \; \in \backslash \in \; \} \; \in \; .\; \in \backslash \in \; .\; \Lambda (S\; .\; F\in )\; .\; F(thin\; Q)\; \subseteq \{\; division\; \} \; \in \; .\; \Lambda (S\; .\; F\in )\; .\; F(thin\; Q)\; = \{\; power\; transpose\; \} \; S\; .\; F\in \; .\; F(thin\; Q)\; \subseteq \{\; since\; prune\; Q\; \subseteq \; \in \backslash \in \; \} \; S\; .\; F\in \; .\; F(\in \backslash \in )\; \subseteq \{\; division\; \} \; S\; .\; F\in$

And the second by:

$\; prune\; Q\; .\; \Lambda (S\; .\; F\in )\; .\; F(prune\; Q)\; .\; (S\; .\; F\in )˘\; \subseteq \{\; since\; prune\; Q\; \subseteq \; Q/\ni ,\; converse\; \} \; prune\; Q\; .\; \Lambda (S\; .\; F\in )\; .\; F(Q/\ni )\; .\; F\ni \; .\; S˘\; \subseteq \{\; division\; \} \; prune\; Q\; .\; \Lambda (S\; .\; F\in )\; .\; FQ\; .\; S˘\; \subseteq \{\; monotonicity:\; FQ\; .\; S˘\subseteq \; \Lambda (S\; .\; F\in )˘.\; Q\; \} \; prune\; Q\; .\; \Lambda (S\; .\; F\in )\; .\; \Lambda (S\; .\; F\in )˘.\; Q\; \subseteq \{\; since\; \Lambda (S\; .\; F\in )˘is\; a\; function,\; that\; is,\; f\; .\; f˘\subseteq \; id\; \} \; prune\; Q\; .\; Q\; \subseteq \{\; since\; thin\; Q\; \subseteq \; Q/\ni ,\; division\; \} \; Q/\ni \; .\; Q\; \subseteq \{\; since\; Q\; transitive\; \} \; Q$

Endproof.

The proof above uses transitivity of Q but not reflectivity. I need reflectivity to construct base cases, for example, to come up wit this specialised Pruning Theorem for lists:

$foldr\; (prune\; Q\; .\; \Lambda (S\; .\; (id\; \times \; \in )))\; \{e\}\; \subseteq \; prune\; Q\; .\; \Lambda (foldr\; S\; e)$

if S . (id × Q˘) ⊆ Q˘. Λ(S . (id × ∈)).