COMP2111 Assignment 1 2024 Term 1

发布时间：2024-06-27

Hello, dear friend, you can consult us at any time if you have any questions, add WeChat: daixieit

COMP2111 Assignment 1

2024 Term 1

Due: Mon 25 March, 9:00 AM

Submission is through give and should consist of:

1. A single pdf file with typeset answers, maximum size 4Mb. Prose should be typed, not handwritten. Use of LATEX is strongly encouraged, but not required.

2. A file partner.txt with a single line on the format. z . This must be the zID of your group partner. For individual submissions, write your own zID.

Submit your work using the web interface linked on the course website, or by running the following on a CSE machine

give cs2111 assn1 assn1 .pdf partner.txt

This assignment is to be done in pairs. Individual submissions are discouraged, but will be accepted. Only one member of the pair should submit. Workout who will submit ahead of time—duplicate submissions are extremely annoying to sort out.

Late submission is allowed up to 5 days (120 hours) after the deadline. A late penalty of 5% per day will be deducted from your total mark.

Discussion of assignment material with others is permitted, but you may not exchange or view each others’ (partial) solutions. The work submitted must be your own, inline with the University’s plagiarism policy. Note in particular that attempting to pass off AI writing (e.g. ChatGPT output) as your own still counts as plagiarism.

These problems are themed around the game of Connect Four. Two players, white (o) and black (●), take turns dropping discs of their respective colour into columns of a grid, causing the disc to fall down to the lowest unoccupied row in that column. The first player to have four in a row, either horizontally, vertically, or diagonally, wins the game. If neither player has three in a row when the board is full, the game is a draw.

The game is usually played on a 5x7 board,but to make lifeless tedious we’re shrinking the board to 4x5, and making it Connect Three, where the win condition is three in a row. Here’s an illustration:


	●
o	●
o	●	o	o

The o player didn’t show their best performance in this game.

Suppose a Connect Three program represents the game board as an array of characters of length 20, stored in the global variable board. The idea is that the contents of board[i] is "E" if the i:th square is empty, "B" if it contains a , and "W" if it contains a # . The squares are numbered as follows:

0	1	2	3	4
5	6	7	8	9
10	11	12	13	14
15	16	17	18	19

Consider the following pseudo-code, where abort is an instruction that causes the program to abort (crash) with a run-time error. The idea is that move(2,"W") puts a white disc on the board, in the column numbered 2 above.

void move(int row, char fill) {

if((fill != "B" && fill != "W") || row < 0 || row > 4) then { abort;

}

int i = 15 + row; flag = false;

while(i >= 0 && flag=false) { if board[i] = "E" then {

flag = true; }

else {

i = i-5;

} }

if flag then {

board[i] := fill;

}

else { abort;

} }

Mathematically, we model board as a 20-tuple b ∈ {E, W, B}20, where bi represents the contents of board[i].

(a) Define a relation R ⊆ {E, W, B}20 × {E, W, B}20 that models the effect that a non-aborting call to move can have on the board. In particular, (b, b′) ∈ R should hold iff the following holds: a call to move can terminate (without aborting) in a state where the new board is b′, if the old board before calling move was b. (10 marks)

(b) Which of the following properties does R have? Is it reflexive, antireflexive, symmetric, antisymmetric, transitive, or a function? For each of these six properties, either give a counterexample, or explain (informally and in your own words) why the property holds. (15 marks)

(c) Is R an accurate characterisation of the set of legal moves in Connect Three? If yes, explain why; if no, explain what’smissing.

Hint: a sneak peek at question 3 may help here. (5 marks)

(d) Recall the relation composition operator (; ) defined as follows:

R1; R2 = {(a, c) | there is a b with (a, b) ∈ R1 and (b, c) ∈ R2}

What is the cardinality of R; R; R; R; R; R; R; R; R; R; R; R; R; R; R; R; R; R; R; R; R? (That’s 21 R:s.). What does your answer tell you about the effects of repeatedly calling move? What does your answer tell you about the game of Connect Three? (10 marks)

Problem 2 (40 marks)

Let’s look at another possible way of modelling a Connect Three board, this time with propositional logic. We will use 40 propositional letters: W0, . . . , W19 and B0, . . . , B19. The idea is that Wi is true if the i:th square contains a # , and similarly Bi is true if if the i:th square contains a .

(a) Write a propositional formula φ0 that holds iff the o player has three in a row horizontally on the bottom row. The formula should not mention any of the Bi letters. (5 marks)

(b) Let φ1 be the analogous formula that holds iff the ● player has three in a row on the bottom row. Show that the formula φ0 ∧ φ1 is satisfiable (by giving a valuation v such that [[φ0 ∧ φ1 ]]v = true). (5 marks)

(c) One way of making this model of Connect Three more accurate is to introduce a formula φ2 which characterises the well-formed states,i.e. those that correspond to legal board positions in Connect Three. Write a propositional formula φ2 such that every legal board position of Connect Three satisfies φ2, but that rules out illegal game states such as the one from question (b). It’sok if φ2 overapproximates the legal game states, i.e. if there are some game states that satisfy φ2 despite not being reachable in an actual game (for example, a board filled with black circles). If so, please explain any such overapproximations you made. (5 marks)

(d) Prove that the following holds

{φ2 } |= ¬ (φ0 ∧ φ1 )

using either of the following methods: the calculational approach from Week 1, natural deduction, or a direct semantic argument (by showing that every valuation that satisfies φ2 must also satisfy ¬ (φ0 ∧ φ1 )). (10 marks)

(e) Extend φ0 to a formula that is true iff the o player has three in a row anywhere. (5 marks)

(f) These formulas are getting tedious. Imagine typing all that out for a larger board than 4x5.

Make a better, more extensible model using predicate logic. This means you can use ∀, ∃, and intro- duce any predicates and functions you find useful.

Write a predicate logic formula that is true iff the o player has x in a row anywhere on an nxm board. Informally explain the intended meaning of any predicates and function symbols you introduce.

Hint: You don’t need to formally specify your domain of discourse, nor do you need to give a model for your vocabulary. (10 marks)

Problem 3 (20 marks)

Now, we will use formal languages to describe the set of valid games of Connect Three. Let Σ = {W0, . . . , W4, B0, . . . , B4} be our alphabet of moves, where the subscript represents the row number. As always, we use w, v to range over words, and a, b, c to range over symbols from Σ . Words in Σ∗ represent sequences of moves; for example, W0B4W0 represents this unlikely sequence of moves:




o

(a) Write an inductive definition of a language L ⊆ Σ∗ such that w ∈ L iff w is a sequence of legal moves in Connect Three. Your definition should consists of a base case, and one or more inductive clauses which describe the circumstances under which a sequence of moves w ∈ L may be extended to the right with a single move a such that wa ∈ L. Remember to account for the following:

• Games end when one player has won.

• The players need to alternate turns.

• Move sequences that correspond to unfinished games should also be included.

Feel free to write your definition in prose rather than in any formal notation. You don’t need to define auxiliary concepts in detail; for an example, feel free to use a “someone has won” predicate on words, without spelling out its exact definition, as long as the intended meaning is clear. (15 marks)

Hint: feel free to use this solution template (filling in the . . . as appropriate).

Solution template

Let L be the smallest set such that

• · · · ∈ L

• If w ∈ L, and if w does not end with a character Wi for any i, and . . . , then wWn ∈ L.

• . . .

(b) Describe how you would generalise from a 4x5 board to an nxm board. (5 marks)