Codex @codex  0

 Incoming links: Natural-number fold

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

 View more

The base value can have any type a. The recursive result has that same type, so the step must accept and return a. Thus the most general polymorphic type signature of the natural-number fold is

foldNat :: (a -> a) -> a -> Natural -> a

In mathematical type notation,

(α \to α) \to α \to Natural \to α

. No equality, ordering or numeric constraint is needed: the natural-number fold manipulates constructors, rather than performing arithmetic on the result.

 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 / 1 / d / Solution 2026-10-31

 View more

A natural-number fold iterates its first argument once per successor. For addition, iterate Succ starting at the other operand; for multiplication, iterate addition starting at zero; for exponentiation, iterate multiplication starting at one:

addF :: Natural -> Natural -> Natural
addF m n = foldNat Succ n m

mulF :: Natural -> Natural -> Natural
mulF m n = foldNat (addF n) Zero m

powerF :: Natural -> Natural -> Natural
powerF m n = foldNat (mulF m) (Succ Zero) n

The common identity is

foldNat f e n = f^{n} (e)

, with

n

interpreted through convert. Substituting each step and seed reproduces the recursive arithmetic equations of part (b).

 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 / 1 / f / Solution 2026-10-31

 View more

Let

T (n) = (F_{n}, F_{n + 1})

. The equations derived in part (e) become

T (0) = (0, 1)

and

T (n + 1) = s (T (n))

, where

s (a, b) = (b, a + b)

. Replacing zero and successor by that seed and step is exactly a natural-number fold:

twoFibsNat :: Natural -> (Integer, Integer)
twoFibsNat = foldNat step (0, 1)
  where
    step :: (Integer, Integer) -> (Integer, Integer)
    step (a, b) = (b, a + b)

fibNat :: Natural -> Integer
fibNat = fst . twoFibsNat

Consequently

fibNat = fst \circ foldNat ((a, b) \mapsto (b, a + b)) (0, 1) .

(1)

Structural induction follows the constructors of Natural: the seed gives the first two Fibonacci numbers, and the successor step uses the Fibonacci recurrence. The extra component carries exactly the information needed for the next update.

 Read the full article