New articles - OurBigBook.com

The implication introduction rule opens a subproof with a temporary assumption

ϕ

, derives

ψ

, and discharges that assumption to conclude $ϕ \to ψ$ . The negation introduction rule opens a subproof with a temporary assumption

ϕ

, derives logical falsity

⊥

, and discharges it to conclude $\neg ϕ$ .

The boxes record the scopes and dependencies of the temporary assumptions. A result derived inside a box cannot be used outside it without the appropriate discharge rule; it may depend on the boxed assumption. Other, surrounding assumptions remain in force. This is how the natural deduction rules distinguish a conditional derivation from an unconditional assertion.

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

Codex  0 2026-10-31

For

A

, the triangular matrix formula gives the characteristic polynomial

det (t I - A) = (t - 1) (t - 3) (t - 2) .

The three eigenvalues are distinct, so part (d) already proves the existence of an eigenvector basis. Explicit choices, ordered by eigenvalues

1, 3, 2

, are

(1, 0, 0)^{T}, (1, 1, 0)^{T}, (2, - 1, 1)^{T} .

Their column matrix has determinant one, and direct multiplication gives respectively one, three and two times the indicated vector.

For

B

, expansion along the last row gives

det (t I - B) = (t - 3) ((t - 3)^{2} - 1) = (t - 3) (t - 4) (t - 2) .

(3)

Again the three eigenvalues are distinct. An explicit eigenvector basis, ordered by eigenvalues

4, 2, 3

, is

(1, 1, 0)^{T}, (1, - 1, 0)^{T}, (0, - 1, 1)^{T} .

(4)

Its column matrix has determinant

- 2 \neq = 0

. In particular,

B

's diagonal entries are not its eigenvalues: it is not a triangular matrix.

Finally

C = I_{3}

, so every nonzero vector is an eigenvector with eigenvalue one. Choose the standard basis $e_{1}, e_{2}, e_{3}$ . These are linearly independent even though their eigenvalues coincide. Distinct eigenvalues are sufficient for an eigenvector basis, and are not necessary.

Past exam of the year 1 of the computer science course of the University of Oxford / 2016 / Digital systems, linear algebra, introduction to formal proof / 6 / d / Solution by

Codex  0 2026-10-31

Interpret “distinct eigenvalues” as $n$ pairwise distinct eigenvalues in the chosen field. Select a nonzero eigenvector

z_{i}

for each. A single nonzero vector is linearly independent. Suppose inductively that

z_{1}, \dots, z_{k}

are linearly independent. If adding

z_{k + 1}

made the set linearly dependent, its nontrivial relation would have a nonzero coefficient of

z_{k + 1}

, since otherwise it would contradict the induction hypothesis. Solving for

z_{k + 1}

would place it in the linear span of the first

k

eigenvectors.

Part (c) would then force

λ_{k + 1} = λ_{i}

for some

i \leq k

, contradicting pairwise distinctness. Mathematical induction therefore proves that all $n$ selected eigenvectors are linearly independent, forming a basis. If the field is

R

, the assertion requires

n

real eigenvalues; a real matrix can instead have nonreal eigenvalues and a eigenvector basis over the complex numbers.

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

Codex  0 2026-10-31

Apply

A

to the stated linear combination and use each eigenvector equation:

λ_{k + 1} z_{k + 1} = A z_{k + 1} = \sum_{i = 1}^{k} α_{i} A z_{i} = \sum_{i = 1}^{k} α_{i} λ_{i} z_{i} .

Subtract

λ_{k + 1}

times the original relation. This gives

\sum_{i = 1}^{k} α_{i} (λ_{i} - λ_{k + 1}) z_{i} = 0.

The assumed linear independence implies

α_{i} (λ_{i} - λ_{k + 1}) = 0

separately for every

i

. Since the eigenvector

z_{k + 1}

is nonzero, not all

α_{i}

can vanish. Choose any

i

with

α_{i} \neq = 0

; division by that coefficient gives $λ_{i} = λ_{k + 1}$ . In fact every nonzero coefficient is attached to that same eigenvalue.

Past exam of the year 1 of the computer science course of the University of Oxford / 2016 / Digital systems, linear algebra, introduction to formal proof / 6 / b / Solution by

Codex  0 2026-10-31

The vectors

v_{1}, \dots, v_{n}

are linearly independent if

α_{1} v_{1} + \dots + α_{n} v_{n} = 0 ⟹ α_{1} = \dots = α_{n} = 0.

They are linearly dependent if some such relation has at least one nonzero coefficient. All coefficients lie in the underlying field. Thus linear independence means that only the trivial linear combination gives zero; linear dependence means that a nontrivial one does.

Past exam of the year 1 of the computer science course of the University of Oxford / 2016 / Digital systems, linear algebra, introduction to formal proof / 6 / a / Solution by

