Unique parsing of finite syntax

Induct on construction stages to verify that every expression starts with an opening parenthesis, ends with its matching closing parenthesis, and has positive parenthesis balance at every nonempty proper prefix. A parent contributes one to the balance while its child words each have nonnegative balance and total balance zero; leaf interiors have no parentheses. Thus these assertions hold for leaves and are preserved by all constructors.

For a word known to be an expression, the second token is its unique constructor tag. Scan from its opening parenthesis: commas at balance one separate exactly its outer fields, because child interiors have balance at least two. The first return to balance zero is the end of the expression. These boundaries depend only on the word, not on a proposed construction.

The tag prescribes the sorts of the fields, and any function or relation symbol prescribes their number through its arity. The scan therefore recovers every child word uniquely. Existence follows from membership in the constructor closure. Every child omits at least the outer opening, tag and closing tokens, so is shorter; strong induction on length also recovers all descendant parses.