School of Computing and Information Systems
COMP30026 Models of Computation Assignment 1
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.
Copyright By PowCoder代写 加微信 powcoder
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.
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.
Challenge 2 – Negative Implications
We have seen that implication can be re-written into an equivalent formula using the following equivalence
𝐹 ⇒𝐺 ≡ ¬(𝐹 ∧¬𝐺) (2.1)
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.
(¬𝑃 ⇒(¬𝑄∧𝑄⇒f)) ⇒ (((𝑃 ⇒¬(𝑅⇒𝑄))∧¬𝑃) ⇒ ¬(𝑃 ⇒¬(𝑅⇒𝑄))) (2.2)
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.
𝐹∧𝐺 ≡ 𝐺∧𝐹 ¬𝐹 ∧(𝐹 ⇒𝐺) ≡ ¬𝐹
(2.3) (2.4) (2.5)
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.
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.
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 oftheeightlettersistolet𝐴correspondtoinput000(thatis,𝑃 =𝑄=𝑅=f),𝐵to001(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
Α00011111100A Β00111111110B Γ01011001000C Δ01100100111D Ε10011011010E Ζ10110000011F Η11001111100H Λ11100100101L
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.
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.
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)
# 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.
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≤𝑖
msort = msort (take n xs) `merge` msort (drop n xs)
where n = length xs `div` 2
merge [] rs = rs
merge ls [] = ls
|l
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.
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.
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 𝑥 + 𝑦 = 𝑧:
∀𝑥 𝑃 (𝑎, 𝑥, 𝑥)
∀𝑥∀𝑦∀𝑧 (𝑃 (𝑥, 𝑦, 𝑧) ⇒ 𝑃 (𝑠(𝑥), 𝑦, 𝑠(𝑧)) ∀𝑥∀𝑦 (𝑃 (𝑥, 𝑦, 𝑧) ⇒ 𝑃 (𝑦, 𝑥, 𝑧))
(Identity element) (Recursive relation) (Commutativity)
(6.1) (6.2) (6.3)
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:
∀𝑥∃𝑦 (𝐸(𝑥) ⇒ 𝑃 (𝑦, 𝑦, 𝑥)) (6.4) ∀𝑥∀𝑦 (𝑃 (𝑦, 𝑦, 𝑥) ⇒ 𝐸(𝑥)) (6.5)
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
∀𝑥 (𝐸(𝑥) ⇒ 𝐸(𝑠(𝑠(𝑥)))) (6.6) 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.
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
程序代写 CS代考 加微信: powcoder QQ: 1823890830 Email: powcoder@163.com