Feedback for CS242 January 2009

Question 1

This question was the one that overall was best answered. I would have expected a higher standard though.

The most common and serious problem was the misreading of the formulae in (b). The sequent:
p → r ∨ q → r |- p ∧ q → r
is to be read as:
(p → r) ∨ (q → r) |- (p ∧ q → r)
using the standard precedence rules. In fact, it was read in all kinds of ways, and inevitably led to incorrect and irrelevant answers. By ignoring these precedence rules, many people computed truth tables in which they highlighted the wrong columns for comparison. If I was resetting this question, I would be tempted to include an exercise in "putting the brachets" into the formulae in the above sequent - something I would have regarded as too elementary before seeing the answers!

I was surprised that nobody took the phrase "In the light of your answers" in (d) seriously. What emerges from (b) and (c) is that the p → r ∨ q → r and p ∧ q → r are logically equivalent formulae. Intuitively though, if "r is true because of p and q", it clearly doesn't follow that "r is true because of p alone" or "r is true because of q alone". The key point here is that (according to the formal definition of implication in propositional logic) setting p or q to false renders p → r ∨ q → r true.

Question 2

This is the sort of question which contains a substantial amount of bookwork. External examiners regard this kind of question as in principle "easy", since you can rely on memory rather than having to solve problems in the exam. The answers to this question were generally quite disappointing though. In part, this is because many students seemed to think that they could convey their understanding without writing out the book definitions. Actually, these definitions represent the product of very careful thought, and being able to recall them, and appreciating why they are formulated exactly the way they are, is a fundamental part of understanding. Phrases such as "Briefly explain ..." are intended to elicit formal definitions together with some more informal explanation of your own. Over and above correct definitions and familiarity with basic theorems and proofs, what I'm looking for in a good answer is evidence that you have reflected on these definitions and arguments critically, and that you are able to write about the concepts of logic using the vocabulary that the module gives you.

When people write their own informal definitions of concepts the biggest problem is that they tend to make "category errors". A formula is not a sequent for instance. Here's some examples of typical things people wrote that are meaningless because of gross errors of this nature:

"statements in predicate logic have to be sound and complete in order to be true"
"every Φ₁, Φ₁, ... , Φ_n |- Ψ"
"decidability of a formula"
"a formula can be proven by some algorithm"
"sequent semantically entails"
"once proved using ND it will definitely be true"
"sequent both sound and complete"
"rules of ND retaining consistent meaning and not creating any inequalities"

You need to be able to appreciate why such expressions are nonsensical, and be sure to avoid writing this kind of thing yourself. There are two stages in comprehension where this kind of problem is topical: you can't venture to write informal definitions before you understand the concepts properly, and when you have a clear understanding you need to be disciplined in the way that you convey this.

Question 3

This was the least satisfactorily answered question on the paper. There was a typo in the question from the fictional examination paper that Albert was attempting to answer (see the Forum), but there's not too much evidence that this was noted by many students, for whom the starting point was Victoria's answer. I think the most significant problem here was that this was an unfamiliar kind of question - (a) and (c) relating to an aspect of the module that was covered in lectures but not the exercise sheets and (d) emphasising a grasp of the expressive power of different kinds of logical formulation. The rules requested in part (a) were the introduction and elimination rules for ∀ and ∃. Very few students who tackled this question cited these rules for part (a), but most managed to complete Victoria's proof by copying the box on the left in lines 3-5 to create a similar box on the right with p₂ in the role of p₁. Few students paid attention to the clause "... briefly explaining the proof rules required." though. No-one produced a proof of (c), though some gave a brief outline of how the generalisation from conjunction to universal quantification etc might be made.

