Captain's Log: Logical Foundations of Programming, Fall 2007
-
1: August 20 (Monday)
-
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.
-
2: August 22 (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.
No office hours, or review session, today.
-
August 24 (Friday)
-
Class canceled (Instructor out of town)
-
August 27 (Monday)
-
Class canceled (Instructor out of town)
-
3: August 29 (Wednesday)
-
Homework 1 in.
Using
these slides,
cover 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.
No review session today.
-
4: August 31 (Friday)
-
Homework 2 out. Go briefly through comments on Homework 1.
Using
these slides,
cover 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).
Elimination and introduction rule for
the identity predicate.
Demonstrate "Fitch",
using Exercise 2.20 (part of HW2).
-
September 3 (Monday)
-
Labor Day: student/university holiday
-
5: September 5 (Wednesday)
-
Using
these slides (except 18--21),
cover Chapter 3:
Negation, Conjunction, Disjunction.
Compare "\/" to "exclusive or".
Ambiguities in FOL (and in English), and how to resolve them.
Do Exercises 2.7,
3.19,
3.15.
Graded Homework 1 back.
-
6: September 7 (Friday)
-
Homework 2 in. Homework 3 out (including Quiz 1).
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), 4.34, and 4.17.
-
7: September 10 (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 Exercise 4.43.
-
8: September 12 (Wednesday)
-
Graded Homework 2 back; go through some model solutions.
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.
Today's review session will be from 5:30pm to 6:00pm (still in N122).
-
9: September 14 (Friday)
-
Homework 3 in. Homework 4 out.
Cover Chapter 5, introducing
two crucial proof principles:
proof by cases; proof by contradiction (indirect proof).
(Do Exercises 5.1-5.7.)
-
10: September 17 (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: September 19 (Wednesday)
-
Continue Chapter 6,
working through some examples of how to construct proofs
using the rules given,
for instance for 3 of the 4 arguments which
constitute DeMorgan's laws.
Reminder: never reuse sentences from a subproof which has ended
(Fitch actually prevents that).
Do Exercises 6.28 and 6.19;
the latter proves
a general pattern which was used twice in Exercise 4.27.
-
12: September 21 (Friday)
-
Homework 4 in. Homework 5 out.
Graded Homework 3 back; go through some model solutions.
Finish Chapter 6, with more examples of how to construct
proofs: Exercise 6.33 (excluded middle), and the last (and most difficult)
of the 4 arguments constituting DeMorgan's laws.
Cover Section 7.1, introducing a new connective:
"->" (which might be pronounced "implies").
Touch on Exercises 7.1, 7.2, and 7.6;
briefly touch on Exercise 7.21.
-
13: September 24 (Monday)
-
Cover Section 7.2, introducing one more connective:
"<->" (to be pronounced "if and only if",
abbreviated "iff").
Touch on Exercises 7.3, 7.4, 7.7, 7.8.
Cover most of Sections 8.1 and 8.2:
motivated by the examples in Exercise 8.1,
we show how to reason about ->
as formalized by Elimination and Introduction rules;
those are applied in Exercises 8.24 & 8.19,
and also to establish the principle of contraposition (p.199).
-
14: September 26 (Wednesday)
-
Finish Sections 8.1 and 8.2: Elimination and Introduction rules
for <->,
in particular,
discuss how to prove a chain of biconditionals
(cf. Exercise 8.15).
Do Exercises 8.27 & 8.35 (8.7)
-
15: September 28 (Friday)
-
Homework 5 in. Graded Homework 4 back (briefly touching on model solutions).
Introduce the notion of truth-functional completeness
(Section 7.4), further illustrated by
Exercises 7.26 & 7.30.
Do Exercise 8.48, showing the power and convenience of TautCon.
-
October 1 (Monday)
-
Student holiday
-
16: October 3 (Wednesday)
-
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.
Do Exercise 8.50, again showing the power and convenience of TautCon,
and Exercise 8.29.
Graded Homework 5 back (briefly touching on model solutions).
-
17: October 5 (Friday)
-
Test I.
Homework 6 out.
-
18: October 8 (Monday)
-
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.
-
19: October 10 (Wednesday)
-
Graded Test I back.
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 the program from
Question 4 in
Fall 2003, Exam III
(where a formal proof was required; we did an informal).
-
20: October 12 (Friday)
-
Homework 6 in. Homework 7 out.
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).
-
21: October 15 (Monday)
-
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 Wednesday.
-
22: October 17 (Wednesday)
-
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).
We also address how to translate claims such as
"at least two".
-
23: October 19 (Friday)
-
Homework 7 in. Homework 8 out. Graded Homework 6 back.
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).
Do (parts of) Exercises 9.16 & 9.17.
-
24: October 22 (Monday)
-
Cover Sections 10.3 and 10.4,
presenting DeMorgan as well as a number of other quantifier equivalences
(summarized on p.282).
-
25: October 24 (Wednesday)
-
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).
The axiomatic method (Section 10.5) enables us to prove
consequences that (unlike first-order consequences)
are due to the intrinsic meaning of
predicate symbols.
We looked into Exercises 10.1(3&5), 10.8, 10.13, 10.14, 10.18.
-
26: October 26 (Friday)
-
Homework 8 in.
Wrap up the axiomatic method (Section 10.5),
doing Exercise 10.30.
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).
-
27: October 29 (Monday)
-
Homework 9 out.
Graded Homework 7 back.
Continue Chapter 11, with emphasis
(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.
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.
-
28: October 31 (Wednesday)
-
Graded Homework 8 back, going through model solutions.
We wrap up Chapter 11 (not covering Section 11.7)
by doing Exercise 11.18(2&5),
by discussing function symbols (Section 11.6, cf. Exercise 1.15), and by
Exercise 11.45 which 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!
-
29: November 2 (Friday)
-
Test II
-
30: November 5 (Monday)
-
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
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.
-
31: November 7 (Wednesday)
-
Mention the method of General conditional proof (Section 12.3),
reflected in the (other) Introduction rule for the
Universal quantifier (Section 13.1).
Mention that our proof system is sound and complete (Section 13.4).
More examples of proofs which use the newly introduced
rules for quantifiers (cf. Section 13.3):
three of the four "DeMorgan inferences".
-
32: November 9 (Friday)
-
Homework 9 in.
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 (cf. Question 4 of test II) the issue of axiomatization (Section 12.5),
illustrated by comparing Exercise 13.32 (use of AnaCon) to
Exercise 13.33 (use of an axiom).
-
33: November 12 (Monday)
-
Homework 10 out. Graded Test II back.
Wrap up Chapters 12 & 13:
-
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 Homework 10.
-
Do Exercises 12.28 and 12.13, presenting variants of
"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!
-
34: November 14 (Wednesday)
-
Verification of programs reading arrays,
in particular develop a program for finding the maximum element of an array
(Section 8.1 in
Lecture notes on Program Verification).
-
35: November 16 (Friday)
-
Verification of programs modifying arrays
(Section 8.2 in
Lecture notes on Program Verification).
Also develop a program that decides whether an array is sorted.
-
36: November 19 (Monday)
-
Homework 10 in. Homework 11 out.
Wrap up the previous weeks:
look at the challenging exercises
11.20 & 11.26 from Homework 9;
do Exercise 13.52 which encodes Russell's paradox;
do Exercise 12.37 where we give axioms for "MoreSides".
A brief appetizer,
proving a formula for the sum of angles in an n-polygon,
for the "induction" principle.
-
November 21-23 (Wednesday-Friday)
-
Thanksgiving holiday
-
37: November 26 (Monday)
-
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.
Do Exercise 16.15.
Amtoft has no office hours today, due to Landon lecture.
-
38: November 28 (Wednesday)
-
Graded Homework 10 back, mentioning Exercise 12.15 and Exercise 7.
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).
Do Exercise 16.1 (induction is a pleasant principle!)
and Exercise 16.2 (where premises are inconsistent).
-
39: November 30 (Friday)
-
Homework 11 in. Homework 12 out.
We introduce immutable lists (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).
-
40: December 3 (Monday)
-
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.
-
41: December 5 (Wednesday)
-
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.
Graded Homework 11 back.
-
42: December 7 (Friday)
-
Homework 12 in.
Go through model solutions for Homework 11 and Homework 12.
As an appetizer for future encounters with logic
(though not part of the exam material in this course),
we briefly introduce CTL (computation tree logic).
-
December 10 (Monday)
-
Review session CANCELED
due to inclement weather forecast.
-
December 12 (Wednesday)
-
-
Final exam, 11:50am-1:40pm.
Torben Amtoft