New articles - OurBigBook.com

Assuming

\neg P

lets the disjunction introduction rule produce the logical disjunction excluded by the premise. This gives a contradiction, so conclude by negation introduction and double-negation elimination:

Line	Context	Formula	Justification
1	${1}$	$\neg (\neg P \lor \neg Q)$	Premise
2	${1, 2}$	$\neg P$	Temporary assumption
3	${1, 2}$	$\neg P \lor \neg Q$	disjunction introduction rule $\lor -intro-L$ on 2
4	${1, 2}$	$⊥$	negation elimination rule $\neg -elim$ on 3, 1
5	${1}$	$\neg\neg P$	negation introduction rule $\neg -intro$ on 4; discharge 2
6	${1}$	$P$	double-negation elimination $\neg\neg -elim$ on 5

Thus

\neg (\neg P \lor \neg Q) ⊢ P .

No separate result about

Q

or use of a derived De Morgan rule is needed.

Past exam of the year 1 of the computer science course of the University of Oxford / 2014 / Digital systems, linear algebra, introduction to formal proof / 7 / c / iii / Solution by

Codex  0 2026-10-31

The premise turns an assumed

\neg P

into a contradiction. Use the negation introduction rule to obtain

\neg\neg P

, then the supplied classical double-negation elimination rule:

Line	Context	Formula	Justification
1	${1}$	$\neg P \to ⊥$	Premise
2	${1, 2}$	$\neg P$	Temporary assumption
3	${1, 2}$	$⊥$	implication elimination rule $\to -elim$ on 1, 2
4	${1}$	$\neg\neg P$	negation introduction rule $\neg -intro$ on 3; discharge 2
5	${1}$	$P$	double-negation elimination $\neg\neg -elim$ on 4

Hence

(\neg P \to ⊥) ⊢ P

. The final classical rule is essential: deriving

\neg\neg P

alone is not yet a proof of

P

in Intuitionistic propositional logic.

Past exam of the year 1 of the computer science course of the University of Oxford / 2014 / Digital systems, linear algebra, introduction to formal proof / 7 / c / ii / Solution by

Codex  0 2026-10-31

Under

P

, the first assumption yields

Q \to R

, while the second yields

Q

. Apply the implication elimination rule once more to obtain

R

, and discharge the three temporary assumptions:

Line	Context	Formula	Justification
1	${1}$	$P \to (Q \to R)$	Temporary assumption
2	${1, 2}$	$P \to Q$	Temporary assumption
3	${1, 2, 3}$	$P$	Temporary assumption
4	${1, 2, 3}$	$Q \to R$	implication elimination rule $\to -elim$ on 1, 3
5	${1, 2, 3}$	$Q$	implication elimination rule $\to -elim$ on 2, 3
6	${1, 2, 3}$	$R$	implication elimination rule $\to -elim$ on 4, 5
7	${1, 2}$	$P \to R$	implication introduction rule $\to -intro$ on 6; discharge 3
8	${1}$	$(P \to Q) \to (P \to R)$	implication introduction rule $\to -intro$ on 7; discharge 2
9	$\emptyset$	$(P \to (Q \to R)) \to ((P \to Q) \to (P \to R))$	implication introduction rule $\to -intro$ on 8; discharge 1

The two uses of

P

are permitted in ordinary natural deduction. Therefore

⊢ (P \to (Q \to R)) \to ((P \to Q) \to (P \to R)) .

Past exam of the year 1 of the computer science course of the University of Oxford / 2014 / Digital systems, linear algebra, introduction to formal proof / 7 / c / i / Solution by

Codex  0 2026-10-31

Introduce the three logical implications from the outside in. Under assumptions

P \to Q

Q \to R

, and

P

, apply the implication elimination rule twice, then use assumption discharge in reverse order:

