CS计算机代考程序代写 Haskell COMP30026 Models of Computation – Logic Concepts

COMP30026 Models of Computation – Logic Concepts

COMP30026 Models of Computation
Logic Concepts

Bach Le / Anna Kalenkova

Lecture Week 2 Part 2 (Zoom)

Semester 2, 2021

Models of Computation (Sem 2, 2021) Logic Concepts c© University of Melbourne 1 / 22

This Lecture is Being Recorded

Models of Computation (Sem 2, 2021) Logic Concepts c© University of Melbourne 2 / 22

Knights and Knaves Puzzle

On the island of Knights and Knaves, everyone is a knight or knave.
Knights always tell the truth. Knaves always lie.

Today there is a census on the island!

You are a census taker, going from house to house. Fill in what you
know about each of these three houses.

In house 1: Husband: We are both knaves.

Models of Computation (Sem 2, 2021) Logic Concepts c© University of Melbourne 3 / 22

Knights and Knaves Puzzle

On the island of Knights and Knaves, everyone is a knight or knave.
Knights always tell the truth. Knaves always lie.

Today there is a census on the island!

You are a census taker, going from house to house. Fill in what you
know about each of these three houses.

In house 1: Husband: We are both knaves.

In house 2: Wife: At least one of us is a knave.

Models of Computation (Sem 2, 2021) Logic Concepts c© University of Melbourne 3 / 22

Knights and Knaves Puzzle

On the island of Knights and Knaves, everyone is a knight or knave.
Knights always tell the truth. Knaves always lie.

Today there is a census on the island!

You are a census taker, going from house to house. Fill in what you
know about each of these three houses.

In house 1: Husband: We are both knaves.

In house 2: Wife: At least one of us is a knave.

In house 3: Husband: If I am a knight then so is my wife.

Models of Computation (Sem 2, 2021) Logic Concepts c© University of Melbourne 3 / 22

Knights and Knaves Puzzle

On the island of Knights and Knaves, everyone is a knight or knave.
Knights always tell the truth. Knaves always lie.

Today there is a census on the island!

You are a census taker, going from house to house. Fill in what you
know about each of these three houses.

In house 1: Husband: We are both knaves.

In house 2: Wife: At least one of us is a knave.

In house 3: Husband: If I am a knight then so is my wife.

If you like these puzzles, Raymond Smullyan has written several
books that you will like.

Models of Computation (Sem 2, 2021) Logic Concepts c© University of Melbourne 3 / 22

Logic and Computer Science

Before we get to more sophisticated logic and its applications, let us
establish a vocabulary and some important concepts.

“The relationship between computation and mathematical

logic will be as fruitful in the next century as that between

analysis and physics in the last.”

John McCarthy

Models of Computation (Sem 2, 2021) Logic Concepts c© University of Melbourne 4 / 22

Validity and Satisfiability

A propositional formula is valid if no truth assignment makes it false.
Otherwise it is non-valid.

It is unsatisfiable if no truth assignment makes it true. Otherwise it is
satisfiable.

A valid propositional formula is a tautology.

An unsatisfiable propositional formula is a contradiction.

Models of Computation (Sem 2, 2021) Logic Concepts c© University of Melbourne 5 / 22

Tautology Example

(¬P ∧ Q)⇒ (P ⇒ R) is valid:

P Q R ¬P ∧ Q P ⇒ R (¬P ∧ Q)⇒ (P ⇒ R)

f f f f t t

f f t f t t

f t f t t t

f t t t t t

t f f f f t

t f t f t t

t t f f f t

t t t f t t

Models of Computation (Sem 2, 2021) Logic Concepts c© University of Melbourne 6 / 22

Logically, “Valid” Means Vacuous

In ordinary discourse, we may praise somebody by saying “the point
you make is valid.”

But in formal logic, a valid statement is not that laudable; in a sense
it is void of information. For example, A⇒ A is a vacuous statement,
and valid.

“If Trump is sane then Trump is sane” tells us nothing about whether
Trump is sane—the statement is true whatever the case may be.

You don’t even have to know who Trump is, or what it means to be
sane, in order to agree: The statement is inherently true.

Models of Computation (Sem 2, 2021) Logic Concepts c© University of Melbourne 7 / 22

