Application of Set Theoretic Model of Sequences

P222 Discrete Maths
OOSS Topic 7
Module INM175Discrete Mathematics
Topic 7
Set Theoretic Models
Some Useful Constructions in Set Theory (for the modeler)
Modelling LIST in Set Theory
Sequence (or list) Seq X : N+ X
s: Seq X •dom(s) = [1..#s]

Catenation (of lists) _ ^ _ : ((Seq X)  (Seq X))(Seq X)
i  #s  (s^t) i = s i
i > #s  (s^t) i = t ( i - #s )

Extract (from list) extract: N+  (Seq X )  (Seq X )
i>j  (extract i s) j = s j
i  j  (extract i s) j = s (succ j)

The signature in the last definition is said to be Curried (after the logician Haskell B. Curry).
Instead of taking two arguments and delivering a result,
extract takes one argument and delivers a function that takes the next argument before delivering the final result.
Directed Graphs
A simple directed graph is just a homogeneous relation.
By separately identifying the edges and vertices, we can generalise our model of directed graph (or DG) to the 4-tuple (sequence of four sets),
DG =
where V is the set of edges;
E is the set of vertices;
and in, out: EV
map each edge to the vertices that it goes to and comes from,
respectively.
(Note that this is the just structure that we used in our ‘airline timetable’ example earlier.)
Reachability
Now we can derive from the tuple the relation next, that maps each vertex to those that are ‘one step ahead’, thus
next: VV
next = in ° out-1
and we can use transitive closure to derive the relation reachable,
which maps each vertex to those that can be ‘reached’ from it,
along some ‘path’ of contiguous edges, thus:
reachable : VV
reachable = next+

Directed Acyclic Graphs
Cycles in graphs are paths that lead from a vertex to itself.
A directed acyclic graph (or DAG) is a DG in which,
from every vertex, no path returns to that vertex.
Clearly, a DG is acyclic iff no vertex is reachable from itself, that is,
its reachability relation and the identity relation on its vertices are disjoint
reachable Ç Id(V) = Æ.
The roots of a DAG are those vertices that no edges enter
roots: ÃV
roots = dom(next) - ran(next)
The leaves of a DAG are those that no edges leave
leaves: ÃV
leaves = ran(next) - dom(next)
Forests and Trees
We can also read a DAG backwards, by deriving from its 4-tuple the relation that maps each vertex to its predecessors, thus:
pred : V«V
pred = out ° in-1 = next-1
A DAG is a forest when no vertex has more than one predecessor, i.e.
pred: VV
‘Family trees’ are forests, because the family has more that one ‘ancestor’!
A forest with a single root is called a tree. A DAG is a tree when
#roots = 1
The directory structure in your computer is a tree, at the root of which is the name of a ‘volume’ (such as ‘C:\’ in Windows, or ‘\’ in Unix).
Adjacency and Connectivity
The adjacency relation maps each vertex to those that are ‘one step away’ in either direction. It is the union of next and pred
adj: V«V
adj = next È pred
(think of this as the original graph with the arrowheads removed)

The transitive closure of adjaceny gives the relation that maps each vertex to those that are connected to it by paths of any length in either direction
connected: V«V
connected = adj+

Connected Graphs
connected is an equivalence relation.
(You should check that assertion for yourself!)
So the quotient of the set of vertices by connected will partition the set of vertices into equivalence classes, all the vertices in each of which are connected to each other but not to any vertex in any other set.
This quotient tells us whether the original graph had any ‘islands’: that is, zones which were entirely disconnected from the rest.
A connected graph has no islands, so satisfies the predicate
V/connected = {V}

Subtyping and Inheritance
The definition of directed graph has been extended by adding constraints.
Trees are restricted forests,
which are restricted directed acyclic graphs,
which are restricted directed graphs.
If we call the class of all trees TREE, etc., we have
TREE Ì FOREST Ì DAG Ì DG
and similarly for connected and undirected graphs.
These are examples of subtyping, or inheritance, which you will meet much more of in object-oriented design.
Quick Revision of Set Theory
Some Set Operators
Products and Relations
Cartesian product  (x,y) (XY) (xX) (yY)
Relation  (XY) = (XY)
XY denotes the set of all relations from X to Y
i.e. any relation R of signature XY is a subset of XY.
If a pair (x,y) R, we may write xRy.

Given any relation R: X Y
domain dom dom R = {xX | y:Y • xRy}
range ran cod(R) = {yY | x:X • xRy}
inverse -1 (y,x)R-1 (x,y) R

More Relational Operators
Given any X’ X
image [ _ ] yR[X’]  x:X’ • xRy

Given any relation S: Y Z
composition  (x,z)SR  y:Y •xRy  ySz

Given any ZX
domain restriction  R Z = R (ZY)

Properties of Relations
Functions
Blank Presentation

OOSS Discrete Maths
Topic 8
Module INM175Discrete Mathematics
Topic 8
Algebraic Theories
Natural Numbers Revisited
The operators
zero:  N a nullary or constant operator
and succ: N  N a unary operator
are constructors of N , that is, every value of N may be denoted by a term involving only these operators. So the following axioms hold for N
1. zero Î N
2. "x:N×$y:N×y=succ x
Peano’s Axioms
Now, let us add the following axioms:
3. "x:N×succ x  zero
4. "x,y:N×succ x = succ y ® x=y
5. if, for any property,Q, Q(zero) Ù ("x:N×Q(x) ® Q(succ x),
then "x:N×Q(x).
Axiom 5 is the Principle of Mathematical Induction.
These five predicates are Peano’s axioms [Giuseppe Peano (1858-1932)]
They define certain properties of N, but do not refer to any representation of it (except that it contain a distinguished element called ‘zero’).
Theories and Models
This form of definition is called a theory, whose subject is a sort, in this case, N.
A model of a theory has some set of values, for its sort, and some functions, for its operators, that satisfy its axioms.
The set NAT = {0,1,2, ...} is a model of N.
The term algebra of a theory consists of the language (i.e. the set of strings of symbols) generated by considering the theory’s signature as a grammar.
The term algebra of N is the set {‘zero’, ‘succ zero’, ‘succ succ zero’, ...} where zero is modelled by the string ‘zero’ and
succ by the function that appends the ‘succ‘ to the front of its argument.
The constructors of a theory are the operators (including the constants) that together can generate all the terms.

Theory Extensions
When we define a new binary operator on N
plus: N, N  N
we extend the term algebra with an infinite number of new terms such as
‘plus(zero,zero)’, ‘plus(succ zero,zero)’, ‘succ plus (zero,zero)’,
But some of these terms denote the same value of N, so we must add the following (recursive)
Axioms
plus (zero, n) = n
plus ((succ m), n) = succ (plus (m,n))
Calculation
Plus is defined in terms of itself, but the recursion always terminates.
Let 1=‘succ zero’, 2=‘succ succ zero’, 3=‘succ succ succ zero’
and use the axioms to compute 1+2
plus(succ zero,succ succ zero)
= succ(plus(zero,succ succ zero) by axiom 2
[Axiom 6 is inapplicable here because, by axiom 1, succ zero  zero]
= succ succ succ zero by axiom 1
[Axiom 7 is inapplicable here because, by axiom 1, succ zero  zero]
Since the final expression does not match the left-hand-side of any of our axioms, our computation stops, and the result denotes the value 3.
Quotient Algebra
Conservative Extension
Our extension is conservative because it introduces:

no junk, because every term involving plus is provably equivalent, under the axioms, to one involving only zero and succ, so in every model which satisfies the axioms, the result of adding any two values of the type N must be in N; and

no confusion, because no pair of distinct terms (that is, terms which are not defined to be equivalent under the original axioms) are equated by the extension.
Algebraic Proof Rules
Whenever an abstract data type is extended, the extension must be proved to be conservative.
Testing is not adequate because these are infinite structures.
The proof rules involved are equational reasoning and structural induction.
These were just the rules that we used in our proofs using the Principle of Mathematical Induction.
Multiplication in N
Multiplication (´) in N is an extension of the theory N with plus:
Signature mult: N, N ® N
Axioms "m,n:N×
mult (zero, n) = zero
mult ((succ m), n) = plus (n,mult(m,n))
Note that this refers to plus which was defined earlier.
Conservative extension is transitive.

Exponentiation in N
The exponentiation operator, mn extends N with plus and multiply
Signature exp: N, N ® N
If 0n = 0 and m0 =1 for all m and n,
then 00 = 0 and 00 = 1
so, by equational reasoning, 1 = 0 a clear case of confusion!
By convention, 00 is an illegal operation i.e. exp(zero,zero) is undefined
Axioms m,n:N
exp (zero,succ n) = zero
exp(succ m,zero) = succ zero
exp (succ m,succ n) = mult(succ m,exp(succ m,n))
The Theory BOOL
The simplest theory, TRIV, has just one set in its quotient algebra, i.e. all terms in the theory are equal to each other. It is of no interest!
The Boolean logic that we studied in Topic 2 is a model of the theory whose quotient algebra has exactly two partitions so we call it
Sort BOOL
Signature T: ® BOOL
F: ® BOOL

This has two constants, T and F, which we modelled as true and false, respectively. We assert that these terms are not equal to each other simply by not providing an axiom that equates them.
Extensions to BOOL
We extend BOOL by adding the usual operators:
Signatures not: BOOL ® BOOL
and: BOOL, BOOL ® BOOL
or: BOOL, BOOL ® BOOL
Axioms "x:BOOL×
not T = F
not F = T
and(T,x) = x
and(F,x) = F
or(T,x) = T
or(F,x) = x
Combining N and BOOL
To define operators whose models are relations on the Natural Numbers, we combine the theories N and BOOL and extend them together.
For example, ‘less-than’ (modelled by the relation <) may be defined as a binary function from N to BOOL:
Sorts N, BOOL
Signature less-than: N, N ® BOOL
Axioms "m,n:N×
less-than(zero, zero) = F
less-than(zero, succ n) = T
less-than(succ m, zero) = F
less-that(succ m,succ n) = less-than(m,n)
Blank Presentation

OOS Discrete Maths
Topic 9
Module INM175Discrete Mathematics
Topic 9
Abstract Data Types
The theory COLL of ITEM
Sorts COLL, ITEM
Operators (the constructors of COLL)
nil: COLL
unit: ITEM  COLL
pair: COLL, COLL  COLL
The terms of this theory "look like" binary trees, with a single "root", arbitrary depth, and either singleton terms of the sort ITEM, or "empty" trees at their "leaves".
The sort ITEM is a parameter. We know nothing of its structure.
SOME TERMS OF COLL
The theory TREE of ITEM
Sorts TREE, ITEM
Operators (the constructors of TREE)
empty: TREE
one: ITEM  TREE
join: TREE, TREE  TREE
(So far, this is identical to the theory COLL except in name).
Axioms x:TREE
join(x,empty) = x (empty is the
join(empty,x) = x identity of join)
SOME TERMS OF TREE
CONSERVATIVE EXTENSIONS OF TREE
We may extend this theory by adding such operators as:

left, right: TREE  TREE Note that these are partial.
leaf: TREE  ITEM So is this.
not-empty: TREE  BOOL These are predicates.
eq-tree: TREE, TREE  BOOL This is a relation.
width, depth: TREE  N These are interpretations.

Axioms for is-empty
Axioms "i:ITEM; x,y:TREE
is-empty empty = T
is-empty unit i = F
is-empty join(x,y) = and(is-empty x, is-empty y)

Here, we have ensured that exactly one axiom is applicable to every term of the sort TREE of ITEM by doing a case analysis over all the constructors.
We have also referred to the BOOL operator, or, which we defined earlier.

Axioms for left
Axioms "i:ITEM; x,y:TREE
left join(x,y) = left x , if is-empty y
= left y, if is-empty x
= x, otherwise
left is undefined for all but one constructor, join. We could say left empty = ^ (the undefined value, called bottom)
left unit i = ^
but it is just as accurate simply to omit these equations.
The remaining axiom has three cases. Each is guarded by the predicate that follows the keyword if. Guards use the values (T and F) returned by BOOL operators as truth values. The operator is undefined for any value not covered by the guards.
Otherwise serves the same purpose as else in imperative programming languages. But this ‘pattern-matching’ style of definition used here is characteristic of the declarative programming languages, such as LISP, Prolog, APL and Haskell.
Axioms for width
Axioms "i:ITEM; x,y:TREE
width empty = zero
width unit i = succ zero
width join(x,y) = plus(width x, width y)

The result is in N, so we have operators of N, all of which were defined earlier, in the definitions.
This operator is total, so is defined everywhere.

Review of Extension
All these operators were defined using:
• case analysis, over all the constructors;
• operators defined previously, in this or other theories; and
• recursion, where the right hand side applies the operator to a term that is strictly “smaller” (i.e. represented by a shorter string in the term algebra) than the one on the left.
An extension will be conservative if it follows these principles and introduces no confusion.
eq-tree, the predicate that determines whether two terms of TREE are in the same equivalence class, is crucial to the theory but very hard to define. We ease this problem by defining a normal form for TREEs.
A NORMAL FORM OF TREE
Given the partition of the terms induced by the axioms, we select a representative member of each equivalence class.
If we restrict our attention to terms of TREE which are either empty or non-empty and contain no empty branches, we will have defined a normal form of TREE, that is, a subset of the terms, all of which are distinct, and such that every other term is equivalent, under the axioms, to exactly one term of the subset.
[Of course, we must prove that this is a normal form of TREE, but we will not do that here.]
Each time we identify a normal form, we must define:
a predicate, to detect terms in normal form, and
an operator, to generate the normal form term equivalent to its argument.
Normal Form Predicate for TREE
Signature nf-tree: TREE ® BOOL
Axioms "i:ITEM; x,y:TREE
nf-tree empty = T
nf-tree unit i = T
nf-tree join(x,y) = and(no-empties x,no-empties y)
This uses the further predicate:
Signature no-empties: TREE ® BOOL
Axioms "i:ITEM; x,y:TREE
no-empties empty) = F
no-empties unit i = T
no-empties join(x,y) = and(no-empties x, no-empties y)
Normal Form Operator for TREE
Signature make-nf-tree: TREE ® TREE
Axioms "i:ITEM; x,y:TREE
make-nf-tree empty = empty
make-nf-tree unit i = unit i
make-nf-tree join(x,y) = make-nf-tree x, if is-empty y
= make-nf-tree y, if is-empty x
= join(make-nf-tree x,make-nf-tree y), otherwise

Equivalence Predicate for TREE
Now the problem of defining eq-tree is easily solved
Signature eq-tree: TREE, TREE  BOOL
Axioms "x,y:TREE
eq-tree(x,y) = (make-nf x = make-nf y)

Note that an equals sign (=) on the right hand side of an axiom is always syntactic, that is, it responds True only if its arguments are identical terms.
The predicate eq-tree computes the semantic equivalence between terms that may be non-identical but occupy the same equivalence class.
The theory LIST of ITEM
Sorts LIST, ITEM
Operators null: LIST
single: ITEM  LIST
cat: LIST, LIST  LIST
Equations x: LIST
cat(x, null) = x (null is the
cat(null, x) = x identity of cat)
So far, this is just the theory TREE except in name(s).
We now add the axiom that cat is associative
Axioms x,y,z: LIST
cat(cat(x,y),z) = cat(x,cat(y,z))
SOME TERMS OF LIST
These two terms are in the same equivalence class
(because associativity allows a LIST to be thought of as a "flattened" TREE.
cat(single a, cat(single b, single b))


cat(cat(single a, single b), single b)

But these two are not
cat(single a, cat(single b, single b))


cat(single a, cat(single b, single b))

Extensions of LIST
Signatures
first , tail: LIST ® LIST partial
head , last: LIST ® ITEM partial
reverse: LIST ® LIST total
is-empty, is-single: LIST ® BOOL predicates
length: LIST ® N interpretation
eq-list: LIST, LIST ® BOOL
Again, the equivalence predicate, eq-list, is crucial but hard to define, so we seek a normal form of LIST.
A NORMAL FORM OF LIST
This normal form is defined recursively as follows:
every normal form term is either
identically null or
the cat of a single LIST with a normal form term.
For example, this is the normal form term
representing the LIST [a,b,b,c,a]
An Alernative Theory of LIST
This normal form suggests the following alternative theory of LISTs:
Signatures null: ® LIST
cons: ITEM ® LIST
where the cons operator appends the ITEM to the head of the LIST.
This theory, which needs no axioms, is the basic data type of both LISP and Prolog.
The constructors of the original theory can be defined as conservative extensions of this one, thereby proving that both are theories of the same abstract data type.
The theory of LIST presented earlier is usually called MONOID in the mathematical literature.
It also appears frequently in computing, for example, in the design of compilers.
The theory BAG of ITEM
Sorts BAG, ITEM
Operators empty: BAG
one: ITEM  BAG
merge: BAG, BAG  BAG
Axioms x,y,z: BAG
merge(x, empty) = x (empty is the
merge(empty , x) = x identity of merge)
merge(merge(x,y),z) = merge(x, merge(y,z)) (merge is associative)
So far, this is just the theory LIST except in name(s).
We now add the axiom that merge is commutative
merge(x,y) = merge(y,x)
SOME TERMS OF BAG
merge(one a, merge(one b, one a))

is equivalent to

merge(merge(one a, one a), one b)

but, still

merge(one a, merge(one b, one b))

is not equivalent to

merge(merge(one a, one a), one b)
Extensions of BAG
Signatures is-empty, is-single: BAG ® BOOL
count: ITEM, BAG ® NAT
remove: ITEM, BAG ® BAG
eq-bag: BAG, BAG ® BOOL

remove could have several possible meanings
The expression remove(i,b) might take just one instance of the ITEM i from the BAG b, or it might remove all of them.
And it might be defined only if there is at least one i in b, or alternatively whether or not b has any is in it. Try them all.
The equivalence predicate is again hard to define, so we seek a Normal Form for BAG.
A NORMAL FORM OF BAG
The sequence in which ITEMs are added to BAGs is not significant to their equivalence. So we may pick a particular sequence for our normal form.
But we need some ordering relation on ITEMs. Without being specific, we can denote this relation as  : ITEM, ITEM  ITEM
Then our normal form consists of those terms of BAG that are
identically empty, or
the merge of a singleton BAG (one i for some ITEM i)
with a normal form term, which is itself
either empty or
is a merge whose first argument is
a singleton BAG (one j for some ITEM) where i  j.
Note that the operation make-nf-bag defines a sorting function
and its axioms implement a sorting algorithm.
The theory SET of ITEM
Sorts SET, ITEM
Operators empty: SET
single: ITEM  SET
union: SET, SET  SET
Axioms x,y,z: SET
union(x, empty) = x (empty is the
union(empty , x) = x identity of union)
union(union(x,y),z) = union(x, union(y,z)) (union is associative)
union(x,y) = union(y,x) (union is commutative)
So far, this is just the theory BAG except in name(s).
We now add the axiom that union is idempotent
union(x,x) = x
SOME TERMS OF SET
The SET can be thought of as a BAG with no "duplicates".

union(single a, union(single b, single a))




union(union(single a, single b), single b)

Extensions of SET
These include the set operations that we merely asserted when we started this module. Now we have the chance to define them formally.

Signatures intersection: SET, SET ® SET
cardinality: SET ® NAT
is-empty, is-single: SET ® BOOL
member: ITEM, SET ® BOOL
proper-subset, subset: SET, SET ® BOOL
eq-set: SET, SET ® BOOL
As usual, equivalence is hard to define, so we seek a Normal Form for SET.
A NORMAL FORM OF SET
The number of times that a given ITEM is added to a SET is not significant. So we may pick a particular number (the obvious candidate is 1) for our normal form.
We still need an ordering relation on ITEMs, but this time it must be a strict order, usually denoted by "<", so that duplicates are omitted.

Then our normal form will comprise
empty, and
all those terms of the form union(one i,x), where
either x is empty
or x is union (one j,y) , where
i < j and y is in normal form.
SUMMARY OFAlgebraic Specification
A theory presentation consists of
a signature, which contains
• a set of sorts,
• a set of operators, each taking zero or more arguments and delivering one result from these sorts, where some of these operators are the constructors; and
a (possibly empty) set of axioms,
quantified over variables ranging over the sorts and
defining each operator in terms of each constructor.
The terms of a theory are the sentences in the language defined by the signature, considered as a grammar.
The equations partition the set of terms into equivalence classes.
Terms in different equivalence classes denote distinct values
in all models of the theory.
And next ....
Like LIST, both BAG and SET, can be presented in alternative theories, based on their Normal Forms.
A theory abstracts away from its models, presenting only the properties that all their models must satisfy. But here we see that an abstract data type can have many alternative theories. So how do we describe the properties that a theory must have?

This question lies at the heart of modern mathematics and leads to abstract algebra, topology and category theory, where many of the most important results in computer science have been found.

But that is for another course. This one is over.
Blank Presentation