代写COMP30026、代写Java，c++程序

日期：2022-09-18 06:33

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.