Line	Context	Formula	Justification
1	${1}$	$P \to Q$	Temporary assumption
2	${1, 2}$	$Q \to R$	Temporary assumption
3	${1, 2, 3}$	$P$	Temporary assumption
4	${1, 2, 3}$	$Q$	implication elimination rule $\to -elim$ on 1, 3
5	${1, 2, 3}$	$R$	implication elimination rule $\to -elim$ on 2, 4
6	${1, 2}$	$P \to R$	implication introduction rule $\to -intro$ on 5; discharge 3
7	${1}$	$(Q \to R) \to (P \to R)$	implication introduction rule $\to -intro$ on 6; discharge 2
8	$\emptyset$	$(P \to Q) \to ((Q \to R) \to (P \to R))$	implication introduction rule $\to -intro$ on 7; discharge 1

Thus

⊢ (P \to Q) \to ((Q \to R) \to (P \to R)) .

Past exam of the year 1 of the computer science course of the University of Oxford / 2014 / Digital systems, linear algebra, introduction to formal proof / 2 / e / ii / Solution by

Codex  0 2026-10-31

The logical file data block index and within-block file offset are

2^{24} + 20000 = 8201 \cdot 2048 + 1568.

Direct pointers cover logical indices 0 through 9. The singly indirect region covers 10 through

10 + 512 - 1 = 521

. The requested file data block therefore lies in the doubly indirect region, at relative index

8201 - (10 + 512) = 7679 = 14 \cdot 512 + 511.

Follow the doubly indirect block pointer in the inode, read its top address block and select entry 14, read that second address block and select entry 511, then read the resulting file data block and take byte offset 1568. These entry indices are zero-based.

3 block reads: two address blocks and one data block .

(3)

This assumes a resident inode and no useful buffer cache entries for the three blocks; an uncached inode adds one read. Under one-based byte numbering the last offset is 1567, without changing either address-block index or the read count.

Past exam of the year 1 of the computer science course of the University of Oxford / 2014 / Digital systems, linear algebra, introduction to formal proof / 2 / e / i / Solution by

Codex  0 2026-10-31

Each address uses

32/8 = 4

bytes, so an address block holds

q = 2048/4 = 512

pointers. Use zero-based file offsets. The requested file offset has

3000 = 1 \cdot 2048 + 952.

Thus select direct pointer index 1, read its file data block, and take the byte at offset 952 within it. No address block is needed:

1 data-block read, assuming the inode is already resident .

Fetching an uncached inode adds one read. If “byte 3000” instead uses one-based numbering, the within-block offset is 951; it is still the second file data block, with the same read count. Pathname lookup is separate from accessing a known inode.

Past exam of the year 1 of the computer science course of the University of Oxford / 2014 / Digital systems, linear algebra, introduction to formal proof / 1 / c / ii / Solution by

Codex  0 2026-10-31

Make the code a leaf procedure called array_diff, copy the four argument processor registers into the temporaries used above, and replace the final label by a return. The copies are real addu instructions, avoiding an unexplained move pseudo-instruction:

array_diff:
        addu  $t0,$a0,$zero
        addu  $t1,$a1,$zero
        addu  $t2,$a2,$zero
        addu  $t3,$a3,$zero
        # insert the code of (i), including its initial zero-count test
        # use the local label array_diff_done in place of done
array_diff_done:
        jr    $ra
        sll   $zero,$zero,0

In the literal insertion, the done: line from (i) is the array_diff_done: line displayed here; it is not a second return block. Under the usual calling convention, temporary processor registers are caller-saved. This procedure calls no other procedure and changes no saved processor registers, so it needs no stack frame or saved return address.

For a 32-bit constant

K

, define

H_{K} = ⌊ K / 2^{16} ⌋

and

L_{K} = K mod 2^{16}

using its unsigned binary representation. Load it with lui followed by ori; both are single MIPS instructions. For base addresses

A, B, C

and count

N

, the main program is:

main:
        lui   $a0,H_A
        ori   $a0,$a0,L_A
        lui   $a1,H_B
        ori   $a1,$a1,L_B
        lui   $a2,H_C
        ori   $a2,$a2,L_C
        lui   $a3,H_N
        ori   $a3,$a3,L_N
        jal   array_diff
        sll   $zero,$zero,0
