Taking modeling seriously
Lincoln
15 July 2013
This document contains some hands-on exercises for the Alloy
tutorial. Some of these are adapted from other sources (listed
at the bottom of the document).
1 Exercise 1: Hello, world
Launch the Alloy Analyzer.
-
From the Execute menu, select
any of run creata
,
run ecce
,
check deus_creator
, or
check deus_solus_creator
.
-
If the predicate you ran has instances,
or if the assertion you checked has counter-examples,
the Analyzer will show you one. Examine the diagram.
Select the Next icon to ask for another
instance or counter-example.
2 Exercise 2: Signatures and fields
2.1 Who owns the mule?
(From Willis 1997, puzzle P1-1).
This puzzle requires the use of the logical
connectives and, or,
and not (at least, the instructor's
solution uses them and the instructor couldn't find a way to
do without them), but does not require anything more elaborate
by way of logical machinery.
Three farmers who have shared the use of a mule for some time
disagree as to who owns the animal. It is not certain,
however, that the responsibility of ownership is desired.
They have asked Socrates to settle the issue. The three
make the following statements. Each makes one true and one
false statement.
A.
- It is C's mule.
- I can make no claim to it.
B.
- C has no right to it.
- It is A's mule.
C.
- It is my mule.
- B's second statement is false.
Socrates hesitates for scarcely an instant and
determines the owner. To which farmer does the mule belong?
2.2 Bibliographic objects
The
Functional requirements for bibliographic objects (IFLA, 1997;
rev. 2009) defines four types of bibliographic objects: works,
expressions, manifestations, and items, with the following relations
holding between related objects:
-
realizes(Expression, Work). One to many: one
work may be realized by many expressions, but each expression realizes
exactly one work.
-
embodies(Manifestation, Expression). Many to
many: one expression may be embodied by many manifestations, and each
manifestation embodies one or more expressions.
-
exemplifies(Item, Manifestation). One to many:
one manifestation may be exemplified by many item, but each item
exemplifies exactly one mnaifestation.
Write an Alloy model to describe the four types of object
and their formal relations. You may assume either that the four
types of object are disjoint, or that they are not necessarily
disjoint.
Time and interest permitting, write two models (one making
the types disjoint, one not doing so) and compare them.
3 Exercise 3: Sets and set operators
(From Summers 1968, puzzle 5).
Mary's ideal man is tall, dark, and handsome.
She knows four men:
Alec, Bill, Carl, and Dave. Only one of the four men
has all of the characteristics Mary requires.
- Only three of the men are tall, only two are dark, and only one
is handsome.
- Each of the four men has at least one of the required traits.
- Alec and Bill have the same complexion.
- Bill and Carl are the same height.
- Carl and Dave are not both tall.
Which one of the four men satisfies all of Mary's requirements?
4 Exercise 4: sentential logic
(These exercises in sentential logic are adapted from Jeffrey 1967, sec. 3.18).
4.1 Crumm and Moriarty
Assume these to be true:
- Crumm is not guilty.
- Moriarty is guilty if Crumm is.
4.2 Moriarty's escape
Assume these to be true:
- If Moriarty has escaped, then either Holmes has bungled or
Watson is on the job.
- Holmes has not bungled unless Moriarty has escaped.
- Watson is not on the job.
Does this follow?
- Moriarty has escaped if and only if Holmes has bungled.
5 Exercise 5: Quantification
(Adapted from Jeffrey 1967, ch. 6).
5.1 Holmes and Moriarty
Assume these to be true:
- Holmes, if anyone, can trap Moriarty.
- Holmes cannot [trap Moriarty].
Does this follow?
- No one can [trap Moriarty].
5.2 Watson and Moriarty
Given:
- If Watson can trap Moriarty, anyone can.
- Holmes cannot.
5.3 Mortality
Given:
- Everyone is mortal.
- No one is immortal.
5.4 Whom Alma loves
Given:
- Everyone whom Alma loves, loves Alma.
Does this follow?
- If Alma loves everyone, then everyone loves Alma.
5.5 More about Alma
Given:
- Unless Alma loves herself, she loves no one.
[N.B. the conjunction unless has the
same truth function as (inclusive) or.]
Do either of these follow?
- Alma loves Bert if she loves herself.
- Alma loves Bert only if she loves herself.
6 Exercise 6: Relational operators
The exercise below is placed here partly because one natural
assertion to formalize is Leibniz's claim that either all concepts
depend on (and are thus reducible to) some set of primitive concepts,
or else there must be an infinite series of dependencies. Given
a depends_on
relation describing immediate dependencies,
we can generate its transitive closure to get the set of all the
other concepts on which a given concept depends.
6.1 Leibniz on primitive concepts
(From Leibniz 1679). Leibniz writes:
It is the greatest remedy for the mind
if a few thoughts can be found
from which infinite others arise in order,
just as from the assumption of a few numbers, from one to ten,
all the other numbers can be derived in order.
Whatever is thought by us is either conceived through itself,
or involves the concept of another.
Whatever is involved in the concept of another is again
either conceived through itself
or involves the concept of another;
and so on.
So one must either proceed to infinity,
or all thoughts are resolved into
those which are conceived through themselves.
If nothing is conceived through itself,
nothing will be conceived at all. For what is conceived
only through others will be conceived in so far as
those others are conceived, and so on;
so that we may only be said to conceive something
in actuality
when we arrive at those things which are conceived
through themselves.
Can an Alloy model illustrate this argument?
Do the conclusions follow from the premises stated?
Do they require additional premises?
In case of doubt, by “conclusions” I mean here
the sentences
“So one must ... themselves”
and “If nothing is ... at all.”
7 Other exercises
These range in complexity; some of them are easiest
if you can arrange items in a sequence (which we don't
cover until late in the day).
7.1 Russell's Barber
(From Jeffrey 1967, exercises 7.10 and 7.12).
7.1.1 Consistency checking
Is this consistent?
- There is someone who shaves exactly those people who do not
shave themselves.
7.1.2 Inference
Given:
- There is a man in town who shaves all men in town who do not
shave themselves.
Does this follow?
- Some man in town shaves himself.
7.2 The best player
(From Summers 1968, puzzle 1).
Mr. Scott, his sister, his son, and his daughter
are tennis players. The following facts refer to the people
mentioned:
- The best player's twin and the worst player are of opposite sex.
- The best player and the worst player are the same age.
Which one of the four is the best player?
7.3 Murder in the family
(From Summers 1968, puzzle 3).
Murder occurred one evening in the home of a married couple
and their son and daughter. One member of the family murdered
another member, the third member witnessed the crime,
and the fourth member was an accessory after the fact.
- The accessory and the witness were of opposite sex.
- The oldest member and the witness were of opposite sex.
- The youngest member and the victim were of opposite sex.
- The accessory was older than the victim.
- The father was the oldest member.
- The killer was not the youngest member.
Which one of the four — father, mother, son, or daughter
— was the killer?
7.4 Socrates, Plato, Aristotle
(From Jeffrey, exercise 9.3a).
Given
- Socrates taught Plato.
- Socrates had at most one student.
- Aristotle was a student of someone whom Socrates taught.
Does it follow that:
7.5 A week in Arlington
(From Summers 1968, puzzle 11). Do sequences
make this easier to formulate?
In the town of Arlingon the supermarket, the department store,
and the bank are open together on one day each week.
- Each of the three places is open four days a week.
- On Sunday all three places are closed.
- None of the three places is open on three consecutive days.
- On six consecutive days:
the department store was closed on the first day
the supermarket was closed on the second day
the bank was closed on the third day
the supermarket was closed on the fourth day
the department was closed on the fifth day
the bank was closed on the sixth day
On which one of the seven days are all three places in Arlington open?
7.6 The eight-queens problem
(An old programming chestnut).
Place eight queens on a chessboard in such a way
that no queen threatens any other queen.
It may be simplest to define the more
general n-queens problem, and
then write a predicate that holds if the
number of queens is eight.
A Sources
Jeffrey, Richard C.
Formal logic: its scope and limits.
New York:
McGraw-Hill,
1967.
xii + 238 pp.
Leibniz, Gottfried Wilhelm.
‘Of an organon or ars magna of thinking’
(c. 1679),
pp. 1-4 of his
Philosophical writings,
ed.
G. H. R. Parkinson,
tr. Mary Morris and G. H. R. Parkinson.
London:
Dent;
Vermont:
Charles E. Tuttle
1934; rev. ed. 1973;
rpt. 1995.
xxxvi + 267 pp.
Summers, George J.
New puzzles in logical deduction.
New York:
Dover,
1968.
vi + 121 pp.
Willis, Norman D.
False logic puzzles.
New York:
Sterling,
1997.
[96] pp.