SourceForge.net LogoThe Eiffel Compiler / Interpreter (tecomp)

doc/papers/proof/predicates as sets

Predicates as sets

Mathematical sets

Sets abound in mathematics. If a mathematician wants to treat a collection of objects which satisfy a certain property as an entity, he defines a set.

Sets are a very powerful tool in specifications. In order to obtain good readability we introduce a set like notation.

Set expressions

The expression

  {1,2,3}
 

is the set of the three numbers "1", "2" and "3". But in general the elements of a set are expressed by a boolean expression. The expression

  {x:NATURAL: x.is_even}
 

is the set of all natural numbers which are even. This is the basic notation for mathematical sets in our programming language.

  {x:T: bexp}    -- set of all x which satisfy the boolean expression `bexp'
 

The variable "x" is a bound variable. Its name is not relevant and can be changed arbitrarily, i.e. we have

  {x:T: bexp} = {y:T: bexp[x:=y]}   -- "y" must not occur free in `bexp'
 
  -- bexp[x:=y]: all free occurrences of `x' within `bexp' substituted by `y'
 

In many cases the type T of the bound variable can be inferred from the context. In these case the expression

  {x: bexp}
 

is sufficient to describe the set.

The notation "{a,b,...}" is just a shorthand.

  -- shorthand
  {a,b,...} = {x:T: x~a or x~b or ...}
 

