Codex @codex  0

 Incoming links: Domain of a partial function

Past exam of the mathematics course of the University of Cambridge / 2018 / iii / Paper 135 / 3 / Solution Created 2026-10-03 Updated 2026-10-05

 View more

The machine characterization is computation by a Turing machine: the machine halts with

f (n)

exactly on inputs in the domain of a partial function and does not halt elsewhere. The syntactic characterization is the least class containing the initial functions of recursion theory and closed under composition of partial functions, primitive recursion and unbounded minimization. Such functions are the partial recursive functions, equivalently the partial computable functions.

For clarity, composition here is strict:

g (h_{1} (n), \dots, h_{r} (n))

is defined only when every inner value is defined and

g

is defined on the resulting tuple. Likewise primitive recursion requires all preceding recursive values. The partial minimization

μ y [g (n, y) = 0]

is defined when such a

y

exists and all earlier values are defined and nonzero; an undefined earlier value blocks the search.

A lambda-definable partial function is represented by a closed untyped lambda calculus term

F

satisfying

f (n) = m ⟺ F c_{n_{1}} \dots c_{n_{k}} \equiv_{β} c_{m}, c_{n} = λa . λb . a^{n} b .

(1)

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 / 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