The question this layer answers
What can be represented, proved, or computed?
The language of structure. This layer connects Logic, Graphs, Matrices, Probability, Proof to the rest of the computing stack.
A model is a choice about what matters
Suppose a library owns one copy of a book. Two readers want to reserve it. Before choosing a language, specify the state: holder is either a reader identifier or none. The operation reserve(reader) succeeds only when holder = none. On success it sets holder = reader; otherwise it leaves the state unchanged and reports a conflict. This tiny specification already tells us more than “build a reservation app.” It names the possible states, legal changes, and observable outcomes.
An invariant is a property every reachable state must satisfy. Here it is “at most one reader holds this copy.” It is not enough to draw a happy path. List the initial state and every operation that can change it. A cancellation must check who owns the reservation. A return operation must not accidentally clear somebody else's later reservation. Operations outside the model are a common source of broken guarantees.
Prove something small, completely
Consider this program over nonnegative integers:
total = 0
i = 1
while i <= n:
total = total + i
i = i + 1
return total
At each loop check, use the invariant total = 1 + … + (i − 1) and 1 ≤ i ≤ n + 1. Initially the sum is empty, so it is zero. An iteration adds i, then increments i; the same equation holds with the new value. The nonnegative quantity n − i + 1 decreases by one on every executed iteration, so the loop terminates. At exit, i = n + 1, and the invariant gives the sum from 1 through n. Initialization, preservation, termination, and the exit condition each do a different job.
For n = 3, the states at the loop check are:
| i | total | Continue? |
|---|
| 1 | 0 | Yes |
| 2 | 1 | Yes |
| 3 | 3 | Yes |
| 4 | 6 | No |
The proof assumes mathematical integers. A fixed-width machine integer can overflow. A proof about one arithmetic model is not automatically a proof about another. State assumptions beside your result.
Claims, examples, and limits
Testing n = 3 confirms one execution. It does not establish the universal claim. Conversely, one legal input that fails is enough to disprove that claim. Try removing the increment: the sum relationship no longer advances to the required exit, and positive inputs do not terminate. “Nothing bad happens” and “something useful eventually happens” are different obligations.
For the library, an invariant argument still depends on whether reservation is indivisible. Two concurrent callers can both observe none. Later chapters will give us synchronization and transactions to make that assumption real. Mathematics helps identify the promise; systems engineering must enforce it.
Before moving on: write a precondition, a postcondition, and an invariant for cancelling a reservation. Include a request from the wrong reader. Then complete the state-machine lab below.
Continuous change and accumulation
Some computer science uses continuous models even though the implementation stores finite representations. The final studies in this section derive derivatives, gradients, the chain rule, definite integrals, and numerical approximation. These tools support optimization in machine learning, physical simulation, and quantitative error analysis. Keep a mathematical statement about a real-valued function separate from the behavior of its floating-point implementation.
Work the derivative and integration problems before the learning-systems and simulation sections. Use the linked MIT calculus courses for a full sequence of lectures, exercises, and exams when these ideas are new.
Free Mathematics & logic lessons
Representation is the first engineering decision
Real situations contain unlimited detail. A representation deliberately preserves some distinctions and discards others: a graph keeps entities and relationships; a bitmap keeps sampled colour; an account balance keeps an agreed unit and precision. An algorithm is only meaningful after those states and operations are defined.
A support queue can be a FIFO list when fairness means arrival order, a priority heap when severity dominates, or several queues when service classes have separate promises. The customers did not change. The representation changed which operation became cheap and which policy became natural.
How software earns a guarantee
A universal claim must survive every valid case, so one counterexample defeats it. A constructive proof shows how to produce an object. Induction handles recursively built or repeated structure. In programs, an invariant is a statement kept true before and after each step; together with termination, it turns local reasoning into an end-to-end guarantee.
Assume an array sorted in ascending order. Search a half-open interval [low, high): compare the midpoint, return on equality, and otherwise discard only the region sortedness proves cannot contain the target. If the target exists, it stays in the candidate interval. The interval strictly shrinks; if it becomes empty before a match, the target is absent.
Sets, graphs, matrices, and probability
Sets answer membership and overlap. Graphs expose relationships and paths. Matrices encode linear transformations and pairwise structure in a form machines can process efficiently. Probability represents uncertainty rather than pretending incomplete knowledge is certainty. Mature problem solving means switching lenses without confusing the model for the world.
Users and films form a bipartite graph. The same edges form an interaction matrix. A model can then estimate a probability that a user values an unseen film. Each view supports a different operation: traversal, linear algebra, or calibrated decision-making.
Prove the model survives a changed assumption
Define valid inputs, required outputs, invariants, and explicitly excluded cases before choosing code. Then an implementation can be tested or proved against that contract. When requirements change, you can identify which assumption broke instead of patching symptoms blindly.
Represent the lift with floor, direction, door state, and pending requests. State the invariant “the car never moves while a door is open.” A transition that sets direction before closing the door is a concrete counterexample trace. The repair belongs in the transition rules, and tests should include the once-failing trace.
Translate requirements into statements that can be proved or refuted.
Prove infinite families of claims using explicit base cases and preservation steps.
Model collections and mappings without confusing identity, membership, and cardinality.
Use bijections, inclusion-exclusion, and the pigeonhole principle to reason about finite systems.
Connect graph definitions to traversal certificates and structural arguments.
Understand coordinates, composition, rank, and what a matrix actually does.
Measure local change and propagate it through a computation.
Connect continuous change to finite sums and controlled error.
Practice lab: Make an unsafe lift impossible
About 25 minutes. No programming required. You only need to follow a sequence and distinguish a statement from a counterexample.
Use a two-floor lift. Its state is (floor, door, moving), initially (0, open, false). Events are CLOSE, OPEN, MOVE, and ARRIVE. MOVE heads toward the other floor; ARRIVE finishes that journey. Assume the door sensor is reliable. Your rule: moving implies door = closed.
- Write the permitted state changes for all four events. Decide what an invalid event does.
- Find the unsafe trace in a design that lets OPEN run at any time. Show the state after each event.
- Repair the rule and argue that every permitted transition preserves the invariant. Then give a reason this safety argument alone cannot guarantee that a waiting passenger gets served.
Hint
Try CLOSE → MOVE → OPEN. Do not hide “already moving” or “already open” inside an unstated assumption.
Worked solution
CLOSE shuts the door. OPEN is allowed only when stopped. MOVE is allowed only when stopped with the door closed. ARRIVE is allowed only while moving; it changes floor and sets moving to false. Invalid events leave the state unchanged and report rejection. The broken trace is (0, open, false) → (0, closed, false) → (0, closed, true) → (0, open, true). Guarding OPEN removes the last transition. Initially the invariant holds; each permitted transition preserves it, so induction covers every finite trace. A controller that never accepts MOVE is safe but useless: serving requests needs a separate progress assumption and policy.
- Show a concrete unsafe state, not just “it might break.”
- Check all event types, including invalid events.
- Separate safety from eventual service and name the sensor assumption.
Change one assumption
If a door sensor can falsely report “closed,” explain why a proof about sensor state no longer proves the physical door is closed.
Specify, prove, and calculate
Move from a precise contract to a proof, then use discrete and continuous models. A correct numerical result needs a stated domain and an argument that survives a changed input.
1. Model and counterexample · allow 30 minutes
Find the policy that the English sentence actually specifies
A service has users U, documents D, predicates Owns(u,d), Staff(u), and MayRead(u,d). Its policy says: owners may read; staff may read; everyone else may not. Write an equivalence defining MayRead, not only an implication.
- Tabulate all four combinations of ownership and staff membership.
- Formalize “every document has an owner” and negate it.
- Construct a model where every document has an owner but one user cannot read anything.
- Explain what each statement means when D is empty. Identify the extra requirement needed if an empty document collection should fail validation.
Get a starting hint
An implication constrains one direction. An equivalence specifies both permission and denial. Quantifier domains matter even when there are no records.
Compare your reasoning with the worked solution
For all u∈U,d∈D, MayRead(u,d) iff Owns(u,d) OR Staff(u). The outputs for (Owns,Staff)=(0,0),(0,1),(1,0),(1,1) are 0,1,1,1. The implication Owns→MayRead alone permits an implementation that lets everyone read everything.
Ownership is ∀d∈D ∃u∈U Owns(u,d). Its negation is ∃d∈D ∀u∈U NOT Owns(u,d). Take U={Ada,Bo}, D={X}, Ada as X's sole owner, and no staff. Every document is owned, but Bo has no readable document.
When D is empty, both universally quantified policy rules and the ownership requirement hold vacuously. “Every user can read a document” fails for a nonempty U. If validation requires a collection to exist, state |D|>0 separately. Do not alter logical implication to hide a missing existence requirement.
Check your reasoning
- Specify allowed and denied cases, not just owner access.
- Reverse both quantifiers correctly when negating ownership.
- Distinguish an empty document set from a nonempty set containing an unowned document.
2. Invariant and termination · allow 40 minutes
Prove a loop, then locate the broken update
For nonnegative integer n, initialize i=0 and total=0. While i<n, execute i=i+1 and then total=total+i. Prove that the returned total is n(n+1)/2. State the invariant before the loop guard, establish initialization and preservation, and supply a termination measure.
A programmer swaps the two assignments. Trace n=3, derive what the changed loop computes for general n, and repair it in two different ways. Explain why testing the first thousand inputs cannot establish the universal claim.
Get a starting hint
Choose an invariant describing exactly the integers already included in total. The two programs have different included ranges.
Compare your reasoning with the worked solution
Before each original guard, 0≤i≤n and total=i(i+1)/2. It holds at i=0. If i<n, the new i is old i+1, and adding that value changes total to (i+1)(i+2)/2 in old-i notation. Thus preservation holds. The nonnegative integer n−i decreases by one per iteration; termination gives i=n and the postcondition.
The swapped loop adds old i, so n=3 adds 0,1,2 and returns 3. Its invariant is total=i(i−1)/2, yielding n(n−1)/2. Restore the original ordering, or keep the swapped ordering but add i+1 instead of i. Both repairs give 6 for n=3 and 0 for n=0. Tests can refute a universal assertion with one counterexample, but finitely many passing instances do not cover the unbounded input domain.
Check your reasoning
- Write the invariant at a specified program point.
- Use a decreasing integer measure rather than saying the loop obviously ends.
- Explain the changed sum with a new invariant, not only a trace.
3. Definition and proof · allow 35 minutes
Design an equivalence relation without losing identity
Let records be pairs (department,localId). Define x~y when their department strings become equal after lowercasing ASCII letters. Prove or refute reflexivity, symmetry, and transitivity. Give the equivalence classes of (CS,1),(cs,2),(Math,1),(MATH,2),(Art,3).
A colleague instead defines x≈y when either their department matches under this normalization OR their localId is equal. Find a three-record counterexample to transitivity. Explain why using ≈ to merge database records can make the final result depend on processing order.
Get a starting hint
Equality after a deterministic normalization is an equivalence relation. A union of two equivalence relations need not be transitive.
Compare your reasoning with the worked solution
Let f extract and lowercase the department. x~y means f(x)=f(y), so each required property follows from the corresponding property of equality. The classes are {CS1,cs2}, {Math1,MATH2}, and {Art3}, using abbreviated record names. The quotient identifies departments; it does not establish that records describe the same person.
For ≈ choose a=(CS,1), b=(CS,2), c=(Math,2). Then a≈b through department, and b≈c through localId, while a is unrelated to c. A greedy merger that compares an incoming record only with a group's representative can put b with a or c depending on ordering. Computing transitive closure would produce an equivalence relation, but would merge all three and change the intended meaning. The repair requires a justified identity rule, not merely a more convenient algorithm.
Check your reasoning
- Prove all three properties for the first relation.
- Make the counterexample satisfy two links while breaking the third.
- Separate a mathematical equivalence class from real-world personal identity.
4. Combinatorial derivation · allow 35 minutes
Count valid credentials with overlapping constraints
A toy credential is a length-four string over {A,B,C,0,1}. Repetition is allowed. It must contain at least one letter and at least one digit. Count valid strings in two independent ways: inclusion-exclusion and conditioning on the number of digit positions.
Now forbid repeated symbols. Recalculate the count, explaining every factor. A teammate multiplies 3×2×5×5 and calls that the original answer. Identify precisely what that expression counts and why it misses valid arrangements. This is a counting exercise, not a recommendation for real passwords.
Get a starting hint
For the first method subtract the all-letter and all-digit cases from 5^4. For the second, choose positions before filling them.
Compare your reasoning with the worked solution
With repetition, 5^4−3^4−2^4=625−81−16=528. The excluded sets cannot overlap for a nonempty string. Conditioning on k digit positions gives Σ(k=1..3) C(4,k) × 2^k × 3^(4−k)=216+216+96=528.
Without repetition there are P(5,4)=120 ordered strings. Every selection of four distinct symbols from this alphabet includes both types because there are only three letters and two digits, so all 120 qualify. Alternatively exactly one digit gives C(4,1)P(2,1)P(3,3)=48, and exactly two gives C(4,2)P(2,2)P(3,2)=72.
The expression 3×2×5×5=150 forces the first position to be a letter and the second a digit, then allows either type in the last two positions. It counts a strict subset of valid strings, excluding 0ABC and AA01, among others.
Check your reasoning
- State whether positions and repeated symbols matter.
- Reconcile two independent counts.
- Explain the flawed expression by describing its sample space.
5. Graph construction and proof · allow 40 minutes
Prove when a dependency schedule exists
Jobs A,B,C,D,E,F have prerequisite edges A→C, B→C, C→D, B→E, E→F. Give two valid topological orders. Trace a zero-indegree algorithm, updating counts after each removal.
Prove that every nonempty finite directed acyclic graph has a zero-indegree vertex. Use that fact to justify the algorithm. Add D→B and identify a cycle. Explain why a priority queue of alphabetically smallest ready jobs makes output deterministic but does not make a cyclic input schedulable.
Get a starting hint
Assume every remaining vertex has an incoming edge and repeatedly follow predecessors. Finiteness forces a repeated vertex.
Compare your reasoning with the worked solution
Initial indegrees are A 0,B0,C2,D1,E1,F1. One order is A,B,C,D,E,F; another is B,E,F,A,C,D. For alphabetical selection, remove A (C becomes 1), B (C becomes 0,E becomes 0), C (D becomes 0), D, E (F becomes 0), then F.
If a finite nonempty directed graph had no zero-indegree vertex, start anywhere and repeatedly choose an incoming predecessor. Eventually a vertex repeats, producing a directed cycle. Therefore a DAG has a removable vertex. Removing it preserves acyclicity, so induction yields a full order. Conversely, each output edge points from an earlier removal to a later one because a target cannot become ready before its prerequisites are removed.
Adding D→B creates B→C→D→B. The algorithm may still remove A, but eventually has unremoved vertices and no ready vertex. A tie-breaking policy only chooses among eligible jobs; it cannot satisfy contradictory dependencies.
Check your reasoning
- Give a complete trace including changing indegrees.
- Use finiteness explicitly in the existence proof.
- Detect a cycle by unremoved vertices, not by the existence of multiple possible orders.
6. Linear algebra · allow 35 minutes
Separate an invertible transform from information loss
Represent a 2D point as a column vector. Apply A=[[1,2],[0,1]] to v=(3,−1). Derive A inverse and recover v. Then apply B=[[1,1],[2,2]] to v. Find a different point with the same B image and explain why no inverse can recover every input.
For the pipeline “apply A, then B,” compute the combined matrix and its output on v. Compare with “apply B, then A.” State what the determinant tells you in this two-dimensional linear setting.
Get a starting hint
Column-vector pipelines compose right to left. A nonzero vector mapped to zero supplies pairs of indistinguishable inputs.
Compare your reasoning with the worked solution
Av=(1,−1). A inverse=[[1,−2],[0,1]], which maps (1,−1) back to (3,−1). Bv=(2,4), and B(2,0)=(2,4). The difference (1,−1) lies in B's null space, so distinct inputs collapse and no inverse exists on all of R².
BA=[[1,3],[2,6]], giving BA v=(0,0). AB=[[5,5],[2,2]], giving AB v=(10,4). The results differ because matrix multiplication is not generally commutative. det(A)=1, indicating an invertible area-preserving linear shear; det(B)=0 indicates collapse onto a line or smaller subspace. An inverse can sometimes be defined after restricting a domain, but that restriction is an additional contract and does not restore discarded information for arbitrary inputs.
Check your reasoning
- Respect column-vector order when composing matrices.
- Exhibit two explicit inputs with one output.
- Distinguish singularity from a numerical implementation error.
7. Calculus and falsification · allow 40 minutes
Check a gradient by two independent methods
For f(x,y)=(xy−2)^2+x^2, derive both partial derivatives. Evaluate the gradient at (1,1), and take one simultaneous gradient-descent step with learning rate 0.1. Calculate the loss before and after.
Check the y derivative numerically with [f(1,1+h)−f(1,1−h)]/(2h), h=0.001. Explain why an implementation that updates x before computing the y gradient is a different algorithm. Does one successful step prove every learning rate decreases this loss? Give a counterexample from the same starting point.
Get a starting hint
Apply the chain rule to the squared residual. Store both old coordinates until both new coordinates have been computed.
Compare your reasoning with the worked solution
Let r=xy−2. Then ∂f/∂x=2ry+2x and ∂f/∂y=2rx. At (1,1), r=−1 and the gradient is (0,−2). The simultaneous step gives (1,1.2), and loss changes from 2 to 1.64. The central difference is [(−0.999)^2+1−((−1.001)^2+1)]/0.002=−2.
Updating one coordinate before evaluating the other derivative generally evaluates derivatives at different points. The x update happens to be zero in this example, so this particular input does not expose that bug; test a point such as (2,1). A finite-difference check should vary inputs rather than relying on one coincidental agreement.
From (1,1), a simultaneous step with rate 2 gives (1,5), whose loss is 10. A descent direction and a sufficiently small step are different requirements. A single decreasing example does not establish a global step-size guarantee.
Check your reasoning
- Derive both partial derivatives before substituting numbers.
- Use the old parameter vector for a simultaneous step.
- Find both a numerical agreement and a counterexample to an overbroad claim.
8. Approximation and error · allow 35 minutes
Bound accumulated work instead of guessing it
A toy arrival rate is r(t)=2+t² requests per second over 0≤t≤2. Compute the exact integral. With two equal-width intervals, compute left, right, midpoint, and trapezoidal estimates. Identify which are bounds and justify your answer from monotonicity or curvature.
Repeat the left and right sums with four intervals. Explain why the difference between them shrinks, and why an integral of a model rate need not be an integer count from one observed run.
Get a starting hint
For interval width 1, evaluate r at 0,1,2 and at the midpoints 0.5,1.5. Monotonicity orders endpoint rectangles.
Compare your reasoning with the worked solution
The exact accumulation is [2t+t³/3]₀²=20/3≈6.6667. With two intervals, left=2+3=5; right=3+6=9; midpoint=2.25+4.25=6.5; trapezoidal=(5+9)/2=7. Because r increases, left is a lower bound and right an upper bound. Convexity makes the midpoint estimate low and the trapezoidal estimate high here.
For four intervals of width 0.5, sampled rates are 2,2.25,3,4.25,6. Left=0.5(2+2.25+3+4.25)=5.75 and right=0.5(2.25+3+4.25+6)=7.75. Their gap is Δt[r(2)−r(0)]=2, versus 4 with width 1. This telescoping expression explains the improvement for this partition. A smooth rate may model expected arrivals; one observed realization is an integer random count. Numerical integration error and error in the rate model are separate sources of uncertainty.
Check your reasoning
- Keep rate and accumulated-count units distinct.
- Justify error direction rather than infer it from one number.
- Separate approximation error from the adequacy of the rate model.
Study the underlying methods
Section project: Prove a reservation protocol preserves ownership
4 to 6 hours. Model a small reservation system before writing an implementation. Let U be a finite set of users, S a finite set of seats, and owner a partial function from S to U. Initially no seat has an owner. Reserve(u,s) succeeds only when s is unowned; Release(u,s) succeeds only when owner(s)=u. Rejected operations leave the state unchanged. Inputs are finite operation traces, and outputs are the resulting ownership relation plus one success or rejection result per operation. Produce a precise transition specification, an induction proof of safety, and a catalogue of minimal counterexamples to weakened rules. Use three seats and two users for a hand-checked transition table or optional exhaustive Python enumerator. Keep safety separate from availability: this protocol makes no fairness or eventual-reservation promise. Submit the definitions, proof obligations, representative traces, and a short discussion of which assumptions would break if operations could interleave inside a transition. The assignment can be completed on paper; code is a useful finite-instance checker, not a replacement for the general proof. For every rejected trace step, identify the failed precondition. Distinguish properties guaranteed by the partial-function representation from properties established by the transition rules, so the proof does not assume its own conclusion.
Milestones
- Define valid states, operation preconditions, successful transitions, and rejection behavior using sets and quantifiers.
- Prove by induction over trace length that each seat has at most one owner and that only its current owner can release it.
- Enumerate the small model and construct counterexamples for an unchecked reservation and an unchecked release.
- Distinguish a safe execution that repeatedly rejects one user from a genuine liveness guarantee.
Acceptance criteria
- The empty trace yields an empty ownership relation, and the proof explicitly establishes this base case.
- Reserve(A,s), Reserve(B,s) yields success then rejection and leaves A as the sole owner.
- Reserve(A,s), Release(B,s) rejects the release without changing any ownership entry.
- The proof handles both successful and rejected transitions for an arbitrary valid prior state.
- The small model contains exactly (|U|+1)^|S| valid ownership states, with the counting argument explained.
- At least one infinite or indefinitely extendable safe trace demonstrates why safety does not imply eventual success for every requester.
Add an atomic transfer operation and prove its safety, then exhibit how a two-step release-and-reserve imitation fails to provide the same observable contract.
Practise Mathematics & logic free →