Fixed coding primitive recursive arithmetic and sequences

The recursions $a+0=a$, $a+(b+1)=S(a+b)$, $a\cdot 0=0$, $a\cdot (b+1)=a\cdot b+a$, $a^0=1$, $a^{b+1}=a^{b}a$ give addition, multiplication and powers. Predecessor is $P(0)=0$, $P(b+1)=b$, so truncated subtraction is , . The zero test $Z(0)=1$, $Z(b+1)=0$ yields and . All are applications of the schemes, with total values even at zero.

For PR $u(\mathbf{a},j)$, accumulate sums from initial value zero and products from one for $j=0,\dots ,B-1$ by primitive recursion on $B$. Products of Boolean values give bounded universal quantification and $1$ minus a product of complements gives bounded existential quantification. For a PR predicate $R$, its least witness at most $B$ with failure value $B+1$ is ${\sum }_{j=0}^B{\prod }_{i=0}^j(1-[R(\mathbf{a},i)])\mathrm{.}$ If the least witness is $r$, precisely the terms $j<r$ equal one; if none exists, all $B+1$ terms equal one. Bounded maximum can be obtained by searching in reverse or accumulating the latest successful index, initially zero. Conditional branches are arithmetic combinations with a Boolean selector.

For $d>0$, divisibility $d\mid z$ is $\mathrm{\exists }q\le z(dq=z)$. A quotient, if present, is found by bounded least search. On $z>0$, let $a$ be the largest $a\le z$ such that $2^a\mid z$. Such an $a$ exists since $2^0=1$. A maximal one has odd quotient: an even quotient would make $2^{a+1}$ divide $z$. Repeated division by two strictly decreases a positive even number, so this process terminates at an odd positive integer. It also proves uniqueness: if $2^{a}u=2^{b}v$ with odd positive $u,v$ and $a<b$, cancellation would make $u$ even. Thus the bounded definition is exactly the two-adic valuation. The odd quotient has the unique form $2b+1$; find $b\le z$ by bounded search. These are the claimed head and tail functions with explicit zero branches.

For $z>0$, $\mathrm{tail}(z)=(z\mathrm{/}{2}^a-1)\mathrm{/}2<z$. Let $t(z,0)=z$ and $t(z,j+1)=\mathrm{tail}(t(z,j))$. Primitive recursion makes $t$ PR. A strictly decreasing sequence of positive naturals starting at $z$ has at most $z$ terms: after $j$ decreases its value is at most $z-j$. Therefore $\mathrm{\ell }(z)={\sum }_{j<z}(1-Z(t(z,j)))$ is precisely the list length. The list represented by any natural is well-founded; conversely successive cons operations encode each finite list, and the unique head/tail decomposition makes the encoding injective. Its coordinate function is $\mathrm{head}(t(z,i))$, zero when $i\ge \mathrm{\ell }(z)$.

Define $r(z,0)=0$ and $r(z,j+1)=\mathrm{cons}(\mathrm{head}(t(z,j)),r(z,j))$. Then $\mathrm{rev}(z)=r(z,\mathrm{\ell }(z))$ reverses the list: after $j$ steps it contains the first $j$ entries in reverse order, by checking the initial value and the cons step. Appending $a$ is $\mathrm{rev}(\mathrm{cons}(a,\mathrm{rev}(z)))$. To concatenate $z$ with $w$, start the accumulator at $w$ and cons the entries of $\mathrm{rev}(z)$ in order, stopping after $\mathrm{\ell }(z)$ steps. Its result is the entries of $z$ followed by those of $w$. These bounded folds are PR even though their accumulator values need not be bounded by the input code.

Bounded list predicates are sums/products of tests on these coordinates. In particular a word parser can maintain a cursor and finite coded state for at most the word's length plus one iterations. Each iteration reads a coordinate, compares bounded lengths, updates arithmetic counters and appends decoded letters; on failure it records a fixed failure state and remains there. Every such update is one of the PR operations already proved, so primitive recursion implements the entire bounded scan. Binary numeral conversion uses the fold $v\mapsto 2v+\text{bit}$; the reverse conversion finds the largest $j\le v+1$ with $2^j\le v$ when $v>0$, then uses bounded division to obtain its bits, with the separate one-bit representation of zero. Empty lists have length zero and reverse zero; a singleton $\mathrm{cons}(a,0)$ has length one and coordinate zero equal to $a$. Empty sums/products are zero/one. No unbounded minimization or inference from computability to PR has been used.