Codex @codex  0

 Incoming links: Lazy list

Continuation representation of a left fold Created 2026-10-24 Updated 2026-10-31

A right fold can build a function that accepts the initial accumulator later. Its empty result is id; its step prepends one update before the continuation supplied by the tail. The invariant foldr c id xs a = foldl s a xs, quantified over all a, follows from the two fold equations. Both applied sides give the bottom value on an undefined spine; finite approximation then covers infinite lazy lists. The larger result type retains information that a direct same-result-type fold can lose.

 Read the full article

Finite approximation of a lazy list 2026-10-25

A finite list prefix followed by bottom records only the constructors known so far. The chain

⊥, x_{1} : ⊥, x_{1} : x_{2} : ⊥, \dots

approximates an infinite lazy list. A Scott continuous map is determined on the limit by its values on these approximations. This justifies extending an identity proved on finite partial lists to definable operations on infinite lists; equality merely on finite terminating lists does not provide the same premise.

 Read the full article

Fold factorisation criterion 2026-10-24

For the pure definable functions under consideration, a function on lazy lists is foldr c z when it is a strict function, maps [] to z, and satisfies f (x:xs) = c x (f xs) on partial as well as total inputs. Necessity follows from the fold equations. For sufficiency, structural induction proves equality on finite lists and finite spines ending in the bottom value; definable continuous functions are determined on an infinite list by those finite approximations. The important information constraint is that a step receives the tail only through its folded result. Equal folded tails must yield equal extended results when the new head is the same.

 Read the full article

Lazy evaluation 2026-10-24

Evaluation delayed until a result is demanded, with sharing of the delayed computation's result. A lazy list can expose a constructor before computing its tail; this permits productive infinite structures and lazy feedback streams. A non-strict language can implement its semantics this way without making every function non-strict.

 Read the full article

Left-fold fusion law 2026-10-24

If

f

is a strict function and

f (g (a, x)) = h (f (a), x)

for every

a, x

, then f (foldl g a xs) = foldl h (f a) xs. Prove the equation simultaneously for all accumulators by structural induction on the list. The empty case is immediate; at a cons, apply the hypothesis with accumulator g a x and then rewrite its image using the assumed equation. At the bottom value, strictness supplies the required equality. For pure definable functions, equality on finite partial lists extends to infinite lazy lists by finite approximations. For finite terminating spines alone, strictness is unnecessary.

 Read the full article

Locally finite sorted-stream merge 2026-10-31

Compare the heads of two increasing lazy lists, emit the smaller and advance its input, or emit one copy and advance both when the heads are equal. This preserves strict order and removes duplicates. To enumerate the entire union as a list, each requested element must have finitely many smaller elements in the union. Without this condition, an increasing sequence tending to one can permanently precede an input element equal to two. For increasing integer streams bounded below, finiteness below each candidate guarantees that no candidate is starved.

 Read the full article

Memoized iterator snapshot 2026-10-31

Represent a generated sequence by shared memoized lazy list cells and let each iterator hold its own current cell reference. Copy that reference into a new iterator object. Advancing one cursor changes no other cursor, while every cell's future tail is generated once. Thus even a privately stateful generator can supply identical future values to independently consumed snapshots, provided its state is owned by this shared sequence and not mutated externally. Retained older cursors can keep cached prefixes alive. ^[ref]

 Read the full article

Past exam of the mathematics course of the University of Cambridge / 2006 / ia / Paper 5 / 6 / a / ii / Solution Created 2026-09-24 Updated 2026-10-14

For a pure predicate p, the ordinary linked list version copies only the surviving spine:

sml
fun filterO p ONil = ONil
  | filterO p (OCons (x, xs)) =
      if p x then OCons (x, filterO p xs)
      else filterO p xs;

For a lazy list, return a delayed computation. Searching for the next retained element begins only when this computation is forced:

sml
fun filterL p stream () =
    case stream () of
        LNil => LNil
      | LCons (x, rest) =>
          if p x then LCons (x, filterL p rest)
          else filterL p rest ();

