Set Theory and Relations in Discrete Mathematics
do
midterm
A X B ≡ {(a, b) | a ∈ A, b ∈ B}
Pow(S) ≡ {e | e ⊆ S} Power set has 2^n Elements. A binary relation is an element of A x B.
The Squares of integers { x : N | (exists y : Z | x = y*y)}Set ha s at least one element exists x | x in S. Set has no elements not (exists x | x in S) also S = {} Set Has exactly one element exists x : S | (forall y : S| y = x) also a | S = {a} Set has at least two elements Exists x : S | (exists y : S | y != x ) – Set has exactly two elements exists x : S | (exists y : S | y != x /\ (forall z : S | z = x \/ z = y)) also Exists x | (exists y | x != y /\ S = {x,y}
Injective(1to1)
means that every member of
“A” has its own unique matching member in “B”.
Surjective means that every “B” has at least
One matching “A” (maybe more than one).
Function-ness
I and D onto-ness
U1-1ness
I and D.-
Composition (;)
Preserves function-ness, onto-ness, 1-1-ness
– Closure (+)
Does not preserve function-ness Preserves onto-ness Does not preserve 1-1-ness
– Transpose (~) Does not preserve
Function-ness Does not preserve
Onto-ness Preserves 1-1-ness
Function Can be one to one and many to one
COMPOSITION Map domain of first to image of second – Given s: A x B and r: B x C then s;r : A x C s;r ≡ {(a,c) | (a,b) ∈ s and (b,c) ∈ r} • For example – s == {(red,1), (blue,2)} – r == {(1,2), (2,4), (3,6)} – s;r = {(red,2), (blue,4)}
TRANSPOSE written ~r, is what You get when you reverse all the pairs in r. ~r≡ {(b,a) | (a,b) ∈ r} . ChildOf == ~Parent – DescendantOf == (~Parent)+
CLOSURE:
For example –
GrandParent == Parent;Parent – Ancestor == Parent+ r+ ≡ r ∪
(r;r) ∪ (r;r;r) ∪ …
Predicates
are used to
Apply constraints. A relation is
A structure that relates atoms. It is a set of tuples, each tuple being a
Sequence of atoms.
Signatures are classes of entitieFis.
elds
Define relations between signatures. Extends means subset.
• Extensions of the same signature are Mutually disjoint, as are top-level signatures
• All extensions of an abstract
Signature
A form a partition of A.
Set
Any number – some:
One or more – lone :
Zero or one – one :
Exactly one
Sig Book { addr: Name some -> lone Addr }
sig
S {f: T -> one V} – For each element s of S, over the triples that start with
S: f maps each T-element to exactly one V-element .
none, univ and ident
Are 3 predefined sets in Alloy.
.
T1.T2 is not defined if t1 and t2 are both Unary tuples
(p.Q).R and p.(q.R) are not always equivalent ? Because q may be unary.
^r = r + r.R + r.R.R + … Transitive closure
Matt.^children // Mac’s descendants – matt.^(~children) // Mac’s ancestors
*r = ^r + iden REFLECTIVE TRANSITIVE CLOSURE
– S <: r contains Tuples of r starting with an element in s – r :> s contains tuples of r Ending with an element in s
– P ++ q = p – (domain(q)
“No person can have more than one father and Mother ”
all p: Person | (lone (children.P & Man)) and
(lone (children.P & Woman)) $$$ “A person P’s siblings are those people,
Other than P, with the same parents as P”
All p: Person | p.Siblings = {q: Person | p.Parents = q.Parents} – p $$$
“Every married man (woman) has a wife (husband)“ all p:Married |(p in Man => p.
spouse in
Woman) and (p in Woman => p.Spouse in Man)
Second: all p: Married |let q = p.Spouse |(p in Man => q in Woman)
And (p in Woman => q in Man) $$$ “A spouse can’t be a sibling “ no p:
Married | p.Spouse in p.Siblings $$$ A
Person can't be married to a blood relative no p: Married |some (p.*parents
& (p.Spouse).*parents)} $$$ At
Most one father and mother fact
LoneParents {all p: Person | lone (p.Parents & Man) and lone (p.Parents
& Woman)}$$$ No person has a parent that is also a sibling assert a1
{ all p: Person | no p.Parents & p.Siblings }$$$A person’s siblings are
His/her siblings’ siblings WRONG assert a2 { all p: Person | p.Siblings =
P.Siblings.Siblings }$$$No person shares a common ancestor with his/her
Spouse (i.E., spouse isn’t related by blood)
assert a3 { no p: Married | some
(p.^parents & p.Spouse.^parents) } $$$ Two persons are blood rela>ves
Iff they have a common ancestor pred
BloodRelated [p: Person, q: Person] {
Some (p.*parents & q.*parents) } – A person can't be married to a blood
Rela>ve no p: Married | BloodRelated[p, p.Spouse]$$$ Func>ons are
Good for: – set expressions you want to reuse in different contexts Predicates
Are good for: – formulas you want to reuse in different context.
-
--------------- Signatures ----------------
abstract sig Person {
children: set Person,
likes: set Person,
loves: set Person,
spouse: lone Person
}
sig Man, Woman extends Person {}
one sig John extends Man {}
one sig Mary ex
tends Woman {}
---
-------------
Functions
—————
— Define the parents relation as an auxiliary
one
fu
n parents [] : Person -> Person { ~children }
fun wife [p: Person] : Woman
{
p.Spouse & Woman
}
fun husband [p: Person] : Man {
{ m : Man | wife[m] = p }
}
pred isMarried [p: Person] {
some p.Spouse
}
—————- Facts —————-
fact
{
a
ll p:Person | p !In p.Spouse
spouse = ~spouse
}
fact {
— (a) John likes Mary but she does not like him.
Mary in John.Likes and not (John in Mary.Likes)
— (b) Only one person l
ikes John.
one lik
es.John
— (c) Everybody loves somebody
.
all p
: Person | some p.Loves
— (d) Married people love their spouses.
all p: Person | isMarried[p] => p.Spouse in p.Loves
— (e) There is no one that everybody likes.
no p: Person | all q: Person | p in q.Likes
— (f) Mary likes whomever John likes.
John.Likes in Mary.Likes
— (g) Everybody who has children likes at least one of them.
all p: Person | some p.Children => some (p.Likes & p.Children)
— (h) No two men have the same wife
all p: Man | all q: Man – p | wife[p] != wife[q]
— (i) Not everybody has sons.
some p: Person | no (p.Children & Man)
— (j) John has daughters.
#(John.Children & Woman) > 1
— (k) John only has daughters.
all p: John.Children | p in Woman
— (l) There is a man who everybody else dislikes.
some p: Man | likes.P in p
— (m) No one’s parents have the same sex.
all q: Person | all p1 : q.Parents | all p2: q.Parents – p1 |
p1 in Man <=> p2 in Woman
— (n) You must like somebody to love them
.
all
p,q: Person | q in p.Loves => q in p.Likes
}
run {} for 5
assert B5a {
— Everybody has a mother.
all p: Person | some (p.Parents & Woman)
}
assert B5b {
— John does not like himself.
John !In John.Like
s
}
a
ssert B5c {
— Mary likes herself.
Mary in Mary.Likes
}
assert B5d {
— A woman’s spouse is a man.
all m: Woman | m.Spouse in Man
}
assert B5e
{
— Y
ou cannot have more than two (biological) parents.
all p: Person | #p.Parents <= 2
}