Question 1

Show, via chains of equivalences, that the following propositions are tautologies.

(a) (p ∧ q) ⇒ (p ⇔ q)

(b) ((p ∨ q) ⇒ r ) ⇒ (¬ p ∨ (q ∨ r ))

Question 2

Show that the tautologies of Question 1 are also theorems of our proof system by exhibiting proof trees in which there are no undischarged assumptions.

Question 3

Simplify, using the one-point rule and other rules of predicate logic, the following statement.

(∃ z : N • (∃ x : N • (x < 1 ∧ x = z ∧ y = x )) ∨ (y = z ∧ z = 1))

You should assume that y ∈ N.

Question 4

Suppose that the relation R is an element of the set X ↔ Y and the relation S is an element of the set Y ↔ Z. Assume further that A is an element of P Z and that B is an element of PX.

Show, via a proof of the form

z → x ∈ A C (R 0 S) ~ B 

⇔
.
.
⇔
z → x ∈ (S B A) ∼ 0 (B C R) ∼

that

A C (R o S) ~ B  = (S 0 A) ~ o (B C R) ~

Question 5

This question pertains to the modelling of a digital music device. We start by introducing four basic types:

[Id,Artist , SongTitle,AlbumTitle]

Next, we introduce three abbreviations:

TrackNumber == N
Length == N
Size == N

Finally, we assume the existence of a set, Time.

We now introduce three functions, song details, track data, and plays:

song details : Id → (SongTitle × Artist × AlbumTitle)
track data : Id → (Time × Length × Size)
plays : seq (Id × Time)

Here, assuming an identifier, i ∈ Id:

• song details (i ) captures the details of a track;
• (track data (i )).1 is the time at which the file was added, (track data (i )).2

is the length (in seconds) of the track, and (track data (i )).3 is the size (in bytes) of the file; and

• (i , t ) ∈ ran plays indicates that track i was played at time t .

Complete the axiomatic definition by adding the following constraints.
(a) The domain of song details should be the same as the domain of track data.

(b) Only tracks appearing in song details and track data may appear in plays.

(c) No track can be played before it has been added to song details and track data.

(d) The elements of plays should be ordered in an earliest-first fashion.

Question 6

Building on the definitions of Question 5, define expressions that capture the following.

(a) The set of duplicate tracks - where duplicates are defined as tracks which have the same song title and artist.

(b) The details of all tracks - in the form (song title, artist, album title)

- that are at least 5 minutes long.

(c) The details of all tracks - in the form (song title, artist, album title)

- that have been played at least 10 times.

(d) The set of all albums that are at least 60 minutes in length. (We assume that 'albums' are determined by values of type AlbumTitle.)

(e) The set of all artists that have received at 1000 minutes of 'play time'.

Question 7

Building on the definitions of Question 5, define the following functions.

(a) A function that takes an identifier as input and returns the number of plays of that song (as defined by plays).

(b) A function that takes an album title as input and returns the set of song titles associated with it (as per song details).

(c) A function that takes an identifier as input and, by taking account the contents of song details, track data and plays, returns a tuple of type SongTitle × Artist × AlbumTitle × Time × N, where the fourth component is the 'last played' time and the fifth component is the
number of plays. (You should feel free to assume the existence of an element null ∈ Time).

Question 8

Assume the following definition
Play == Id × SongTitle × Artist × AlbumTitle × Time × N
Here, the fifth component is the 'last played' time and the sixth component is the number of plays of the track. Again, you should feel free to assume the existence of an element null ∈ Time.

Define the following recursive functions.

(a) A function that takes an element of type seq Play and returns the total number of plays of songs appearing in that sequence. We shall call this function totalplaysS .

(b) A function that takes an element of type seq Play and filters by those songs appearing in song details.

(c) A function that takes an element of type seq Play and returns the identifier of the last played song.

Question 9

We may define a free type representing a tree-like structure as follows:

PlayTree ::= Stalk | NodehhPlay × PlayTreeii |
BranchhhPlayTree × PlayTreeii
Show how the functions of Question 8 might be reproduced using this structure in place of seq Play. We shall call the first of these - which takes an element of type PlayTree and returns the total number of plays of songs appearing in that tree - totalplaysT .

Question 10

(a) Write down a structural induction principle for the PlayTree free type.

(b) Define a function, TreeToSequence, that maps a tree to a sequence: it takes an element of PlayTree and returns an element of seq Play as output. In particular, we would expect the property of part (c) to hold.

(c) Show, using a suitable structural induction principle, that

∀ t : PlayTree •

totalplaysT (t ) = totalplaysS (TreeToSequence (t ))