Minimal proof obligations for ordered sets

Dirk Nowotka

Turku Centre for Computer Science, 20520 Turku, Finland

Abstract

We show how the smallest set of lemmas can be generated that is sufficient to prove an assumed partial-order relation on a finite set. This idea is developed from a mathematical formulation up to an algorithm implemented in ML. The process of establishing a Hasse diagram from a set of subsets serves as an applicative example.

1 Introduction

This paper describes an algorithm that is useful for minimizing the proof effort to establish a partial order over a finite set.

Suppose, we have a finite set of objects A and a preorder relation ≼ on A, and also, it is assumed to be hard to check whether or not x ≼ y, for some x, y ∈ A. Further, suppose that something is already known about ≼, namely a partial order ≤ contained in ≼. Now, let our goal be to show that actually ≤ = ≼. For that, we need to check that all elements in A not related in ≤ are also not related in ≼. Formally, for all x, y ∈ A we have x ≰ y implies x ⋠ y. Since it is assumed to be difficult to check the membership property for ≼, we look for the smallest number of pairs (x, y) ∉ ≤ to be investigated.

The following example illustrates that often not all possible pairs have to be considered. Let A = {a, b, c} be a set of sets and we investigate the subset relation on A. Assume, further we only know that a ⊆ b, so in this case ≤ = {(a, a), (b, b), (c, c), (a, b)}. Proving now that ≤ = ⊆, means to show that the following Hasse diagram of A is correct for ⊆.

b c a

For that, we need to show that for all x, y ∈ A, if x ≰ y then x ⊈ y, which means in our case to check: b ⊈ a, b ⊈ c, c ⊈ b, a ⊈ c, and c ⊈ a. But

Preprint submitted to Elsevier Preprint 25th April 2001

actually, once we know that a ⊈ c, we immediately have that b ⊈ c because we know a ⊆ b, and similarly, from c ⊈ b follows that c ⊈ a. So instead of five propositions we need to prove only three.

This paper shows how the smallest set of pairs S ⊆ {(x, y) | x ≰ y}, from which follows that ≤ = ≼, can be calculated. We give an algorithm and also show that S is unique for a given problem.

The topic of this paper was originally motivated by the practical goal to reduce work on comparing sets of formal languages, see for example [FV98] where this result is cited as a personal communication. There, given a set of sets of languages which are to be arranged in a Hasse diagram can be a nontrivial task, since comparing the expressive power of certain methods to generate a language might be difficult.

This paper is divided into two parts: Section 2, where the result is given, and Section 3, where we give an implementation of it.

2 Minimal Proof Obligations

Our terminology is chosen acording to the motivation given in the introduction. Since this is about a method to verify a finite partial-order relation on its elements, let us call a finite nonempty set universe which is ment to contain the objects of our interest, and let a preorder on a universe represent the actual relation the induced partial-order relation of which we would like to determine, called goal. Let further a partial-order relation that is contained in the goal denote a set of assumptions in a goal. A set of assumptions should represent the knowledge that we assume to be precise about the goal, it is defined to be a partial-order instead of a preorder by identifying elements of the universe in question that are known to be related symetrically in its goal. By proving the validity of our goal, we mean to show that our assumptions are precise, that is, the set of assumptions equals the goal.

Let us fix a universe A, a goal ≼ on A, and a set of assumptions ≤ in ≼. The result we present now is how to determine the smallest set of pairs not in ≤ that is sufficient to show ≤ = ≼ and how that can be used in prove efforts such as arranging sets in a Hasse diagram.

We write x ρ y for a pair (x, y) contained in ρ, where x ∈ M, y ∈ N, and ρ ⊆ M × N. Our notations are taken from [BS81].

Example 1 (Hasse diagram) Let us fix a running example. Let our universe M = {p, q, r, s, t} be a set of sets. Suppose that the subset relation ⊆ on M is our goal with the known pairs p ⊆ q, q ⊆ s, q ⊆ t, and r ⊆ t, so, our set of assumptions ⊂ is the transitive reflexive closure of the set {(p, q), (q, s), (q, t), (r, t)}.

We want to show that the assumed set inclusions are proper and elements which are not related by ⊆ are incomparable indeed. In fact, we want to prove that

[figure: s; t; q; r; p]

is the most general Hasse diagram for (M, ⊆). Of course, we need to show that q properly contains p, i.e., p ⊈ q, that s and r are incomparable, i.e., r ⊈ s and s ⊈ r, and so on. Naturally, we wish to prove only those lemmas which are absolutely necessary to establish the result under the given assumption.

In order to prove ≤ = ≼, we have to show that any pair (x, y) not in ≤ is also not in ≼. This is easy to see, since ≼ ⊆ ≤ by the above requirement, and we have ≤ ⊆ ≼ by definition.

Let ⊐ = ≤^{c} be called the complete set of lemmas, so x ⊐ y, with x, y ∈ A, is called a lemma.

The complete set of lemmas is the counterpart of our assumptions. It gives us the lemmas that ought to be proven to get the complete picture, i.e., to have a statement about every possible relation between the investigated objects which does not contradict the assumptions. In some sense, the proof relation gives us complete negative knowledge by saying what is not known by assumption.

Example 2 (Hasse diagram—continued) In this example, x ⊐ y translates to x ⊈ y for x, y ∈ M. There are exactly fourteen lemmas in ⊐:

{q ⊈ p, p ⊈ t, s ⊈ q, r ⊈ q, t ⊈ q, s ⊈ t, s ⊈ r,
p ⊈ s, p ⊈ r, q ⊈ r, r ⊈ p, t ⊈ r, t ⊈ s, r ⊈ s}

Fortunately, most lemmas follow from others directly, and we will see which of them.

