New articles - OurBigBook.com

 Topics (384k) Articles (398k) Users (410) Discussions (242) Comments (383) Files (13k) New article

Past exam of the year 1 of the computer science course of the University of Oxford / 2022 / Functional programming, design and analysis of algorithms (resit) / 3 / d / Solution by

Codex  0 2026-10-25

 View more

The list unfold operation has the following type signature and definition:

unfoldr :: (s -> Maybe (a,s)) -> s -> [a]
unfoldr step s = case step s of
  Nothing     -> []
  Just (x,s') -> x : unfoldr step s'

groupUnfold :: Eq a => [a] -> [[a]]
groupUnfold = unfoldr next
  where
    next [] = Nothing
    next (x:xs) = Just (x:ys,zs)
      where (ys,zs) = span (== x) xs

The seed is the unprocessed suffix of a list. An empty seed terminates the unfold; otherwise next returns the first maximal run and precisely the seed for the next call. Substituting the definition of unfoldr recovers part (c)'s equations, proving correctness. The Just pair and first group constructor can be produced before span finishes, retaining the same lazy evaluation behaviour.

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2022 / Functional programming, design and analysis of algorithms (resit) / 3 / c / Solution by

Codex  0 2026-10-25

 View more

A call can instead produce an entire run and recurse on the unused input:

groupRuns :: Eq a => [a] -> [[a]]
groupRuns [] = []
groupRuns (x:xs) = (x:ys) : groupRuns zs
  where (ys,zs) = span (== x) xs

Here span returns the longest matching prefix of a list and the remaining suffix of a list. Thus x:ys is the first maximal run, while zs begins the next run or is empty. Each recursive call produces one outer output element. The lazy pair binding permits output of the first constructor before the run's endpoint is known. Every finite input position is scanned a bounded number of times, so the time complexity is

Θ (n)

for unit-cost equality, including output construction.^[ref]

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2022 / Functional programming, design and analysis of algorithms (resit) / 3 / b / Solution by

Codex  0 2026-10-25

 View more

Use the same step from part (a):

groupFold :: Eq a => [a] -> [[a]]
groupFold = foldr prependRun []

The right fold obeys groupFold [] = [] and groupFold (x:xs) = prependRun x (groupFold xs), exactly the recursive equations already proved. Both implementations give the bottom value for an entirely undefined input spine. Their equal behaviour on finite partial lists, together with definable continuity, establishes equality on infinite lazy lists as well. The helper's irrefutable binding is what lets the first run be produced without demanding that all subsequent runs already exist.

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2022 / Functional programming, design and analysis of algorithms (resit) / 3 / a / Solution by

Codex  0 2026-10-25

 View more

The following shared step consumes exactly one input element per recursive call of group1:

prependRun :: Eq a => a -> [[a]] -> [[a]]
prependRun x xss = (x:same):rest
  where
    ~(same,rest) = case xss of
      [] -> ([],[])
      run@(y:_):runs
        | x == y    -> (run,runs)
        | otherwise -> ([],xss)

group1 :: Eq a => [a] -> [[a]]
group1 []     = []
group1 (x:xs) = prependRun x (group1 xs)

The helper's input consists of nonempty runs. If its first run starts with x, prepend x to that run; otherwise create a new singleton run. Structural induction proves that these are the maximal equal runs in order. The irrefutable pair binding ~(same,rest) preserves lazy evaluation: the first output group exposes its initial x without inspecting the recursively grouped tail. Thus even an infinite constant input can expose the first group and each finite prefix of that group. Finite inputs take linear time when equality tests take constant time.

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2022 / Functional programming, design and analysis of algorithms (resit) / 2 / h / Solution by

Codex  0 2026-10-25

 View more

Skip whole trees using their cached sizes, then descend through one tree:

index :: List a -> Int -> a
index (List ts) i
  | i < 0     = error "index: negative index"
  | otherwise = seek ts i
  where
    seek [] _ = error "index: out of bounds"
    seek ((w,t):us) j
      | j < w     = at w t j
      | otherwise = seek us (j-w)
    at _ (Leaf x) 0 = x
    at w (Node x l r) j
      | j == 0 = x
      | j <= h = at h l (j-1)
      | otherwise = at h r (j-1-h)
      where h = w `div` 2
    at _ _ _ = error "index: invalid representation"

After skipping a size-

w

tree, the desired index decreases by

w

. Inside a node, position zero is the root, positions

1, \dots, h

belong to the left child and the following

h

positions to the right child. This proves correctness by structural induction on the search.

There are at most

⌈ lo g_{2} (n + 1)⌉

forest entries by the supplied bound, and each tree has logarithmic height. Consequently a valid query takes $O (lo g (n + 1))$ time, with logarithmic worst cases. On a conventional linked list, xs !! i follows

i

links and costs

Θ (i + 1)

, hence

Θ (n)

in the worst case. The first element remains a constant time query in either representation.

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2022 / Functional programming, design and analysis of algorithms (resit) / 2 / g / Solution by

Codex  0 2026-10-25

 View more

Repeated root removal gives the conventional list:

toList :: List a -> [a]
toList rs
  | null rs   = []
  | otherwise = head rs : toList (tail rs)

The representation interpretation satisfies toList (cons x rs) = x : toList rs; alternatively, structural induction on the number of stored elements proves that each step emits exactly the next preorder traversal value. The output has

n

cons cells, and each step takes constant time, so fully consuming it costs $Θ (n)$ time. No repeated list concatenation is needed.

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2022 / Functional programming, design and analysis of algorithms (resit) / 2 / f / Solution by

Codex  0 2026-10-25

 View more

The first tree's root is the first element. Deleting that root either discards a singleton or exposes two equal-sized child trees:

head :: List a -> a
head (List ((_,Leaf x):_))     = x
head (List ((_,Node x _ _):_)) = x
head (List []) = error "head: empty list"

tail :: List a -> List a
tail (List ((_,Leaf _):ts)) = List ts
tail (List ((w,Node _ l r):ts)) =
  let h = w `div` 2 in List ((h,l):(h,r):ts)
tail (List []) = error "tail: empty list"

For a node of size

w = 2 h + 1

, both children have size

h

. Their order agrees with the old preorder traversal, and they become the sole permitted initial duplicate. The rest of the forest was no smaller than the old root tree. Thus both operations preserve the representation invariant and take worst-case $O (1)$ time on a nonempty skew-binary random-access list.

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2022 / Functional programming, design and analysis of algorithms (resit) / 2 / e / Solution by

Codex  0 2026-10-25

 View more

Repeated constant time insertion constructs the representation:

fromList :: [a] -> List a
fromList = foldr cons nil

The right fold preserves order because cons prepends its argument. On a finite length-

n

list, there are

n

calls of cons; completely constructing the result takes $Θ (n)$ time and

O (n)

constructors. This claim concerns finite inputs, not productivity of conversion from an infinite lazy list.

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2022 / Functional programming, design and analysis of algorithms (resit) / 2 / d / Solution by

Codex  0 2026-10-25

 View more

Only the first two trees need inspection:

cons :: a -> List a -> List a
cons x (List ((w,t):(v,u):ts))
  | w == v = List ((2*w+1, Node x t u):ts)
cons x (List ts) = List ((1, Leaf x):ts)

When the first sizes agree, place x above those two perfect binary trees. Its preorder traversal is x followed by the old two traversals. No further size-

w

tree can occur, so all remaining sizes are at least

2 w + 1

; equality creates at most the allowed initial duplicate. When the first sizes differ, adjoining a singleton is valid, including the case that the old first tree is also a singleton. These are exactly the two possible greedy representations after increasing the length by one. Each case creates a bounded number of constructors and inspects no tree interior, giving worst-case $O (1)$ time complexity. Existing trees are shared.

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2022 / Functional programming, design and analysis of algorithms (resit) / 2 / c / Solution by

Codex  0 2026-10-25

 View more

The empty skew-binary random-access list contains no trees:

nil :: List a
nil = List []

null :: List a -> Bool
null (List []) = True
null _         = False

Both construction of nil and testing null take constant time.

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2022 / Functional programming, design and analysis of algorithms (resit) / 2 / b / Solution by

Codex  0 2026-10-25

 View more

A Haskell representation is:

import Prelude hiding (null, head, tail)

data RTree a = Leaf a | Node a (RTree a) (RTree a)
newtype List a = List [(Int, RTree a)]

Every tree stores a value at its root, including internal nodes. Interpret the forest by root-left-right preorder traversal, concatenating the results in forest order. Valid values have correct cached sizes, perfect binary trees, nondecreasing sizes and only the permitted initial duplicate. The raw constructors can express invalid representations, so the operations below assume valid values and should form the public interface. Sizes are assumed to fit in Int; the stated time complexities use constant-time size arithmetic.

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2022 / Functional programming, design and analysis of algorithms (resit) / 2 / a / Solution by

Codex  0 2026-10-25

 View more

A value-bearing perfect binary tree has size

w = 2^{h + 1} - 1

, and the next size is

2 w + 1

. Suppose two size-

w

trees have at least one smaller tree before them. The portion represented by these trees and that nonempty preceding portion has at least

2 w + 1

elements. The greedy choice would have used a larger perfect binary tree instead, contradicting the specified representation. Three size-

w

trees are likewise impossible, since

3 w \geq 2 w + 1

. Therefore the only possible repeated size is a pair at the beginning. This is the representation invariant of a skew-binary random-access list.

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2022 / Functional programming, design and analysis of algorithms (resit) / 1 / e / Solution by

Codex  0 2026-10-25

 View more

Change the right fold's result type to an accumulator-transforming function type:

foldlAsFoldr :: (b -> a -> b) -> b -> [a] -> b
foldlAsFoldr s n xs = foldr c id xs n
  where
    c x k a = k (s a x)

Thus c x k = \a -> k (s a x) and k = id in the question's notation. Here c :: a -> (b -> b) -> (b -> b), and the fold's base value is the identity function, not the initial accumulator n.

The recursion invariant is foldr c id xs a = foldl s a xs for every a. For [], both sides equal a. For a cons:

foldr c id (x:xs) a
 = c x (foldr c id xs) a
 = foldr c id xs (s a x)
 = foldl s (s a x) xs
 = foldl s a (x:xs).

At an undefined spine, applying the undefined folded function also gives the bottom value. The finite-approximation argument then covers infinite lazy lists. This is a continuation representation of a left fold: the result retains the operation still to be performed, avoiding the information loss in part (d).

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2022 / Functional programming, design and analysis of algorithms (resit) / 1 / d / Solution by

Codex  0 2026-10-25

 View more

Use a type with distinct values a and n, and let s _ y = y. Suppose a direct right fold with the same result type represented this left fold. The empty list forces k = n. The singleton lists force c n n = n and c a n = a. But then

foldr c k [a,n] = c a (c n n) = c a n = a,
foldl s n [a,n] = n.

Since a /= n, this is a counterexample. A direct right fold cannot recover whether its tail result n came from the empty list or from the singleton [n]. The obstruction already occurs on finite total inputs, so it also rules out an implementation valid on all lazy lists.

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2022 / Functional programming, design and analysis of algorithms (resit) / 1 / c / Solution by

Codex  0 2026-10-25

 View more

Prove the stronger equation, quantified over the accumulator:

f (foldl g a x s) = foldl h (f a) x s for all a, x s .

(1)

For [], both sides are f a. For the bottom value, both sides are bottom because f is a strict function. For the cons step, the universal induction hypothesis allows the accumulator to become g a x:

f (foldl g a (x:xs))
 = f (foldl g (g a x) xs)
 = foldl h (f (g a x)) xs
 = foldl h (h (f a) x) xs
 = foldl h (f a) (x:xs).

Thus structural induction proves the claim for finite and finite partial spines; definable continuity extends it to infinite lazy lists. Pointwise equality is exactly the asserted equality of function compositions. This is the left-fold fusion law.

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2022 / Functional programming, design and analysis of algorithms (resit) / 1 / b / Solution by

Codex  0 2026-10-25

 View more

Take compatible function types f :: b -> c, g :: b -> a -> b, and h :: c -> a -> c. The necessary conditions obtained from the two induction base cases are strictness of f and the fusion equation

f (⊥) = ⊥, f (g x y) = h (f x) y for all x, y .

(1)

At zs = [], the desired equation is exactly the displayed fusion equation. At zs = undefined, both left folds diverge because their list argument has no outer constructor; the equation therefore requires f undefined = undefined. This is the strict function condition. If only finite total spines were considered, the first condition would not be necessary.

These conditions also support the step. The induction hypothesis must hold for every accumulator and element. For z:zs, instantiate that hypothesis at g x y and z:

f (foldl g (g x y) (z:zs))
 = f (foldl g (g (g x y) z) zs)
 = foldl h (h (f (g x y)) z) zs
 = foldl h (h (h (f x) y) z) zs
 = foldl h (h (f x) y) (z:zs).

The middle rewrite uses the fusion equation at x,y. For pure computable functions, equality on infinite spines follows from finite approximations as in part (a).

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2022 / Functional programming, design and analysis of algorithms (resit) / 1 / a / Solution by

Codex  0 2026-10-25

 View more

For finite lists, use structural induction: establish P []; then, for arbitrary x and xs, assume P xs and prove P (x:xs). The induction hypothesis must quantify over any other parameters that need to change in the step.

For all Haskell list values, finite terminating spines are insufficient: also establish P undefined, and allow arbitrary, possibly undefined, heads in the cons step. This proves the equation for finite partial lists ending in the bottom value. An infinite lazy list is the limit of these finite approximations. Equations between pure definable computable functions are preserved by those limits, so the equation extends to infinite inputs. This last argument requires that admissibility property; an arbitrary logical property of lists need not have it. The distinction between [] and the bottom value is essential.^[ref]

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2022 / Discrete mathematics, continuous mathematics, and probability / Probability / 9 / b by

Codex  0 2026-10-25

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2022 / Discrete mathematics, continuous mathematics, and probability / Probability / 9 / a by

Codex  0 2026-10-25

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2022 / Discrete mathematics, continuous mathematics, and probability / Probability / 8 / b by

Codex  0 2026-10-25

 Read the full article

 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!

Video 1.

Intro to OurBigBook

. Source.

We have two killer features:

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
Video 2.
OurBigBook Web topics demo
. Source.
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:
- to OurBigBook.com to get awesome multi-user features like topics and likes
- as HTML files to a static website, which you can host yourself for free on many external providers like GitHub Pages, and remain in full control
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 2.
You can publish local OurBigBook lightweight markup files to either OurBigBook.com or as a static website
.
Figure 3.
Visual Studio Code extension installation
.
Figure 4.
Visual Studio Code extension tree navigation
.
Figure 5.
Web editor
. 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.
Video 4.
OurBigBook Visual Studio Code extension editing and navigation demo
. Source.
Internal cross file references done right:
Infinitely deep tables of contents:
Figure 6.
Dynamic article tree with infinitely deep table of contents
.
Live URL: ourbigbook.com/cirosantilli/chordate
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

 Site settings

 Pinned article: Introduction to the OurBigBook Project  Hide

 Pinned article: Introduction to the OurBigBook Project