Use merge sort, stopping before an empty or singleton linked list would be split.
PROCEDURE MergeSort(less: LESS; VAR p: List);
VAR q, r: List;
BEGIN
  IF p.count > 1 THEN
    Split(p, q, r);
    MergeSort(less, q); MergeSort(less, r);
    Merge(less, q, r, p)
  END
END MergeSort;
By induction on the length, each recursive call returns a sorted permutation of its input. Part (d) makes both child lengths smaller than the parent whenever the parent length exceeds one; part (e) combines the sorted children. No data linked list nodes are newly allocated or lost. Unreachable headers may be reclaimed by garbage collection.
At each level the total splitting and merge algorithm work is linear; approximately equal halves give logarithmic depth. Consequently
There are header allocations over the whole execution; those allocations should not be confused with the logarithmic call stack bound.
Assume less is a lawful strict comparison, for example a strict weak order, and the two input linked lists are disjoint and sorted by it. Allocate a result header and move existing data linked list nodes; do not copy their values.
PROCEDURE Merge(less: LESS; q, r: List; VAR p: List);
VAR result: List; last, a, b: Tail;
BEGIN
  NEW(result); result.count := q.count + r.count;
  result.tail := NIL; last := result;
  a := q.tail; b := r.tail;
  WHILE (a # NIL) & (b # NIL) DO
    IF less(b,a) THEN
      last.tail := b; b := b.tail
    ELSE
      last.tail := a; a := a.tail
    END;
    last := last.tail
  END;
  IF a # NIL THEN last.tail := a ELSE last.tail := b END;
  q.tail := NIL; q.count := 0;
  r.tail := NIL; r.count := 0;
  p := result
END Merge;
The loop invariant says that the segment from result.tail through last is a sorted prefix of the desired merge algorithm, containing exactly the nodes already removed from the two unread chains. Every element of this prefix is no greater than either unread head. Choosing the smaller unread head maintains this property; choosing from q on a tie also gives stable sorting.
At exit, at most one unread chain is nonempty, and its sorted suffix can be attached as a whole. Each original data linked list node occurs exactly once in the result, and its saved count is correct. Clearing the consumed headers prevents them from claiming ownership of the result's nodes.
Reuse p as q's header and allocate one new header for r. Cut after data elements, allowing .
PROCEDURE Split(p: List; VAR q, r: List);
VAR n, k, i: INTEGER; last: Tail;
BEGIN
  n := p.count; k := n DIV 2;
  q := p; NEW(r);
  last := q;
  FOR i := 1 TO k DO last := last.tail END;
  r.tail := last.tail; last.tail := NIL;
  q.count := k; r.count := n-k
END Split;
The traversal starts at the dummy header node, so after steps last precedes the suffix assigned to r. Cutting that link produces two finite disjoint linked lists. Their concatenated abstraction function is the original list, with order preserved, and
Both empty and singleton inputs work without special traversal cases. The time complexity is and only one header is allocated.
The representation invariant is
Every reachable non-NIL pointer designates an allocated linked list node of the appropriate extension type. The header is not a data element. In operations consuming two separate linked lists, their headers and data chains must additionally be disjoint; this ownership precondition prevents accidental aliasing during a destructive merge algorithm.
A dummy header node gives the first actual linked list node a predecessor, just like every other element. Linked-list deletion and insertion at the front can therefore update a predecessor's tail with the same code used in the middle. An empty linked list is represented by a header whose tail is NIL.
For finite acyclic chains, define the abstraction function recursively by
Here the list contains linked list nodes themselves. For an extension storing a value value, its value-level abstraction function is . Finiteness and absence of a graph cycle ensure that these recursive definitions terminate. A dummy header node is excluded by applying to its tail.
Use half-open rectangles . Split the longer dimension at its middle. If rows are the longer dimension, binary search the middle row for its first entry at least . Equality returns immediately; otherwise part (e) leaves only an upper-right and a lower-left rectangle. A middle-column split uses the transposed argument.
PROCEDURE SearchRect(x, r0, r1, c0, c1: INTEGER;
                     VAR i, j: INTEGER): BOOLEAN;
VAR mid, lo, hi, k: INTEGER;
BEGIN
  IF (r0 >= r1) OR (c0 >= c1) THEN RETURN FALSE END;
  IF r1-r0 >= c1-c0 THEN
    mid := r0 + (r1-r0) DIV 2;
    lo := c0; hi := c1;
    WHILE lo < hi DO
      k := lo + (hi-lo) DIV 2;
      IF f[mid,k] < x THEN lo := k+1 ELSE hi := k END
    END;
    IF lo < c1 THEN
      IF f[mid,lo] = x THEN i := mid; j := lo; RETURN TRUE END
    END;
    IF SearchRect(x, r0, mid, lo, c1, i, j) THEN
      RETURN TRUE
    END;
    RETURN SearchRect(x, mid+1, r1, c0, lo, i, j)
  ELSE
    mid := c0 + (c1-c0) DIV 2;
    lo := r0; hi := r1;
    WHILE lo < hi DO
      k := lo + (hi-lo) DIV 2;
      IF f[k,mid] < x THEN lo := k+1 ELSE hi := k END
    END;
    IF lo < r1 THEN
      IF f[lo,mid] = x THEN i := lo; j := mid; RETURN TRUE END
    END;
    IF SearchRect(x, r0, lo, mid+1, c1, i, j) THEN
      RETURN TRUE
    END;
    RETURN SearchRect(x, lo, r1, c0, mid, i, j)
  END
END SearchRect;

PROCEDURE DivideSearch(x: INTEGER; VAR i, j: INTEGER): BOOLEAN;
BEGIN
  RETURN SearchRect(x, 0, M, 0, N, i, j)
END DivideSearch;
The lower-bound binary search invariant says that entries before lo are smaller than and entries from hi onward are at least , within the splitting row or column. At its end, either equality is found or the splitting line is strictly separated around . Endpoint cuts lo=c0, lo=c1, lo=r0, or lo=r1 are valid and merely make one candidate rectangle empty.
The recursion invariant is that the current rectangle contains every still-possible answer assigned to that call. The discarded rectangles are excluded by monotonicity; both retained rectangles inherit monotonicity. Each nonempty child has a strictly smaller longest dimension after at most two levels, so the recursion terminates, including one-row and one-column cases. The concise construction is
Monotonicity gives two excluded rectangles:
Indeed the first entries are at most , and the second are at least . In particular, the entire splitting row contains no answer. The only remaining candidates are the upper-right rectangle and the lower-left rectangle . These are the exclusions guaranteed by the given adjacent inequalities; further comparisons may exclude more.
Implement staircase matrix search from the top-right corner. In the following Oberon-style code, & denotes short-circuit conjunction; all guarded accesses respect array bounds.
PROCEDURE Staircase(x: INTEGER; VAR i, j: INTEGER): BOOLEAN;
VAR r, c: INTEGER;
BEGIN
  r := 0; c := N-1;
  WHILE (r < M) & (c >= 0) DO
    IF f[r,c] = x THEN i := r; j := c; RETURN TRUE
    ELSIF f[r,c] < x THEN INC(r)
    ELSE DEC(c)
    END
  END;
  RETURN FALSE
END Staircase;
The loop invariant is that every occurrence not yet returned lies in
Initially this is the whole array. If , every entry of row in the candidate rectangle is smaller than , so increasing discards no possible answer. If , every entry of column in that rectangle is greater than , so decreasing is safe. These conclusions follow from monotonicity even when repeated values occur.
The loop variant decreases on every unsuccessful iteration. If a dimension becomes empty, the loop invariant proves absence. For positive dimensions the path inspects at most entries; an initially empty dimension causes no inspection. Thus
Write , assuming . By monotonicity, is at least every value in the first row and at most every value in the last column. Hence
The same observation applies to the top-right corner of any remaining rectangular subarray of this monotone matrix.
Use a linear search over every pair of array indices.
PROCEDURE SearchAll(x: INTEGER; VAR i, j: INTEGER): BOOLEAN;
VAR r, c: INTEGER;
BEGIN
  FOR r := 0 TO M-1 DO
    FOR c := 0 TO N-1 DO
      IF f[r,c] = x THEN i := r; j := c; RETURN TRUE END
    END
  END;
  RETURN FALSE
END SearchAll;
For a worst-case lower bound, consider an input in which every inspected element differs from . If an element remains uninspected, changing just that element to gives an indistinguishable execution requiring the opposite answer. Therefore a correct exact search algorithm must inspect all elements in the worst case.
The printed phrase “at least ” uses the upper-bound notation for a lower-bound claim. Its precise interpretation is
This is an adversary argument for access to arbitrary independent array entries.
With the fixed array f visible to the procedures, use a Boolean result for success and two output array indices:
TYPE Search = PROCEDURE(x: INTEGER; VAR i, j: INTEGER): BOOLEAN;
On success, , , and . On failure there is no occurrence; the output indices are unspecified. Thus
Maintain a cursor to the first unread marker. A fork consumes its own marker and then two complete encodings, in left-to-right order.
PROCEDURE Decode(VAR code: ARRAY OF INTEGER;
                 VAR pos: INTEGER): Tree;
VAR marker: INTEGER; left, right: Tree;
BEGIN
  marker := code[pos]; INC(pos);
  IF marker = 0 THEN RETURN 0 END;
  ASSERT(marker = 1);
  left := Decode(code, pos);
  right := Decode(code, pos);
  RETURN NewFork(left, right)
END Decode;
Start with pos := 0; t := Decode(code, pos), with sufficient unused arena space. The valid-input precondition ensures that every read exists and every fork has two encoded subtrees. Evaluating the two recursive calls in separate statements fixes their order.
Structural induction shows that decoding reconstructs the same binary tree shape and leaves the cursor just after its encoding. The tree handles need not coincide with the original handles: the abstract tree does. The result is
The time complexity is linear in the encoding length, with call stack space bounded by the height of a binary tree.
Let be the final output length, the number of emitted markers, and the number of pending handles. Each pending subtree contributes at least one future marker, so
Store output from the low end and the stack from the high end of the same array. A pop frees one cell before the next write. For a fork, the two pushed children each account for at least one of the remaining markers. Thus the two regions never overlap.
PROCEDURE PreorderShared(t: Tree; VAR out: ARRAY OF INTEGER;
                         VAR count: INTEGER);
VAR top, cap: INTEGER; p: Tree;
BEGIN
  cap := LEN(out); count := 0;
  top := cap-1; out[top] := t;
  WHILE top < cap DO
    p := out[top]; INC(top);
    IF p = 0 THEN
      out[count] := 0; INC(count)
    ELSE
      out[count] := 1; INC(count);
      DEC(top); out[top] := nodes[p-1].right;
      DEC(top); out[top] := nodes[p-1].left
    END
  END
END PreorderShared;
The loop invariant includes count <= top, with pending handles in out[top..cap) and final markers in out[0..count). The preceding accounting proves every intermediate write also respects array bounds. This uses the integer handle representation chosen in part (b). Simply putting a pointer into a genuinely Boolean-typed cell would not be valid Oberon.
Use an explicit stack of handles. Push the right subtree first, so that the left subtree is removed first by the LIFO stack.
PROCEDURE PreorderIter(t: Tree; VAR out: ARRAY OF INTEGER;
                       VAR count: INTEGER;
                       VAR stack: ARRAY OF Tree);
VAR top: INTEGER; p: Tree;
BEGIN
  count := 0; top := 1; stack[0] := t;
  WHILE top > 0 DO
    DEC(top); p := stack[top];
    IF p = 0 THEN
      out[count] := 0; INC(count)
    ELSE
      out[count] := 1; INC(count);
      stack[top] := nodes[p-1].right; INC(top);
      stack[top] := nodes[p-1].left; INC(top)
    END
  END
END PreorderIter;
The loop invariant says that the already written prefix, followed by the preorder traversals of the pending subtrees in top-to-bottom stack order, equals the entire required output. Popping a leaf of a rooted tree transfers one marker to the prefix. Popping a fork transfers its marker and replaces its remaining work by left then right subtree work. Both preserve the loop invariant. The number of as-yet-unwritten vertices decreases by one per iteration, proving termination.
The time complexity is linear in the output length. The maximum stack size is at most one plus the height of a binary tree.
For parts (b)–(e), use array indices as tree handles. This also makes the shared storage in part (d) type-correct: both pending handles and output markers occupy integer cells. Zero denotes a leaf of a rooted tree; a positive handle denotes a fork whose children are in nodes[t-1]. Only finite acyclic structures are admitted. An allocated fork's children are themselves valid handles.
CONST MaxForks = 100000;
TYPE Tree = INTEGER;
     Node = RECORD left, right: Tree END;
     Arena = ARRAY MaxForks OF Node;
VAR nodes: Arena;
    used: INTEGER;

PROCEDURE NewFork(left, right: Tree): Tree;
BEGIN
  ASSERT(used < MaxForks);
  nodes[used].left := left; nodes[used].right := right;
  INC(used);
  RETURN used
END NewFork;

PROCEDURE Preorder(t: Tree; VAR out: ARRAY OF INTEGER;
                   VAR count: INTEGER);
  PROCEDURE Visit(p: Tree);
  BEGIN
    IF p = 0 THEN
      out[count] := 0; INC(count)
    ELSE
      out[count] := 1; INC(count);
      Visit(nodes[p-1].left); Visit(nodes[p-1].right)
    END
  END Visit;
BEGIN
  count := 0; Visit(t)
END Preorder;
Initialize used := 0 before constructing any trees; NewFork allocates within this arena. The fixed capacity is an implementation parameter and may be replaced by a dynamically allocated arena. The returned prefix out[0..count) encodes Boolean values by and . This encoding is part of the chosen representation, not a conversion of a pointer into a Boolean value.
The recursion invariant is that Visit(p) appends exactly the preorder traversal of the subtree represented by p. If the full binary tree has forks, it has leaves; hence
Each occurrence is visited once, using linear time complexity and a call stack bounded by the height of a binary tree. The arena is the input representation, not an extra copy made by the traversal.
In executable Haskell, the algebraic data type declaration uses data, rather than the printed type. A leaf of a rooted tree contributes False; a fork contributes True followed by its left and right subtrees in that order.
data Tree = Leaf | Fork Tree Tree

preorder :: Tree -> [Bool]
preorder Leaf       = [False]
preorder (Fork l r) = True : (preorder l ++ preorder r)
This is a preorder traversal of a full binary tree, including the leaves. Structural induction proves correctness: the leaf of a rooted tree case has precisely one output, and the fork case concatenates the correct preorder traversals of its two subtrees after its own marker.
An equivalent version avoids repeatedly copying the left list through list concatenation:
preorder t = walk t []
  where
    walk Leaf rest       = False : rest
    walk (Fork l r) rest = True : walk l (walk r rest)
Its strengthening is walk t rest = preorder t ++ rest. Each vertex constructs one list cell, so this version has linear time complexity. The concise result is
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
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.
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
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.
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
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.

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!
We have two killer features:
  1. 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-calculus
    Articles 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/derivative
  2. 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.
    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.
  3. https://raw.githubusercontent.com/ourbigbook/ourbigbook-media/master/feature/x/hilbert-space-arrow.png
  4. Infinitely deep tables of contents:
    Figure 6.
    Dynamic article tree with infinitely deep table of contents
    .
    Descendant pages can also show up as toplevel e.g.: ourbigbook.com/cirosantilli/chordate-subclade
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