COMP30026 Models of Computation
Assignment 1
Released: 26 Aug. 2022; Deadline: 16 Sep. 2022
Aims & 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 which you will find in the
remainder of this document. Your answers to Challenge 5 and Challenge 6 are to be submitted
through Gradescope, for which there is a menu item on Canvas. The remaining challenges 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.
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.
1
Challenge 1 – Predictably Inconsistent Weather
The city of Melbourne, Australia is infamous for its predictably inconsistent weather. The mobile
apps Parrot and Carrot compete to predict the correct weather over the next three days. Mel-
bourne’s weather has a habit of making a fool of the apps’ developers, such that at any time, only
one of the two apps makes a correct prediction.
Despite this, Harald still can use this information to get accurate weather forecasts for the week,
so that they don’t get wet on their commutes to-and-from university. On a Monday, Harald checks
both the Carrot and Parrot apps, where they make the following predictions:
Carrot: “It will rain on Tuesday and Wednesday.”
Parrot: “If it rains on Monday, it will rain on Wednesday.”
Task 1A. Capture, as a single propositional formula, the information that was thereby available
to Harald. You will need to take into account which app makes each prediction. Use propositional
letters as follows:
∶ Carrot’s prediction is correct ∶ Parrot’s prediction is correct
∶ It rains on Monday ∶ It rains on Tuesday ∶ It rains on Wednesday
Task 1B. Harald tries to determine the weather forecast for the week from those two predictions,
but realises they do not yet have enough information. Determine which truth assignments to
, ,, , make your formula from Task 1A true.
Task 1C. Harald opens their window blinds and looks outside to check for any chance of rain.
Based on that information, they now knew exactly what the weather would be for Monday, Tuesday
and Wednesday. Given this information, determine, for each of Monday, Tuesday and Wednesday,
whether it rains or not.
Submission and Marking: Your answer should be submitted on Grok. You will find the
submission 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 1
mark, the rest are worth 0.5 marks each.
2
Challenge 2 – Negative Implications
We have seen that implication can be re-written into an equivalent formula using the following
equivalence
In this challenge we will generalise this result to rewrite all of the connectives we have seen
using ∧ and ?. To this effect, we will show that {∧, } is functionally complete as we can represent
all formulas using only ∧ and ?.
Task 2A. Using the equivalence defined in (2.1), re-write the following formula to remove all
instances of the ? connective. You must not perform any other transformations.
Task 2B. The formula (2.2) can be simplified. Using only the equivalences (2.1) and (2.3)–
(2.5) you can simplify your answer for Task 2A. Provide the most simplified formula using (2.1)
and (2.3)–(2.5), with no instances of . This should contain the smallest number of connectives
possible.
Task 2C. Generalising the re-writing rule (2.1), we can re-write all other connectives using only
∧ and ?. Write a Haskell function that can re-write any formula into an equivalent formula that
uses only ∧, ?, and any variables. Your function should not produce any double-negatives, such
as .
Submission and Marking: Your answer should be submitted on Grok. You will find the
submission 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 2A and Task 2B
are worth 0.5 marks each for a correct answer; Task 2C is worth 1 mark based proportionally on
the number of passed test cases.
3
Challenge 3 – Logic on Display
In this challenge we will consider an unconventional 8-segment display which
is like a 7-segment display, but has an additional diagonal LED from the
top-right to bottom-left of the display. Arrays of such displays are commonly
used to display characters in remote controls, blood pressure monitors, dish-
washers, and other devices. We label each LED –, with being the diagonal
segment, as shown here.
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 ten combinations that allow
the display of a digit in the range 0–9). In that case, the display can be
controlled through a small number of input wires with four wires providing
24 input combinations, enough to cover the ten different digits.
Here we are interested in using an 8-segment display for some Greek letters. We want it to be
able to show eight different letters, namely Α, Β, Γ, Δ, Ε, Ζ, Η, and Λ. For example, to show Α,
all the display segments, except and , should be lit up, giving the pattern A. In detail, we want
the eight different letters displayed respectively as:
A, B, C, D, E, F, H, L
Since there are eight letters, we need three input wires, modelled as propositional variables , ,
and . We will need to decide on a suitable encoding of the eight letters. One possibility encoding
of the eight letters is to let correspond to input 000 (that is, = = = f), to 001 (that
is, = = f and = t), etc. If we do that, we can summarise the behaviour of each input
combination in the table below:
letter display
Α 0 0 0 1 1 1 1 1 1 0 0 A
Β 0 0 1 1 1 1 1 1 1 1 0 B
Γ 0 1 0 1 1 0 0 1 0 0 0 C
Δ 0 1 1 0 0 1 0 0 1 1 1 D
Ε 1 0 0 1 1 0 1 1 0 1 0 E
Ζ 1 0 1 1 0 0 0 0 0 1 1 F
Η 1 1 0 0 1 1 1 1 1 0 0 H
Λ 1 1 1 0 0 1 0 0 1 0 1 L
Each of the eight segments – can be considered a propositional function of the variables , ,
and . 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 –. For example, segment is turned off (is false) when the input is 011, 110,
or, 111. So, can be captured as.
For efficiency reasons, we often want the circuit to use as few gates as possible. For ex-
ample, the above equation for shows that we can implement this output using fifteen gates.
But = is an equivalent implementation, using
fewer gates. Moreover, the eight functions might be able to share some circuitry. For example,
if we have already implemented a sub-circuit defined by = ∧ (introducing as a name for
the sub-circuit), then we can define = , and we may be
able to re-use 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 eight functions are designed.
4
Task 3A. 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, more simply, 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 + P i
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 says that = . Note the use of a helper
function , allowing and to share some circuitry. Also note that we do not allow any feedback
loops in the circuit. In the example above, depends on , so is not allowed to depend, directly
or indirectly, on (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
26 gates or fewer. A further 0.5 is awarded if a correct solution uses 20 gates or fewer.
Optionally, you can submit your circuit design to a leaderboard. Your position on this board is
not reflective of your final grade and can be used anonymously. The leaderboard site can be found
here https://comp30026.ddns.net/leaderboard.
5
Challenge 4 – Property-Based Testing
Unlike unit tests that only test a single use case of a program, Property-Based Testing allows
programmers to provide a specification of their programs, as logical properties that should hold if
their program is implemented correctly. There are two types of properties that one can test about
their code. One is data invariants which are light sanity checks and the others are full functional
specifications.
For example, consider the following definition of reverse in Haskell
reverse :: [a] -> [a]
reverse [] = []
reverse (x:xs) = reverse xs ++ [x]
A nice property of a reverse function is that when composed with itself, it is the identity.
That is, to say
reverse (reverse ) = (4.1)
This property is not enough to show that the reverse is functionally correct, so we say that
this is a data invariant of reverse. For example, consider we replaced the definition of reverse
with id (the identity function), the property (4.1) still holds.
For a full specification of the reverse function, we require a stronger property as follows
length (reverse ) = length
∧ 0 ≤ < length reverse !! = !! (length 1) (4.2)
This specifies that the length of the reversal of some list, , is the same as the length of , and
for each value of the reversal of some list, , at index , the value in at the opposing end of
must be the same as said value in the reversal of . Take a moment to convince yourself this is
true for a correct implementation of reverse and some example lists .
In Haskell, the QuickCheck library1 provides property-based testing. This library is probably
older than many of you, appearing first in 1999, and has been ported to well over 30 languages. In
summary, QuickCheck generates a series of randomised inputs that are tested against the properties
similar to the properties we have previously seen. QuickCheck then reports any test cases that fail
as counter-examples. You do not need to learn or understand QuickCheck to solve this
challenge.
Through this challenge, we will use a simplified model of property-based testing in Haskell. We
are concerned with the functional correctness of sorting functions. To begin, we will be considering
the following merge sort, msort.
msort :: (Ord a) => [a] -> [a]
msort xs@(_:_:_) = msort (take n xs) `merge` msort (drop n xs)
where n = length xs `div` 2
merge [] rs = rs
merge ls [] = ls
merge lls@(l:ls) rrs@(r:rs)
| l < r = l:merge ls rrs
| otherwise = r:merge lls rs
msort xs = xs
As we may have multiple sorting functions to test, the functions we will implement to test for
these properties we will see will parameterise which sorting function is to be tested, and so will
have the following form
1https://hackage.haskell.org/package/QuickCheck
6
sortProperty :: (Ord a) => ([a] -> [a]) -> [a] -> Bool
sortProperty sort input = {- Boolean expression -}
Testing individual sorting functions is then performed with sortProperty msort, etc.
Task 4A. Implement a function, sortLength, that checks the following property: the result of
sorting some input must have the same length as the input.
Task 4B. Implement a function, sortHead, that checks the following property: if the input is
not empty, then the head element of the sorted input is the least element of the input.
Task 4C. Implement a function, sortIsSorted, that checks the following property: the result of
sorting some input is in sort-order, i.e., the result is a non-decreasing list.
Task 4D. The following is a functional specification of all sorting functions:
sortSpec :: (Ord a) => ([a] -> [a]) -> [a] -> Bool
sortSpec sort input =
elem (sort input) (permutations input) && sortIsSorted sort input
That is to say, a function sorts its input if the output is a permutation of the input and the
output is in sort-order.2
With the following (incorrect) implementation of qsort, provide two values, example and
counterExample, that are an example and a counter-example, respectively, for the sortSpec func-
tional specification with respect to the qsort function.
qsort :: (Ord a) => [a] -> [a]
qsort [] = []
qsort (pivot:rest) = qsort lesser ++ [pivot] ++ qsort greater
where lesser = filter (< pivot) rest
greater = filter (> pivot) rest
That is, sortSpec qsort example should be True and sortSpec qsort counterExample
should be False.
Submission and Marking: Your answer should be submitted on Grok. You will find the
submission 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. Your functions should
hold only for the properties asked. Each of Task 4A, Task 4B, and Task 4C are worth 0.5 marks,
each based proportionally on the number of test cases passed. Task 4D is worth 0.5 marks, with
0.25 marks awarded for each correct value provided.
2Note: this specification depends on the definition of the property from Task 4C that you must implement yourself.
7
Challenge 5 – Interpreting Resolutions
Consider the following predicate logic formulas.
Task 5A. Show that is non-valid, by providing an appropriate interpretation I.
Task 5B. Show that ∨ is valid using resolution, explicitly stating all substitutions used.
Submission and Marking: Your answers to Challenge 5 and Challenge 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. The process of resolution should be displayed as a tree.
8
Challenge 6 – Evenness
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 , but any other symbol would do) and a one-place function
symbol (we will use , for “successor”). The idea is that 0 is represented by , 1 by (), 2 by
(()), and so on. In general, () represents the successor of , that is, +1. Logicians prefer this
“successor” notation, because it uses so few symbols and supports recursive definition-—a natural
number is either ‘’ (the base case), or it is of the form ‘()’, 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 addition by introducing a predicate symbol for the
addition relation, letting (, , ) stand for + = :
Similarly, using the addition relation we can now define the evenness of a number by introducing
the predicate symbol for evenness, letting () stand for is even:
Task 6A. Now, the goal is to prove the well-known property of natural numbers that if is an
even number then + 2 is also even. Use resolution to show that
is a logical consequence of the axioms (6.1)–(6.5).
Task 6B. We have defined what an even number is and a theorem about even numbers, but we
still don’t know if even numbers exist! Using resolution, show that
is a logical consequence of the axioms (6.1)–(6.5) and the theorem (6.6). 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 (((()))).
Give that substitution and explain what it means in terms of natural numbers.
Submission and Marking: Your answers to Challenge 5 and Challenge 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. The process of resolution should be displayed as a tree.
9
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 Challenge 5 and Challenge 6, if you produce an MS Word document, it must be exported
and submitted 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. Illegible or poorly-written submission
will likely attract few, if any, marks. 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.
Academic Honesty Statement
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.