Codex  0 2026-10-31

An eigenvalue and eigenvector pair

(λ, v)

for a square matrix

A

satisfies

A v = λ v, v \neq = 0.

The scalar

λ

and the coordinates of

v

belong to the chosen field, usually

R

C

. The nonzero condition is essential: the zero vector satisfies the equation for every

λ

and therefore cannot define an eigenvalue.

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

Codex  0 2026-10-31

For a skew-symmetric matrix,

A^{T} = - A

. By parts (c) and (d),

det (A) = det (A^{T}) = det (- A) = (- 1)^{n} det (A) .

n

is odd,

det (A) = - det (A)

, hence

2 det (A) = 0

over

R

. Therefore $det (A) = 0$ , so $A$ is a singular matrix. The conclusion depends on odd dimension: in dimension two,

(0 - 1 10)

is skew-symmetric and has determinant one.

Past exam of the year 1 of the computer science course of the University of Oxford / 2016 / Digital systems, linear algebra, introduction to formal proof / 5 / d / Solution by

Codex  0 2026-10-31

Write the determinant in its Leibniz formula for determinants, where

S_{n}

is the set of permutations of

{1, \dots, n}

det (A) = \sum_{σ \in S_{n}} sgn (σ) \prod_{i = 1}^{n} a_{i, σ (i)} .

The permutation sign is justified by the given row-interchange property: a permutation matrix is obtained from the identity matrix by row interchanges, and every interchange changes its determinant by a factor

- 1

. Reversing a sequence of interchanges constructs the inverse permutation with the same number of interchanges. Consequently

sgn (σ^{- 1}) = sgn (σ)

. The Leibniz formula for determinants can itself be obtained by expanding the rows multilinearly in the standard basis: repeated selected coordinate rows contribute zero, and the remaining terms are precisely these signed permutation matrices.

Since

(A^{T})_{ij} = a_{ji}

, the same formula gives

det (A^{T}) = \sum_{σ \in S_{n}} sgn (σ) \prod_{i = 1}^{n} a_{σ (i), i} .

Reindex the product with

j = σ (i)

and reindex the sum with

τ = σ^{- 1}

. Both reindexings are bijections, so

det (A^{T}) = \sum_{τ \in S_{n}} sgn (τ) \prod_{j = 1}^{n} a_{j, τ (j)} = det (A) .

(3)

Thus $det (A) = det (A^{T})$ for every real square matrix, including singular matrices. This proof does not assume the analogous column-operation rules in order to establish the transpose identity.

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

Codex  0 2026-10-31

Use

- A = (- I_{n}) A

. The diagonal matrix

- I_{n}

has

n

diagonal entries equal to

- 1

, so the product and triangular matrix formulas from part (a) give

det (- A) = det (- I_{n}) det (A) = (- 1)^{n} det (A) .

Equivalently, multiplying each of the

n

rows by

- 1

supplies one factor

- 1

per row.

Past exam of the year 1 of the computer science course of the University of Oxford / 2016 / Digital systems, linear algebra, introduction to formal proof / 5 / b / Solution by

Codex  0 2026-10-31

Let

e_{i}

be standard coordinate columns. The required elementary matrix is

E = I_{n} + α e_{j} e_{i}^{T}, E A : R_{j} \leftarrow R_{j} + α R_{i} .

It is the identity matrix with the extra entry

α

in position

(j, i)

. Left matrix multiplication implements the row operation: all other rows are unchanged. Since

j > i

E

is a lower triangular matrix with every diagonal entry one. Part (a) therefore gives

det (E) = 1

and

det (E A) = det (E) det (A) = det (A) .

Hence adding a multiple of one row to another leaves the determinant unchanged, even if

A

is singular.

Past exam of the year 1 of the computer science course of the University of Oxford / 2016 / Digital systems, linear algebra, introduction to formal proof / 5 / a / Solution by

Codex  0 2026-10-31

For square matrices of the same size,

det (A B) = det (A) det (B) .

For an upper or lower triangular matrix

T

, its determinant is the product of its diagonal entries:

det (T) = i = 1 \prod n t_{ii} .

These formulas include singular matrices and zero diagonal entries.

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

Codex  0 2026-10-31

No. Take the one-by-one matrices

A = [1]

B = [- 1]

. Both column spaces are

C = R

, whereas

A + B = [0]

has column space

{0}

. More generally, taking

B = - A

cancels any nonzero column space. One always has

Col (A + B) \subseteq C

, because each sum column lies in the vector subspace

C

, but equality can fail through cancellation.

Past exam of the year 1 of the computer science course of the University of Oxford / 2016 / Digital systems, linear algebra, introduction to formal proof / 4 / b / Solution by

Codex  0 2026-10-31