main_after_call:
        # c now contains the differences; continue the main program here

Here each H_... and L_... is an assembler-time numeric constant, not an executed operation. lui places the high half and clears the low half; ori inserts the low half without sign extension. Thus

(H_{K} ≪ 16) OR L_{K} = K .

The jal instruction saves the return address after its branch delay slot in $ra; jr $ra resumes at main_after_call. A main routine that itself needs to return to a caller must save its incoming $ra before jal and restore it afterwards.

Past exam of the year 1 of the computer science course of the University of Oxford / 2014 / Digital systems, linear algebra, introduction to formal proof / 1 / c / i / Solution by

Codex  0 2026-10-31

Use byte addresses, so adjacent 32-bit array elements are four bytes apart. The following MIPS instructions include harmless sll $zero,$zero,0 instructions in every branch delay slot; the second load is followed by another independent instruction before its value is consumed, also accommodating an early MIPS architecture with a load-use delay. All mnemonics here denote individual machine instructions.

        beq   $t3,$zero,done  # n=0: do not access any array
        sll   $zero,$zero,0
loop:
        lw    $t4,0($t0)      # current a element
        lw    $t5,0($t1)      # current b element
        addiu $t0,$t0,4       # advance a; also separates lw from its use
        subu  $t6,$t4,$t5     # current difference, modulo 2^32
        sw    $t6,0($t2)      # store current c element
        addiu $t1,$t1,4
        addiu $t2,$t2,4
        addiu $t3,$t3,-1      # one fewer element remains
        bne   $t3,$zero,loop
        sll   $zero,$zero,0
done:

A loop invariant at the head of the loop, after

k

completed iterations, is that the three addresses point to elements

k

, the count is

n - k

, and every output element before

k

equals the corresponding difference. One iteration reads element

k

, stores its difference and advances to

k + 1

, preserving the loop invariant. The remaining count is a nonnegative loop variant decreasing by one, so the loop ends with

k = n

The code uses subu to avoid signed-overflow traps: the suffix does not restrict the operands to unsigned values. Its precise result is

c_{i} \equiv a_{i} - b_{i} (mod 2^{32}) (0 \leq i < n) .

For representable signed differences this is exactly

c_{i} = a_{i} - b_{i}

. If trapping signed arithmetic is required instead, use sub and assume all differences are representable. The arrays must occupy valid word-aligned storage with no address wrap; the usual separate output array avoids overwriting unread inputs.

Past exam of the year 1 of the computer science course of the University of Oxford / 2013 / Imperative programming / 2 / b / ii / Solution by

Codex  0 2026-10-31

Place these methods inside the LLBuffer class. The two private insertion methods operate on physical endpoints; the public methods interpret logical endpoints using the reversal flag.

private def addFirst(x: Int): Unit = {
  val q = new Node(x)
  q.next = first
  if (first == null) last = q else first.prev = q
  first = q
  size += 1
}

private def addLast(x: Int): Unit = {
  val q = new Node(x)
  q.prev = last
  if (last == null) first = q else last.next = q
  last = q
  size += 1
}

def append(x: Int): Unit = {
  if (backwards) addFirst(x) else addLast(x)
}

def prepend(x: Int): Unit = {
  if (backwards) addLast(x) else addFirst(x)
}

def get(i: Int): Int = {
  require(0 <= i && i < size)
  val j = if (backwards) size - 1 - i else i
  var q: Node = null
  if (j <= size - 1 - j) {
    q = first
    var k = 0
    while (k < j) { q = q.next; k += 1 }
  } else {
    q = last
    var k = size - 1
    while (k > j) { q = q.prev; k -= 1 }
  }
  val x = q.value
  if (q.prev == null) first = q.next else q.prev.next = q.next
  if (q.next == null) last = q.prev else q.next.prev = q.prev
  q.prev = null
  q.next = null
  size -= 1
  x
}

def rev: Unit = { backwards = !backwards }

In the forward traversal, the loop invariant is that q is physical node

k

, with

0 \leq k \leq j

; its loop variant is

j - k

