Notes on Well-founded sets

 

DEFINITION  (Binary Relation).

 Let S be a set. A binary relation on S is a subset of the cartesian product S x S.

 In other words, a binary relation R on S is a set of pairs of elements of S. Given a relation R, we use the usual prefix notation x R y to denote that the element x of S is in the relation R with the element y of S. We can also say that "x precedes y" according to the relation R, since a binary relation represents a sort of "precedence" between elements of S.   We will often use symbols like <<, pr, etc. to denote a binary relation. Later on we will use the notation  ( S, << )   to stress that the set S is provided with a binary relation <<.


 

DEFINITION ( Descending Sequence ).

A descending sequence in (S, <<) is a sequence s0, s1, s2, s3 ..., finite or infinite, of elements of S such that

....  <<  s3  <<  s2  <<  s1  <<  s0

 

DEFINITION  ( Well-Founded Set ).

A set  (S, <<)  is well-founded    iff    it does not exist any infinite descending sequence of elements of S.


 

DEFINITION  ( Minimal Element ).

Let (S, <<) be a set equipped with a relation.
An element x of S is said to be minimal if there exists no element y in S such that y << x.

 

It can be proved that any well-founded set has at least one minimal element (of course can have also many minimal elements, even an infinite number)

Example 1. Let us consider the set N of natural numbers, and let us consider the following relation << on natural numbers:  n<<m iff  (n and m are odd and n<m) or (n and m are even and n<m).

Is (N,<<) well-founded? You can easily check that it is so. What are its minimal elements? Well, it has two minimal elements: 0 and 1.

 

Pay attention to the difference between the notion of minimal element  (x is minimal in (S,R) if there exists no y such that  yRx ) and the notion of minimum element (x is the minimum in (S,R) if for all y we have that xRy).



In order to be able to use the notion of well-founded sets when defining a recursive function, the following notion is useful.

Definition (Induced precedence relation)

Let f be a function (program) recursively defined. The precedence relation induced by f on its domain is the following:

x<<y     iff    f(y) is defined in terms of f(x)

 

The notion of well-founded set allows us to formally prove the termination of recursive programs. To do that we have first to recognize what is the domain of our program; then we have to identify the induced precedence relation over the elements of the domain.
Then we have to verify that the domain, equipped with such a precedence relation is a well founded set. It is also necessary to be sure that our program is correctly defined on the minimal elements of the domain.

 Remark. Sometimes, in order to be sure of termination, it is easier to consider a larger precedence relation than the induced one.
The precedence relations induced by complex programs tend to be a bit weird. Larger relations (that is relations containing more pairs) sometimes are easier to handle and to be proven well-founded.

 

Consider for instance the Haskell function

even 0 = True
even 1 = False
even n = even (n-2)

Is it correctly defined? yes, since we know that it is true that 0 is even, that 1 is not even and that, otherwise, n is even if and only if n-2 is even.

Does it always terminate?  yes, because it is defined on the domain N of natural numbers, and if we consider (N,<<) as defined in the Example 1 above, we know that this is a well-founded set. Moreover, the well-founded relaion contains the precedence relation induced by the function definition. In fact the recursive call in the body is made on the element n-2, and we can easily see that  n-2 << n. We see also that  the function is correctly defined on the minimal elements of our well-founded set, that is 0 and 1.

 

 Remark. Sometimes, when a recursive program does not terminate, the problem is that the domain is not well-founded with respect to the relation we have in mind when we write the recursive calls in the body.

 

Definition (lexicographic and product relations)


Given two sets with two relations:

(S1, <<1)     and     (S2, <<2)

we can define the following relations on the cartesian product:

1)

((S1 x S2), <<LEX)
where <LEX is the relation of lexicographic precedence defined as follows:

(s1, s2) <<LEX (s'1, s'2)   if and only if   s1 <<1 s'1 or (s1 = s'1 and s2 <<2 s'2)

2)
                                                                                   (S1 x S2), <X),
where <X is the product precedence relation as follows:

(s1, s2) <X (s'1, s'2)   if and only if   s1 <<1 s'1  and s2 <<2 s'2
 

 


You see, when we look for a name in the telephone directory we use a lexicographic precedence relation.

 

It is possible to prove the following easy theorem.

 

Theorem

Let   (S1, <<1)     and     (S2, <<2)  be sets equipped with binary relations.

If  (S1, <<1)     and     (S2, <<2) are well-founded, then also ((S1 x S2), <<LEX) and (S1 x S2), <X) are well-founded.

 

If in a precedence relation we have that a<<b and there is no c such that a<<c<<b, then a is called an immediate predecessor of b.

Sometimes we can describe a precedence relation by means of diagrams in which an element which is an immediate predecessor of another is put below it and it is connected by an edge.