The University of Melbourne
School of Computing and Information Systems COMP30026 Models of Computation
Assignment 1, 2021
Released: 26 August. Deadline: 16 September at 23:00
Aims and Procedure
One aim of this assignment is to improve and test your understanding of propositional logic and first-order predicate logic, including their use in mechanised reasoning. A second aim is to develop your skills in analysis and formal reasoning about complex concepts, and to practise writing down formal arguments with clarity.
This document is the assignment spec. There are six challenges. The first four are to be completed on Grok, where you will find a module called “Assignment 1”. That module also contains more detailed information about submission formats and how to submit your answers in Grok. Your answers to Challenges 5 and 6 are to be submitted through Gradescope, for which there is a menu item on Canvas. You are required to solve the challenges individually. You will probably find them to be of varying difficulty, but each is worth 2 marks, for a total of 12.
Challenge 1
As a blade runner, Rick Deckard’s task is to identify replicants. These look exactly like humans, but they have in fact been manufactured in the labs of Tyrell Corporation. Some replicants are programmed to always speak the truth, while others are programmed to always lie. Unfortunately the same goes for the humans that Deckard deals with: some are always truthful, and the rest always lie. One day, Deckard interviewed two individuals, X and Y , who made these statements:
X: “Y is a truthful human” Y : “X is a lying replicant”
Task 1A. Capture, as a single propositional formula, the information that was thereby available to Deckard. You will need to take into account who makes each statement. Use propositional letters as follows:
P: X is truthful R: X is human
Q: Y is truthful S: Y is human
Task 1B. Deckard, a competent logician, realised that the two statements would not allow him to determine whether either was human or not. Determine which truth assignments to P , Q, R, S make your formula from Task 1A true.
Task 1C. Now, Deckard later found out, from a reliable source, whether Y was truthful or not, and based on that information, he knew exactly whether X was human and also whether Y was human. Given this information, determine, for each of X and Y , whether they are a human or a replicant.
Submission and marking. Your answer should be submitted on Grok. You will find the sub- mission format explained there. You will receive some feedback from some elementary tests. These merely check that your input has the correct format; they should not be relied upon for correctness. We will test your solution comprehensively after the deadline. Task 1A is worth one mark, the rest 0.5 mark each.
Challenge 2
Conjunctive normal form (CNF) is an adequate representation of Boolean functions, because every Boolean function can be written as a conjunction of disjunctions or literals. The set {∧,∨,¬} suffices to write all possible Boolean functions, that is, that set of connectives is functionally complete. In fact, from De Morgan’s laws we can conclude that {∧, ¬} is a functionally complete set of connectives, since P ∨ Q ≡ ¬(¬P ∧ ¬Q), so that disjunction can always be translated into negation and conjunction. Similarly {∨, ¬} is functionally complete.
Task 2. Show that {⇒,f} is functionally complete. That is, show that every propositional formula has a logically equivalent formula that uses only variables, the “if–then” connective, and the constant f (denoting “false”). We ask you to do this by writing a Haskell function that turns an arbitrary propositional formula into an equivalent one that uses only ⇒ and f (plus any parentheses or propositional letters you need).
Submission and marking. Your answer should be submitted on Grok. You will find the sub- mission format explained there. You will receive some feedback from elementary wellformedness checks; correctness is your responsibility. We will test your solution comprehensively after the deadline. The mark for this challenge will be based on the proportion of test cases passed, for up to 2 marks.
Challenge 3
i
k l
mn o
Here we are interested in using a 7-segment display for some uppercase letters. We want it to be able to show eight different letters, namely A, B, C, D, E, F, G, and H. For example, to show A, all the display segments, except o, should be lit up, giving the pattern . In detail, we want the eight different letters displayed as , , , , , , , and , respectively. Since there are eight letters, we need three input wires, modelled as propositional variables P, Q, and R. We will need to decide on a suitable encoding of the eight letters. One possibility is to let A correspond to input 000 (that is, P = Q = R = f), B to 001 (that is, P = Q = f and R = t), and so on. If we do that, we can summarise the behaviour of each input combination in the table below:
letter P Q R i j k l m n o display
A0001111110 B0011111111 C0101100101 D0111110111 E1001101101 F1011101100 G1101100111 H1110111110
A 7-segment display is an arrangement of seven LEDs (labelled
i–o), as shown here. Arrays of such displays are commonly used
to display characters in remote controls, blood pressure monitors, j dishwashers, and other devices. Each LED can be on or off, but
in most applications, only a small number of on/off combinations
are of interest (such as the 10 combinations that allow the display
in a digit in the range 0–9). In that case, the display can be con-
trolled through a small number of input wires. For example, four
input wires provide 24 input combinations, enough to cover the ten
different digits.
Each of the seven segments i–o can be considered a propositional function of the variables P, Q, and R. This kind of display can be physically implemented with logic circuitry, using circuits to implement a boolean function for each of the outputs. Here we assume that only three types of logic gates are available: An and-gate takes two inputs and produces, as output, the conjunction (∧) of the inputs. Similarly, an or-gate implements disjunction (∨). Finally, an inverter takes a single input and negates it (¬). We can specify such a circuit by writing down the Boolean equations for each of the outputs i–o. For example, segment i is turned off (is false) exactly when the input is 111. So, i can be captured as ¬P ∨¬Q∨¬R.
For efficiency reasons, we often want the circuit to use as few gates as possible. For example, the above equation for i shows that we can implement this output using five gates. But i = ¬(P ∧Q∧R) is an equivalent implementation, using only three gates. Moreover, the seven functions might be able to share some circuitry. For example, if we have already implemented a sub-circuit defined by u = Q ∧ R (introducing u as a name for the sub-circuit), then we can define i = ¬(P ∧ u), and we may be able to re-use u while implementing the other outputs (rather than duplicating the same gates). In some cases it may even be feasible to design a circuit that is not minimal for a given function, but provides a minimal solution when all seven functions are designed.
Task 3. Design such a circuit, using as few gates as possible. You can define any number of sub-circuits to help you reduce the gate count (simply give each a name).
Submission and marking. Your answer should be submitted on Grok. Submit a text file circuit.txt consisting of one line per definition. This file will be tested automatically, so it is important that you follow the notational conventions exactly. We write ¬ as – and ∨ as +. We write ∧ as ., or, simpler, we just leave it out, so that concatenation of expressions denotes their conjunction. Here is an example set of equations (for a different problem):
# An example of a set of equations in the correct format:
i = -Q R + Q -R + P -Q -R
j = u + P (Q + R)
k = P + -(Q R)
l=u+Pi
u = -P -Q
# u is an auxiliary function introduced to simplify j and l
Empty lines, and lines that start with ‘#’, are ignored. Input variables are in upper case. Negation binds tighter than conjunction, which in turn binds tighter than disjunction. So the equation for i says that i = (¬Q∧R)∨(Q∧¬R)∨(P ∧¬Q∧¬R). Note the use of a helper function u, allowing j and l to share some circuitry. Also note that we do not allow any feedback loops in the circuit. In the example above, l depends on i, so i is not allowed to depend, directly or indirectly, on l (and indeed it does not).
To test your equations and count the number of gates used, you can click Terminal and enter the command test. To stop the Terminal click Stop.
There is one mark for a correct solution. An additional 0.5 is awarded if a correct solution uses 24 gates or fewer. A further 0.5 is awarded if a correct solution uses 18 gates or fewer.
Challenge 4
The logic of equality. Is it possible to assign values to the variables a, b, c, and d, so that the formula (a=b)∧(b=c)∧(c=d)∧¬(a=d) is true? How about the formula (a=c) ⇔ (¬(a=b)∨¬(b=c))? These are examples of satisfiability questions in the system of equality logic. A formula in equality logic includes a collection of variables, such as a, b, c, and d. These variables are related to one another by equalities, such as (a=b). Equalities are assembled into formulas using connectives,
like the ones we are familiar with from propositional and predicate logic: ∧, ∨, ¬, ⇒, ⇔, and ⊕. An equality logic formula is satisfiable if there is some assignment of values to its variables that makes the formula evaluate to true, under the usual semantics of equality and the logical connectives.
Task overview. In this challenge, you will complete an implementation of a satisfiability decision procedure for equality logic formulas. The decision procedure will work as follows:
1. You will devise a way of modelling an equality logic formula as an equisatisfiable propositional logic formula, using the strategy below.
2. You will implement this modelling strategy as a Haskell function that translates equality logic formulas into propositional logic formulas, supported by some scaffolding code we provide. We break this step down into four implementation tasks, described below.
3. We provide a satisfiability algorithm1 for propositional logic, which will decide whether your propositional formula (and thus also the original equality logic formula) is satisfiable or not.
The strategy. The key to satisfying an equality logic formula in is knowing which variables to assign to the same values. If we know whether or not each pair of variables shares a value, we have all we need to evaluate the formula. If this information were to be encoded in propositional logic, what propositions might we use? To encode an equality logic formula in propositional logic is to use these propositions to capture the logical structure of the original formula, along with the special properties of the equality relation, in a single propositional formula. The four tasks below will guide you to capturing this strucure.
Task 4A. Using your propositional variables, implement a Haskell function to encode the logical constraints implied by an equality logic formula’s connectives as a formula in propositional logic.
Task 4B. Equality is a reflexive relation: A variable always equals itself, so a formula like (a=a) is always true in equality logic. Using your propositional variables, implement a Haskell function to encode the constraints implied by this property as a formula in propositional logic.
Task 4C. Equality is also a symmetric relation: Equality can’t be true in one ‘direction’ and not the other. (a=b) and (b=a) are equivalent in equality logic. Using your propositional variables, implement a Haskell function to encode the constraints implied by this property as a formula in propositional logic. Hint: Depending on your propositional variables, this may be a short formula.
Task 4D. Finally, equality is a transitive relation: Equalities chain together. If we know (a=b) and (b=c), then we must have (a=c) too, even if this is not specified directly in an equality logic formula. Using your propositional variables, implement a Haskell function to encode the constraints implied by this property as a formula in propositional logic. Hint: For each individual group of three variables2, consider all of the ways in which the transitive property could affect the formula.
Submission and marking. Your answer should be submitted on Grok. You will find the sub- mission format explained there. You will receive some feedback from some tests that check the output for some simple examples. These tests should not be relied upon for correctness. We will test your solution comprehensively after the deadline. The mark for this challenge will be based on the proportion of test cases passed, for up to 2 marks.
1In case you are curious: The algorithm uses the Tseytin transform (Assessed Worksheet 2) to efficiently convert your propositional formula to conjunctive normal form, and then passes it to a SAT solver.
2It’s not necessary to consider every possible group of three variables that could form a transitive arrangement. Our scaffolding code finds a sufficient list of triples, using a graph triangulation algorithm on the network of equalities implied by the equality logic formula. All you need to do is handle these groups of three variables.
Challenge 5
Consider the four first-order predicate formulas
F1: ∃x(∃u(∀v(P(u,v,x)))⇒∃y(Q(x,y))) G: F1⇒F2
F2 : ∃x (∀v (∃u (P(u,v,x)))⇒∃y (Q(x,y))) H : F2 ⇒F1
Task 5A. Determine whether G is valid or not. Either provide a proof that uses resolution to
show validity, or else specify an interpretation that makes G false.
Task 5B. Determine whether H is valid or not. Either provide a proof that uses resolution to
show validity, or else specify an interpretation that makes H false.
Submission and marking. Your answers to Challenges 5 and 6 should be submitted through Gradescope as a single PDF document, no more than 2 MB in size. Marks are primarily allocated for correctness, but elegance and how clearly you communicate your thinking will also be taken into account.
Challenge 6
The notation we use for first-order predicate logic includes function symbols. This allows a very simple representation of the natural numbers. Namely, for natural numbers, we use terms built from a constant symbol (here we choose a, but any other symbol would do) and a function symbol of arity 1 (we will use s, for “successor”). The idea is that 0 is represented by a, 1 by s(a), 2 by s(s(a)), and so on. In general, s(x) represents the successor of x, that is, x+1. Logicians prefer this “successor” notation, because it uses so few symbols and supports recursive definition—a natural number is either ‘a’ (the base case), or it is of the form ‘s(. . .)’, where . . . is a term representing a natural number. (Of course, for practical use, we prefer the positional decimal system.)
With successor notation, we can capture the usual “less than or equal” ordering of N (the set of natural numbers) with these two axioms, where L(x, y) stands for x ≤ y:
∀y(L(a, y)) (1) ∀x∀y(L(x, y) ⇒ L(s(x), s(y))) (2)
(1) says that 0 is smaller than or equal to any natural number, and (2) says that if x ≤ y then x+1 ≤ y+1. Similarly, we can capture addition by introducing a predicate symbol for the addition relation, letting P (x, y, z) stand for x + y = z:
∀y(P (a, y, y)) (3) ∀x∀y∀z(P (x, y, z) ⇒ P (s(x), y, s(z))) (4)
Turning the conjunction of (1)–(4) into clausal form, we end up with this set of clauses: {{L(s(v1), s(v2)), ¬L(v1, v2)}, {L(a, v3)}, {P (s(v4), v5, s(v6)), ¬P (v4, v5, v6)}, {P (a, v7, v7)}}
Task 6A. Use resolution to show that
∃x∃y(L(s(a), x) ∧ P (y, y, x)) (5)
is a logical consequence of the axioms (1)–(4).
Task 6B. Your resolution proof will not only establish the truth of (5). The resolution proof provides a sequence of most general unifiers, one per resolution step, and when these are composed, in the order they were generated, you have a substitution that solves the constraint 1 ≤ x∧y+y = x. Give that substitution and explain what it means in terms of natural numbers.
Submission and marking. Your answers to Challenges 5 and 6 should be submitted through Gradescope as a single PDF document, no more than 2 MB in size. Marks are primarily allocated for correctness, but elegance and how clearly you communicate your thinking will also be taken into account.
Further Submission Advice
The deadline is 16 September at 23:00. Late submission will be possible, but a late submission penalty will apply: a flagfall of 1 mark, and then 1 mark per 12 hours late.
Note that on Grok, “saving” your file does not mean submitting it for marking. To submit, you need to click Mark and then Submit. You can submit as many times as you like. What gets marked is the last submission you have made before the deadline.
For Challenges 5 and 6, if you produce an MS Word document, it must be exported and sub- mitted as PDF, and satisfy the space limit of 2 MB. We also accept neat hand-written submissions, but these must be scanned and provided as PDF. If you scan your document, make sure you set the resolution so that the generated document is no more than 2 MB. The Canvas module, from which you downloaded this document, has advice to help you satisfy the 2 MB requirement while maintaining readability.
Being neat is easier if you type-set your answers, but not all typesetting software does a good job of presenting mathematical formulas. The best tool is LATEX, which is worth learning if you expect that you will later have to produce large technical documents. Admittedly, diagrams are tedious to do with LATEX, even when using sophisticated packages such as Tikz. You could, of course, mix typeset text with hand-drawn diagrams. In case you want to use this assignment to get some LATEX practice, we will leave the source for this document in the Canvas module where you find the PDF version.
Make sure that you have enough time towards the end of the assignment to present your solutions carefully. A nice presentation is sometimes more time consuming than solving the problems. Start early; note that time you put in early usually turns out more productive than a last-minute effort. For Challenge 3 in particular, you don’t want to submit some “improved” solution a few minutes before the deadline, as it may turn out to be wrong and you won’t have time to change your mind.
By submitting work for assessment you implicitly declare that you understand the University’s policy on academic integrity and that the work submitted is your original work. You declare that you have not been unduly assisted by any other person (collusion). In this assignment, individual work is called for, but if you get stuck, you can use the Ed Discussion board to ask any questions you have. As long as nobody directly gives away solutions, our discussion forum is both useful and appropriate for this; we can all use it to support each other’s learning. If your question is simply to clarify some aspect of the assignment, your post can be ‘public’, but if it reveals anything about your attempted solution, make sure it is submitted as a ‘private’ post to the teaching team. Soliciting help from sources other than the above will be considered cheating and will lead to disciplinary action.