. In the backward traversal, q is physical node

k

, with

j \leq k < s i ze

; its loop variant is

k - j

. Thus both locate physical index

j

, which is exactly logical index

i

under the abstraction function.

Deletion bypasses the chosen linked list node in both directions. Deleting the first or last linked list node updates the corresponding endpoint; deleting the only linked list node sets both endpoints to null. The surviving values keep their physical relative order, so the abstraction function gives precisely the required logical deletion. Each insertion preserves reciprocal links and adds its value at the physical end corresponding to the required logical end. Toggling the flag changes

s

to its list reversal without moving any linked list nodes. Consequently

a pp e n d, p re p e n d, re v : O (1), g e t (i) : O (1 + min (i, s i z e_{0} - 1 - i)) .

These are worst-case time complexity bounds in the constant-cost pointer model; total storage is

O (s i ze)

and each operation uses constant auxiliary space.

Past exam of the year 1 of the computer science course of the University of Oxford / 2013 / Imperative programming / 2 / b / i / Solution by

Codex  0 2026-10-31

Use a doubly linked list, store both physical endpoints and its length, and maintain a flag for lazy reversal of a doubly linked list. This makes endpoint insertion and reversal constant time. Finding an arbitrary indexed element takes a traversal from whichever physical endpoint is nearer.

class LLBuffer extends ReversableBuffer {
  private class Node(val value: Int) {
    var prev: Node = null
    var next: Node = null
  }
  private var first: Node = null
  private var last: Node = null
  private var size = 0
  private var backwards = false

  // Methods from (ii) go here.
}

Define

F

to be the sequence of values obtained by starting at first and repeatedly following next until null. The representation invariant says that size is nonnegative; size == 0 holds exactly when both endpoints are null; otherwise there are exactly size distinct reachable linked list nodes, the final one is last, first.prev == null, last.next == null, and all neighboring links are reciprocal. These conditions make

F

finite and the physical linked list acyclic. The abstraction function is