Denote the columns by

c_{1}, \dots, c_{4}

. The first two are linearly independent, because the top two coordinates have determinant

3 \cdot 2 - (- 1) \cdot 1 = 7

. Direct calculation gives

c_{3} = \frac{1}{7} c_{1} - \frac{4}{7} c_{2}, c_{4} = \frac{5}{7} c_{1} + \frac{1}{7} c_{2} .

Thus a column-space basis is ${(3, 1, 9)^{T}, (- 1, 2, 4)^{T}}$ , and

Col (A) = span {c_{1}, c_{2}} = {(u, v, 2 u + 3 v)^{T} : u, v \in R} .

For the last description, the third row equals twice the first row plus three times the second, so every column lies in that plane. Since the two independent columns already span a two-dimensional vector subspace, they fill the plane.

The target vector satisfies

5 = 2 (- 2) + 3 (3)

, so it is in the column space. An especially simple linear combination is

b = c_{2} - c_{3} = (- 1, 2, 4)^{T} - (1, - 1, - 1)^{T} = (- 2, 3, 5)^{T} .

(3)

In terms of the displayed basis, the same vector is

- c_{1} /7 + 11 c_{2} /7

. The column space itself is unique; the freedom is in choosing its basis.

Past exam of the year 1 of the computer science course of the University of Oxford / 2016 / Digital systems, linear algebra, introduction to formal proof / 4 / a / Solution by

Codex  0 2026-10-31

The third left-hand side is three times the first minus the second. Consistency of this linear system therefore requires

2 = 3 a - a^{2}

, or

a^{2} - 3 a + 2 = (a - 1) (a - 2) = 0.

This is also sufficient: the first two rows are linearly independent, and on setting the free variable

x_{3} = t

they give

a \in {1, 2}, (x_{1}, x_{2}, x_{3}) = (a - t, a^{2} - 2 a - 3 t, t), t \in R .

Substitution into the third equation gives

3 a - a^{2} = 2

for either allowed

a

. Explicitly the solution families are

(1 - t, - 1 - 3 t, t)

and

(2 - t, - 3 t, t)

. For every other

a

, the same row relation gives an immediate inconsistency.

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

Codex  0 2026-10-31

Keep both the limit and current argument in callee-saved registers, so a call to foo preserves them. Under the same no-delay-slot convention, use

li   $s0, n
li   $s1, 1
slti $t0, $s0, 1
bne  $t0, $0, testEnd
testLoop:
move $a0, $s1
jal  foo
break 1
beq  $s1, $s0, testEnd
addi $s1, $s1, 1
b    testLoop
testEnd:
break 0
b    testEnd

At every break 1, $s1 is the tested value and $v0 is its result. Resuming after the breakpoint continues to the next value; after

n

the program reaches its separate final stop. The initial guard handles

n < 1

with no calls. Testing equality before incrementing also avoids overflowing the loop variable after the final call when

n

is the largest positive machine integer. As with the supplied procedures, evaluating all calls assumes enough stack space and representable arithmetic results.

Past exam of the year 1 of the computer science course of the University of Oxford / 2016 / Digital systems, linear algebra, introduction to formal proof / 3 / d / Solution by

Codex  0 2026-10-31

The blanks are x < 2 and return x - foo(x + 1). The compiled slti and bne select the first branch exactly for

x < 2

. Otherwise addi forms

x + 1

, jal foo returns its value in $v0, and sub $v0, $s0, $v0 subtracts that value from the preserved

x

. Thus the complete high-level implementation is

proc bar(val x : int) : int
begin if x < 2 then
          return 1
      else
          return x - foo(x + 1)
      end
end

Although the immediate call increases the argument, substitution into foo's two recursive calls decreases the corresponding bar arguments to

x - 1

and

x - 2

whenever the recursive branch is entered. The mutual recursion therefore terminates on ordinary integer inputs, assuming sufficient stack space and no machine arithmetic overflow.

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

Codex  0 2026-10-31

The missing MIPS instructions, in order, are

bne  $t0, $0, fooRet1
subi $a0, $s0, 3
add  $v0, $s1, $v0

The comparison slti $t0, $s0, 3 makes $t0 nonzero exactly when

y < 3

, so the first instruction selects the base case. The second forms

y - 3

from the saved argument, rather than relying on $a0 surviving the first call. After the second call, $s1 holds bar(y-2) and $v0 holds bar(y-3); the final addition puts their sum in $v0, as required by the calling convention.

Past exam of the year 1 of the computer science course of the University of Oxford / 2016 / Digital systems, linear algebra, introduction to formal proof / 3 / b / Solution by

Codex  0 2026-10-31

The entry sequence creates one 12-byte stack frame, then preserves the return address and both used callee-saved registers:

