Captain's Log: Logical Foundations of Programming, Spring 2008
-
1: January 18 (Friday)
-
Go through course syllabus.
A brief motivation for why to study this course,
with an example (square root) illustrating that
for the specification of software,
First Order Logic (FOL) is very helpful,
as is the notion of logical consequence.
Introduce "Tarski's World", using software package.
Before next time: read the introduction of LPL (the text book),
start playing with the software,
and preferably start reading a bit of Chap 1.
-
January 21 (Monday)
-
University Holiday (Martin Luther King)
-
2: January 23 (Wednesday)
-
Homework 1 out.
The "submit" software was demonstrated.
We covered Chapter 1 of textbook.
A number of worlds presented,
together with corresponding
variants of FOL (to be used as running examples throughout course).
Important concepts:
individual constants (names), function symbols (with arity),
predicates (with arity).
Terms are built from constants and function symbols (can be nested);
an atomic sentence is a predicate applied to one or more terms.
-
3: January 25 (Friday)
-
Using
these slides,
we covered Sections 2.1 and 2.5:
an argument has a number of premises and one conclusion,
and we distinguish between valid (some of which are also sound)
and invalid arguments;
counterexamples are used to
demonstrate that a given argument is invalid (that is, the conclusion is
"non-sequitur").
Do Exercises 2.4, 2.3, 2.8, 2.14, 2.22.
-
4: January 28 (Monday)
-
Using
these slides,
we covered Sections 2.2-2.4, giving
examples of how to derive a conclusion from a set of premises,
thereby demonstrating that the given argument is valid.
For formal proofs, we use the deductive system F,
implemented as the software Fitch (tuned for Tarski's world);
we mention the
Elimination and the Introduction rule for
the identity predicate.
Demonstrate "Fitch",
using Exercises 2.20 (part of HW1) and 2.17.
-
5: January 30 (Wednesday)
-
Homework 1 in. Homework 2 out.
Using
these slides (except 17--20),
we cover Chapter 3:
Negation, Conjunction, Disjunction.
Compare "\/" to "exclusive or".
Ambiguities in FOL (and in English), and how to resolve them.
Do Exercises 3.28 & 3.15.
-
6: February 1 (Friday)
-
Start on Chapter 4, stating
DeMorgan's laws which can be verified using truth tables,
and also some other (tautological) equivalences:
commutativity, associativity, distributivity, etc.
Using DeMorgan, and double negation, a sentence can be converted
to Negation Normal Form (NNF).
Do Exercises 4.31(7) and 4.34.
-
7: February 4 (Monday)
-
Continue Chapter 4.
The notion of a tautology.
Using that \/ distributes over /\,
a sentence can be converted into
Conjunctive Normal Form (CNF),
convenient for
checking whether a tautology.
Dually, we have Disjunctive Normal Form (DNF).
Do Exercises 4.17 and 4.41.
-
8: February 6 (Wednesday)
-
Finish Chapter 4.
We introduce the notions of logical equivalence and TW-equivalence,
forming a hierarchy (similar to Figure 4.1, p.102):
for two sentences to be TW-equivalent they
must be equivalent in Tarski's world;
to be logically equivalent they must be equivalent in
all possible worlds;
to be tautologically equivalent they must be equivalent
for all combinations of truth values (thereby in all possible worlds, and even
some impossible worlds!)
Similarly, we have a hierarchy of
"necessities" (Figure 4.1),
illustrated by Exercise 4.8,
and a hierarchy of "consequences"
which is reflected in the Fitch rules Taut Con, FO Con, Ana Con.
Graded Homework 1 back.
Last day for 100% refund for a course with 78 or more calendar days
(10 or more weeks in length).
-
9: February 8 (Friday)
-
Homework 2 in. Homework 3 out.
Cover Chapter 5, introducing
two crucial proof principles:
proof by cases; proof by contradiction (indirect proof).
Do Exercises 5.1-5.7.
-
10: February 11 (Monday)
-
Cover Sections 6.1-6.3,
presenting various elimination and introduction rules.
Disjunction elimination corresponds to
"proof by cases" (an example of which we see in Exercise 6.5);
negation introduction corresponds to
"proof by contradiction".
-
11: February 13 (Wednesday)
-
Go through model solutions for Homework 2.
Continue Chapter 6,
using the rules given to construct proofs
for 3 of the 4 arguments which
constitute DeMorgan's laws.
Do Exercise 6.19, proving
a general pattern which was used twice in Exercise 4.27.
Do Exercise 6.33, proving the law of Excluded Middle.
Last day for 50% refund for a course with 78 or more calendar days
(10 or more weeks in length).
-
12: February 15 (Friday)
-
Homework 3 in. Homework 4 out. Graded Homework 2 back.
Work through Exercises
6.6 & 6.13 & 6.14 from Homework 3.
Finish Chapter 6, with more examples of how to construct
proofs: the last (and most difficult)
of the 4 arguments constituting DeMorgan's laws,
and Exercise 6.28.
Reminder: never reuse sentences from a subproof which has ended
(Fitch actually prevents that).
-
13: February 18 (Monday)
-
Cover Section 7.1, introducing a new connective:
"->" (which might be pronounced "implies").
Do Exercise 7.15(2,6,12);
touch on Exercises 7.1, 7.2, 7.7, 7.21.
Motivated by the examples in Exercise 8.1,
we show (cf. Sections 8.1 and 8.2) how to reason about ->
as formalized by Elimination and Introduction rules;
those are applied in Exercises 8.19 & 8.24,
and also to establish the principle of contraposition (p.199).
-
14: February 20 (Wednesday)
-
Continue reasoning about ->,
doing Exercises 7.6 and 8.35 (8.7).
Cover Section 7.2, introducing one more connective:
"<->" (to be pronounced "if and only if",
abbreviated "iff"); we touched upon Exercises 7.3 & 7.4.
Present Elimination and Introduction rules for
<-> (cf. Sections 8.1 and 8.2);
we did Exercise 8.27.
This Thursday (February 21) is
last day to drop a course without a W being recorded for a course
with 98 calendar days (14 or more weeks in length).
-
15: February 22 (Friday)
-
Homework 4 in. Homework 5 out. Graded Homework 3 back.
Wrap up the treatment of <->, in particular
discussing how to prove a chain of biconditionals
(cf. Exercises 7.8 and 8.15).
Introduce the notion of truth-functional completeness
(Section 7.4),
further illustrated by Exercise
7.30.
-
16: February 25 (Monday)
-
Motivated by Exercise 7.32,
we state that
the formal system F is sound,
and also complete
(Section 8.3, omitting the proofs of the theorems).
This concludes Part I of the textbook.
Go through selected exercises from Homework 4:
6.20, 6.32, 8.25.
Do Exercises 8.48 and 8.50,
showing the power and convenience of TautCon.
-
17: February 27 (Wednesday)
-
Graded Homework 4 back.
Embark on
Lecture notes on Program Verification.
Motivated by a program for computing the factorial function,
we introduce the crucial notion of loop invariants,
as described in Section 5 of the notes.
-
18: February 29 (Friday)
-
Briefly cover Sections 1-4 of
Lecture notes on Program Verification:
writing specifications as Hoare triples;
the notions of partial correctness (never get a wrong result)
versus total correctness (always get the right result);
the three-stage approach to software engineering.
Apply the proof principles for program verification using
loop invariants, stated in
Sections 5.2 and 5.3 of
Lecture notes on Program Verification,
to programs (one inefficient, another efficient) computing the n'th power of x.
-
19: March 3 (Monday)
-
Present an example of how to develop a program together
with its correctness proof,
then show that the methodology even enables us to construct
an efficient program
(Section 6 of
Lecture notes on Program Verification).
Amtoft has no office hours Tuesday.
-
20: March 5 (Wednesday)
-
Homework 5 in.
Discuss the general relationship between formal and informal proofs.
Cover Section 7 of
Lecture notes on Program Verification:
we introduce the notion of valid assertions (defined by proof rules);
showing that a program is well-annotated is a formal and fine-grained
way of proving its correctness.
We further illustrated the approach using
Question 4 from
Fall 2003, Exam III
(solution here)
for which we gave an informal correctness proof last Friday.
-
March 6 (Thursday)
-
4-4:45pm: Review session in N122.
-
21: March 7 (Friday)
-
Test I.
-
22: March 10 (Monday)
-
Homework 6 out.
Brief appetizer for Part II of the book:
motivated by the desire to express the four Aristotelian forms
(Section 9.5) in FOL, and later to handle program verification for complex data
structures, we
introduce variables (Section 9.1)
and forall/exists quantifiers (Section 9.2).
Do selected parts of Exercises 9.16 & 9.17.
We also address how to translate claims such as
"at least two".
-
23: March 12 (Wednesday)
-
Graded Test I back, going through model solutions.
Continue (and finish) Chapter 9, getting more familiar with quantifiers.
In addition to expressing the four Aristotelian forms, we
address how to translate numeric claims such as
"exactly one" or "at most one".
Sketch the definition of a well-formed formula, abbreviated wff,
and introduce the notion of free and bound variables (Section 9.3).
-
24: March 14 (Friday)
-
Homework 6 in. Homework 7 out.
Cover Sections 10.3 and 10.4,
presenting DeMorgan as well as a number of other quantifier equivalences
(summarized on p.282).
Observe that universal quantification can be expressed using existential
quantification, at the price of adding two negations, as in the database query
"find the companies which have customers in all states"
which is equivalent to
"find the companies such that there does not exist a state
where they have no customers".
-
March 17-21
-
Spring (Easter) break
-
25: March 24 (Monday)
-
Truth and consequences in the presence of quantifiers:
while the tautological approach is still of (limited) use (Section 10.1),
we shall focus on the crucial notion of first-order consequence
(Section 10.2).
A first-order consequence (FO consequence for short) is
an argument which remains valid if the predicates in question
(except for the identity "=") are consistently replaced by
other (even nonsense) predicates;
the proof rules to be introduced in Chapters 12 and 13
enable us to prove all FO consequences (and nothing but
FO consequences).
We looked into Exercises 10.1(3&5), 10.8, 10.13, 10.14, 10.18.
Last day to drop a course with 98 calendar days
(14 or more weeks in length) with a "W".
-
26: March 26 (Wednesday)
-
Graded Homeworks 5 & 6 back; go through some of the model solutions.
Introduce the axiomatic method (Section 10.5) which enables us to prove
consequences that (unlike first-order consequences)
are due to the intrinsic meaning of
predicate symbols, as illustrated by
Exercise 10.30.
-
27: March 28 (Friday)
-
Homework 7 in. Homework 8 out.
Embark on Chapter 11, taking a closer look at English sentences whose
translation into FOL requires both universal and existential
quantification,
for instance
Exercise 11.16 (3) &
Exercise 11.43 (3).
Emphasis is (cf. Section 11.5)
on the difference between "weak" (for all x there exists a y
that works for that x) and "strong" (there exists a y that
works for all x)
readings of an English sentence:
the corresponding translations
are not FO-equivalent, though in certain cases they
may be TW-equivalent.
In general, the proper translation into FOL of an English sentence
is often determined by context,
as illustrated by Exercise 11.43 (1,2).
-
28: March 31 (Monday)
-
We finish Chapter 11 (not covering Section 11.7),
looking at some interesting (and surprising!) translations
from English to FOL:
-
We encounter a "donkey sentence" (p.301) which has
to be paraphrased before it becomes obvious how to translate it:
even though the sentence strongly suggests the use of an existential
quantifier, this will not work and we have to use a universal quantifier
instead. This is further illustrated by
Exercises 11.18(2&3) and 11.19(3).
-
Exercise 11.45 considers two seemingly non-equivalent English
sentences and shows them to be equivalent:
here, the key part is our ability to infer
Ex~P(x) from ~AxP(x);
observe that claiming ExQ(x) does not entail
that we have any idea about the name of the object
satisfying Q!
Finally, we show how to translate function symbols
(Section 11.6, cf. Exercise 1.15).
-
29: April 2 (Wednesday)
-
We embark on proof rules for the quantifiers:
-
Universal instantiation and Existential generalization (Section 12.1),
the latter leading to a discussion
of Fermat's
Last Theorem
which was eventually
proved
by Andrew Wiles;
-
the method of Existential instantiation (Section 12.2),
reflected in the Elimination rule for the
Existential quantifier (Section 13.2);
-
the method of and
Universal generalization (Section 12.3), reflected
in the Introduction rule for the Universal quantifier (Section 13.1).
Do Exercises 13.13 & 13.14 & 13.3.
-
30: April 4 (Friday)
-
Mention (Section 13.4) that our proof system is sound (thanks to side conditions requiring
names to be fresh) and complete.
More examples of proofs (cf. Section 13.3) which use the newly introduced
rules for quantifiers; we do
three of the four "DeMorgan inferences".
Mention the method of General conditional proof (Section 12.3),
reflected in the (other) Introduction rule for the
Universal quantifier (Section 13.1).
-
31: April 7 (Monday)
-
Do the last "DeMorgan inference",
showing Ex~P(x) from ~AxP(x).
This inference (cf. p.355)
is not accepted by "intuitionists" as it doesn't
give us any clue about which x satisfies ~P;
in general
intuitionists don't like the ~Elim rule but we shall not follow
their restricted approach!
Discuss the tricky interaction between
existential instantiation and universal generalization (Section 12.4);
we can prove "weak reading" from "strong reading"
but (fortunately) not the other way round (due to the requirement
that a boxed constant does not occur outside its subproof).
Continue the issue of axiomatization (Section 12.5),
illustrated by comparing Exercise 13.32 (use of AnaCon) to
Exercise 13.33 (use of an axiom).
-
32: April 9 (Wednesday)
-
Graded Homework 7 back; go through model solutions.
Homework 8 in; go through model solutions.
-
April 10 (Thursday)
-
4-4:45pm: Review session in N122.
-
33: April 11 (Friday)
-
Test II.
-
34: April 14 (Monday)
-
Discuss Test II, going through model solutions.
Prove the equivalence
between two alternative ways
of expressing "there exists at most one P"
(something which probably cannot be done using the laws from
Chapter 10), cf. Exercises 13.49 & 13.50 from the upcoming Homework 9.
-
35: April 16 (Wednesday)
-
Homework 9 out. Graded Test II back.
Verification of programs reading arrays,
illustrated by developing a program for deciding whether an array is sorted
(Section 8.1 in
Lecture notes on Program Verification).
-
April 18 (Friday)
-
Class canceled (All-University Open House)
-
36: April 21 (Monday)
-
Do Exercises 12.28 and 12.13, presenting variants of the Catch-22
situation captured by
"The Barber Paradox" (p.333)
which has deep implications for modern mathematics
in that it expels us from
"Cantor's paradise":
naive set theory leads to contradictions, as demonstrated by
Exercise 13.52 which encodes Russell's paradox.
Do Exercise 12.37 where we give axioms for "MoreSides".
Specify and write a program for
finding the maximum element of an array
(Section 8.1 in
Lecture notes on Program Verification).
-
37: April 23 (Wednesday)
-
Homework 9 in. Homework 10 out.
Verification of programs modifying arrays
(Section 8.2 in
Lecture notes on Program Verification).
Thursday April 24, Amtoft has office hours from 3pm to 4pm.
-
38: April 25 (Friday)
-
We embark on the exciting topic of mathematical induction
(handing out lecture notes),
a special case of which we have seen already in the proof principle
for program invariants: if an assertion
phi holds after zero loop iterations, and
if phi holds after k+1 loop iterations provided
that phi holds after k loop iterations,
then phi holds after any number of loop iterations.
We cover Section 16.3 in the textbook, dealing with induction
on natural numbers:
if we prove Q(0), and prove that Q(n) implies Q(n+1),
then Q holds for all natural numbers!
The textbook contains a minor error:
on p. 454, the first natural number is defined to be
zero, but Proposition 4 only holds if
the first natural number is assumed to be one.
(We can start anywhere as long as we are consistent;
to prove a formula for the sum of angles in an n-polygon
we must start at three.)
Do Exercise 16.15.
-
39: April 28 (Monday)
-
Continue mathematical induction on natural numbers:
-
Look at Exercise 16.18 from the upcoming homework;
we realized that the result cannot be proved as it is
and that we need to prove a stronger property,
telling not only that the sum of the first n cubes is a square
but also what it is the square of!
-
Define the fibonacci function on natural numbers.
Using the
golden ratio,
we can state (and prove) a formula for the value of the n'th fibonacci number,
something which would be virtually impossible to do without the
induction principle
(a slightly different formulation of which is required,
cf. Section 2.1 in
Lecture notes on Induction).
-
40: April 30 (Wednesday)
-
Homework 10 in. Homework 11 out.
We introduce immutable lists
and show how to reason about this important data structure,
cf. Section 3 in
Lecture notes on Induction:
-
We give an inductive definition of lists,
using which we write some recursive functions manipulating lists,
like "sumlist" and "removezero"
(cf. the upcoming homework).
-
We state the induction principle for lists,
and prove by induction that
for all lists x, sumlist(removezero(x)) = sumlist(x).
-
41: May 2 (Friday)
-
Graded Homework 9 back.
Verification of programs with procedures,
using Section 9 in
Lecture notes on Program Verification.
Also show, using a board simulation, how to implement
recursive procedures.
-
42: May 5 (Monday)
-
Show how the use of Hoare triples and quantifiers enables us to express
secrecy of data as well as integrity of data,
as described in
Section 10 in
Lecture notes on Program Verification.
-
43: May 7 (Wednesday)
-
Homework 11 in.
Go through model solutions for Homeworks 9 & 10.
As an appetizer for future encounters with logic
(though not part of the exam material in this course),
we introduce CTL (computation tree logic).
-
44: May 9 (Friday)
-
Review session, going through some previous exam questions.
Graded Homework 11 back; go through model solutions.
-
May 13 (Tuesday)
-
Final exam, 11:50am-1:40pm
Torben Amtoft