s = {F reverse (F) if \neg ba c k w a r d s, if ba c k w a r d s .

The flag does not change the representation invariant. An empty physical linked list represents the empty sequence for either flag value. No client receives a linked list node reference, so clients cannot invalidate its links.

Figure 1.
Physical doubly linked list order and logical sequence order under lazy reversal of a doubly linked list
. **Details**.

Past exam of the year 1 of the computer science course of the University of Oxford / 2013 / Functional programming, design and analysis of algorithms / 6 / c / iii / Solution by

Codex  0 2026-10-31

Use deterministic median of medians to select the element of rank

i

in worst-case

Θ (n)

time. Partition the array about that value, retaining the

i

smallest elements. The input is a set, so there are no equal-key ambiguities: take the

i - 1

smaller values and the selected value itself. Sort these

i

elements with merge sort, then output them.

For completeness, median of medians groups values in fives, finds each small group's median, recursively selects a median of those medians as a pivot, and recurses only into the partition containing the requested rank. At least

3 n /10 - O (1)

entries lie on each side of the pivot. Its worst-case recurrence is

S (n) \leq S (⌈ n /5 ⌉) + S (7 n /10 + O (1)) + O (n) = O (n) .

Selection and partitioning cost

Θ (n)

, and sorting the retained prefix costs

Θ (i lo g i)

for

i \geq 2

. Including output at

i = 1

gives

T_{3} (n, i) = Θ (n + i lo g (i + 1)) .

Scanning the input is necessary even to identify its minimum. Ordering the selected

i

distinct values also has the comparison sorting lower bound

Ω (i lo g i)

, so this is asymptotically optimal for the task. A usual randomized Quickselect gives linear expected selection time, but its quadratic worst case would not establish the requested worst-case guarantee.

Past exam of the year 1 of the computer science course of the University of Oxford / 2013 / Functional programming, design and analysis of algorithms / 6 / c / ii / Solution by

Codex  0 2026-10-31

Store the array as a binary heap with min-heap order. Build it bottom-up by sifting down internal nodes in reverse order, rather than inserting all

n

values one at a time. The sum of subtree heights is

O (n)

, so construction costs

Θ (n)

. Then perform

i

minimum extractions: output the root, move the last remaining entry to the root, and sift it down to restore the heap order.

Each extraction returns the smallest remaining key, so the outputs are the

i

smallest keys in increasing order. For a heap of current size

s

, an extraction takes

O (lo g (s + 1))

time. Hence

T_{2} (n, i) = O (n + \sum_{j = 0}^{i - 1} lo g (n - j + 1)) = O (n + i lo g n) .

The tight worst-case bound for this ordinary binary heap implementation is

T_{2} (n, i) = Θ (n + i lo g n) .

When the extraction term is substantial, worst-case extractions follow root-to-leaf paths of logarithmic length; when

i

is small, the linear construction already dominates. The bound stays valid at

i = n

, since

lo g (n!) = Θ (n lo g n)

. Building by

n

separate insertions would lose the linear construction bound and is unnecessary.

Past exam of the year 1 of the computer science course of the University of Oxford / 2013 / Functional programming, design and analysis of algorithms / 6 / c / i / Solution by

Codex  0 2026-10-31

Assume

1 \leq i \leq n

. Apply a worst-case

Θ (n lo g n)

comparison sort, such as merge sort or heapsort, to the whole array, then copy its first

i

entries to the output. The copying costs

Θ (i)

, so

T_{1} (n, i) = Θ (n lo g n + i) = Θ (n lo g n) (n \geq 2) .

The comparison sorting lower bound makes the full-sort stage tight. For the sample array, the sorted order begins

2, 6, 7

, which is the required prefix for

i = 3

. This method spends time ordering all

n - i

unreported elements as well.

Past exam of the year 1 of the computer science course of the University of Oxford / 2013 / Functional programming, design and analysis of algorithms / 2 / e / ii / Solution by

Codex  0 2026-10-31

Write

S_{j} = ℓ_{1} + \dots + ℓ_{j}

, with

S_{0} = 0

. At the

j

th step of the left fold, the left operand of list concatenation is the accumulated prefix of length

S_{j - 1}

. Fully forcing these concatenations repeatedly copies earlier elements. Including the traversal of the outer list and the whole output spine gives

T_{left} = Θ (k + N + j = 1 \sum k - 1 S_{j}) = Θ (k + N + t = 1 \sum k - 1 (k - t) ℓ_{t}) .

For singleton inner lists, this becomes

Θ (1 + 2 + \dots + (k - 1)) = Θ (k^{2})

, whereas the right fold takes

Θ (k)

. More generally, for equal positive length

r

, the left fold takes

Θ (r k^{2} + k)

O (k N + k)

bound is tight in the worst case over length distributions, but is not a tight formula for every distribution: if all

N

elements occur only in the final inner list, all earlier accumulators are empty and the cost is

Θ (k + N)

. Lazy evaluation changes when the work happens; it does not remove repeated prefix traversal when the whole result is demanded.

Past exam of the year 1 of the computer science course of the University of Oxford / 2013 / Functional programming, design and analysis of algorithms / 2 / e / i / Solution by

Codex  0 2026-10-31

Let there be

k

inner lists, of lengths

ℓ_{1}, \dots, ℓ_{k}

, and let

N = \sum_{j} ℓ_{j}

. Evaluate the whole output list spine, taking each input element as an already available value. The defining equation (x:xs) ++ ys = x : (xs ++ ys) shows that list concatenation traverses its left operand, sharing its right operand.

The right fold puts each original inner list on the left of exactly one concatenation. Thus its total element traversal is proportional to

N

, and visiting the outer list costs

k

T_{right} = Θ (k + N) .

The

k

term matters when many inner lists are empty. With

k

rows each of length

r

, the bound is

Θ (k + k r)

. In particular, with uniformly bounded positive row length it is linear in

k

Past exam of the year 1 of the computer science course of the University of Oxford / 2013 / Functional programming, design and analysis of algorithms / 1 / b / ii / Solution by

Codex  0 2026-10-31

Both uses of x in this definition have the same monomorphic type within the body. Write x :: u -> v. The inner application x z forces z :: u and has type v; the outer application x (x z) forces v = u. Thus x :: u -> u. Finally, x (x z) is applied to y, so u must itself be a function type, say a -> b. This gives

f :: ((a -> b) -> a -> b) -> a -> (a -> b) -> b
f x y z = x (x z) y

The principal type is therefore

((α \to β) \to (α \to β)) \to α \to (α \to β) \to β .

The argument x transforms a function into another function of the same type. The body transforms z twice, then applies the resulting function to y; no recursive type equation is required.

Past exam of the year 1 of the computer science course of the University of Oxford / 2013 / Functional programming, design and analysis of algorithms / 1 / b / i / Solution by

Codex  0 2026-10-31

In the type signature map :: (u -> v) -> [u] -> [v], the supplied function is concat :: [[a]] -> [a]. Type inference therefore identifies u with [[a]] and v with [a]. Consequently,

map concat :: [[[a]]] -> [[a]]

Thus

[[[α]]] \to [[α]]

is the principal type. For example, map concat [[[1],[2,3]],[[4],[]]] gives [[1,2,3],[4]]: it concatenates each inner group, preserving the outermost grouping.

Past exam of the year 1 of the computer science course of the University of Oxford / 2013 / Discrete mathematics, probability and continuous mathematics / 9 / b / ii / Solution by

Codex  0 2026-10-31

Let

W = U^{2}

. On

0 \leq U \leq 1

, squaring preserves order. Therefore for

0 \leq w \leq 1

F_{W} (w) = P (U^{2} \leq w) = P (U \leq w) = w .

Including the tails gives the cumulative distribution function

F_{W} (w) = ⎩ ⎨ ⎧ 0 w 1 w < 0, 0 \leq w \leq 1, w > 1.

Differentiating on the interior of the support gives the probability density function

f_{W} (w) = ⎩ ⎨ ⎧ \frac{1}{2 w} 0 0 < w < 1, otherwise .

(3)

The divergence near zero is integrable:

\int_{0}^{1} (2 w)^{- 1} d w = 1

. There is no point mass at zero, and the assigned value of a probability density function at a single endpoint does not affect the probability distribution.

Past exam of the year 1 of the computer science course of the University of Oxford / 2013 / Discrete mathematics, probability and continuous mathematics / 9 / b / i / Solution by

Codex  0 2026-10-31

Assume

a < b

. An increasing affine map sends the two endpoints to zero and one when

c a + d = 0

and

c b + d = 1

. Solving gives

c = \frac{1}{b - a}, d = - \frac{a}{b - a} .

Indeed, for

0 \leq t \leq 1

, the cumulative distribution function of the transformed random variable is

P (\frac{V - a}{b - a} \leq t) = P (V \leq a + (b - a) t) = \frac{a + ( b - a ) t - a}{b - a} = t,

which is the cumulative distribution function of the continuous uniform distribution on

[0, 1]

A decreasing affine map works too, by swapping the endpoints:

c = - \frac{1}{b - a}, d = \frac{b}{b - a} .

(3)

These are the two possible choices, since the image interval must have endpoints zero and one. The case

a = b

cannot be transformed into a nondegenerate continuous uniform distribution by deterministic constants.

Past exam of the year 1 of the computer science course of the University of Oxford / 2013 / Discrete mathematics, probability and continuous mathematics / 9 / a / ii / Solution by

Codex  0 2026-10-31

The factor

2 x - x^{3} = x (2 - x^{2})

is positive on

(0, 2)

and negative on

(2, 2)

. For every nonzero

α

, the proposed probability density function is therefore negative on an interval. The choice

α = 0

has total integral zero. In fact,

\int_{0}^{2} (2 x - x^{3}) d x = [x^{2} - \frac{x ^{4}}{4}]_{0}^{2} = 0,

so no scaling could normalise it even without the sign obstruction. Consequently

No value of α gives a probability density function; no corresponding expectation exists .