Transcript Document

Predicates and quantifiers
Chapter 8
Formal Specification using Z
1
Predicates
• A predicate is a logical statement that depends on a value
or values. When a predicate is applied to a particular value
it becomes a proposition. For example:
• prime(x)
• depends on some numeric value of x
• prime(7)
• is a true proposition; the only devisors of 7 are 1 and 7.
• Prime(6) is a false proposition; 6 can be divided by 2,3.
• A predicate can be viewed as a propositional function, that
for some set of arguments returns to either true or false
2
Quantifiers
•
•
•
•
•
Consider the following statements:
All cats have tails.
Some people like cake.
Everyone gets a break once in a while.
All these statements indicate how frequently
certain things are true. In predicate calculus
we use quantifiers in this context.
3
Universal Quantifier
• The Universal Quantifier is written :
A
and is pronounced ‘for all’. It is often used in
the form :
A declaration | constraint predicate
Which states the for the declarations given,
restricted to certain values (the constraint),
the predicate holds.
4
Universal Quantifier
• The constraint may be omitted.
• The declaration introduces a typical element
that is then optionally constrained or
restricted in some some way: For example:
Constraint
A i: N | i < 10
Predicate
i2 < 100
Separators
Which states that for all natural numbers less
than 10 their square is less that 100 .
5
Universal Quantifier
• A universal quantifier can be viewed as a
chain of conjunctions. So:
A i: N | i < 10
i2 < 100
is equivalent to:
02 < 100 L 12 < 100 L . . L 92 <
100
If the set of values over which the variable is
universally quantified is empty, then the
quantification
is defined as true.

A i: N | 0 i < 0
i2 < 100
6
Existential Quantifier
• The Existential Quantifier is written :
E
and is pronounced ‘there exists’. It is often used
in the form :
E declaration | constraint predicate
The declaration introduces a typical element
that is then optionally constrained or
restricted in some way: For example:
E i: N | i < 10
i2 < 100
7
Existential Quantifier
• There may be more than one value of i for
which this is true, in the previous example
there are ten values, 0 to 9, that satisfy the
predicate. Another example:
Even(x)  E k: Z
k*2=x
The existential quantifier can be
considered as a chain of disjunctions
(ors). If the set of values over which the
variable is existentially quantified is empty,
then the quantification is defined as false.
E i: N | 0 i < 0
i2
< 100
8
Unique Quantifier
• The unique quantifier is similar to the
existential quantifier except that it states that
there exists only one value for which the
predicate is true. It is written as:
E1
• An example:
E1i: N | i < 1 0
i2 < 100 L i2 > 80
9
Unique Quantifier
• The previous unique quantifier example is
equivalent to saying that the predicate holds for
i, but there is no value j for which it holds This
is written as:
E1i: N | i < 1 0
i2 < 100 L i2 > 80