If we have a set we can ask whether an element belongs to the set

  a in {x:T: bexp}     -- Does `a' belong to the set "{x:T: bexp}"?
 

For this boolean expression the following equivalence is evident

  a in {x:T: bexp}  =  bexp[x:=a]
 
  -- bexp[x:=a]: all free occurrences of `x' within `bexp' substituted by `a'
 

The set of all elements of a certain type is

  {x:T: True}
 

and the empty set is

  {x:T: False}
 

We can build the union ("+") and the intersection ("*") of sets and the complement ("-") of sets with the following notations

  {x:T: e1} + {x:T: e2}  =  {x:T: e1 or e2}    -- set union
 
  {x:T: e1} * {x:T: e2}  =  {x:T: e1 and e2}   -- set intersection
 
  -{x:T: e}              =  {x:T: not e}       -- set complement
 

The relation "<=" is the subset relation with the following notation

  {x:T: e1} <= {x:T: e2}    -- Is the first set contained in the second?
 
  -- The "<=" operator is defined as
  ({x:T: e1} <= {x:T: e2}) = (all(x:T) e1 => e2)
  --                                      ^ boolean implication
  --                       ^ boolean equality
  --         ^ subset relation
 

Two sets are equal if they contain the same elements

  ({x:T: e1} = {x:T: e2}) = (all(x:T) e1 = e2)
  --                                     ^ boolean equality
  --                      ^ boolean equality
  --         ^ set equality
 

Clearly for sets defined with arbitrary boolean expressions the subset operator "<=" and the set equality operator "=" are not decidable in general. Therefore they must be represented by ghost functions.

Predicates: The type of sets

The set expression "{x:T: bexp}" has the type PREDICATE[T]. Since predicates are used frequently there is the shorthand T? for PREDICATE[T].

Basic functions

The type PREDICATE[T] is a builin type with the following basic definitions

  -- module: "predicate"
 
  immutable class
      PREDICATE[G]
  end
 
  feature         -- Basic functions
      in (e:G, p:G?): BOOLEAN
              -- Is the element `e' contained in the set `p'?
          note built_in end
 
      <= (a,b:G?): ghost BOOLEAN
              -- Is `a' a subset of `b'?
          ensure
              Result = all(x:G) x in a => x in b
          end
 
      = (a,b:G?): ghost BOOLEAN
              -- Do the sets `a' and `b' have the same elements?
          ensure
              Result = (a<=b and b<=a)
          end
 
      * (a,b:G?): G?
              -- The intersection of the sets `a' and `b'.
          ensure
              Result = {x: x in a and x in b}
          end
 
      + (a,b:G?): G?
              -- The union of the sets `a' and `b'.
          ensure
              Result = {x: x in a or x in b}
          end
 
 
      - (a:G?): G?
              -- The complement of the set `a'.
          ensure
              Result = {x: not (x in a)}
          end
 
      0: G?
              -- The empty set
          ensure
              Result = {x: False}
          end
 
      1: G?
              -- The universal set
          ensure
              Result = {x: True}
          end
  end
 

Subset and equality relation

The subset relation is reflexive and antisymmetric

  feature
      all(a,b:G?)
          ensure
              reflexive:     a<=a                   -- def "<="
              antisymmetric: a<=b => b<=a => a=b    -- def "<=", "="
          end
          -- Note: - Implication "=>" is right associative
          --       - "p=>q=>r" is equivalent to "p and q => r"
  end
 

The transitivity of the subset relation can be verified with the following detailed proof.

  feature
      transitive:
      all(a,b,c:G?)
          require
              r1: a<=b
              r2: b<=c
          check
              c1: all(x:G)
                  require
                      r3: x in a
                  check
                      c2: x in b    -- r3, r1, def "<="
                  ensure
                      x in c        -- c2, r2, def "<="
                  end
          ensure
              a<=c       --  c1, def "<="
          end
  end
 

The reflexivity, symmetry and transitivity of the equality relation is an immediate consequence of the definition and the corresponding properties of the subset relation.

  feature
      all(a,b,c:G?)
          ensure
              reflexive:    a=a
              symmetric:    a=b => b=a
              transitive:   a=b => b=c => a=c
          end
  end
 

Intersection and union

The intersection of two sets "a*b" is contained in both sets, therefore it has to be a subset of both sets. If we build the intersection of a set "b" with one of its subsets "a" then the intersection must be equal to the subset. The fact that "a<=b" is equivalent to "a=a*b" is evident. Here is a pedantic proof of this fact.

  all(a,b:G?)
      check
          c1: require
                  r1: a<=b
              check
                  c2: all(x) x in a => x in b    -- r1, def "<="
                  c3: all(x)
                          require
                              r2: x in a
                          ensure
                              x in a and x in b  -- r2, c2
                          end
                  c4: all(x)
                          require
                              r3: x in a and x in b
                          check
                          ensure
                              x in a     -- r3
                          end
              ensure
                  a=a*b                         -- c3, c4, def "="
              end
 
          c5: require
                   r4: a=a*b
              check
                   c6: all(x) x in a => x in a*b     -- r4, def "="
                   c7: all(x) x in a => x in b
                       require
                           r5: x in a
                       check
                           c8: x in a*b              -- r5, c6
                           c9: x in a and x in b     -- c8, def "*"
                       ensure
                           x in b                    -- c9
                       end
              ensure
                   a<=b
              end
      ensure
          a<=b = (a=a*b)    -- c1, c5
      end
 

Note that this proof just requires the expansion of function definitions and the application of some very simple laws of logic. Therefore the proof engine can do this proof automatically.

With a similar technique it can be shown that the commutative, associative and absorption laws for "*" and "+" are valid. The reader is encouraged to do the detailed proofs. Here just the assertions are stated with a hint on how to construct the proof.

  all(a,b:G?)
      ensure
          com_1:    a*b = b*a             -- def "=", "*"
          com_2:    a+b = b+a             -- def "=", "+"
          assoc_1:  a*b*c = a*(b*c)       -- def "=", "*"
          assoc_2:  a+b+c = a+(b+c)       -- def "=", "+"
          absorb_1: a = a*(a+b)           -- def "=", "*", "+"
          absorb_2: a = a+(a*b)           -- def "=", "*", "+"
          dist_1:   a*(b+c) = a*b+a*c     -- def "=", "*", "+"
          dist_2:   a+(b*c) = (a+b)*(a+c) -- def "=", "*", "+"
      end
 

The empty and the universal set

The empty set is the neutral element of set union and the universal set is the neutral element for set intersection. The intersection of a set with its complement yields the empty set and the union of a set with its complement yields the universal set. This is expressed in the following assertions:

  all(a:G?)
      ensure
          -- proof: expansion of function definitions and elementary laws
          --        of logic
          neutral_0: a+0 = a
          neutral_1: a*1 = a
          compl_0:   a*(-a) = 0
          compl_1:   a+(-a) = 1
      end
 

Predicates are boolean lattices

In the last chapters some elementary laws have been shown which are satisfied by predicates. Exactly these laws are the axioms of a boolean lattice (see article about boolean lattices). From this we can conclude that predicates are boolean lattices, i.e. the class PREDICATE can inherit from BOOLEAN_LATTICE and inherit all the additional properties of a boolean lattice (e.g. order reversal, de Morgan's laws, double negation).

  immutable class
      PREDICATE
  inherit
      ghost BOOLEAN_LATTICE
          redefine
              <=
          end
  end
 

Two remarks are important:

Set of sets

We can build set of sets i.e. expressions of type T??.

Some examples

The set "ss1" defined as

  ss1 = {s:NATURAL?: all(n,m:NATURAL) n in s => m in s => n+m in s}
 

describes the set of all set of natural numbers which are closed with respect to addition. Some examples of sets which belong to the specified set of sets:

  s0 = {}
  s1 = {0,2,4,...}              -- Warning: Ellipsis ... is not part of the
  s2 = {0,3,6,...}              --          programming language
  s3 = {0,2,3,4,6,8,9,10,12,14,15,...}
  s4 = {2,3,4,6,8,9,10,12,14,15,...}
  s5 = {2,3,4,6,8,9,10,11,12,14,15,...}  -- s4 plus multiples of "11"
  ...
  sn = {0,1,2,3,...}
 
  s0 in ss1, s1 in ss1, ...
 

If we have a set of sets like "ss1" we can ask the questions "What is the intersection of all sets of "ss1?". Note that "ss1" contains an infinite number of sets, therefore such a function cannot be obtained by combining the intersection operator "*". From the above definition it is clear that the empty set is the intersection of all sets of "ss1".

In order to make the question a little bit more interesting we construct another set of sets

  ss2 = {s:NATURAL?: 2 in s and 3 in s}
 

and ask the question "What is the intersection of all sets contained in "ss1*ss2 (i.e. the set of sets which satisfy both conditions)?". The set "ss1*ss2" has the two members "s3" and "s4" and a lot of supersets of these two sets. The intersection of all these sets is "s4".

From this example one might conclude that the intersection of a set of sets is always a member of the set of sets. But this is not true. For a simple counterexample consider the set of sets

  ss3 = {s:NATURAL?: 2 in s or 3 in s}
 

and build the intersection of all sets in "ss1*ss3". The set "ss1*ss3" has the following members

  {0,2,4,...}
  {2,4,6,...}
  {0,3,6,...}
  {3,6,9,...}
  -- and many supersets of these sets
 

The intersection of all these sets is the empty set which is not contained in "ss1*ss3" because it fails the specification to contain either "2" or "3".

Infimum and supremum

We can define a function "infimum" to return the intersection of a set of sets and a function "supremum" to return the union of a set of sets.

  feature
      infimum(pp:G??): ghost G?
              -- The intersection of all sets contained
              -- in the set of sets `pp'.
          ensure
              Result = {x: all(p) p in pp => x in p}
          end
 
      supremum(pp:G??): ghost G?
              -- The union of all sets contained
              -- in the set of sets `pp'.
          ensure
              Result = {x: some(p) p in pp and x in p}
          end
  end
 

The set "pp.infimum" contains only the elements which are contained in all sets in "pp", i.e. "pp.infimum" is the intersection of all sets in "pp". The set "pp.supremum" contains only elements which are contained in at least one set of "pp", i.e. "pp.supremum" is the union of all sets in "pp".

But is "pp.infimum" really an infimum and "pp.supremum" supremum? This question is nontrivial because the notions "infimum" and "supremum" are defined independently of "intersection" and "union".

Let us recall the definition of an infimum. The infimum of a set "pp" (here set of sets) is the maximum of the lower set of "pp". The lower set of "pp" is the set of all sets which are subsets of all sets in "pp"

  pp.low_set = {p: all(q) q in pp => p<=q}
 

In order to prove that "pp.infimum" is an infimum we have to prove

  all(pp:G??)
      ensure
          contained: all(p) p in pp => pp.infimum<=p
          maximum:   all(q) (all(p) p in pp => q<=p) => q<=pp.infimum
      end
 

A detailed proof of "contained":

  contained:
  all(pp:G??, p:G?)
      require
          r1: p in pp
      check
          c1: all(x:G?)
              require
                  r2: all(r) r in pp => x in r
              ensure
                  x in p    -- r1, r2
              end
          c2: {x: all(r) r in pp => x in r} <= p  -- def "<=", c1
      ensure
          pp.infimum<=p   -- c2, def "infimum"
      end
 

A detailed proof of "maximum":

  all(pp:G??, q:G?)
      require
          r1: all(p) p in pp => q<=p
      check
          c1: all(x:G, r:G?)
              require
                  r2: x in q
                  r3: r in pp
              check
                  c2: all(p) p in pp => x in p    -- r2, r1
              ensure
                  x in r                          -- r3, c2
              end
          c3: q <= {x: all(r) r in pp => x in r}  -- c1
      ensure
          q<=pp.infimum    -- c3, def "infimum"
      end
 

The proof that "pp.supremum" is the minimum of "pp.up_set" is a similar excercise.

The infimum of the empty set is the universal set and the supremum of the empty set is the empty set. I.e. we have

  {p:G?: False}.infimum   = 1
  {p:G?: False}.supremum  = 0
 

These claims are proved by simple expansion of the definitions of "infimum" and supremum" and elementary laws of logic.

Predicates as complete lattices

A complete lattice is a lattice where each set of elements has an infimum and a supremum. In the previous chapter we have defined the two functions "infimum" and "supremum" and have shown that the return value of these functions satisfies the specification of an "infimum" and a "supremum" respectively. Therefore the class PREDICATE can inherit not only from the class BOOLEAN_LATTICE but also from the class "COMPLETE_LATTICE" because it satisfies the axioms of both. I.e. we can define the class PREDICATE as

  immutable class
      PREDICATE[G]
  inherit
      ghost BOOLEAN_LATTICE
          redefine
              <=
          end
      ghost COMPLETE_LATTICE
          redefine
              <=
              0
              1
          end
  end
 

The class PREDICATE overrides the definitions of "<=", "0" and "1" of its parent COMPLETE_LATTICE because it has its own definition of these functions. But we have demostrated that the class PREDICATE satisfies the definitions of these inherited functions.

With this declaration all assertions of the module "boolean_lattice" and "complete_lattice" are inherited as valid assertions.

Emacs suffix

 Local Variables:
 mode: outline
 coding: iso-latin-1
 outline-regexp: "=\\(=\\)*"
 End:
Table of contents

- Mathematical sets

- Set expressions

- Predicates: The type of sets

- Basic functions

- Subset and equality relation

- Intersection and union

- The empty and the universal set

- Predicates are boolean lattices

- Set of sets

- Some examples

- Infimum and supremum

- Predicates as complete lattices

- Emacs suffix


ip-location