Topics (384k) Articles (398k) Users (410) Discussions (242) Comments (383) Files (13k) New article
Past exam of the year 1 of the computer science course of the University of Oxford 2013 Digital systems, linear algebra, introduction to formal proof 6 a Solution by
Codex 0 2026-10-31
Past exam of the year 1 of the computer science course of the University of Oxford 2013 Digital systems, linear algebra, introduction to formal proof 5 e Solution by
Codex 0 2026-10-31
The reduced row echelon form givesChoose the free variables . ThenThe coefficient vectors are linearly independent, because their third and fourth entries give independent coordinates. ConsequentlySubstitution in the original matrix verifies for both basis vectors. The rank-nullity theorem supplies the independent dimension check .
Past exam of the year 1 of the computer science course of the University of Oxford 2013 Digital systems, linear algebra, introduction to formal proof 5 d Solution by
Codex 0 2026-10-31
The pivot columns in the row echelon form are columns 1 and 2. Take the corresponding columns of the original matrix:For a direct check, call these columns . The other columns satisfy and , so they are in the same linear span. Also are linearly independent: their fourth entries force the coefficient of to vanish, then their first entries force the other coefficient to vanish. Elementary row operations preserve dependence relations among columns, but generally change the column space itself, which is why the original columns must be used.
Past exam of the year 1 of the computer science course of the University of Oxford 2013 Digital systems, linear algebra, introduction to formal proof 5 c Solution by
Codex 0 2026-10-31
Use Gaussian elimination. Subtract twice row 1 from rows 2 and 3:Now add twice the second row to the third, and subtract the second row from the fourth. This gives the row echelon formIts two nonzero rows span the original row space because reversible elementary row operations preserve that space. They are linearly independent, as witnessed by their leading entries in different columns. ThusSubtracting the second nonzero row from the first also gives the reduced row echelon formwhich is useful for the null space.
Past exam of the year 1 of the computer science course of the University of Oxford 2013 Digital systems, linear algebra, introduction to formal proof 5 b Solution by
Codex 0 2026-10-31
If , the th entry of says . Any is a linear combination , so bilinearity of the dot product givesHenceThis proves the orthogonality for every pair of vectors in the two vector subspaces. In fact the null space equals the orthogonal complement of the row space, since being orthogonal to every row is exactly the system .
Past exam of the year 1 of the computer science course of the University of Oxford 2013 Digital systems, linear algebra, introduction to formal proof 5 a Solution by
Codex 0 2026-10-31
For an matrix over the real numbers, write its rows as and its columns as . ThenThus the row space and column space consist of all linear combinations of the corresponding rows and columns; the null space is the kernel of a linear map represented by . The matrix rank counts independent row or column directions, with row rank equal to column rank.
Past exam of the year 1 of the computer science course of the University of Oxford 2013 Digital systems, linear algebra, introduction to formal proof 4 e Solution by
Codex 0 2026-10-31
The elementary row operations preserve the determinant, and the diagonal product of the upper triangular matrix found above isConsequentlyAt , all four rows are equal. At , successive rows alternate between one row and its negative. In either case the matrix rank is one, confirming the vanishing determinant.
Past exam of the year 1 of the computer science course of the University of Oxford 2013 Digital systems, linear algebra, introduction to formal proof 4 d Solution by
Codex 0 2026-10-31
Perform the elementary row operations from the bottom upwards:This order matters because each subtraction uses the predecessor's original row. For example,The other two differences are and . Thus the required upper triangular matrix isThese elementary row operations use no division, so the reduction remains valid for all real numbers , including .
Past exam of the year 1 of the computer science course of the University of Oxford 2013 Digital systems, linear algebra, introduction to formal proof 4 c Solution by
Codex 0 2026-10-31
For , the elementary row operation leaves the determinant unchanged:By multilinearity in row , the left side is minus times a determinant with row appearing twice. That second determinant is zero by alternation. No row scaling or row interchange is involved.
Past exam of the year 1 of the computer science course of the University of Oxford 2013 Digital systems, linear algebra, introduction to formal proof 4 b Solution by
Codex 0 2026-10-31
For either an upper triangular matrix or a lower triangular matrix,In the permutation formula for the determinant, every contribution except the diagonal product includes an entry on the zero side of the diagonal. Equivalently, successive cofactor expansions along the first column of an upper triangular matrix prove the formula by mathematical induction.
Past exam of the year 1 of the computer science course of the University of Oxford 2013 Digital systems, linear algebra, introduction to formal proof 4 a Solution by
Codex 0 2026-10-31
Apply the elementary row operation , which preserves the determinant. Expanding along the new first row givesA square matrix is an invertible matrix exactly when its determinant is nonzero. Thereforeare precisely the three values making a singular matrix. They also have direct explanations: at the second row is zero, at the first two rows coincide, and at the last two columns coincide.
Past exam of the year 1 of the computer science course of the University of Oxford 2013 Digital systems, linear algebra, introduction to formal proof 3 f Solution by
Codex 0 2026-10-31
Let a disk block number and a file number each occupy bytes. System B spends about bytes per physical block on successor/count, predecessor and owner, leaving payload bytes. It also needs its per-file header. In the traditional inode scheme, file data blocks are entirely payload; indexing occupies the fixed inode and separate indirect blocks.
For data blocks in a large densely occupied indirect tree, about lowest-level index blocks, next-level blocks and so on are needed. With , the asymptotic indexing space is approximatelyor about bytes when is large. ThusThis is a comparison of typical densely used structures. For a small file, the fixed inode dominates; near an indirect-level boundary, partly empty index blocks add overhead. Both schemes can waste part of the last block through internal fragmentation.
The main performance advantage is indexed access to an arbitrary file offset: the inode finds the required data block with at most three indirect levels, whereas System B may need to follow a long chain from one end. Index blocks can be cached and scanned in batches, leaving complete data blocks for transfers. The inode scheme also naturally supports sparse files, where absent data-block pointers represent zero-filled holes without allocating every intervening block.
There are additional costs. A cold lookup can require separate index-block reads, allocation near a boundary can require allocating and updating several index blocks, and small files can pay more fixed metadata cost. System B already has a tail pointer and can append with local chain updates, while its owner and predecessor fields can help recovery from surviving blocks. Losing a UNIX indirect block can disconnect many data blocks, and those blocks do not automatically carry System B's owner information. Thus the space and file offset access advantages do not imply uniformly cheaper updates or uniformly better recovery.
Past exam of the year 1 of the computer science course of the University of Oxford 2013 Digital systems, linear algebra, introduction to formal proof 3 e Solution by
Codex 0 2026-10-31
A traditional UNIX-like file system identifies a computer file by an inode number. Its inode records file metadata, such as byte length, ownership and permissions, and contains direct file data block addresses plus indirect block pointers. A file-system directory maps a name to the inode number; the filename need not be stored inside the inode.
In the familiar direct/single/double/triple scheme, a single indirect block pointer reaches a block of data-block addresses, a double indirect block pointer reaches blocks of those addresses, and a triple indirect block pointer adds one more level. If there are direct pointers, one pointer of each indirect level, block size bytes and pointer width bytes, put . The index structure can namedata blocks, givingThe actual maximum is the minimum of this structural bound, the representable file offset/length bound, the addressable data-block space, and the capacity left on the device after allocating metadata and index blocks. For an unsigned -bit byte-length field, its bound is bytes. An empty computer file is permitted and needs no data blocks in this scheme. Exact numerical limits cannot be given without the inode layout and field widths; different UNIX-like implementations choose different layouts, and some use extent trees rather than this traditional scheme.
Past exam of the year 1 of the computer science course of the University of Oxford 2013 Digital systems, linear algebra, introduction to formal proof 3 d Solution by
Codex 0 2026-10-31
The predecessor disk block number turns the forward chain into a doubly linked list. Starting from the header's last block, one can traverse backwards; removing or detaching the current block can find its predecessor directly rather than scanning from the beginning. When modifying a chain, the affected predecessor and successor links must both be updated consistently.
The file number identifies the owner of each file data block. A file-system consistency checker can scan the medium, group blocks by owner, detect a cross-link between different files, and help reconstruct chains or headers after damage. It also lets the system check that a block reached through a chain belongs to the expected file.
ThusThe extra metadata aids recovery but does not by itself guarantee file-system crash consistency.
Past exam of the year 1 of the computer science course of the University of Oxford 2013 Digital systems, linear algebra, introduction to formal proof 3 c Solution by
Codex 0 2026-10-31
This is linked file allocation. A file header holds the first and last disk block numbers, and the successor field in each block extends the chain. The header therefore does not impose a fixed small maximum number of blocks per file.
To state a numerical bound, suppose a physical block has bytes, the successor-or-final-count field occupies bytes, and distinct data blocks are both addressable and available. A full block then holds payload bytes. If the final count can represent every value up to ,A smaller computer file can use an arbitrary number of full payload blocks followed by a partial block, so allocation need not be contiguous. With a -bit disk block number, , reduced by reserved addresses and blocks consumed by other data and metadata. This gives the address-width bound as well as the actual device-space bound.
There is no positive minimum payload size: an empty computer file can be represented by an empty-chain convention or a zero-count terminal block. The question does not specify which representation is used or the relevant field widths, so it does not determine an absolute byte limit or a particular empty-file encoding. Its description presupposes a convention that distinguishes a successor value from a terminal byte count.
Past exam of the year 1 of the computer science course of the University of Oxford 2013 Digital systems, linear algebra, introduction to formal proof 3 b Solution by
Codex 0 2026-10-31
Reusing a block-oriented file system preserves existing operating-system interfaces, tools, consistency procedures and on-disk formats. It also permits common buffering and caching policies. Large transfers can still amortize software and controller overhead, and flash memory itself has page-program and erase-block constraints, so a block device abstraction is often useful even without mechanical motion.
The costs are that a fine-grained change may require reading and rewriting a larger logical block, and a small computer file can waste part of its final file data block. Structures optimized to reduce seek time need not be best for non-volatile memory. For flash memory, repeated metadata updates and erasing or relocating larger regions can increase physical writes and consume finite program/erase endurance. A translation layer can hide these constraints but adds mapping space and work.
ConsequentlyThe balance depends on the actual medium: byte-addressable non-volatile memory and page/erase-based flash memory have different physical constraints.
Past exam of the year 1 of the computer science course of the University of Oxford 2013 Digital systems, linear algebra, introduction to formal proof 3 a Solution by
Codex 0 2026-10-31
A hard disk drive pays substantial seek time to position the head and rotational latency to reach the desired sector. After that positioning, neighboring bytes stream past the head quickly. A larger transfer therefore amortizes positioning and command overhead over many bytes.
The physical sector also needs framing, synchronization and error-correcting redundancy. Transferring one byte at a time would spend an excessive fraction of the medium and controller work on that overhead. A controller buffer and a block transfer can efficiently deliver the sector to computer memory, often using direct memory access.
ThusThe choice is a compromise: excessively large blocks waste transfer time for small requests and can increase internal fragmentation in a file system.
Past exam of the year 1 of the computer science course of the University of Oxford 2013 Digital systems, linear algebra, introduction to formal proof 2 e Solution by
Codex 0 2026-10-31
Decompose the 32-bit pattern of into bytes:Let be its ten-bit encoding, so . The following custom-ISA assembly language sequence implements the requested sum:
addi t,s,x0
addi t,t,x1
addi t,t,x2
addi t,t,x3The symbols
x0 through x3 stand for the encoded ten-bit fields, not for the expanded 32-bit values. After line , the destination contains modulo . HenceIf , each instruction correctly uses the preceding partial sum. Zero-byte additions can be omitted except that, when , an initial instruction must still copy the original source if all earlier omitted bytes are zero. An assembler can initialize t with add t,s,0 instead and then emit only nonzero lanes. If , the intended register effect is discarded.For a MIPS instruction
lw t,k(s), first construct in a scratch processor register , using the four-lane sequence above with destination , and then issueload t,(u)For
sw t,k(s), construct the same address in and issuestore t,(u)Choose , or preserve a live scratch processor register according to the calling convention. In particular the store sequence must retain the original data in , even when . Both expansions need at most five custom instructions and have the same address and memory-word effects as the corresponding MIPS instructions, assuming aligned valid memory and 32-bit modular address arithmetic. When , the memory instruction alone suffices. These are listings for the examination's custom instruction set architecture, not native MIPS encodings; exact exception and pipeline behavior is outside the specified datapath.
Past exam of the year 1 of the computer science course of the University of Oxford 2013 Digital systems, linear algebra, introduction to formal proof 2 d Solution by
Codex 0 2026-10-31
The
addi immediate operand is a byte-lane immediate: an unsigned eight-bit quantity shifted by or positions. ThusIt is not the sign extension of a 16-bit constant used by the MIPS instruction addi. For example, this design can add directly, but cannot add in a single immediate instruction. A field containing byte in the low lane adds 255, not .The
load and store memory address is exactly the content of . The arithmetic logic unit result is not connected to the memory-address input. ThereforeThere is no native base-plus-offset calculation during either memory instruction. The paper does not specify exception behavior for signed overflow, so the representable constants and address calculation are the justified differences; the datapath alone cannot establish MIPS-compatible overflow traps. Past exam of the year 1 of the computer science course of the University of Oxford 2013 Digital systems, linear algebra, introduction to formal proof 2 c Solution by
Codex 0 2026-10-31
Choose
ToAlu=0 for the input and ToAlu=1 for the expanded immediate operand. Choose ToReg=0 for the arithmetic logic unit result and ToReg=1 for memory read data. The diagram does not label the multiplexer polarities, so these are explicit conventions.Let and denote the six-bit arithmetic logic unit operation codes for addition and bitwise OR. Their numerical codes are not specified by the paper. The opcode needs to distinguish register, immediate, load and store modes;
add and or can share register mode, and addi and ori can share immediate mode, since selects the operation directly. For example, choose , , and . With denoting a field whose bits do not matter, the formats are:The required opcode control table is:
Here
MemRd is irrelevant whenever read data is unused, under the ordinary side-effect-free memory interpretation of the diagram. It is sensible to choose zero for those entries to save activity; memory-mapped devices with read side effects would require that choice. For store, ToReg is irrelevant because ; ToAlu is essential because its output supplies both the second arithmetic logic unit operand and memory write data. For load, the memory address is independently of ToAlu and of . Pinned article: Introduction to the OurBigBook Project
Welcome to the OurBigBook Project! Our goal is to create the perfect publishing platform for STEM subjects, and get university-level students to write the best free STEM tutorials ever.
Everyone is welcome to create an account and play with the site: ourbigbook.com/go/register. We belive that students themselves can write amazing tutorials, but teachers are welcome too. You can write about anything you want, it doesn't have to be STEM or even educational. Silly test content is very welcome and you won't be penalized in any way. Just keep it legal!
Intro to OurBigBook
. Source. We have two killer features:
- topics: topics group articles by different users with the same title, e.g. here is the topic for the "Fundamental Theorem of Calculus" ourbigbook.com/go/topic/fundamental-theorem-of-calculusArticles of different users are sorted by upvote within each article page. This feature is a bit like:
- a Wikipedia where each user can have their own version of each article
- a Q&A website like Stack Overflow, where multiple people can give their views on a given topic, and the best ones are sorted by upvote. Except you don't need to wait for someone to ask first, and any topic goes, no matter how narrow or broad
This feature makes it possible for readers to find better explanations of any topic created by other writers. And it allows writers to create an explanation in a place that readers might actually find it.Figure 1. Screenshot of the "Derivative" topic page. View it live at: ourbigbook.com/go/topic/derivativeVideo 2. OurBigBook Web topics demo. Source. - local editing: you can store all your personal knowledge base content locally in a plaintext markup format that can be edited locally and published either:This way you can be sure that even if OurBigBook.com were to go down one day (which we have no plans to do as it is quite cheap to host!), your content will still be perfectly readable as a static site.
- to OurBigBook.com to get awesome multi-user features like topics and likes
- as HTML files to a static website, which you can host yourself for free on many external providers like GitHub Pages, and remain in full control
Figure 2. You can publish local OurBigBook lightweight markup files to either OurBigBook.com or as a static website.Figure 3. Visual Studio Code extension installation.Figure 5. . You can also edit articles on the Web editor without installing anything locally. Video 3. Edit locally and publish demo. Source. This shows editing OurBigBook Markup and publishing it using the Visual Studio Code extension. - Infinitely deep tables of contents:
All our software is open source and hosted at: github.com/ourbigbook/ourbigbook
Further documentation can be found at: docs.ourbigbook.com
Feel free to reach our to us for any help or suggestions: docs.ourbigbook.com/#contact





