Primitive-recursive sentinel coding for certified syntax

From the initial functions and parameter recursion in F1 define $a+0=a$, $a+Sn=S(a+n)$, $a\cdot 0=0$, $a\cdot Sn=a\cdot n+a$, $\mathrm{pred}(0)=0$, $\mathrm{pred}(Sn)=n$, and , . Set $z(0)=1,z(Sn)=0$. Then equality is and $a\le b$ has characteristic function . Products, complements and $rg+(1-r)h$ implement Boolean tests and case splits for a 0–1 test $r$. Bounded sums/products have initial values 0/1 and append one term, so are primitive recursive.

For a 0–1 predicate $r$, ${\sum }_{j<N}{\prod }_{i\le j}(1-r(i))$ counts the unsuccessful initial positions: it equals the least successful index, or $N$ if none succeeds. This explicitly proves bounded search, consistent with bounded closure F2. Powers satisfy $b^0=1,b^{n+1}=b\cdot b^n$. For $d>0$ put $q(a,d)={\sum }_{j=1}^a[dj\le a]$ and , and set both to 0 for $d=0$. The successful indices are exactly $1,\dots ,q$; thus $dq\le a<d(q+1)$, giving quotient and remainder. Every operation just defined is primitive recursive.

Put $P(u,v)=(u+v{)}^2+u$. For a fixed sum $t$, its values occupy $[t^2,t^2+t]$ with distinct offsets $u$; the next interval starts at $(t+1{)}^2>t^2+t$. Hence $P$ is injective. Both coordinates are at most $P(u,v)$, including $(0,0)$. Bounded search therefore gives its range test and inverses, with zero off-range. Nesting a fixed number of these pairs stores a fixed register tuple. Decode, apply the finitely many update functions, and encode again: ordinary primitive recursion on the one state code implements the simultaneous register recursion, regardless of how large the registers grow.

For $s>0$, its binary width is $\mathrm{\ell }(s)=1+{\sum }_{j=1}^s[2^j\le s]$, and $\mathrm{\ell }(0)=1$. Indeed the powers of two are strictly increasing and $2^s>s$ for $s\ge 1$ including s=1; induction proves this bound. Thus the counted indices give the largest exponent below $s$. The left-to-right bit at $j<\mathrm{\ell }(s)$ is the remainder modulo 2 of the quotient of $s$ by $2^{\mathrm{\ell }(s)-1-j}$; elsewhere return zero. Horner updating $v\mapsto 2v+b$ evaluates any specified payload. These are primitive-recursive register computations by steps 2.1–3.1.

Parse the canonical binary word of $s>0$. After the initial 1, count the consecutive 1s to the first 0; failure to find that delimiter is invalid. Their number is $k$. At each of $k$ block starts $p$, find the next zero below $\mathrm{\ell }(s)$ and let $m$ be its distance. Require $m\ge 1$, require $m$ payload bits after the delimiter to fit, and require their first bit to be 1 unless $m=1$. Evaluate those bits by Horner and advance by $2m+1$. Finally require the position to equal $\mathrm{\ell }(s)$. Each scan and block loop has at most $\mathrm{\ell }(s)+1$ iterations. A persistent error flag freezes invalid states. The counters, current position, flag and requested entry are finitely many registers, so step 3.1 proves primitive recursiveness. At the end reset length and coordinates to zero on failure, and coordinates to zero outside $0\le j<k$.

The header and every block delimiter determine their lengths uniquely. Each canonical payload therefore recovers its unique original natural number. Induction over the blocks proves that parsing an encoded list returns that list; conversely, a successful parse consumes the whole word and reconstruction reproduces it. Thus two lists with the same code have equal length and equal entries. The word 10 has k=0 and no payload, so parses successfully as the empty list.

For construction represent a word by value and width $(v,L)$; concatenating $(w,M)$ gives $(v{2}^M+w,L+M)$. The length-k header is $(2^{k+2}-2,k+2)$. For $m=\mathrm{\ell }(a)$ the entry block has width $2m+1$ and value $(2^m-1)2^{m+1}+a$. Fixed-arity encoders concatenate finitely many such blocks. Append and concatenation build the enlarged header and copy coordinates from the validated inputs, followed by the new entry or second list, using their lengths as bounds. Induction on the number copied gives exactly the required output list. Invalid inputs return 2. Finally a history recursion stores its current list code, computes the primitive-recursive next value from it and appends. This is one ordinary parameter recursion; retrieving a coordinate supplies the result.