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 = ∈\∈ ∩ Q/∋

The definition induces the universal property:

X ⊆ prune Q . ΛS   ≡    ∈ . X ⊆ S   ⋀   X . S˘⊆ Q

Any preorder R induces a lax preorder ∋ . R. If a relation S is monotonic on , 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 . Λ(S . F∈)) ⊆ prune Q . Λ(fold S)

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

prune Q . Λ(S . F∈) . F(prune Q) ⊆ prune Q . Λ(S . F∈)

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

∈ . prune Q . Λ(S . F∈) . F(prune Q) ⊆ S . F∈   ⋀
prune Q . Λ(S . F∈) . F(prune Q) . (S . F∈)˘ ⊆ Q

The first inclusion is proved by:

     ∈ . prune Q . Λ(S . F∈) . F(prune Q)
⊆     { since prune Q ⊆ ∈\∈ }
     ∈ . ∈\∈ . Λ(S . F∈) . F(thin Q)
⊆     { division }
     ∈ . Λ(S . F∈) . F(thin Q)
=     { power transpose }
     S . F∈ . F(thin Q)
⊆     { since prune Q ⊆ ∈\∈ }
     S . F∈ . F(∈\∈)
⊆     { division }
     S . F∈

And the second by:

     prune Q . Λ(S . F∈) . F(prune Q) . (S . F∈)˘
⊆     { since prune Q ⊆ Q/∋, converse }
     prune Q . Λ(S . F∈) . F(Q/∋) . F∋ . S˘
⊆     { division }
     prune Q . Λ(S . F∈) . FQ . S˘
⊆     { monotonicity: FQ . S˘⊆ Λ(S . F∈)˘. Q }
     prune Q . Λ(S . F∈) . Λ(S . F∈)˘. Q
⊆     { since Λ(S . F∈)˘is a function, that is, f . f˘⊆ id }
     prune Q . Q
⊆     { since thin Q ⊆ Q/∋, division }
     Q/∋ . Q
⊆     { 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 . Λ(S . (id × ∈))) {e} ⊆ prune Q . Λ(foldr S e)

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

Leave a Reply

Your email address will not be published. Required fields are marked *

You may use these HTML tags and attributes: <a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <cite> <code> <del datetime=""> <em> <i> <q cite=""> <strike> <strong>