verify_typed_context_pumping.py

#!/usr/bin/env python3
"""Finite audit for the typed-context and visible-stack pumping note.

The unrestricted statements are proved in the accompanying note.  This
program exhausts small typed paths and Dyck derivation trees, then checks that
every extracted one-hole context remains valid when iterated.
"""

from __future__ import annotations

from dataclasses import dataclass
from functools import lru_cache
import json


@dataclass(frozen=True)
class Tree:
    bracket: int | None = None
    inside: "Tree | None" = None
    suffix: "Tree | None" = None

    @property
    def empty(self) -> bool:
        return self.bracket is None


EPSILON = Tree()
OPEN = "(["
CLOSE = ")]"


@lru_cache(maxsize=None)
def trees(pairs: int) -> tuple[Tree, ...]:
    if pairs == 0:
        return (EPSILON,)
    result: list[Tree] = []
    for inside_pairs in range(pairs):
        suffix_pairs = pairs - 1 - inside_pairs
        for bracket in range(2):
            for inside in trees(inside_pairs):
                for suffix in trees(suffix_pairs):
                    result.append(Tree(bracket, inside, suffix))
    return tuple(result)


def word(tree: Tree) -> str:
    if tree.empty:
        return ""
    assert tree.inside is not None and tree.suffix is not None
    return OPEN[tree.bracket] + word(tree.inside) + CLOSE[tree.bracket] + word(tree.suffix)


def balanced(value: str) -> bool:
    stack: list[str] = []
    matching = {")": "(", "]": "["}
    for symbol in value:
        if symbol in OPEN:
            stack.append(symbol)
        elif not stack or stack.pop() != matching[symbol]:
            return False
    return not stack


def contexts(tree: Tree) -> list[tuple[str, str, str]]:
    """Return (left, hole, right) for every proper descendant S-node."""
    if tree.empty:
        return []
    assert tree.inside is not None and tree.suffix is not None
    opening = OPEN[tree.bracket]
    closing = CLOSE[tree.bracket]
    inside_word = word(tree.inside)
    suffix_word = word(tree.suffix)
    result = [
        (opening, inside_word, closing + suffix_word),
        (opening + inside_word + closing, suffix_word, ""),
    ]
    for left, hole, right in contexts(tree.inside):
        result.append((opening + left, hole, right + closing + suffix_word))
    for left, hole, right in contexts(tree.suffix):
        result.append((opening + inside_word + closing + left, hole, right))
    return result


def run_stack(value: str) -> tuple[str, ...] | None:
    stack: list[str] = []
    matching = {")": "(", "]": "["}
    for symbol in value:
        if symbol in OPEN:
            stack.append(symbol)
        elif not stack or stack.pop() != matching[symbol]:
            return None
    return tuple(stack)


def audit() -> dict[str, object]:
    typed_path_cases = 0
    for type_count in range(1, 6):
        # Base-type expansion avoids materializing all paths at once.
        total = type_count ** (type_count + 1)
        for encoded in range(total):
            path = []
            value = encoded
            for _ in range(type_count + 1):
                path.append(value % type_count)
                value //= type_count
            assert len(set(path)) <= type_count
            typed_path_cases += 1

    derivation_trees = 0
    extracted_contexts = 0
    pumped_words = 0
    stack_runs = 0
    two_sided_contexts = 0
    one_sided_contexts = 0
    for pair_count in range(6):
        for tree in trees(pair_count):
            derivation_trees += 1
            original = word(tree)
            assert balanced(original)
            assert run_stack(original) == ()
            for left, hole, right in contexts(tree):
                extracted_contexts += 1
                assert left or right
                if left and right:
                    two_sided_contexts += 1
                else:
                    one_sided_contexts += 1
                for copies in range(5):
                    pumped = left * copies + hole + right * copies
                    assert balanced(pumped)
                    assert run_stack(pumped) == ()
                    pumped_words += 1
                    stack_runs += 1

    # The one-bracket family c^n r^n forces the paired, two-wing case.
    nested_family_checks = 0
    for depth in range(1, 17):
        for outer in range(depth):
            for inner in range(outer + 1, depth + 1):
                left = "(" * (inner - outer)
                hole = "(" * (depth - inner) + ")" * (depth - inner)
                right = ")" * (inner - outer)
                for copies in range(5):
                    assert balanced(left * copies + hole + right * copies)
                    nested_family_checks += 1

    return {
        "status": "pass",
        "scope": "typed paths through five types and all two-bracket Dyck derivation trees through five pairs",
        "typed_path_cases": typed_path_cases,
        "derivation_trees": derivation_trees,
        "extracted_contexts": extracted_contexts,
        "two_sided_contexts": two_sided_contexts,
        "one_sided_contexts": one_sided_contexts,
        "pumped_words": pumped_words,
        "persistent_stack_runs": stack_runs,
        "nested_family_checks": nested_family_checks,
        "does_not_verify": [
            "the unrestricted finite-interface pumping schema",
            "the visibly pushdown grammar characterization",
            "a pumping lemma for all scaffolding automata or PEGs",
            "novelty beyond classical tree and context-free pumping",
        ],
    }


if __name__ == "__main__":
    print(json.dumps(audit(), indent=2))