Captain's Log: Logical Foundations of Programming, Fall 2006

1: August 21 (Monday)
Syllabus handed out. A brief motivation for why to study this course, sketching two examples (square root, array maximum) of how to use First Order Logic (FOL) for the specification of software.
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 23 (Wednesday)
Homework 1 out.
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). Tarski's world illustrated using software package.
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: August 25 (Friday)
Wrap up Chapter 1, doing Exercise 1.16.
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.3 and 2.4.
4: August 28 (Monday)
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" and "Submit" using Exercise 2.20 (part of HW1). Do Exercise 2.7.
5: August 30 (Wednesday)
Homework 1 in. Homework 2 out.
Using these slides, cover Chapter 3: Negation, Conjunction, Disjunction. Compare "\/" to "exclusive or". Ambiguities in FOL (and in English), and how to resolve them.
6: September 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.17, 4.31(7), and 4.34.
September 4 (Monday)
Labor Day: student/university holiday
7: September 6 (Wednesday)
Continue Chapter 4. The notion of a tautology. Using the distributive laws, 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 8 (Friday)
Homework 2 in. Homework 3 out. Graded Homework 1 back.
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.
9: September 11 (Monday)
Cover Chapter 5, introducing two crucial proof principles: proof by cases; proof by contradiction (indirect proof). Do Exercise 5.7.
10: September 13 (Wednesday)
Cover Sections 6.1-6.3, presenting various elimination and introduction rules. Disjunction elimination corresponds to "proof by cases"; negation introduction corresponds to "proof by contradiction". Do Exercises 5.1-5.6, and Exercise 6.5.
11: September 15 (Friday)
Homework 3 in. Homework 4 out. Graded Homework 2 back.
Continue Chapter 6, working through some examples of how to construct proofs using the rules given. Do Exercises 6.28 and 6.19; the latter proves a general pattern which was used twice in Exercise 4.27.
12: September 18 (Monday)
Finish Chapter 6, with more examples of how to construct proofs, for instance for each of the 4 arguments which constitute DeMorgan's laws. Also do Exercise 6.33 (excluded middle). Reminder: never reuse sentences from a subproof which has ended (Fitch actually prevents that).
13: September 20 (Wednesday)
Cover Sections 7.1-7.2, introducing two new connectives: "->" (which might be pronounced "implies") and "<->" (to be pronounced "if and only if", abbreviated "iff").
Touch on Exercises 7.1-7.4, and 7.6-7.8; do Exercise 7.12(2) and briefly touch on Exercise 7.21.
Today, the review session starts at 5:30pm.
14: September 22 (Friday)
Homework 4 in. Homework 5 out.
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, applied in Exercises 8.24, 8.19, 8.35.
15: September 25 (Monday)
Graded Homework 3 back.
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 Exercise 8.29.
16: September 27 (Wednesday)
The notion of truth-functional completeness (Section 7.4).
Motivated by Exercise 7.32, we stated that the formal system F is sound, and also complete (Section 8.3, omitting the proofs of the theorems).
Do Exercises 8.48 & 8.50, showing the power and convenience of TautCon.
This completes Part I of the textbook.
17: September 29 (Friday)
Homework 5 in. Homework 4 graded (GG only).
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.
October 2 (Monday)
Student holiday
Amtoft has no office hours Tuesday (October 3)
18: October 4 (Wednesday)
Motivated by a program for computing the factorial function, we introduce the crucial notion of loop invariants, as described in Section 5 of Lecture notes on Program Verification.
Discuss Homework 5, in particular Exercises 8.30 (showing the tremendous power of "Proof by Contradiction") and 8.52 (showing proper use of TautCon).
19: October 6 (Friday)
Test I.
20: October 9 (Monday)
Graded Test I back. Graded Homework 5 back. Homework 6 out.
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).
21: October 11 (Wednesday)
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).
22: October 13 (Friday)
Homework 6 in. Homework 7 out.
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 Monday. If the chosen invariant is wrong, the method fails, as in (the formal counterpart of) Question 2 from Fall 2004, Exam II.
23: October 16 (Monday)
Discuss the general relationship between formal and informal proofs.
Brief appetizer for Part II of the book: motivated by the desire to express the four Aristotelian forms (Section 9.5) in FOL, 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".
24: October 18 (Wednesday)
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 Exercises 9.16 & 9.17.
25: October 20 (Friday)
Homework 7 in. Homework 8 out.
Present various quantifier equivalences, including DeMorgan (Sections 10.3 and 10.4).
Do Exercises 10.20 & 10.29.
26: October 23 (Monday)
Graded Homework 6 back.
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, 10.8, 10.13, 10.14, 10.18.
27: October 25 (Wednesday)
Wrap up the axiomatic method (Section 10.5), doing Exercises 10.30 & 10.31.
Embark on Chapter 11, looking at English sentences whose translation into FOL requires both universal and existential quantification.
28: October 27 (Friday)
Homework 8 in. 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 (as in Exercise 11.18(4)).
29: October 30 (Monday)
We wrap up Chapter 11 (not covering Section 11.7), 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!
We embark on proof rules for the quantifiers:
30: November 1 (Wednesday)
We finish the proof rules for the quantifiers: Do Exercises 13.14 & 13.3.
Mention that our proof system is sound and complete (Section 13.4).
Briefly cover model solutions for Homework 8.
31: November 3 (Friday)
Test II.
Homework 9 out.
32: November 6 (Monday)
Graded Test II back.
More examples of proofs which use the newly introduced rules for quantifiers (cf. Section 13.3): the four "DeMorgan inferences", the last of which 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!
33: November 8 (Wednesday)
Graded Homework 8 back.
Discuss the tricky interaction between existential instantiation and universal generalization (Section 12.4).
Cover the issue of axiomatization (Section 12.5), illustrated by comparing Exercise 13.32 (use of AnaCon) to Exercise 13.33 (use of an axiom), and by Exercise 12.37 where we gave axioms for "MoreSides".
34: November 10 (Friday)
Homework 9 in. Homework 10 out.
Wrap up Chapters 12 & 13. 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!
Prove the equivalence between two alternative ways of expressing "there exists at most one P".
Look at the challenging Exercise 11.26 from Homework 9.
35: November 13 (Monday)
Verification of programs reading arrays, in particular develop a program for finding the maximum element of an array (Section 10.1 in Lecture notes on Program Verification).
Do Question 4 from Spring 2004, Exam III (suggested solution here).
36: November 15 (Wednesday)
Verification of programs modifying arrays (Section 10.2 in Lecture notes on Program Verification).
37: November 17 (Friday)
Homework 10 in.
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.
38: November 20 (Monday)
Do the challenging Exercise 13.31 from Homework 9.
Go through much of the challenging Homework 10: Exercise 12.15; Exercise 8 (on array programs); Exercise 13.50; Exercise 13.52.
Motivated by computing the sum of angles in an n-polygon, we introduce the exciting topic of induction, where Lecture Notes were handed out.
November 22-24 (Wednesday-Friday)
Thanksgiving holiday
39: November 27 (Monday)
Homework 11 out.
Continue induction, 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.
40: November 29 (Wednesday)
Continue 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!
We introduce immutable lists (cf. Section 3 in Lecture notes on Induction): first we give an inductive definition of lists, using which we write some recursive functions manipulating lists, like "sumlist" and "removezero" (cf. the upcoming homework); next we state the induction principle for lists and prove by induction that for all lists x, sumlist(removezero(x)) = sumlist(x).
41: December 1 (Friday)
Test III.
42: December 4 (Monday)
Graded Test III back.
More examples of induction: 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).
43: December 6 (Wednesday)
Homework 11 in (to the front office).
Class canceled (instructor out of town).
44: December 8 (Friday)
Class canceled (instructor out of town).
December 15 (Friday)
Final exam, 11:50am-1:40pm.

Torben Amtoft