Transcript pTopic8

Module INM175
Discrete Mathematics
Topic 8
Algebraic Theories
INM175 Topic 8
1
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
INM175 Topic 8
2
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’).
INM175 Topic 8
3
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.
INM175 Topic 8
4
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))
INM175 Topic 8
5
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.
INM175 Topic 8
6
Quotient Algebra
The set of all terms
partitioned by the
axioms
zero
plus(zero,zero)
plus(zero, plus(zero,zero))
succ(zero)
and so on ...
plus(zero, succ(zero))
plus(succ(zero),zero))
and so on ...
and so on ...
Every term in the original term algebra is in
one and only one equivalence class.
INM175 Topic 8
7
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.
INM175 Topic 8
8
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.
INM175 Topic 8
9
Multiplication in N
Multiplication () in N is an extension of the theory N with plus:
Signature
Axioms
mult: N, N  N
"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.
INM175 Topic 8
10
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
INM175 Topic 8
"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))
11
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
Signature
BOOL
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.
INM175 Topic 8
12
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
INM175 Topic 8
13
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)
INM175 Topic 8
14