plan(roadmap): leaf-language classes — bounded milestones #449

Summary

This issue proposes a bounded roadmap entry for leaf languages: classes defined by the ordered word of accept/reject leaves of a polynomial-time computation tree. It is a planning issue only and is not ready to implement. Humans should review the scope and the milestone order first.

#399 tried to formalize Vollmer's whole generalized-quantifier survey and was closed as too ambitious, with a note that "a concrete bounded milestone can be proposed later". This issue is that proposal, limited to leaf languages. It does not attempt the full survey.

What the library already has

No leaf-language framework yet. A grep for leaf language, LeafLanguage and leaf word over Complexity/ turns up only unrelated tree code.

Classes already defined by a count over a fixed-length set of witnesses. Each one decides membership from the multiset of verifier answers V (a, w) over w : List Bool of length p (enc a).length. That is the unordered leaf word of a balanced tree:

• NP
• SharpP and GapP
• ParityP (⊕P)
• ModP k and coModP
• PP
• CeqP and coCeqP
• US
• the operators ParityOp and BPOp

Classes that are semantic, not syntactic. UP, FewP, SPP, WPP, AWPP and BPP carry promise or gap conditions, so they are not leaf classes in the plain sense.

Machine models with explicit branches.

• Turing.MultiTapeCTM (Machines/Turing/MultiTape/Counting.lean) has labelled, ordered branches: occurrence indices and branches. That is the raw material for unbalanced leaf words of nondeterministic machines.
• Turing.MultiTapeATM (Classes/Alternation.lean) is an alternating machine.

Results that are prerequisites for the main theorems.

• Barrington's theorem: Circuit/Boolean/Barrington.lean, BranchingProgram/MonoidProgram.lean, Foundations/GroupTheory/Perm/FiveCycle.lean.
• PSPACE and TQBF: Classes/Space.lean, IP/TQBF.
• SigmaP k and PH: Classes/PH.lean.
• ACC0.

Bibliography. references.bib already has Barrington1989, BarringtonTherien1988, BarringtonImmermanStraubing1990, Vollmer1999 and Wagner1986.

Proposed milestones

Each milestone should become its own ready to implement issue only after review.

M1. Balanced polynomial-time leaf classes.

• Define leafWord V p a : List Bool: the answers V (a, w) for w ranging over {0,1}^{p (enc a).length} in lexicographic order.
• Define BLeafP (B : Set (List Bool)) enc: A is in the class when there are a polynomial p and a polynomial-time V with a ∈ A ↔ leafWord V p a ∈ B.
• Use the same encPair enc encBits verifier conventions as NP, SharpP and PP, so the existing classes can be compared directly.

M2. Existing classes as leaf classes. Prove equalities with the library's definitions, not new definitions:

• NP = BLeafP {w | true ∈ w} and the dual for coNP;
• ParityP (odd number of trues);
• ModP k (count of trues is nonzero mod k);
• PP (strict majority);
• CeqP (exactly half, after the usual GapP shift);
• US (exactly one);
• P, using a leaf language that looks only at the first letter.

The docstring should explain why UP, SPP and BPP are not of this form.

M3. Elementary structure.

• Monotonicity in B, and complement: BLeafP Bᶜ gives the complements.
• Robustness under padding the witness length.
• The easy direction of the Bovet–Crescenzi–Silvestri / Vereshchagin criterion: if B reduces to B' by polylog-time bit-reductions (≤_plt), then BLeafP B ⊆ BLeafP B'. This needs a definition of ≤_plt with explicit random-access input, as feat(complexity): formalize Vollmer's generalized quantifier framework #399 noted.

M4. Upper bound. BLeafP B ⊆ PSPACE for every regular B, more generally for B decidable in polylogarithmic space. Evaluate the exponentially long leaf word bit by bit in lexicographic order without storing it.

M5. PSPACE as a regular leaf class (Hertrampf, Lautemann, Schwentick, Vollmer, Wagner 1993). PSPACE = BLeafP (word problem of A₅).

• The lower bound lifts the existing Barrington commutator construction from formulas to the quantifier tree of TQBF.
• This milestone reuses the most existing infrastructure, so it is the natural headline result.

M6. The polynomial hierarchy. SigmaP k = BLeafP B_k for suitable languages B_k with k quantifier blocks, compared with Classes/PH.lean.

M7. Long-term entries for ROADMAP only; no implementation proposed now.

• Unbalanced leaf languages of MultiTapeCTM (Leaf^P) and their relation to BLeafP.
• The full oracle criterion: for all oracles, Leaf(A) ⊆ Leaf(B) iff A ≤_plt B (Bovet–Crescenzi–Silvestri 1992; Vereshchagin 1993).
• Monoid classification of regular leaf classes: aperiodic gives levels of PH, solvable gives the modular counting hierarchy, non-solvable gives PSPACE.
• Logspace and logtime leaf languages (Jenner–McKenzie–Thérien 1996), connecting to the existing ACC0 and Barrington work.
• Generalized Lindström quantifiers (Burtschick–Vollmer 1998).

Fidelity notes (from #399)

• Leaf words are ordered. Results such as M5 depend on the order, so unordered counts do not suffice.
• State uniformity, the input-access model and the treatment of exponentially long leaf words with binary-output indexing explicitly.
• Balanced and unbalanced models differ in general. Do not identify them without a proof.
• Check each cited statement against its source before stating it. In particular, the exact form of the M6 languages and the class bounds in M7 need source confirmation.

References

• D. P. Bovet, P. Crescenzi, R. Silvestri, A uniform approach to define complexity classes, TCS 104 (1992).
• N. K. Vereshchagin, Relativizable and nonrelativizable theorems in the polynomial theory of algorithms, Izv. Ross. Akad. Nauk 57 (1993).
• U. Hertrampf, C. Lautemann, T. Schwentick, H. Vollmer, K. W. Wagner, On the power of polynomial time bit-reductions, Structure in Complexity Theory 1993.
• B. Jenner, P. McKenzie, D. Thérien, Logspace and logtime leaf languages, Inf. Comput. 129 (1996).
• H.-J. Burtschick, H. Vollmer, Lindström quantifiers and leaf language definability, IJFCS 9 (1998).
• H. Vollmer, A generalized quantifier concept in computational complexity theory (1998), https://arxiv.org/abs/cs/9809115 (see feat(complexity): formalize Vollmer's generalized quantifier framework #399).

Requested action

• Review the scope and milestone order.
• If accepted, add a "Leaf languages" row to ROADMAP and open M1 as the first ready to implement issue.

Opened by worker-crei-dc679113 (AI assistance: Claude Code, Claude Opus 5.5).