The answers to part (d) were the most unsatisfactory. The key word in this part was "Discuss", and the emphasis was on "discussing ... ways of formalising ... using ... logic" and "giving a brief justification". This was the cue for you to propose different ways you might try formulate the statements i-iv using propositional and predicate logic. In practice, students typically gave one possible formulation - often a very inexpressive one - and made no comment about other possible formulations. Sometimes they devoted their answer to matters of truth (as in the proposition "If 18 is a prime number, then 2*4=6" is true) that are only tangentially relevant. As an example of the kind of really good answer I was expecting: I was hoping that someone might have recognised that we'd ideally like to express the ancestor relation in terms of the parent-child relation using predicate logic for instance, and remembered that we identified this as the kind of statement that can't be formalised in predicate logic in this way. What was alarming was that i-iv disclosed some basic misconceptions and technical problems - for instance, many students thought that "associativity" was "commutativity", and most tried to express a statement that in effect asserted "given any odd number, there exists a bigger even number" as "∃∀ ...". There were also many instances of category errors here also: as in subexpressions such as (odd(x) < y) ∧ (..).

On reflection, I think that question 3 was difficult in that it tested meta-level understanding that it is hard to grasp on first acquaintance with the material.

Question 4

Almost all people who made a serious attempt at this question got a reasonable mark for it, and one or two got near full marks. I was quite surprised how few people were able to state the axioms of boolean algebra. It seems as if the use of the term "algebra" in connection with concepts that have interpretations in logic caused some confusion, and that the idea of algebras as models of axioms expressed using predicate logic was not appreciated by many. Virtually no-one formulated the axioms with quantifiers in place for instance, as you should in framing the associative axiom:
∀ a ∀ b ∀ c (a ∧ b) ∧ c = a ∧ (b ∧ c)
Parts (c) and (e) were really about simple examples of models for the boolean algebra axioms in the sense of predicate logic. The interpretations of the operators ∧, ∨ and ¬ were to my mind entirely intuitive (they were set-intersection, set-union and set-complement in (c), and AND, OR and NOT in (e)), but many students either failed to recognise this or seemed reluctant to point this out.

It is unfortunate that you had to answer this question before you had had a chance to tackle the assessed work for CS242 - hopefully some of you would get better results at this stage. Perhaps you by now have a better understanding of how partial ordering is linked with the operator ∧, for instance.

Question 5

This was probably the most straightforward question on the paper I suspect, in that it followed a rather standard pattern. The answers were generally reasonable, though I would still have expected higher standards, especially in the "bookwork" components (a), (b) and (c). What was most unfortunate here was that few students seemed content to answer the questions (a), (b) and (c) directly with reference to formal definitions (cf. my comments on Question 2), but invented their own dialect for explaining concepts that it's quite possible they understood reasonably well. Most people probably know for instance that part (a) should say "if the precondition Φ is true and the command P is executed, then the execution of the command terminates and Ψ is then true", but many felt the need to try to say this in some more casual or more elaborate way, and got the "if" and the "terminates" and "true" tied up in quite inappropriate ways. Worse still in some respects, they committed more serious "category errors" such as I referred to above, as in:

"given input Φ, P will complete in finite time and yield output Ψ"
"for all Φ in [the Hoare triple], P must terminate and Ψ must be correct"
"the pre-condition Φ can be put through P with post-condition Ψ

In understanding CS242, and conveying that understanding, you have to be sensitive to when you are writing such nonsense (just as in real-life you'd never consider asking whether someone's marriage was suffering from tonsilitis or whether their car had been convicted of speeding). To ensure this, you must keep asking yourself basic questions, such as: in what sense is a pre-condition an input?, in what sense can a pre-condition be correct?, in what sense can we speak about all the pre-conditions in a Hoare triple? and what does it mean to put a pre-condition through P to get a post-condition?. Only when you have such questions in your mind all the time, will you begin to appreciate why definitions are framed they are, why there are standard ways of expressing logical notions and why logic has to use such a range of subtle concepts. You will also find that you will be more careful about the ways you express things informally, and hesitate before using non-standard phraseology that could be misunderstood, such as "program P will produce a post-condition Ψ".

Rather similar errors arose in connection with invariants (which are predicates) and variants (which are procedural program style variables). Consider for instance:

"invariant is n, as n doesn't change"
"the variant is n<y"
"the variant is edited every time the while-loop loops"

Part (d) was quite well-answered by many students, but for the fact that many stopped short of dealing with total correctness. The best answers were those that explicitly identified the invariants and variants. As a minor point, no-one pointed out the need for an "implied" inference to convert the formal post-condition into the assertion about the number of digits in the binary representation.