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:

– The class PREDICATE must inherit BOOLEAN_LATTICE as a ghost parent. This is
necessary because PREDICATE defines the relations “<=” and “=” as ghost
functions. In the BOOLEAN_LATTICE these relations are defined as normal
relations. By inheriting the parent as “ghost” the descendant has the
freedom to define the functions as ghost functions or normal functions.

– The class BOOLEAN_LATTICE has a definition of “<=”. The class PREDICATE
overrides this definition. This has to be indicated in the inheritance
clause. The definition of “<=” from BOOLEAN_LATTICE becomes a proof
obligation within the class PREDICATE. In the previous chapters the
equivalence of “a<=b” and “a=a*b” have been proved.

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.

Advertisements
  1. Leave a comment

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: