Use pattern matching on the two data constructors, concatenating the left subtree's inorder traversal, the root label, and the right subtree's inorder traversal:
data Tree = Leaf | Fork Tree Int Tree

inorder :: Tree -> [Int]
inorder Leaf = []
inorder (Fork l x r) = inorder l ++ [x] ++ inorder r
Here Leaf represents the empty binary tree, rather than a labelled leaf. The printed declaration uses type; an executable Haskell algebraic data type requires data, as above. By structural induction, the two equations return precisely the prescribed inorder traversal:
(1)
An Oberon pointer refers to a record containing an integer label and two subtree references:
TYPE
  Tree = POINTER TO Node;
  Node = RECORD
    left, right: Tree;
    label: INTEGER
  END;
Use NIL for the empty binary tree, including either absent child. The representation invariant requires a finite, acyclic binary tree with disjoint left and right subtrees. In particular, shared nodes would represent a different structure and invalidate destructive traversal arguments.
(1)
Give the visiting procedure a procedure type:
TYPE Visit = PROCEDURE(x: INTEGER);

PROCEDURE Inorder(t: Tree; p: Visit);
BEGIN
  IF t # NIL THEN
    Inorder(t.left, p);
    p(t.label);
    Inorder(t.right, p)
  END
END Inorder;
Structural induction establishes algorithm correctness: an empty binary tree makes no calls; otherwise the first recursive call visits precisely the left subtree, then the root is visited once, then the second recursive call visits precisely the right subtree. Assume p does not modify the binary tree. With constant-cost p, there is constant work per node and empty child occurrence:
(1)
where is the height of a binary tree and storage is the call stack.
Split the half-open array segment at its midpoint, using one entry for the root:
PROCEDURE MakeTree(VAR u: ARRAY OF INTEGER;
                   a, b: INTEGER): Tree;
VAR m: INTEGER; t: Tree;
BEGIN
  IF a = b THEN RETURN NIL END;
  m := a + (b-a) DIV 2;
  NEW(t);
  t.label := u[m];
  t.left := MakeTree(u, a, m);
  t.right := MakeTree(u, m+1, b);
  RETURN t
END MakeTree;
The precondition is . Set . For the child sizes are and , differing by at most one. The same construction in both subtrees proves subtree-size balance at every node. Structural induction also gives the inorder traversal , followed by , followed by , hence precisely ; no sortedness assumption is needed.
Exactly records are allocated. Each nonempty recursive call makes two child calls, so there are calls including empty segments. Under constant-cost allocation and reference parameter passing,
(1)
For positive this is proportional to ; the empty case takes constant time. The call stack has depth.
The VAR marker passes a reference parameter, so every recursive call accesses the same array without copying it. Read-only access does not make copying necessary. Under the examination's value parameter convention, omitting VAR copies the whole actual array, not merely the selected segment .
If its length is , the calls therefore cost for . For a whole-input construction, :
(1)
Copying only the shrinking segments would instead lead to , but that is a different parameter passing model from passing the same actual array on every call.
Use destructive inorder traversal by right rotations. A right tree rotation preserves inorder traversal but moves the first unvisited node closer to the root:
PROCEDURE InorderDestructive(t: Tree; p: Visit);
VAR q: Tree;
BEGIN
  WHILE t # NIL DO
    WHILE t.left # NIL DO
      q := t.left;
      t.left := q.right;
      q.right := t;
      t := q
    END;
    p(t.label);
    t := t.right
  END
END InorderDestructive;
The outer loop invariant states that the labels already passed to p, followed by the inorder traversal of t, equal the original inorder traversal. The remaining nodes form a binary tree disjoint from the nodes already visited. The inner loop invariant preserves the remaining inorder traversal: if the old root is , its left child is , and the three unchanged subtrees are , then both shapes have order .
Figure 1.
A right tree rotation preserves inorder traversal and exposes the next node
. Details.
At inner-loop exit, t.left = NIL, so the root is the first remaining node. Visiting it and replacing t by t.right preserves the outer loop invariant. The procedure changes child pointers and makes the old root reference unusable as the original binary tree. Assume p neither changes the binary tree nor depends on its old shape.
(1)
Let be the number of nodes and let the left-size potential of a binary tree be
(1)
Equivalently counts nodes outside the right spine, so ; for a nonempty binary tree of nodes, .
For the right tree rotation in part (f), write the old shape as . Before and after,
(2)
Thus each inner iteration decreases by exactly one, making an inner loop variant. Removing a root with empty left subtree leaves unchanged and decreases by one. Therefore decreases on every rotation or visit, while decreases on every completed outer iteration. These are bounds used for proof; the program never computes them.
There are exactly visits and exactly rotations, since the final empty binary tree has potential zero. Counting constant-cost p,
(3)
The nested loops therefore have linear total running time, despite one outer iteration potentially making many rotations.
Track the length r of the trailing constant segment of an array, and the best length m anywhere in the processed prefix:
i := 1; r := 1; m := 1;
WHILE i < n DO
  IF a[i] = a[i-1] THEN r := r+1 ELSE r := 1 END;
  IF r > m THEN m := r END;
  i := i+1
END;
The loop invariant is: ; r is the length of the longest constant suffix of ; and m is the length of the longest constant segment of an array within . Initially all three lengths are one, using .
When the next entry equals its predecessor, the trailing constant segment extends by one; otherwise its new length is one. Every new plateau either was already in the old prefix or ends at the new entry, so taking the larger of the old m and the new r preserves the loop invariant. The loop variant is , a nonnegative integer decreased by one. At termination , so
(1)
The auxiliary space is , and correctly returns one without entering the loop.
Use binary search on an interval with unequal endpoint values. The array need not be sorted:
l := 0; r := n;
WHILE r-l > 1 DO
  m := l + (r-l) DIV 2;
  IF b[l] # b[m] THEN r := m ELSE l := m END
END;
k := l;
The loop invariant is
(1)
It holds initially by the given endpoint inequality, which also implies . When , . If , replacing maintains unequal endpoints. Otherwise , so replacing maintains them. This does not require monotonicity or even just two possible values.
The positive integer width is a loop variant, reduced to at most its old half rounded up. On exit , giving
(2)
There are at most iterations. The additive constant handles .
Return the exclusive endpoint of the maximal initial run:
PROCEDURE Run(a, b: INTEGER): INTEGER;
VAR c: INTEGER;
BEGIN
  IF a = b THEN RETURN b END;
  c := a+1;
  WHILE c < b DO
    IF u[c-1] > u[c] THEN RETURN c END;
    c := c+1
  END;
  RETURN c
END Run;
The loop invariant is and is nondecreasing. An unsuccessful adjacent-order test extends the run by one; a strict descent at prevents any extension across it. If , the whole segment is a run. The loop variant is .
(1)
For a run of length , the running time is , including at most one failed extension test; an empty segment takes .
Use a merge algorithm with one unread index in each run. Here u is the module's array; the destination is disjoint from the source and lies within the array bounds:
PROCEDURE Merge(a, b, c, d: INTEGER);
VAR i, j, k: INTEGER;
BEGIN
  i := a; j := b; k := d;
  WHILE (i < b) & (j < c) DO
    IF u[i] <= u[j] THEN
      u[k] := u[i]; i := i+1
    ELSE
      u[k] := u[j]; j := j+1
    END;
    k := k+1
  END;
  WHILE i < b DO
    u[k] := u[i]; i := i+1; k := k+1
  END;
  WHILE j < c DO
    u[k] := u[j]; j := j+1; k := k+1
  END
END Merge;
Let denote the original two runs. The first loop invariant says and is the sorted merge of and ; moreover each emitted value is at most every unread value. Choosing the smaller head preserves that condition. Equal heads are taken from the first run, giving stable sorting within this merge. The loop variant is .
For each copying loop, the output remains the sorted merge of the consumed prefixes, at least one source run is exhausted, and only the indicated suffix remains. The respective loop variants are and . At exit both source runs are exhausted:
(1)
The destination's multiset is the sum of the two source multisets.
Treat the live array segment as a FIFO queue of runs. Remove its first two runs, append their merged result, and repeat:
PROCEDURE Sort(a, b: INTEGER; VAR c, d: INTEGER);
VAR x, y, z: INTEGER;
BEGIN
  c := a; d := b;
  WHILE c < d DO
    x := Run(c, d);
    IF x = d THEN RETURN END;
    y := Run(x, d);
    z := y-c;
    Merge(c, x, y, d);
    c := y;
    d := d+z
  END
END Sort;
Compute both run boundaries before writing the destination, which starts at the old d. The untouched suffix is followed by the new merged run. The endpoints returned in c,d always describe the live sequence; obsolete values before c are ignored. As allowed, assume enough destination capacity.
For example, becomes the live sequence , then . The first merge combines and , and the second combines and .
(1)
Let be the original sequence and . The loop invariant is
(1)
Here denotes the multiset of entries. The capacity condition uses the question's assumption of sufficient space. Removing two runs of combined length and appending their merge preserves the length and multiset. It also leaves all live values in one contiguous segment.
For a nonempty live sequence, let be its number of maximal initial runs obtained by repeatedly cutting at strict adjacent descents. The loop variant is . If x = d, there is one run and the procedure returns a sorted permutation. Otherwise the iteration removes two runs and appends one; it cannot create a new descent inside that appended run. The appended run may join the last old run, further reducing , so decreases by at least one. There are at most merges.
(2)
For , the loop is skipped and the empty segment is already sorted. No global stability claim is needed: moving a merged run behind other runs can change the order of equal-labelled occurrences.
Let be the total length of the two runs in merge . Because destinations are always appended beyond the old endpoint, the exact space consumption is
(1)
A simple valid bound is , using at most merges. The FIFO queue schedule permits the sharper asymptotic bound
(2)
To prove the upper bound, group merges into rounds. Mark the old end of the live segment, and finish a round when all runs present at its start have been consumed. If there are such runs, at most merges occur. Only the last merge can pair one remaining old run with an already appended run. Consequently at most runs remain; coalescence can only reduce this number. Every start-of-round entry is merged once, and entries in the one possible already appended run are merged at most once more. A round writes at most entries. After at most rounds there is one run, giving for .
For a matching family, let and use repetitions of . Each initial run has length two. Every merged run still starts at zero and ends at one, so adjacent runs never coalesce. In each of the complete merging levels exactly entries are written. Hence
(3)
on this family. For an already sorted input, no merge occurs and .
If the merge algorithm from part (b) is retained with a disjoint destination, use a circular buffer of cells. Represent the live segment by its start modulo and its length . The other cells are free; the next merge needs at most output cells. Appending its output and advancing the live start releases exactly as many obsolete source cells. Logical run boundaries and copying indices are reduced modulo . The final sorted sequence may wrap, in which case an array rotation makes it contiguous. Thus
(1)
This is also the worst-case requirement if all source cells must be retained until a whole disjoint merge has been written: the final two runs can have combined length .
Under the question's literal wording, however, no running time requirement or disjoint-output restriction is imposed on the modified implementation. The absolute smallest array is
(2)
To achieve this, replace the disjoint-output merge by an in-place merge: compare the next unread values of the two adjacent runs; when the second is smaller, save it in one scalar, shift the intervening first-run block right by one, and insert it before that block. This is a sorted merge using no extra array. Its loop invariant is that the finished prefix is the sorted merge of the consumed portions and the two remaining runs stay sorted. Each step consumes one value, proving termination.
After merging the first two runs in place, rotate the merged prefix behind the untouched suffix. Three array reversals implement this rotation with one scalar: reverse the merged prefix, reverse the suffix, then reverse the whole segment. The resulting live sequence is exactly the one produced in part (c). Repeat the same run schedule until sorted. The shift and reversal loops respectively preserve the copied block and exchanged end pairs; their loop variants are the unshifted length and half the unreversed length. The modification can be substantially slower, but preserves the loop invariant and decreasing run count from part (d). Fewer than cells cannot even hold the specified input entries. Thus is the natural circular-workspace answer for the original merge primitive, while is attainable when minimizing storage over all implementations allowed by the stated time-free specification.
Maintain an integer len, initially zero, with len = length xs:
PROCEDURE Add(x: INTEGER);
BEGIN
  ASSERT(len < N);
  u[len] := x;
  len := len+1
END Add;
The precondition is the abstract capacity condition. Appending at the first unused array index establishes in constant running time.
If get(k) first applies a comparison sort to all entries, the comparison sorting lower bound gives at least comparisons in the worst case. A merge sort or heapsort meets that order, after which indexing costs constant time:
(1)
This is a logarithmic factor worse than linear. The qualification to comparison sorting is necessary: merely saying that keys are integers does not prohibit counting sort for a bounded small range or radix sort under suitable machine-key assumptions. The printed assertion of an unavoidable superlinear bound needs the comparison model.
Keep u[0..len) sorted, with the coupling invariant
(1)
The abstract list retains insertion order, while the concrete array retains its sorted multiset. Initially both are empty.
PROCEDURE Add(x: INTEGER);
VAR i: INTEGER;
BEGIN
  ASSERT(len < N);
  i := len;
  WHILE i > 0 DO
    IF u[i-1] <= x THEN EXIT END;
    u[i] := u[i-1];
    i := i-1
  END;
  u[i] := x;
  len := len+1
END Add;

PROCEDURE Get(k: INTEGER): INTEGER;
BEGIN
  ASSERT((0 <= k) & (k < len));
  RETURN u[k]
END Get;
For insertion, conceptually treat index i as a hole. If is the old sorted prefix of length , the loop invariant is , and , with every shifted value strictly greater than . The loop variant is . The exit condition gives either no left neighbour or a left neighbour at most ; filling the hole establishes sortedness and adds exactly one occurrence, preserving the coupling invariant.
(2)
When the new entry is smaller than every old entry, all old values must move in this contiguous sorted-prefix representation. Binary search can reduce comparisons to locate the insertion point, but cannot remove that linear movement cost. Appending a new largest value takes constant time in this implementation.
The original page permits , but also indexes . The meaningful pivot-position contract is the stronger , with and . Implement this two-way array partition by reserving the last entry as pivot:
PROCEDURE Partition(l, r: INTEGER): INTEGER;
VAR pivot, i, j, tmp: INTEGER;
BEGIN
  ASSERT(l < r);
  pivot := a[r-1];
  i := l; j := l;
  WHILE j < r-1 DO
    IF a[j] < pivot THEN
      tmp := a[i]; a[i] := a[j]; a[j] := tmp;
      i := i+1
    END;
    j := j+1
  END;
  tmp := a[i]; a[i] := a[r-1]; a[r-1] := tmp;
  RETURN i
END Partition;
The loop invariant is
(1)
The segment's multiset is preserved and entries outside are unchanged. The unclassified part is . A smaller entry is swapped into the left group; if , the displaced entry belongs to the greater-or-equal group. Otherwise the entry simply joins that group. The loop variant is .
At exit the final swap installs the pivot at i, giving
(2)
A singleton segment is handled without loop iterations. Equality belongs on the pivot's right side, as required by the printed strict left inequality.
Store the current multiset in an unsorted prefix a[0..len); Add appends exactly as in part (a). The coupling invariant is equality of length and multiset with abstract xs, rather than equality of insertion order. Get applies quickselect:
PROCEDURE Get(k: INTEGER): INTEGER;
VAR l, r, m: INTEGER;
BEGIN
  ASSERT((0 <= k) & (k < len));
  l := 0; r := len;
  LOOP
    m := Partition(l, r);
    IF k = m THEN RETURN a[m]
    ELSIF k < m THEN r := m
    ELSE l := m+1
    END
  END
END Get;
The loop invariant is , the complete array has its original multiset, every discarded entry on the left is at most every active entry, and every active entry is at most every discarded entry on the right. Thus the desired global order statistic is the local one of rank . The two-way array partition result either identifies it or excludes the pivot and the irrelevant side. The positive loop variant strictly decreases unless the procedure returns.
Balanced pivots give , whose geometric series is . More generally, choosing a uniformly random pivot before each call, by swapping a random active entry into a[r-1], gives expected running time on distinct keys: with constant probability, the pivot is in the middle half and the retained side has size at most . Expected work over these shrinking stages is a convergent geometric series.
(1)
The particular last-entry pivot in the displayed code has no unconditional expected guarantee without an input distribution. Its worst case repeatedly discards one entry. Duplicate keys require further care: on an all-equal segment, the strict partition always returns , so selecting the last rank costs even with randomized pivot positions. A three-way array partitioning that groups all keys equal to the pivot restores the usual randomized linear expectation with duplicates; alternatively the stated expectation assumes distinct keys. This is a qualification to the bound, not to the algorithm correctness of the displayed code.
The five printed lines, including the comma and space after every fragment, are:
f1 in C, 
f1 in C, f2 in B, 
f1 in C, f2 in A, f3 in B, 
f1 in A, f2 in A, f3 in ObjB, f4 in B, 
f1 in ObjC, f2 in A, f3 in B, f4 in ObjC, f5 in C,
Scala dynamic dispatch uses the receiver's runtime software class, even though a has the static type A. Thus a.f1 uses C.f1, and a.f2 uses B.f2 whose unqualified f1 still dispatches on the new C receiver.
For a.f3, B.f3 explicitly selects super.f2, which is A.f2. Inside A.f2, the unqualified call to f1 still dispatches to C.f1; super does not replace the receiver. For a.f4, B.f3 in the body of class B means a call on the singleton object B, not on this. That object's f3 calls A.f2, which calls A.f1.
Finally a.f5 calls C.f4 on the singleton object C. That object extends class B, overrides f1 and f4, and inherits class B's f3. Its f4 calls this inherited f3; that selects A.f2, whose f1 dispatches to the object's own override. These distinctions follow member selection and super semantics.[ref]
(1)
List each Scala trait linearization from the most specific software class toward the common base, omitting predefined types:
Life1, Party, Study, Life
Life2, Sport, Exercise, Research, Party, Study, Life
Life3, Research, Study, Sport, Party, Exercise, Life
For example, Sport alone linearizes as Sport, Party, Exercise, Life, while Research alone gives Research, Party, Study, Life. In combining parents, take the right parent's linearization first, deleting from it entries also present in the remaining left-parent linearization, then append the latter. This places a common base after all of its derived traits.[ref]
An unqualified super.describe() continues after the current trait in the actual receiver's Scala trait linearization. Each override prints after its super call, so the output follows the displayed order backwards, starting at Life. The complete output is:
I live.
More on study.
More on party.
I live.
More on study.
More on party.
More on research.
More on exercise.
More on sport.
I live.
More on exercise.
More on party.
More on sport.
More on study.
More on research.
The first three lines belong to l1, the next six to l2, and the final six to l3.
(1)
Use an immutable list as private storage and cache its length. This makes the data refinement transparent without depending on library-specific dynamic array costs:
class DocImpl extends Doc {
  private var chars: List[Char] = Nil
  private var length: Int = 0

  def size: Int = length

  def insert(x: Char, pos: Int): Unit = {
    require(0 <= pos && pos <= length)
    val parts = chars.splitAt(pos)
    chars = parts._1 ::: (x :: parts._2)
    length += 1
  }

  def delete(pos: Int): Char = {
    require(0 <= pos && pos < length)
    val parts = chars.splitAt(pos)
    val old = parts._2.head
    chars = parts._1 ::: parts._2.tail
    length -= 1
    old
  }

  def read(pos: Int): Char = {
    require(0 <= pos && pos < length)
    chars(pos)
  }
}
The representation invariant is , with chars representing the abstract document sequence. splitAt(pos) isolates exactly the prefix before the selected array index-style position. Insertion retains that prefix and the old suffix, placing the new character between them. Deletion returns the old suffix head and retains its tail. Updating the cached length by one preserves the representation invariant. read and size preserve the abstract state.
(1)
The preconditions permit insertion at the end, including position zero in an empty document, but forbid reading or deleting at the end.
Maintain one frequency count for each lowercase alphabet character. Update only after a successful delegated operation:
trait CharTrackPlugIn extends Doc {
  private val counts = Array.fill[Int](26)(0)

  private def lower(x: Char): Boolean = 'a' <= x && x <= 'z'

  abstract override def insert(x: Char, pos: Int): Unit = {
    super.insert(x, pos)
    if (lower(x)) counts(x - 'a') += 1
  }

  abstract override def delete(pos: Int): Char = {
    val old = super.delete(pos)
    if (lower(old)) counts(old - 'a') -= 1
    old
  }

  def getCount(x: Char): Int = {
    assert('a' <= x && x <= 'z')
    counts(x - 'a')
  }
}
For an initially empty underlying implementation that inserts the character it receives and returns the character actually deleted, the representation invariant is
(1)
Insertion increases exactly one applicable frequency count, and deletion decreases the count of the returned character. Uppercase and nonletter characters contribute nothing. Exceptions from failed underlying operations leave the counters unchanged. The stackable trait modification uses abstract override because it delegates to a concrete implementation elsewhere in the mixin chain.[ref]
(2)
The counters depend on the character seen by this trait. A later trait that transforms characters can break the stated underlying-operation assumption; part (d) deliberately exposes that order dependence.
Apply capitalization before delegating insertion:
trait CapitalisePlugIn extends Doc {
  abstract override def insert(x: Char, pos: Int): Unit = {
    super.insert(x.toUpper, pos)
  }
}
Scala's Char.toUpper implements the hinted conversion and leaves ordinary nonletters unchanged. The stackable trait modification intercepts insertion without changing the position, result type or deletion behavior.
(1)
For the implementations above, the output is
0
1
In A, the Scala trait linearization sends insert('a',0) first to CapitalisePlugIn, then to CharTrackPlugIn, then to DocImpl. The counter trait receives 'A', so it does not increment the lowercase 'a' count. The stored document is A.
In B, the counter trait receives 'a', delegates through CapitalisePlugIn, and increments its original argument's counter on return. The stored document is again A, but the counter records one lowercase insertion:
(1)
This demonstrates a composition that violates the count-of-current-document representation invariant for B: an earlier counter cannot assume a later transforming trait inserts its argument unchanged. Subsequent deletion also receives uppercase 'A' and would leave that stale lowercase count. A different valid design could inspect read(pos) after insertion to count the actual stored character; that design would produce 0,0. The stated 0,1 follows the explicit implementation in part (b), whose correctness assumption has now failed in the second composition.
The first matching entry must be retained, and copying an already-started prefix-dropping iterator must not restart the search. Use a private initial buffer together with the underlying iterator snapshot:
class DropUntil[T] private (
    p: T => Boolean, iter: Iter[T],
    saved: Option[T], alreadyStarted: Boolean) extends Iter[T] {

  def this(p: T => Boolean, iter: Iter[T]) =
    this(p, iter, None, false)

  private var pending: Option[T] = saved
  private var started: Boolean = alreadyStarted

  private def prepare(): Unit = {
    if (!started) {
      var found = false
      while (!found && iter.hasNext) {
        val x = iter.next()
        if (p(x)) {
          pending = Some(x)
          found = true
        }
      }
      started = true
    }
  }

  def hasNext: Boolean = {
    prepare()
    pending.nonEmpty || iter.hasNext
  }

  def next(): T = {
    prepare()
    pending match {
      case Some(x) => pending = None; x
      case None =>
        if (!iter.hasNext) throw new NoSuchElementException("DropUntil.next")
        iter.next()
    }
  }

  def copy(): Iter[T] =
    new DropUntil[T](p, iter.copy(), pending, started)
}
Before preparation, the iterator still represents the original remaining sequence. During the search, the loop invariant says that every discarded entry fails the predicate, and pending is either empty or contains the first satisfying entry just consumed. For a finite input, the number of unread entries is a loop variant. After preparation, the abstract remaining sequence is pending.toList followed by the underlying iterator's remaining sequence. Repeated hasNext calls do not discard or test more entries after the first match.
The iterator snapshot copies both the cached entry and the started flag. In particular, copying after the matching entry has been returned continues with the remaining suffix, including later entries that fail p. Restarting new DropUntil(p, iter.copy()) at that point would wrongly drop another prefix.
(1)
As usual, assume a deterministic predicate without shared mutable effects. On an infinite input having no match, the first demand cannot terminate: no finite inspection establishes absence. Independence here concerns cursor state; arbitrary mutation of shared element objects is outside the iterator contract.
Implement the three consumers directly with while loops. These methods consume the receiver; exists stops immediately after the first witness:
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 result = x
    while (hasNext) result = f(result, next())
    result
  }
}
For foreach, the loop invariant is that f has been called once, in order, on exactly the consumed prefix. For exists, provided it has not returned, every consumed entry fails the predicate; a returned true has a witness, while exhaustion proves there is none. For foldLeft, after consumed entries the loop invariant is
(1)
with result = x at . Thus initialization, one further application, and exhaustion prove the required left fold. On finite inputs, the remaining length is a loop variant for each loop. Callbacks are assumed not to mutate this iterator independently.
(2)
With constant-cost callbacks and iterator operations, full consumption costs ; exists may return earlier. Empty inputs respectively do nothing, return false, and return x. Infinite inputs need not terminate, except that exists terminates upon reaching a witness.
If f is a pure function on immutable values, a simple implementation stores the next value and copies it into a fresh FunIter. Part (d)'s suggested mutable programming closure, however, would be shared by such copies and violate independence. A memoized iterator snapshot avoids that contradiction: all cursors share already determined sequence values, but each has its own position.
class FunIter[T](v: T, f: T => T) extends Iter[T] {
  private class Cell(val head: T) {
    lazy val tail: Cell = new Cell(f(head))
  }

  private class Cursor(private var cell: Cell) extends Iter[T] {
    def hasNext: Boolean = true

    def next(): T = {
      val answer = cell.head
      cell = cell.tail
      answer
    }

    def copy(): Iter[T] = new Cursor(cell)
  }

  private val cursor = new Cursor(new Cell(v))

  def hasNext: Boolean = true
  def next(): T = cursor.next()
  def copy(): Iter[T] = cursor.copy()
}
The first cell stores ; its lazily memoized successor stores ; the next stores , and so on. A cell's successor is evaluated at most once. The representation invariant is that each cursor points to the cell holding its next result. next returns that result and advances only this cursor. copy shares the cell, whose future is memoized, rather than the mutable cursor. Advancing either copy therefore cannot skip entries in the other.
(1)
Assume each demanded application of f terminates and generated values are immutable for purposes of observation. A stateful generator should be privately owned by this family of cursors; arbitrary external changes to it cannot be made independent by the supplied interface. Unlike the pure-function implementation, memoization can retain a long prefix while one copy lags far behind another. The question imposes no constant-storage requirement.
Use a programming closure whose private variable holds the next Fibonacci number. Use arbitrary-precision integers to enumerate all terms exactly:
def fibonacci(): Iter[BigInt] = {
  var following = BigInt(1)
  val step: BigInt => BigInt = (current: BigInt) => {
    val result = following
    following = current + following
    result
  }
  new FunIter[BigInt](BigInt(0), step)
}
At the cell containing , the private state immediately before computing its successor is following = F_(i+1). The successor returns that value and sets following to , preserving the recursion invariant. The resulting sequence starts
(1)
Each successor is computed once by the memoized implementation in part (c); interleaved copies see the same already generated successor instead of independently advancing shared programming closure state. Replacing BigInt by Int and the two initial values by 0,1 gives exactly the hinted Int => Int implementation, but eventually incurs integer overflow, so it does not enumerate all mathematical Fibonacci numbers.
An alternative avoiding mutable programming closure state represents the current and next Fibonacci numbers by a pair and uses the pure function with initial state ; a projecting iterator returns the first component. The closure construction above meets the suggested one-number interface directly.
Store one entry per occurrence in an immutable list. Use lower type bounds for arguments that might widen the element type, and remove only the first matching occurrence:
class CoMSet[+T](c: List[T]) {
  private val elems: List[T] = c

