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.
- reflexive in the sense that
∋ ⊆ Q, and
- transitive in the sense that
(Q/∋) . Q ⊆ Q.
Given a lax preorder, we define:
The definition induces the universal property:
By the universal property of
The first inclusion is proved by:
And the second by:
The proof above uses transitivity of