E1i: N | i < 1 0 i2 < 100 L i2 > 80
L ¬(Ej: N | j < 1 0  i j j2 < 100 L j2 > 80)
10
Counting Quantifier
• Some notations use a counting quantifier that
counts for how many values of a variable the
predicate holds. In Z this is not needed, we use
set comprehension instead.
11
Set Comprehension
• Set Comprehension:
• It is possible to give the value of a set by
giving a condition (a predicate) which must
hold true for every member of the set. The
general form is:
• {declaration | constraint expression}
• SetA ::= {x:Z | Even(x) x*x}
12
Set Comprehension
• {declaration | constraint expression}
• The declaration is for a typical element and
it gives the element’s name and type.
• The constraint restricts the possible values
of the typical element. It is a logical
expression which must be true for that value
of the typical element to be included.
• The expression indicates the value to be
held in the set
13
Set Comprehension
• SetA ::= {x:Z | Even(x) x*x}
• The above defines a set of type integer. The
value of x is constrained to be even. Each
element will be the square of an even
integer.
• SetB ::= {x:Z | Even(x) x}
• The above defines a set of type integer. The
value of x is constrained to be even. Each
element will be an even integer.
14
Ranges of numbers
• We have already introduced m..n. This is shorthand for
• {i:Z | m i L n i
i}
15
Relationship between Logic and
Set Theory
• There is a direct relationship between some
of the operations of logic and operations on
sets:
• [X] any set S,T: PX
• S  T == {x:X | x S  x  T x}
• S  T == {x:X | x S  x  T x}
• S \ T == {x:X | x S  x  T x}
16
Summary of Quantifier
A x:T P
for all x of type T, P is true.
E x:T P
there exists an x of type T, such that P is true.
E1 x :T P
there exists a unique x of type T, such that P
is true.
17
Summary of Quantifier
{D | P t}
The set of t’s declared by D where P is true.
18
Mixing Quantifiers
• What is the precedence or associativity
used. Is forAll(x),forAll(y) equivalent to
forAll(y),forAll(x)?
• Assuming standard notation, they are read
left to right; two universal quantifiers
following one another commute (just like
multiplication a*b=b*a).
19
Mixing Quantifiers
• Likewise, if you have two existential
quantifiers, they commute, because
• Exists(x),Exists(y), p(x,y)
• is true if and only if
• Exists(y),Exists(x), p(x,y)
• is true.
20
Mixing Quantifiers
• But if you have mixed universal and existential
quantifiers, you have to be careful. If you write
A(x), E(y), p(x,y)
• that means that for each x, there exists a y, which
may depend on x, for which p(x,y) is true.
• But if you write
E(y), A(x), p(x,y)
• you are saying that there is a y which works for
any given x (including y=x), that make p(x,y) true.
21
Mixing Quantifiers
Let the propositional function g(x,y) be
defined as:
g(x,y) = x< y
Write each of the following propositions in
words and state whether they are true or
false.
1)xy ( g ( x , y ))
2) yx ( g ( x , y ))
22
Mixing Quantifiers
Let the propositional function g(x,y) be defined as:
g(x,y) = x< y
Write each of the following propositions in words and state
whether they are true or false.
1) xy ( g ( x , y ))
2) yx ( g ( x , y ))
1)
For all natural numbers (x) there exists a y such that x< y. The
statement is true if we make y = x + 1. We only require the
existence of one y to make the statement true.
2)
There exists a natural number (y) such that for all x, x<y. The
statement is false when y=x. We only have to find one y that
make the statement false.
23
Exercises
Let O(x,y) be the predicate (or propositional
function) “x is older than y”. The domain of
discourse consists of three people Garry,
who is 30; Ellen who is 20; and Martin who
is 35. Write each of the following
propositions in words and state whether
they are true or false.
24
Exercises
Let O(x,y) be the propositional function “x is older than y”. The domain of
discourse consists of three people Garry, who is 30; Ellen who is 20; and Martin
who is 35. Write each of the following propositions in words and state whether
they are true or false.
xyO( x, y)
xyO( x, y )
xyO ( x, y )
xyO( x, y)
25
Exercises
Let O(x,y) be the propositional function “x is older than y”. The domain of discourse
consists of three people Garry, who is 30; Ellen who is 20; and Martin who is 35. Write
each of the following propositions in words and state whether they are true or false.
xyO ( x, y ) Everyone is older than everyone, False
xyO ( x, y ) Everyone is older than someone, False
xyO( x, y ) Someone is older than everyone, False
xyO( x, y ) Someone is older than someone else, True
26
Exercise
Determine whether each sentence 1-5 is a proposition. If it is a proposition write its
negation.
1. Waiter, will you serve the soup?
2. Write a program to calculate the distance from A to B
3. Four is greater than three.
4. The cat is clever.
5. Today is Christmas Day.
.
27
Exercise
Determine whether each sentence 1-5 is a proposition. If it is a proposition write its
negation.
1. Waiter, will you serve the soup? Answer No
2. Write a program to calculate the distance from A to B Answer No
3. Four is greater than three. Answer Yes. Four is not greater than three.
4. The cat is clever. Answer Yes. The cat is not clever
5. Today is Christmas Day. Answer Yes. Today is not Christmas
The notion of a proposition here is intuitive and id not defined precisely. Roughly
speaking, a proposition is a fact, which is either true or false. So sentences stating facts
are considered to be propositions while commands or questions are not considered
propositions.
28