  def insert[U >: T](x: U): CoMSet[U] =
    new CoMSet[U](x :: elems)

  def delete[U >: T](x: U): CoMSet[T] = {
    def removeOne(xs: List[T]): List[T] = xs match {
      case Nil => Nil
      case h :: tail =>
        if (h == x) tail else h :: removeOne(tail)
    }
    new CoMSet[T](removeOne(elems))
  }

  def count[U >: T](x: U): Int =
    elems.count(y => y == x)

  def union[U >: T](that: CoMSet[U]): CoMSet[U] =
    new CoMSet[U](elems ::: that.elems)
}
A covariant type parameter cannot appear directly as an ordinary object method argument type. The fresh with permits insertion, deletion queries and count queries without imposing such a negative occurrence of . delete can retain result type CoMSet[T] because it introduces no new elements; widening its result to CoMSet[U] would also be valid. union must widen because the other multiset may contain the broader type. The class-private immutable elems is accessible on another instance of the same software class; it is not private[this].[ref]
Let be a multiset multiplicity. The implementations satisfy
(1)
The brackets denote an indicator function. Structural induction on the list proves removeOne removes precisely one equal entry if present, otherwise none. filterNot would incorrectly remove every occurrence. List concatenation adds multiplicities, implementing the paper's additive additive multiset union, rather than the maximum-multiplicity convention sometimes used for that name.
All methods preserve the original immutable object. insert takes constant time through structural sharing; count and delete take time, and union takes time to copy the receiver's list spine. Equality is ordinary stable value equality; finite representable counts are assumed.
Represent a multiset by a pure multiplicity function. Every operation returns a new function describing updated counts:
class ContraMSet[-T](f: T => Int) {
  def count(x: T): Int = f(x)

  def insert(x: T): ContraMSet[T] =
    new ContraMSet[T]((y: T) => f(y) + (if (y == x) 1 else 0))

  def delete(x: T): ContraMSet[T] =
    new ContraMSet[T]((y: T) => {
      val old = f(y)
      if (y == x && old > 0) old - 1 else old
    })

  def union[U <: T](that: ContraMSet[U]): ContraMSet[U] =
    new ContraMSet[U]((y: U) => this.count(y) + that.count(y))
}
An empty instance is new ContraMSet[T]((_: T) => 0). The constructor's precondition is that f is pure and gives a nonnegative integer count, with finite support of a multiset if only finite multisets are intended. Nonnegativity and the support condition are preserved by each operation. Integer overflow must be excluded for this fixed-width count interface.
A contravariant type parameter makes ContraMSet[T] a consumer of values of type T. Thus a counter able to answer queries for every animal can also answer queries restricted to cats. It does not expose or enumerate stored T values. The return type ContraMSet[T] is legal: its outer covariant result position and the class's contravariant argument position together place negatively.
For union, the argument itself is in a negative position, while its ContraMSet argument would reverse that sign. Using ContraMSet[T] directly as the parameter type would therefore put positively and fail the variance-position rule. Introduce : both operands can count every U, and their sum is a ContraMSet[U]. This is a restriction to a common query domain; operations do not promise to preserve counts outside the narrowed domain.[ref]
Pointwise evaluation gives
(1)
No old function is modified, so updates preserve immutable object. Constructing each wrapper takes constant work, but a later count may traverse a chain of previously created programming closures; its running time need not be constant in the history length. This functional representation trades enumeration and direct storage of occurrences for composable counting behavior.

Ancestors (9)

  1. 2015
  2. Past exam of the year 1 of the computer science course of the University of Oxford
  3. Year 1 of the computer science course of the University of Oxford
  4. Computer science course of the University of Oxford
  5. Undergraduate course of the University of Oxford
  6. Course of the University of Oxford
  7. University of Oxford
  8. List of universities
  9. Home

View article source

Discussion (0) New discussion

There are no discussions about this article yet.

Articles by others on the same topic (0)

There are currently no matching articles.
See all articles in the same topic Create my own version