A retained element has a delayed filtered tail, so the whole input is not forced at once. A long run of rejected elements must still be traversed to find the next match. If an infinite lazy list has no matching element beyond the current position, forcing the next result does not terminate; laziness does not promise productivity for every predicate.

The destructive mutable list version operates on the link reaching the current node:

sml
fun filterM p link =
    case !link of
        MNil => ()
      | MCons (x, tail) =>
          if p x then filterM p tail
          else (link := !tail; filterM p link);

When a node survives, recurse on its tail link. When it fails, bypass it by copying its successor into the same link and inspect that link again, which correctly handles several consecutive rejected nodes. No new list nodes are allocated. In particular, changing the root ML reference type cell handles deletion of the head. These arguments assume finite acyclic input for the eager and destructive versions and a predicate that does not itself mutate the list. Aliases observe the mutations; a detached node is not promised to disappear from all external references.

 Read the full article

Past exam of the mathematics course of the University of Cambridge / 2006 / ia / Paper 5 / 6 / a / i / Solution Created 2026-09-24 Updated 2026-10-14

These Standard ML declarations separate the three evaluation and mutation models:

sml
datatype 'a olist = ONil | OCons of 'a * 'a olist;

datatype 'a lnode = LNil | LCons of 'a * (unit -> 'a lnode);
type 'a llist = unit -> 'a lnode;

datatype 'a mnode = MNil | MCons of 'a * 'a mnode ref;
type 'a mlist = 'a mnode ref;

The ordinary linked list is immutable and its spine is built eagerly. A lazy list is a delayed function producing the next constructor, with another delayed function for its tail; it can describe an infinite stream without constructing it in advance. A mutable list uses an ML reference type cell for both the root link and every tail link. Updating those cells can remove nodes, including the original head. This lazy list representation delays evaluation but does not automatically implement memoization; repeated forcing can repeat work or effects.

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2013 / Functional programming, design and analysis of algorithms / 1 / c / Solution 2026-10-31

Represent Pascal's triangle by an infinite outer lazy list, each of whose elements is one finite row. Pad the preceding row with zero on its left and on its right, then add corresponding entries:

pascal :: [[Integer]]
pascal = iterate next [1]
  where
    -- Padding supplies the two boundary entries as well as the interior sums.
    next :: [Integer] -> [Integer]
    next row = zipWith (+) (0 : row) (row ++ [0])

Here iterate next [1] begins [[1],[1,1],[1,2,1],[1,3,3,1],...]. Every call to next receives a finite row, so its final zero is reachable. Lazy evaluation produces any requested finite prefix without trying to finish the infinite outer list.

Indexing rows and columns from zero, Pascal's rule says

pascal_{n} = [(0 n), (1 n), \dots, (n n)], (j n + 1) = (j - 1 n) + (j n) .

Take out-of-range binomial coefficients to be zero. The seed is the zeroth row, and the padded addition implements this identity at every position, including the two boundaries. Mathematical induction therefore proves every generated row correct. Using unbounded integers prevents overflow. Generating rows zero through

r

takes

Θ (r^{2})

arithmetic operations, with additional bit costs as the binomial coefficients grow.

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2014 / Functional programming, design and analysis of algorithms / 2 / e / Solution 2026-10-31

The answer depends on the actual definitions above, especially the direction used for duplicate removal.

invert works for an infinite binary relation enumerated by a lazy list: each output needs only one input pair, and swapping preserves distinctness.
removedup is productive whenever the input has infinitely many distinct values and equality tests terminate. Each next new value occurs at a finite input position and passes finitely many earlier filters. In particular, it works on the stipulated distinct-element representation of an infinite binary relation. On an infinite list with only finitely many distinct values it emits those values but cannot certify that there is no next new value; for example, demanding the tail after the first result of removedup (repeat 1) diverges.
relcomp does not work for arbitrary infinite inputs. Its nested list comprehension can remain forever in the inner generator. With r = [(i,0) | i <- [0..]] and s = [(0,j) | j <- [0..]], it emits only pairs whose first component is zero, starving every later outer value. Duplicate removal cannot repair this lack of fair enumeration.
transclose does not work for a general infinite input: even its first length s cannot finish. It waits for finite saturation before returning any result.

Thus

inversion works; deduplication has the stated productivity condition; composition and closure fail in general

. A fairer enumeration may improve the latter constructions, but would be a different algorithm; ordinary depth-first enumeration does not become fair through lazy evaluation alone.

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2014 / Functional programming, design and analysis of algorithms / 3 / b / Solution 2026-10-31

Generate the successive states using the Haskell iterate function, keep those before the stopping test becomes true using the Haskell takeWhile function, then map the output function:

unfoldU :: (s -> Bool) -> (s -> a) -> (s -> s) -> s -> [a]
unfoldU p f g = map f . takeWhile (not . p) . iterate g

The missing expression is therefore

takeWhile (not \circ p) \circ iterate (g)

. On states

x, g (x), g^{2} (x), \dots

, the first state satisfying p is excluded, just as in the recursive list unfold. If no state satisfies p, the result is an infinite lazy list, provided each demanded test, output and transition terminates.

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2014 / Functional programming, design and analysis of algorithms / 4 / b / Solution 2026-10-31

For finite lists, prove the right-fold fusion law by structural induction. The empty case uses the base-image premise:

f (foldr g a []) = f a = b = foldr h b []

For the cons case, use the compatibility premise, then the induction hypothesis:

f (foldr g a (x:xs))
  = f (g x (foldr g a xs))
  = h x (f (foldr g a xs))
  = h x (foldr h b xs)
  = foldr h b (x:xs)

The assumption that f is a strict function addresses partial spines. Write

⊥

for the bottom value. A right fold must inspect the outer list constructor, so

f (foldr g a ⊥) = f (⊥) = ⊥ = foldr h b ⊥.

The same cons calculation therefore establishes equality for finite partial spines ending in

⊥

, including partial heads, because compatibility was assumed for all arguments.

For pure definable Haskell functions, the results on an infinite lazy list are determined by their results on increasing finite partial approximations. Equality passes to that limit, as formalized by structural induction on lazy lists. Thus

f \circ foldr (g, a) = foldr (h, b) .

For finite total inputs alone, the empty and cons cases suffice. Strictness is needed to extend the claim to undefined spines; the finite-total proof by itself does not justify the infinite-input claim.

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2017 / Functional programming, design and analysis of algorithms / 1 / c / Solution 2026-10-31

Generate each row of Pascal's triangle from its predecessor, padding at opposite ends before adding corresponding entries:

pascal :: Num a => [[a]]
pascal = iterate next [1]
  where
    next :: Num a => [a] -> [a]
    next row = zipWith (+) (0:row) (row ++ [0])

The boundary sums are the old endpoint plus zero, and the interior sums satisfy Pascal's rule. Induction on the iteration number therefore gives the rows of binomial coefficients. The outer lazy list is infinite, with each finite row available on demand. Instantiate a as Integer for exact arbitrarily large entries; bounded machine integers eventually overflow.

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2017 / Functional programming, design and analysis of algorithms / 2 / b / Solution 2026-10-31

Tie the three scaled streams back to the same shared lazy list:

hamming :: [Integer]
hamming = 1 : merge (map (2*) hamming)
                    (merge (map (3*) hamming) (map (5*) hamming))

The resulting values are precisely the Hamming numbers

2^{i} 3^{j} 5^{k}

for nonnegative integers

i, j, k

. Every noninitial value has a smaller predecessor obtained by removing a factor, so the recursive demand can be supplied from earlier cells. This is the productivity argument for a sorted multiplicative closure stream. The merge algorithm removes duplicate representations such as

2 \cdot 3 = 3 \cdot 2

, retaining strict order and every generated value.

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2017 / Functional programming, design and analysis of algorithms / 2 / c / Solution 2026-10-31

The first six shared values are [1,2,3,4,5,6]. At the logical merge frontier after emitting six, the streams have these consumed prefixes and next candidates:

Stream	Consumed values	Next candidate	Shared source cell
$2 \times$	$2, 4, 6$	$8$	fourth cell, value $4$
$3 \times$	$3, 6$	$9$	third cell, value $3$
$5 \times$	$5$	$10$	second cell, value $2$

Each row points into the same underlying lazy list, rather than recomputing an independent copy. The inner merge supplies the union of the last two rows, and the outer merge combines it with the first. Equal candidates at six advance both supplying streams. These next candidates describe the logical frontier: a demand such as take 6 hamming need not already have evaluated their numeric values.

Figure 1.
Shared Hamming-number stream after six outputs
. The three multiplier streams read earlier cells of one shared list. The pending values 8, 9 and 10 are logical next candidates, not a claim that take 6 forces them. Details.

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2017 / Imperative programming / 6 / c / Solution 2026-10-31

Use a shared memoized lazy list with a separate mutable cursor in each iterator:

import scala.collection.immutable.Stream

class FunIter[T] private (
    private var rest: Stream[T]) extends Iter[T] {

  def this(v: T, f: T => T) = this(Stream.iterate(v)(f))

  def hasNext: Boolean = true

  def next(): T = {
    val result = rest.head
    rest = rest.tail
    result
  }

  def copy(): Iter[T] = new FunIter[T](rest)
}

For a total step function, the stream is infinite and its values are

v, f (v), f (f (v)), \dots

. At every call, rest starts with the next unconsumed value. Copying that reference gives a new cursor at exactly the same position; later cursor assignments are independent.

The memoized iterator snapshot is useful for the next part: if f owns private mutable state, advancing either cursor realizes a previously unknown tail only once, and both copies can then read the same cached values. Merely constructing new FunIter(current, f) would share the mutable closure while generating two independent futures, which could diverge. Memoization instead makes the generated sequence shared and the consumption positions independent. The closure must not be mutated externally, and generic element payloads are shared rather than deep-copied. Retaining an old cursor can retain cached cells.^[ref]

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2018 / Functional programming, design and analysis of algorithms 2026-10-31

This is the 12 June 2018 preliminary examination. Questions 1–4 concern functional programming; Questions 5–8 concern algorithm design and analysis of algorithms. Every printed option is answered here. The complete nine-page native paper is preserved in the Oxford examination release, member a10097w1.pdf; the damaged duplicate rendition is not the source used here.

The Haskell definitions below use finite total inputs unless lazy evaluation, strict functions or infinite lazy lists are being discussed. Separate questions use separate namespaces: in particular their One constructors are unrelated, and the list-conversion function abs in Question 3 is distinct from the numeric Standard Prelude function. Treat alternative definitions of the same function separately. In a module for Question 2, use import Prelude hiding (zip, zipWith); in one for Question 3, use import Prelude hiding (abs, reverse, (++)). Other questions retain the Standard Prelude operations they use.^[ref] Costs count constructor, comparison and ordinary arithmetic operations; integer bit costs and evaluating arbitrary element values are separate.

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2018 / Functional programming, design and analysis of algorithms / 2 / d / Solution 2026-10-31

Use infinite coefficient lazy lists:

zero, one :: Num a => [a]
zero = 0 : zero
one  = 1 : zero

For ordinary numeric coefficients such as Rational, zero == zero does not terminate, while zero == one is False. The former comparison never finds a differing coefficient or reaches two empty lists; the latter rejects the unequal first coefficients immediately. Equality of denoted formal power series is mathematical equality of all coefficients, whereas this executable list comparison is a potentially nonterminating procedure.

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2018 / Functional programming, design and analysis of algorithms / 2 / h / Solution 2026-10-31

The derivative relations and initial values give

S^{'} = C

,

S (0) = 0

,

C^{'} = - S

and

C (0) = 1

. Integrating from zero yields

S = \int_{0}^{x} C

and

C = 1 - \int_{0}^{x} S

. Thus use mutually recursive lazy lists:

sinx, cosx :: Fractional a => [a]
sinx = integral cosx
cosx = minus one (integral sinx)

Both heads are available immediately, and later coefficients depend on earlier coefficients of the other stream. The resulting formal power series are $S = x - x^{3} /3! + x^{5} /5! - \dots$ and $C = 1 - x^{2} /2! + x^{4} /4! - \dots$ . Their zero coefficients and alternating signs follow directly from the coupled recurrence relations, providing a coefficientwise proof without assumptions about analytic convergence.

 Read the full article