Primitive recursive syntax and arity checking

For a decidable coding of finite construction trees, the codes of arity-$i$ primitive recursive functions in intension are decidable. Check initial-function tags, then verify the child arities at each composition and recursion node. This is a terminating finite syntax check, distinct from asking whether an arbitrary program's extension happens to be primitive recursive.

Enumerate all valid unary primitive recursive functions in intension by their decidable codes $p_n$, and interpret each extension $F_{p_n}$. The function $d(n)=F_{p_n}(n)+1$ is a total computable function, since each finite construction terminates. If it were primitive recursive, some $F_{p_j}$ would equal $d$, giving $d(j)=d(j)+1$. Repeated extensions in the syntax enumeration do not affect this argument.

A valid finite construction expression from the initial functions of recursion theory by function composition in recursion theory and primitive recursion. Its extension is a primitive recursive function. The construction grammar supplies both a decidable syntax and a total computable interpreter, but no uniformly primitive recursive interpreter for all valid codes.