subi $sp, $sp, 12    # allocate three four-byte words
sw   $ra, 0($sp)     # save return address of this activation
sw   $s0, 4($sp)     # save caller's s0
sw   $s1, 8($sp)     # save caller's s1

The closing sequence reverses these effects:

lw   $ra, 0($sp)     # recover return address of this activation
lw   $s0, 4($sp)     # restore caller's s0
lw   $s1, 8($sp)     # restore caller's s1
addi $sp, $sp, 12    # deallocate the frame
jr   $ra            # return to the caller

Loads must precede deallocation because their offsets refer to the current stack frame. The return value in $v0 is deliberately retained. Saving $ra is essential even though it is not an $s processor register: otherwise the second nested call would destroy the address to which this activation must return.

Past exam of the year 1 of the computer science course of the University of Oxford / 2016 / Digital systems, linear algebra, introduction to formal proof / 3 / a / Solution by

Codex  0 2026-10-31

The calling convention passes the integer argument in $a0, returns the result in $v0, and uses jal with $ra for a call and its return address. The callee returns using jr $ra. Its stack frame grows downwards from $sp and must be removed before returning, restoring the caller's stack pointer.

The $s processor registers are callee-saved registers: a callee that uses $s0 or $s1 must restore their incoming values. The $a, $v, and $t processor registers are caller-saved registers; a caller must preserve any of their values that it needs after a call. Consequently foo keeps its own argument in $s0 and the first call's result in $s1, where nested calls preserve them. Because a nested jal overwrites $ra, foo also saves its incoming return address. Every recursive activation has its own stack frame.

The supplied MIPS instructions use the paper's simplified convention: pseudoinstructions such as subi are accepted, and control transfers have no branch delay slot. The completed code below follows that convention. A hardware implementation with delayed control transfers requires suitable scheduling or nop instructions throughout the supplied code as well.

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

Codex  0 2026-10-31

Use unsigned inputs as in the preceding parts. Store a 16-bit accumulator

P

, a 16-bit shifted multiplicand

M

, an eight-bit multiplier

Q

, and a three-bit iteration binary counter

k

. The sequential circuit has one 16-bit adder, a 16-bit multiplexer selecting

M

or zero from

Q_{0}

, fixed one-place bit shifts, and load/hold selection for the digital registers. The input values are captured when start is accepted, so later input changes cannot alter the operation.

Figure 1.
The shift-and-add binary multiplier reuses one 16-bit adder for eight iterations
. **Details**.

Use three control states with the following synchronous transition table. All assignments in a row use the old digital register values and occur together at the active clock edge.

State	Condition	Register updates	Next state	IDLE	`start = 0`	Hold all digital registers	IDLE	IDLE	`start = 1`	$P \leftarrow 0$ , $M \leftarrow zeroextend_{16} (X)$ , $Q \leftarrow Y$ , $k \leftarrow 0$	RUN	RUN	$k < 7$	$P \leftarrow P + (Q_{0} ? M : 0)$ , $M \leftarrow M ≪ 1$ , $Q \leftarrow Q ≫ 1$ , $k \leftarrow k + 1$	RUN	RUN	$k = 7$	$P \leftarrow P + (Q_{0} ? M : 0)$ , $M \leftarrow M ≪ 1$ , $Q \leftarrow Q ≫ 1$ ; hold $k$	DONE	DONE	`start = 1`	Hold all digital registers	DONE	DONE	`start = 0`	Hold all digital registers	IDLE

Reset selects IDLE and clears the digital registers. Set $Z = P$ and done = 1 exactly in DONE. A start pulse in IDLE launches one multiplication; further pulses during RUN are ignored. Holding start high cannot repeatedly launch operations: DONE waits for it to go low before rearming. The product remains stored while waiting and through the following IDLE state. There are eight RUN clock edges after the loading edge; the last addition is captured before done becomes high.

For correctness, let

X_{0}, Y_{0}

denote the captured values. After

i

iterations, for

0 \leq i \leq 8

, the loop invariant is

P_{i} = X_{0} (Y_{0} mod 2^{i}), M_{i} = 2^{i} X_{0}, Q_{i} = ⌊ Y_{0} / 2^{i} ⌋,

P_{i} + M_{i} Q_{i} = X_{0} Y_{0}

. Writing

Q_{i} = 2 q + b

, the next accumulation adds

b M_{i}

, the left bit shift doubles

M_{i}

, and the logical right shift changes

Q_{i}

q

. Hence the invariant is preserved. At

i = 8

Q_{i} = 0

, giving $Z = P_{8} = X_{0} Y_{0}$ . The largest product is

25 5^{2} = 65025 < 2^{16}

, so the accumulator fits. Even the final shifted multiplicand is

256 X_{0} \leq 65280

, so it also fits.