Now, we observe that some lemmas follow from others directly by using the set of assumtions, e.g., let x_{1} ⊐ y_{1} be established, which translates to x_{1} ⋠ y_{1}, and let also x_{1} ≼ x_{2} and y_{2} ≼ y_{1} by assumption, then x_{2} ⋠ y_{2} immediately follows, since x_{1} ≼ x_{2} ≼ y_{2} ≼ y_{1} would give a contradiction. This observation is expressed in the following definition.

Definition 3 The lemma structure → ⊆ ⊐ × ⊐ on a complete set of lemmas ⊐ is defined by

(x_{1}, y_{1}) → (x_{2}, y_{2}) ⟺ x_{1} ≤ x_{2} and y_{2} ≤ y_{1}

where (x_{1}, y_{1}), (x_{2}, y_{2}) ∈ ⊐.

Proposition 4 A lemma structure → is a partial-order relation.

PROOF. Reflexivity: For any (x, y) in ⊐, we have (x, y) → (x, y) by the reflexivity of ≤. Antisymmetry: Let (x_{1}, y_{1}) → (x_{2}, y_{2}) and (x_{2}, y_{2}) → (x_{1}, y_{1}), then x_{1} ≤ x_{2}, x_{2} ≤ x_{1}, y_{2} ≤ y_{1}, and y_{1} ≤ y_{2}, and also x_{1} = x_{2} and y_{1} = y_{2} since ≤ is antisymmetric, hence, (x_{1}, y_{1}) = (x_{2}, y_{2}). Transitivity: Let (x_{1}, y_{1}) → (x_{3}, y_{3}) and (x_{3}, y_{3}) → (x_{2}, y_{2}), then x_{1} ≤ x_{3}, x_{3} ≤ x_{2}, y_{2} ≤ y_{3}, and y_{3} ≤ y_{1}, and also x_{1} ≤ x_{2} and y_{2} ≤ y_{1} since ≤ is transitive, hence, (x_{1}, y_{1}) → (x_{2}, y_{2}).

Example 5 (Hasse diagram—continued) Reading → as “implies”

(q ⊈ r) → (s ⊈ r)

holds in our example, which follows from the assumption q ⊆ s.

The following theorem shows that the maximal elements in → are necessary and sufficient to prove ≤ = ≼. Let →_{max}= {x ∈ ⊐ | if y → x then x = y, for all y ∈ ⊐} denote the maximal elements in →. It is clear that every nonempty finite partial-order has a nonempty set of maximal elements.

Theorem 6 →_{max} is the smallest set of lemmas to prove ≤ = ≼.

PROOF. (i) We have to show that ⊐ follows from →_{max}. The set →_{max} is not empty if ⊐ is not empty, since → is a partial-order by Proposition 4. So, for every lemma x ⊐ y there is a lemma x′ ⊐ y′ with (p′, q′) ∈→_{max} such that (x′, y′) → (x, y) by the definition of →_{max}. (ii) Every element in →_{max} only follows from itself, which is clear from the definition of →_{max}.

Example 7 (Hasse diagram—continued) The lemma structure of our example is indicated by the following graph, where reflexive and transitive edges are omitted:

[figure: r ⊈ s; q ⊈ p; s ⊈ t; s ⊈ q; p ⊈ r; t ⊈ s; r ⊈ q; q ⊈ r; t ⊈ q; r ⊈ p; s ⊈ p; s ⊈ r; t ⊈ p; t ⊈ r]

One can check that the proposed Hasse diagram on page 3 follows from our set of assumptions and the four lemmas r ⊈ s, q ⊈ p, s ⊈ t, and p ⊈ r.

3 Implementation

The algorithm described in the previous section—take the complement of the set of assumptions and find the maximal elements in the corresponding lemma structure—has been imlpemented as a Haskell program which reads a file containing the describtion of a relation, calculates the transitive reflexive closure, and takes the smallest partial-order relation of that as set of assumptions. A file is generated where these steps are documented and the solution is given. The program can be found at [Now] and it requires the Glasgow Haskell Compiler [GHC] to run.

The following Haskell listing shows the core of our program. It defines a function minlem that takes a list of pairs defining a partial-order relation over some eqtype to a list of pairs of the same type. The argument of minlem represents a set of assumptions, and the result of its evaluation gives the smallest set of pairs that have to be checked to prove the assumption to be precise.

import List
elements :: Eq a => [(a,b)] -> [a]
elements ord = (nub . fst . unzip) ord
complement :: Eq a => [(a,a)] -> [(a,a)]
complement ord = let elems = elements ord
            in  [(x,y) | x <- elems, y <- elems,
                         (x,y) `notElem` ord]
lemma_structure :: Eq a => [(a,a)] -> [(a,a)] -> [((a,a),(a,a))]

lemma_structure ord lems =
  [((x,y),(x',y')) | (x,y) <- lems, (x',y') <- lems,
                     (x,x') `elem` ord, (y',y) `elem` ord]
maxElems :: Eq a => [(a,a)] -> [a] -> [a]
maxElems lemStruct lems =
  let pred x y = if (y,x) `elem` lemStruct then x == y else True
  in  [x | x <- lems, all (pred x) lems]
minlem :: Eq a => [(a,a)] -> [(a,a)]
minlem assume = let lems = complement assume
                in  maxElems (lemma_structure assume lems) lems

References

[BS81] S. Burris and H. P. Sankappanavar. A Course in Universal Algebra. Graduate Texts in Mathematics. Springer-Verlag, 1981.

[FV98] Z. Fülöp and H. Vogler. Syntax-Directed Semantics. Monographs on Theoretical Computer Science. Springer-Verlag, 1998.

[GHC] http://www.haskell.org/ghc/.
[Now] http://www.cs.utu.fi/staff/nowotka/minlem.html.