Natural Numbers Object

definition example program

A natural numbers object $N$ in a cartesian category is an object with two arrows — the introduction rules —

$$Z:1\to NS:N\to N$$

(“zero” and “successor”; $S$ is recursive: its source is $N$ itself) such that for every object $a$ and pair $init:1\to a$, $step:a\to a$ there is a unique $h:N\to a$ with

$$h\circ Z=init,h\circ S=step\circ h.$$

This elimination rule is primitive recursion: $h$ is the sequence $a_0=init$, $a_{n+1}=step(a_n)$. Uniqueness says $N$ contains nothing but $Z,SZ,SSZ,\dots$ — no numbers “before, after, or in between” (adding a $-1$ would allow two $h$‘s generated by the same $(init,step)$).

Sources: DaoFP Chapter 7 (“Recursion”, §7.1 “Natural Numbers”: introduction rules, elimination rules, “In Programming”), §12 (as the Initial Algebra of $1+(-)$), §11 (the induction principle as dependent elimination); 7 Sketches Example 3.13 ($\mathbb{N}$ as the free category on one loop), Exercise 6.7 ($\mathbb{N}$ as initial rig); Kittenlab Lecture 5.

• Not every arrow $N\to a$ is recursive — an arbitrary such arrow contains infinite information; the recursive ones are enough to define $N$. This is the Peano encoding; in Haskell data Nat = Z | S Nat, used mostly for type-level naturals.
• $N$ is the Initial Algebra of the Endofunctor $F(x)=1+x$; $h$ is the catamorphism $\mathrm{fold}[init,step]$ (Lambek: $[Z,S]:1+N\cong N$).
• The recursor rec init step implements all primitive recursive functions, e.g. plus n = rec n S; curried addition $N\to N^N$ uses init = id, step = (S .) (DaoFP Exercise 7.1.2). Iteration in imperative languages is the same thing; compilers turn one into the other (tail-recursion optimization).
• Lists $L_a$ generalize $N$: $N\cong L_1$ (base-one numerals, DaoFP Exercise 7.2.1). A stronger elimination rule — the induction principle — needs dependent types.

JuliaLeanHaskell

Docs: ThCategory (GATlab) · Theories & presentations — Kittenlab Lecture 5

# the recursor: a mapping out of ℕ from init and step
rec(init, step) = n -> n == 0 ? init : step(rec(init, step)(n - 1))
plus(n) = rec(n, x -> x + 1)
plus(3)(4)                                   # 7
double = rec(0, x -> x + 2); double(5)       # 10

Catlab version (run in a fresh Julia session — Catlab exports its own compose, id, FinFunction, …):

# Catlab: ℕ as the free category on one object and one generating loop
using Catlab
@present NatCat(FreeCategory) begin N::Ob; S::Hom(N, N) end

import Mathlib
#check @Nat.rec                 -- the eliminator (dependent: induction principle)
#check @Nat.zero
#check @Nat.succ
#check @Nat.iterate             -- f^[n] : primitive recursion with init = x, step = f
example : (fun n => Nat.rec (motive := fun _ => ℕ) 3 (fun _ acc => acc + 1) n) 4 = 7 := by decide

data Nat where
  Z :: Nat
  S :: Nat -> Nat
 
rec :: a -> (a -> a) -> (Nat -> a)          -- the recursor / elimination rule
rec init step = \n -> case n of
  Z     -> init
  (S m) -> step (rec init step m)
 
plus :: Nat -> Nat -> Nat
plus n = rec n S                            -- init = n, step = S
 
plus' :: Nat -> Nat -> Nat                  -- inlined recursor
plus' n m = case m of
  Z     -> n
  (S k) -> S (plus' k n)