Context-free languages as visible projections

Exact statement

For every finite alphabet $\Sigma$ , a language $L\subseteq\Sigma^*$ is context-free exactly when $L=\pi(A)$ for a visibly pushdown language $A\subseteq(\Sigma\times\{\mathsf c,\mathsf r,\mathsf l\})^*$ , where $\pi$ forgets the action tag. The projection is letter-to-letter and length preserving, and (A) may be recognized by a deterministic visibly pushdown automaton.

StatusSource-verified and reconstructed; not mechanically checked

External reviewThe forward construction and determinization are published results of Alur and Madhusudan; the FPRD application has no documented specialist review.

Context

The theorem isolates one fixed hidden coordinate per input position: whether the tagged machine performs a call, return, or local action.

Hypotheses and scope

The alphabet is finite.
The projection erases only the action tag and never erases an input position.

Proof or evidence

A normalized pushdown transition on a letter is tagged by its stack action, producing a visibly pushdown language whose projection is the original language. Determinization is applied before projection. Conversely, visibly pushdown languages are context-free and context-free languages are closed under homomorphism.

Visible-projection theorem →

Verification notes

The construction, the separate determinization step, the converse closure argument, and the empty-word case were rechecked. Determinism of the tagged automaton is not transferred to the projected language.

Limitations

The theorem does not show that every context-free language is a parsing-expression language.
It does not supply a bounded representation of the existential frontier created by projection.

Open work

Add a direct theorem-level primary-source locator to the public bibliography and seek a specialist check of the normalization conventions.

Notes

Alur--Madhusudan Proposition 1 supplies the forward action-tag embedding, their Theorem 2 separately supplies determinization, and the converse uses VPL subset CFL plus homomorphic closure. The empty word has its unique empty lift. This source theorem locates the forgotten-action seam; it does not prove CFL subset PEL.