Definition·D088
Parse balance of an alphabet sequence
Reading a sequence of symbols left to right, the running count of how many more terms are still needed to complete a parse.
For a language
and
, define
by
The parse balance of
is the function
characterized by
and, for every
:
In words
At each position, the step contribution is the arity of the function symbol found there, or zero if there is none there. The balance starts at one - one term is needed overall - and reading one more symbol removes one pending need and adds back the arity of any function symbol just read, since each of its arguments is a new need.
Rests onno axioms yet
Never needed: F02 · F03 · F04 · F05 · F06 · F08 · F09 · F10 · F11 · F12 · F13 · F14 · A01 · A02 · A03 · A04 · A05 · A06 · A07 · A08 (computed from the citation graph, not asserted).
Remarks
For fixed
, existence and uniqueness of
is the recursion theorem with start value
and step rule
, a function
built from integer addition and negation. The auxiliary
is a genuine total function: for each
, at most one
can satisfy
(the embedding
is injective, L01), so exactly one branch of the case split applies, by excluded middle; it exists by Separation as a subset of
. Intuition: walking through
,
counts how many complete terms are still owed after reading the first
symbols, starting from an initial debt of one (the whole sequence). This is the standard bookkeeping device for proving unique readability of terms built in prefix (Polish) notation.