Validity Checking in Haskell

Given a truth table for a proposition P, it is easy to check if P is
valid: The conjunction of all the entries in P’s column must be true.

To check the validity of 3-place Haskell predicate:

valid3 :: (Bool -> Bool -> Bool -> Bool) -> Bool

valid3 f

= and [f p q r | p <- bs, q <- bs, r <- bs] where bs = [False, True] Models of Computation (Sem 2, 2021) Logic Concepts c© University of Melbourne 8 / 22 Validity Checking in Haskell Given a truth table for a proposition P, it is easy to check if P is valid: The conjunction of all the entries in P’s column must be true. To check the validity of 3-place Haskell predicate: valid3 :: (Bool -> Bool -> Bool -> Bool) -> Bool

valid3 f

= and [f p q r | p <- bs, q <- bs, r <- bs] where bs = [False, True] Poll 2: What does a function to check satisfiability look like? Models of Computation (Sem 2, 2021) Logic Concepts c© University of Melbourne 8 / 22 Contradiction Example P ∧ Q ∧ (¬Q ⇔ (¬P ∨ Q)) is unsatisfiable. Again, we can just complete the truth table. However, it is often possible to apply faster reasoning. In this case, P and Q are conjuncts of the formula, so if a truth assignment maps either to f, the formula evaluates to f. And if P and Q are both mapped to t, the third conjunct becomes (¬t⇔ (¬t ∨ t)), which again evaluates to f. Models of Computation (Sem 2, 2021) Logic Concepts c© University of Melbourne 9 / 22 Substitution Preserves Validity + Unsatisfiability Validity is preserved by substitution of propositional letters by formulas. We saw that (¬P ∧ Q)⇒ (P ⇒ R) is valid, and hence (¬(A ∨ B) ∧ (B ⇔ C ))⇒ ((A ∨ B)⇒ (B ⇔ C )) is valid. (Different letters can be replaced by the same formula, but of course, all occurrences of a letter must be replaced by the same formula.) A formula is unsatisfiable iff its negation is valid. It follows that substitution also preserves unsatisfiability. Models of Computation (Sem 2, 2021) Logic Concepts c© University of Melbourne 10 / 22 Poll 3 Does substitution preserve satisfiability? Models of Computation (Sem 2, 2021) Logic Concepts c© University of Melbourne 11 / 22 Poll 3 Does substitution preserve satisfiability? No — a counter-example is easy: Models of Computation (Sem 2, 2021) Logic Concepts c© University of Melbourne 11 / 22 Poll 3 Does substitution preserve satisfiability? No — a counter-example is easy: Take P (which is clearly satisfiable). Then substitute P by Q ∧ ¬Q. The fact that P can be made true does not mean we cannot also make if false. In fact, the typical propositional formula can be made both true and false; it will simultaneously be satisfiable and non-valid. Models of Computation (Sem 2, 2021) Logic Concepts c© University of Melbourne 11 / 22 Models, Logical Consequence, and Equivalence Let θ be a truth assignment and F be a propositional formula. If θ makes F true then θ is a model of F . G is a logical consequence of F iff every model of F is a model of G as well. In that case we write F |= G If F |= G and G |= F both hold, that is, F and G have exactly the same models, then F and G are (logically) equivalent. In that case we write F ≡ G Models of Computation (Sem 2, 2021) Logic Concepts c© University of Melbourne 12 / 22 Poll 4 Of the following statements, which allow us to conclude P ⇒ Q? P ¬P Q P ⇒ (Q ∧ R) (P ∨ R)⇒ Q ¬P ∨ Q ¬Q ⇒¬P P ⇒ (Q ∨ R) (P ⇒ Q) ∨ R Models of Computation (Sem 2, 2021) Logic Concepts c© University of Melbourne 13 / 22 Poll 4 Of the following statements, which allow us to conclude P ⇒ Q? P ¬P Q P ⇒ (Q ∧ R) (P ∨ R)⇒ Q ¬P ∨ Q ¬Q ⇒¬P P ⇒ (Q ∨ R) (P ⇒ Q) ∨ R Which of the statements are logical consequences of P ⇒ Q? Models of Computation (Sem 2, 2021) Logic Concepts c© University of Melbourne 13 / 22 Substitution Preserves Logical Equivalence If F ≡ G and F ′ and G ′ are the results of replacing each occurrence of letter P (in both) with formula H, then F ′ ≡ G ′. Models of Computation (Sem 2, 2021) Logic Concepts c© University of Melbourne 14 / 22 Interchange of Equivalents Replacing equals by equals yields equals. If 1 F is a sub-formula of H, 2 F ≡ G , and 3 H ′ is the result of replacing F in H by G , then H ≡ H ′. Interchange of equivalents preserves not only logical equivalence. It also preserves logical consequence, validity, and unsatisfiability. Unlike substitution, it even preserves satisfiability. Models of Computation (Sem 2, 2021) Logic Concepts c© University of Melbourne 15 / 22 Some Equivalences Absorption: P ∧ P ≡ P P ∨ P ≡ P Commutativity: P ∧ Q ≡ Q ∧ P P ∨ Q ≡ Q ∨ P Associativity: P ∧ (Q ∧ R) ≡ (P ∧ Q) ∧ R P ∨ (Q ∨ R) ≡ (P ∨ Q) ∨ R Distributivity: P ∧ (Q ∨ R) ≡ (P ∧ Q) ∨ (P ∧ R) P ∨ (Q ∧ R) ≡ (P ∨ Q) ∧ (P ∨ R) Models of Computation (Sem 2, 2021) Logic Concepts c© University of Melbourne 16 / 22 More Equivalences ⇔ and ⊕ are also commutative and associative. Double negation: P ≡ ¬¬P De Morgan: ¬(P ∧ Q) ≡ ¬P ∨ ¬Q ¬(P ∨ Q) ≡ ¬P ∧ ¬Q Implication: P ⇒ Q ≡ ¬P ∨ Q Contraposition: ¬P ⇒¬Q ≡ Q ⇒ P P ⇒¬Q ≡ Q ⇒¬P ¬P ⇒Q ≡ ¬Q ⇒ P Biimplication: P ⇔ Q ≡ (P ∧ Q) ∨ (¬P ∧ ¬Q) Models of Computation (Sem 2, 2021) Logic Concepts c© University of Melbourne 17 / 22 Quiz Find an alternative way of writing biimplication—as a conjunction. Models of Computation (Sem 2, 2021) Logic Concepts c© University of Melbourne 18 / 22 Last Equivalences Let ⊥ be any unsatisfiable formula and let ⊤ be any valid formula. Duality: ¬⊤ ≡ ⊥ ¬⊥ ≡ ⊤ Negation from absurdity: P ⇒⊥ ≡ ¬P Identity: P ∨ ⊥ ≡ P P ∧ ⊤ ≡ P Dominance: P ∧ ⊥ ≡ ⊥ P ∨ ⊤ ≡ ⊤ Contradiction: P ∧ ¬P ≡ ⊥ Excluded middle: P ∨ ¬P ≡ ⊤ Models of Computation (Sem 2, 2021) Logic Concepts c© University of Melbourne 19 / 22 Poll 5 Which of these claims hold? 1 P ⇒ Q ≡ (Q ⇔ (P ∨ Q)) 2 (P ⇒ Q) ∧ (P ⇒ R) ≡ P ⇒ (Q ∧ R) 3 (P ⇒ R) ∧ (Q ⇒ R) |= (P ∧ Q)⇒ R Models of Computation (Sem 2, 2021) Logic Concepts c© University of Melbourne 20 / 22 Next Week Same Time Tune In Learn how symbolic manipulation beats truth tables. We shall be . . . Mechanising deduction based on propositional logic Models of Computation (Sem 2, 2021) Logic Concepts c© University of Melbourne 21 / 22 Exit Puzzle for People Who Like Puzzles Long before Covid-19, Mr. Smith and his wife invited four other couples. When everyone arrived, some of the people shook hands with some of the others. Of course, nobody shook hands with their partner, or themselves, and nobody shook hands with the same person twice. After that, Mr. Smith asked everyone how many times they shook somebody’s hand. He received different answers from all nine! How many times did Mrs. Smith shake hands? Answers to the discussion board Models of Computation (Sem 2, 2021) Logic Concepts c© University of Melbourne 22 / 22