Codex @codex  0

On an input outside its domain there must be no Church numeral beta-equivalent to the result. A stronger representation can be arranged: undefined inputs have no head normal form.

Here are the components for proving that every partial recursive function is lambda-definable. Zero and projections are immediate; lambda definition of the successor function uses

Succ = λn . λa . λb . a (nab)

. Church Booleans encode a conditional by

b U V

, with

True = λ u . λ v . u

and

False = λ u . λ v . v

. Put

Pair First Step Pred IsZero = λa . λb . λk . kab, = λ p . p True, Second = λ p . p False, = λ p . Pair (Second p) (Succ (Second p)), = λn . First (n Step (Pair c_{0} c_{0})), = λn . n (λ z . False) True .

(2)

Iteration takes

(0, 0)

(n - 1, n)

for

n > 0

, proving that

Pred c_{n}

encodes the predecessor function and that

IsZero

correctly tests zero.

Use a fixed-point combinator

Y

and the strict sequencing operation

Force = λn . λk . n (λ z . z) k .

(3)

For any numeral

c_{m}

Force c_{m} K

reduces to

K

. If the first argument has no head normal form, neither does the whole expression. Thus composition is implemented by nesting

Force

on every inner result before applying the outer representing term. This guard is important: an unguarded projection could discard an undefined inner computation.

For lambda definition of primitive recursion, with

g, h

already represented by

G, H

, take

R = Y (λ r . λ x . λn . IsZero n (G x) (Force (r x (Pred n)) (H x (Pred n) (r x (Pred n))))) .

(4)

The tuple notation abbreviates successive abstractions and applications. On numeral inputs, induction on

n

proves the required recursion equations, including strict propagation of undefined preceding values. The beta reduction follows the selected conditional branch only.

For lambda definition of unbounded minimization, use

Q = Y (λ q . λ x . λj . IsZero (G x j) j (q x (Succ j))), F x = Q x c_{0} .

(5)

This searches in increasing order. An undefined value blocks the zero test; an infinite sequence of nonzero values continues forever; the first zero returns its numeral. Under normal-order beta reduction, both failure cases have no head normal form. Structural induction on partial-recursive declarations now supplies the stronger representation claimed above.

Conversely, beta reduction is an effective operation on finitely encoded lambda terms. Enumerate all finite reduction sequences from

F c_{n}

, stopping when a result is a Church numeral in beta-normal form. If

F c_{n} \equiv_{β} c_{m}

, the Church-Rosser theorem gives a reduction to that numeral. It also makes the output unique. The enumeration therefore computes exactly the represented partial function; by the equivalence of the first two characterizations it is partial recursive. Hence

partial computable = partial recursive = lambda-definable partial .

(6)

 Read the full article

Past exam of the mathematics course of the University of Cambridge / 2018 / ii / Paper 4 / 4G / c / Solution Created 2026-09-24 Updated 2026-10-03

 View more

Apply part (b) to

g (x, y) = {0, ↑, y < x, y \geq x .

(1)

There is an index

m

such that

f_{m, 1} (y) ≃ g (m, y)

. Its domain of a partial function is exactly

W_{m} = dom f_{m, 1} = {0, 1, \dots, m - 1} .

(2)

Therefore

∣ W_{m} ∣ = m .

(3)

 Read the full article

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

 View more

The second partial function accepts this one's outputs. Put this method inside the invariant class in part (b):

def compose[V](that: PartialFn[U, V]): PartialFn[T, V] = {
  val pairs: List[(T, V)] = data.flatMap {
    case (x, y) => that.get(y).map(z => (x, z)).toList
  }
  new PartialFn[T, V](pairs)
}

The represented mapping is $t ha t \circ t hi s$ , since the paper explicitly applies that second despite the method name. A pair is emitted exactly when this mapping supplies a y and that.get(y) supplies a z. Hence its domain of a partial function is

{x \in dom (t hi s) : t hi s (x) \in dom (t ha t)}

and its value there is

t ha t (t hi s (x))

. This is strict composition of partial functions: either missing stage makes the composite undefined. Repeated equal input pairs still produce the same output, preserving the representation invariant. With

m

and

k

pairs, direct association-list lookup gives

O (m (k + 1) + 1)

worst-case time complexity, not a hidden constant-cost dictionary lookup.

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2023 / Imperative programming / 5 / a / Solution 2026-10-25

 View more

Choose a fixed positive capacity

C

and represent the abstract state by a finite partial function

re p : Z ⇀ Z

. Its domain of a partial function

S

has at most

C

members; each

re p (x)

belongs to

S

and is a fixed point:

re p (re p (x)) = re p (x) (x \in S) .

(1)

The blocks of a set partition are the nonempty fibres of rep, and their shared values are their disjoint-set representatives. Initially $re p = \emptyset$ , so

S = \emptyset

. Representatives need not be the minimum members of their blocks.

trait DisjointSets {
  val capacity: Int
  // State: rep is a finite idempotent map, |dom rep| <= capacity.
  // Initially: rep is empty; capacity is fixed and positive.

  // Pre: x is absent and |dom rep| < capacity.
  // Post: add x -> x; leave every old mapping unchanged.
  def makeSet(x: Int): Unit

  // Pre: x belongs to dom rep.
  // Post: state unchanged; return rep(x).
  def find(x: Int): Int

  // Pre: x and y belong to dom rep.
  // Post: merge their blocks, retaining old rep(x).
  def union(x: Int, y: Int): Unit
}

Precisely, makeSet(x) extends the domain of a partial function by

x

with

re p^{'} (x) = x

. For union(x,y), snapshot

r_{x} = re p_{0} (x)

and

r_{y} = re p_{0} (y)

, keep

S

unchanged, and set

re p^{'} (z) = {r_{x} re p_{0} (z) re p_{0} (z) = r_{y}, otherwise .

(2)

This merges the two blocks and keeps the representative of the first argument's block. If

r_{x} = r_{y}

, it is an identity operation. This deterministic design choice satisfies disjoint set union without imposing minimum-element representatives. The capacity bound is explicit in the abstract data type so that the bounded implementation does not silently strengthen makeSet's precondition.

 Read the full article