Primitive recursive syntax and arity checking
= 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>.