For nonnegative integer
x and positive integer y, initialize the quotient to zero and subtract one divisor at a time:q := 0; r := x;
WHILE r >= y DO
r := r-y;
q := q+1
ENDThe loop invariant is , , , with
x and y unchanged. It is true initially. A body execution changes to and keeps nonnegative because of the guard. The nonnegative integer loop variant strictly decreases by , so termination follows. At exit the guard supplies ; henceThere are exactly body executions. Under the unit-cost model, the time complexity including initialization and the final test is , which is for integer . This is a bound in the value of x, rather than in its encoded bit length.Let be the two input lengths and suppose numeric comparisons cost constant time. The list-based set representation determines which representation invariant each answer must preserve.
For unsorted lists allowing repetition, retain every left-hand occurrence whose value appears on the right for set intersection, and use list concatenation for set union:
interR xs ys = [x | x <- xs, x `elem` ys]
unionR xs ys = xs ++ ysThe resulting lists represent exactly the desired sets; repeated entries are permitted. Membership by sequential search makes
interR take time complexity in the worst case. The list concatenation in unionR costs to build its copied left spine and shares ys; fully enumerating the resulting list costs .For unsorted, duplicate-free inputs, the same intersection keeps uniqueness, while the union retains
xs and appends only right-hand elements absent from xs:interU xs ys = [x | x <- xs, x `elem` ys]
unionU xs ys = xs ++ [y | y <- ys, not (y `elem` xs)]Neither filtered list has internal repetitions, and the filter in
unionU also excludes overlap with xs. Both operations have worst-case time complexity, customarily written when both lengths are positive. Using the original xs for each membership test avoids searching an ever-growing output.interS [] ys = []
interS xs [] = []
interS (x:xs) (y:ys)
| x < y = interS xs (y:ys)
| x > y = interS (x:xs) ys
| otherwise = x : interS xs ys
unionS [] ys = ys
unionS xs [] = xs
unionS (x:xs) (y:ys)
| x < y = x : unionS xs (y:ys)
| x > y = y : unionS (x:xs) ys
| otherwise = x : unionS xs ysWhen , sortedness proves that cannot occur anywhere in the right list, so it can be discarded from the set intersection or immediately emitted to the set union. The symmetric argument handles ; equal heads are consumed together. Each step consumes at least one input head, so both have worst-case time complexity. These bounds assume the sorted representation invariant is already established; sorting arbitrary inputs has its own cost.
| Representation | Set intersection | Set union, including output traversal |
|---|---|---|
| Unsorted, repetitions allowed | ||
| Unsorted, unique | ||
| Sorted, unique |
Divide-and-conquer algorithms suit problems with largely independent, balanced subproblems and an inexpensive combination step. In merge sort, the two halves are independently sorted and merged in linear time. Its recurrence relation is , giving time complexity.
Dynamic programming suits overlapping subproblems with a compact state description. For the coin change problem, let be the minimum number of coins needed to make amount . With positive denominations containing ,Every optimal nonempty answer has a last coin and an optimal answer for ; otherwise replacing the remainder improves it. Filling takes time complexity and space complexity. Repeated amounts are computed just once. This bound is in the numeric amount , not its binary input length.
A greedy algorithm suits problems where one can prove a greedy-choice property. For unweighted interval scheduling, choose an interval with earliest finishing time, discard overlapping intervals, and repeat. Among optimal schedules, replace the first interval by the earliest-finishing one. The replacement finishes no later, so every later interval remains feasible. Applying the same argument to the remaining intervals proves optimality. After sorting by finish time, a single scan suffices.
These examples separate the relevant structural reasons: independent halves, repeated amount states, and an exchange argument certifying each irreversible choice.
Heapsort uses time for bottom-up heap construction and for each extraction, giving worst-case time complexity. An iterative heapify down on an array uses auxiliary space complexity. Ordinary heapsort is not a stable sorting method.
Quicksort has balanced-case and average-case time complexity when the input order supplies suitably distributed pivot ranks. With the prescribed first-element pivot, sorted inputs produce subproblems of sizes and , giving . With the stated two-way partition convention, all-equal keys also give this worst case. There is no input-independent expected bound without a distribution or randomization assumption. For an in-place array implementation, the recursion stack is when balanced and in the worst case; the functional list trace also allocates new partition spines and copied concatenation prefixes. Ordinary in-place quicksort is not stable sorting; the stable-partition list convention used in the trace can preserve equal-key order at additional allocation cost.
Counting sort uses time complexity for possible consecutive integer keys. The stable sorting version uses auxiliary space complexity including the output array; counting and re-emitting bare keys needs only beyond its output. It is attractive when is small, but a sparse huge key range makes both initialization and count storage expensive. It relies on indexing by bounded integer keys, so it is not subject to the comparison sorting lower bound.
An Oberon recursive procedure can implement the defining recurrence relation directly. Its precondition is ; arithmetic is assumed to remain in the representable integer range.
PROCEDURE Fib(n: INTEGER): INTEGER;
VAR result: INTEGER;
BEGIN
IF n <= 2 THEN
result := 1
ELSE
result := Fib(n-1) + Fib(n-2)
END;
RETURN result
END Fib;Correctness follows by strong induction: the two base inputs give , and for the returned sum is . On each recursive branch the positive integer argument strictly decreases, while recursion stops at or . The well-ordering principle therefore proves algorithm termination.The method repeats many subproblems and has exponential time complexity; termination alone does not make it efficient.
Each merge consumes and copies a total of elements, so its time complexity is . HenceAt any level of the recursion tree, all active subranges are disjoint and together contain at most elements. The total work per level is therefore , and halving gives levels. In fact the full run performs work for .
The shared work array holds elements, and the depth-first recursion has simultaneous activation records with a constant number of scalar variables each. No recursive call allocates a fresh array. ThereforeThe work array is counted in the auxiliary space complexity even though the caller supplies it. If its actual allocated capacity is , the reserved storage is ; choosing capacity gives the stated bound.
Add polynomials by adding equal-power coefficients, interpreting a missing coefficient as zero. Compute into a local record before assigning the output, so the result may safely be the same actual record as either input.
PROCEDURE Add(VAR p, q, result: Polynomial);
VAR t: Polynomial; i: INTEGER; u, v: REAL;
BEGIN
t.len := p.len;
IF q.len > t.len THEN t.len := q.len END;
i := 0;
WHILE i < t.len DO
u := 0.0; v := 0.0;
IF i < p.len THEN u := p.coeff[i] END;
IF i < q.len THEN v := q.coeff[i] END;
t.coeff[i] := u+v;
i := i+1
END;
result := t
END Add;With , the loop invariant is and, for ,
t.coeff[k] is the sum of the two extended input coefficients at . The loop variant is . The inputs remain unchanged throughout the loop, and at exit every active coefficient is correct. The time complexity is for the active arithmetic; assigning the fixed-capacity record can additionally copy its full capacity.For the product, each pair of input terms contributes . Initialize the active result to zero, then accumulate these pairwise contributions:
PROCEDURE Multiply(VAR p, q, result: Polynomial);
VAR t: Polynomial; i, j, k: INTEGER;
BEGIN
t.len := 0;
IF (p.len > 0) & (q.len > 0) THEN
t.len := p.len + q.len - 1
END;
(* Precondition: t.len <= Capacity. *)
k := 0;
WHILE k < t.len DO
t.coeff[k] := 0.0; k := k+1
END;
IF t.len > 0 THEN
i := 0;
WHILE i < p.len DO
j := 0;
WHILE j < q.len DO
t.coeff[i+j] := t.coeff[i+j]
+ p.coeff[i]*q.coeff[j];
j := j+1
END;
i := i+1
END
END;
result := t
END Multiply;The input representation invariants and the capacity precondition are assumed. No coefficient is accessed when either input is the zero polynomial. The initialization loop invariant says coefficients below are zero; its loop variant is
t.len-k.For positive input lengths , the outer loop invariant says that and each coefficient equalsThe inner loop invariant adds the contributions with and to that sum, while . The update adds exactly the next missing term at index , preserving the inner loop invariant. The loop variants are for the outer loop and for the inner loop. On exit all pairs have contributed, yieldingThe product uses arithmetic operations and a temporary coefficient array of capacity
Capacity. Both operations allow trailing zeros; no extra normalization loop is required. Only the active coefficients are meaningful, so inactive record entries are never read by these operations. As in part (a), floating-point coefficients implement these formulas subject to rounding.These solutions follow the original examination of 11 June 2013, code
4208.[ref]Functional programming, design and analysis of algorithms examination paper by the University of Oxford (2013). pp. 2–7, Questions 1–8
Each question's Haskell definitions form a separate namespace; hide redefined Standard Prelude names when compiling them. Unless stated otherwise, arguments are finite and total. Time complexity counts primitive operations; the cost of comparing variable-length words and the growing bit cost of exact integer arithmetic are stated separately where relevant.[ref] Past exam of the year 1 of the computer science course of the University of Oxford 2013 Functional programming, design and analysis of algorithms 8 e Solution Created 2026-10-31 Updated 2026-11-05
Use the two-pass strongly connected component algorithm. First run a complete depth-first search of , starting a new search at each unvisited vertex as necessary. Append each vertex to a list when its recursive call finishes. Next construct the graph transpose by reversing every edge. Reset all visited flags. Process the vertices in decreasing first-pass finishing order, running depth-first search in from each still-unvisited vertex. The newly reached vertices in each such search form one strongly connected component.
To prove this, contract each strongly connected component to one vertex. The resulting condensation graph is a directed acyclic graph, because a directed graph cycle of distinct components would make them mutually reachable and hence a single component. For a component , write for its largest first-pass finishing time. If there is an edge between distinct components, then . Indeed, if the first search reaches before , it can reach , which must finish before the search in finishes. If it reaches first, cannot reach or they would be the same component, so finishes before is discovered.
Among unreported components, the one with greatest therefore has no incoming edge from another unreported component in . In the graph transpose it has no outgoing edge to any other unreported component. A second-pass search cannot escape it, while strong connectivity lets that search reach all its vertices. Earlier reported components are ignored by the visited flags. Repeating this argument provesBoth depth-first searches visit every vertex and scan every edge once, and transposition costs . Therefore the total time complexity is with adjacency lists. Storage for the transpose is , while visited flags, finishing order and the search stack use additional space. No sorting is needed: reverse the list recorded at finishing time.
Place these methods inside the In the forward traversal, the loop invariant is that
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 }q is physical node , with ; its loop variant is . In the backward traversal, q is physical node , with ; its loop variant is . Thus both locate physical index , which is exactly logical index 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 to its list reversal without moving any linked list nodes. ConsequentlyThese are worst-case time complexity bounds in the constant-cost pointer model; total storage is and each operation uses constant auxiliary space.
Use three-way quicksort. Fix the pivot value before moving any entries, and group equal entries together so that none needs a recursive call. These helpers and the sorter belong inside an enclosing scope containing The array partitioning loop invariant iswith unclassified. Swaps preserve the segment's array multiset and leave all entries outside it unchanged. The loop variant decreases in every branch. When swapping an entry from the right into
a.def swap(i: Int, j: Int): Unit = {
val t = a(i); a(i) = a(j); a(j) = t
}
def split(l: Int, r: Int): (Int, Int) = {
// Pre: 0 <= l < r <= a.length.
val p = a(l)
var lt = l
var i = l
var gt = r
while (i < gt) {
if (a(i) < p) {
swap(lt, i)
lt += 1
i += 1
} else if (a(i) > p) {
gt -= 1
swap(i, gt)
} else {
i += 1
}
}
(lt, gt)
}
def quicksort(l: Int, r: Int): Unit = {
require(0 <= l && l <= r && r <= a.length)
if (r - l > 1) {
val (lt, gt) = split(l, r)
quicksort(l, lt)
quicksort(gt, r)
}
}
// Sort the whole array with quicksort(0, a.length).i, do not increment i, since the incoming entry still needs classification. At termination,Here the middle segment is nonempty because the original pivot occurs somewhere in the preserved array multiset. Both recursive segments therefore have length strictly smaller than . Mathematical induction on segment length proves that the two recursive calls sort their segments, and their ordering relative to the middle segment proves the complete sorting postcondition.There is no additional array. The call stack and returned boundary pairs still use auxiliary space. An all-equal input takes one linear scan and no nontrivial recursive calls, so its time complexity is for . Balanced partitions give time complexity; a fixed first pivot can still give on adversarial distinct inputs. The worst-case call stack has entries.
Reuse A useful loop invariant is that the pending segments are pairwise disjoint valid array segments of length at least two; the whole array multiset equals its original value; and every inverted pair of positions lies in a single pending segment. Explicitly, if and , some queued contains both and . Thus all ordering obligations are localized to queued segments.
split and swap, but replace recursive calls with a FIFO queue of unresolved segments. Enqueue only segments of length at least two.def quicksortLoop(): Unit = {
val work = scala.collection.mutable.Queue[(Int, Int)]()
if (a.length > 1) work.enqueue((0, a.length))
while (!work.isEmpty) {
val (l, r) = work.dequeue()
val (lt, gt) = split(l, r)
if (lt - l > 1) work.enqueue((l, lt))
if (r - gt > 1) work.enqueue((gt, r))
}
}Initially the only possible pending segment is the whole array. One array partitioning confines all its remaining inversions to its two child segments. Its equal middle segment is ordered, the left/middle/right boundaries have the correct ordering, and segments of length at most one cannot contain an inversion. Because array partitioning only permutes the selected segment's entries, it cannot create an inversion across a boundary that previously had no inversions. This proves preservation of the loop invariant.
The loop variant is the total pending lengthProcessing one segment removes from and adds at most , strictly less because . Thus is a nonnegative integer and decreases. At exit no pending segment exists, so no inversion exists:The FIFO queue itself can grow to pairs. The time complexity is that of the corresponding recursive quicksort, including linear behavior on equal input. Removing recursion does not make the worst-case time complexity linear or eliminate the work storage.
Traverse the trie along the input string, stopping as soon as the required child is absent. All words and letter collections in this question are assumed to use only lowercase letters The loop invariant is that
a through z; this is the alphabet represented by the given child array. Put the following methods inside the supplied Trie class.def contains(w: String): Boolean = {
var t: Trie = this
var i = 0
while (i < w.length && t != null) {
t = t.children(toIndex(w.charAt(i)))
i += 1
}
t != null && t.complete
}t is the trie node reached by the prefix w.take(i), or null if that prefix has no path, with . If t is null, no extension can be a stored word. Otherwise, following the next character preserves the loop invariant. The loop variant is . At exit,A prefix that exists but is not complete must return false. The empty string is present exactly when the root's complete flag is true. The time complexity is , with constant auxiliary space.Create only the missing nodes along the required trie path, and mark its last node complete.The loop invariant is that the path for
def add(w: String): Unit = {
var t: Trie = this
var i = 0
while (i < w.length) {
val k = toIndex(w.charAt(i))
if (t.children(k) == null) t.children(k) = new Trie
t = t.children(k)
i += 1
}
t.complete = true
}w.take(i) exists and ends at t, while the set of complete words remains unchanged from entry. A fresh node has all children null and complete == false, so creating an unfinished path introduces no stored word. The loop variant is . At termination the full path exists; setting its final flag givesExisting paths and terminal flags are untouched, so adding an existing word is idempotent. Adding the empty string marks the root. The time complexity is because the alphabet size is fixed; at most new trie nodes are allocated.Keep a running total in the mixin, and use only the inherited public operations. Updating after a successful superclass operation leaves the total unchanged if an empty For this trait mixed directly into
pop fails its precondition.trait SumPlugin extends Stack {
private var total = 0
override def push(x: Int): Unit = {
super.push(x)
total += x
}
override def pop(): Int = {
val x = super.pop()
total -= x
x
}
def sum: Int = total
}Stack, its representation invariant is , where is the abstract stack sequence. A successful push adds exactly its argument and a successful pop removes exactly its returned value. ThusThe mixin reads no private Stack fields. Its operations add constant time complexity. As in the paper's Int interface, an unbounded mathematical total requires excluding integer overflow, or replacing the accumulator with BigInt if the interface is allowed to change. A later mixin can transform a pushed value at a different point in the Scala trait linearization; the effect is analyzed in the next part.These operations consume the receiver, as expected for this destructive iterator interface. For
exists stops immediately after the first successful test.trait RichIter[T] extends Iter[T] {
def foreach(f: T => Unit): Unit = {
while (hasNext) f(next())
}
def exists(p: T => Boolean): Boolean = {
while (hasNext) {
if (p(next())) return true
}
false
}
def foldLeft[U](x: U)(f: (U, T) => U): U = {
var acc = x
while (hasNext) acc = f(acc, next())
acc
}
}foreach, after iterations the supplied function has been applied in order to exactly the first entries. For exists, every consumed entry has failed the predicate unless the method is returning true. For the left fold, the loop invariant after consuming entries isEach iteration extends the expression by the next entry on the right. For a finite remaining sequence, its unconsumed length is a common loop variant. ThusAn empty iterator invokes no callback, gives false for exists, and returns from the left fold. On an infinite iterator, exists can terminate when it finds a match; the other two operations ordinarily do not terminate. With constant-cost callbacks, finite input of length takes time complexity and constant auxiliary space.Represent the set by a private list containing each value once. Normalize the constructor input as well as checking future insertions; otherwise duplicate initial entries would violate the intended set behavior.The representation invariant is that
class Set[T](contents: List[T]) {
protected var elems: List[T] = contents.distinct
def add(x: T): Unit = {
if (!elems.contains(x)) elems = x :: elems
}
def delete(): T = {
require(elems.nonEmpty)
val x = elems.head
elems = elems.tail
x
}
}elems contains no duplicates under the chosen stable value equality; the abstraction function forgets its ordering and returns its set of elements. The protected field allows the subclass in part (d) to inspect its contents; that subclass is responsible for preserving the representation invariant if it mutates them.Insertion makes the represented set . Deletion requires , returns some , and leaves . ThusDeletion does not promise to choose a minimum. With this linked list representation, insertion takes time complexity because of its membership check, while deletion takes . Values should not mutate in a way that changes their equality while stored.
Use an upper type bound requiring each element type to implement the supplied comparison interface for its own type. This is F-bounded polymorphism.Use this locally defined
trait Ordered[T] {
def <(that: T): Boolean
}
class MinSet[T <: Ordered[T]](contents: List[T])
extends Set[T](contents) {
def min: T = {
require(elems.nonEmpty)
var best = elems.head
var rest = elems.tail
while (rest.nonEmpty) {
if (rest.head < best) best = rest.head
rest = rest.tail
}
best
}
}Ordered, rather than silently substituting the standard library's different comparison interface. The type bound makes rest.head < best well typed. To interpret the result as a minimum, require the comparison to be a consistent strict total order; merely providing a method named < cannot establish its mathematical laws.The loop invariant is that
best is a minimum among the entries already inspected, and rest is exactly the uninspected suffix. Comparing its next head with best preserves that property. The loop variant is the length of rest. On termination,The method leaves the set unchanged, takes time complexity under constant-cost comparisons, and uses constant auxiliary space. It requires a nonempty set; inherited insertion and deletion continue to preserve the duplicate-free representation invariant.Retain the first element, filter all its further occurrences out of the tail, and recurse:
removedup :: Eq a => [a] -> [a]
removedup [] = []
removedup (x:xs) = x : removedup (filter (/= x) xs)The boxed specification is . The Haskell type class
Eq is needed for comparing values. Structural induction on a finite list proves duplicate removal: filtering removes every further x, and the recursive result contains each remaining distinct value exactly once. In the worst case of all distinct values, successive filters give quadratic time complexity.Use the two-pointer technique, starting at opposite ends of the ordered sequence:
l = 0
r = n - 1
while l < r:
s = S[l] + S[r]
if s == x: return (l, r)
if s < x: l = l + 1
else: r = r - 1
return NONEIf the sum is too small, every remaining pair using
l has sum at most , so discard l. If the sum is too large, every remaining pair using r has sum at least , so discard r. The loop invariant says that every solution not already excluded has both indices in . These two elimination arguments preserve it; at termination fewer than two positions remain.Each unsuccessful iteration decreases by one. Therefore the two-sum problem is solved withThe condition
l < r ensures distinct positions and handles . Under the usual interpretation of “two distinct elements” as two different occurrences, equal values in different positions are allowed. If distinct numerical values are intended instead, reject an equality with : sortedness then makes the entire remaining interval equal, so it contains no distinct-value solution. Both interpretations retain linear time complexity. The comparison assumes exact real-number operations, as in the stated comparison model.