verify_wqo_pumping.py

#!/usr/bin/env python3
"""Finite calibration for the abstract WQO one-sided pumping theorem."""

import itertools
import json
from pathlib import Path


def monotone_maps(size):
    return tuple(itertools.combinations_with_replacement(range(size), size))


def run(initial, word, actions):
    states = [initial]
    state = initial
    for letter in word:
        state = actions[letter][state]
        states.append(state)
    return states


def first_increasing_pair(states):
    return next(
        (i, j)
        for j in range(1, len(states))
        for i in range(j)
        if states[i] <= states[j]
    )


def main():
    map_count = machine_pairs = accepted_words = pump_checks = 0
    for size in range(1, 5):
        maps = monotone_maps(size)
        map_count += len(maps)
        for action_a in maps:
            for action_b in maps:
                machine_pairs += 1
                actions = {"a": action_a, "b": action_b}
                for initial in range(size):
                    for threshold in range(size + 1):
                        for letters in itertools.product("ab", repeat=size):
                            word = "".join(letters)
                            states = run(initial, word, actions)
                            if states[-1] < threshold:
                                continue
                            accepted_words += 1
                            i, j = first_increasing_pair(states)
                            x, y, z = word[:i], word[i:j], word[j:]
                            assert y
                            for repeats in range(1, 6):
                                pumped = run(initial, x + y * repeats + z, actions)[-1]
                                assert pumped >= threshold
                                pump_checks += 1

    # Deletion is not supplied by a one-way comparison: 0 <= 1, y is
    # accepted by the upward set {1,2,...}, but the zero-copy word is not.
    deletion_actions = {"y": (1, 1)}
    assert run(0, "y", deletion_actions)[-1] == 1
    assert run(0, "", deletion_actions)[-1] == 0

    # Monotonicity is essential: swapping 0 and 1 turns the accepted first
    # copy into a rejected second copy despite 0 <= 1 at the first cut.
    swap = {"y": (1, 0)}
    assert run(0, "y", swap)[-1] == 1
    assert run(0, "yy", swap)[-1] == 0

    # Upward closure is essential: increment is monotone, but accepting only
    # state 1 accepts one copy and rejects two.
    increment = {"y": (1, 2, 2)}
    assert run(0, "y", increment)[-1] == 1
    assert run(0, "yy", increment)[-1] == 2

    result = {
        "status": "pass",
        "scope": "all pairs of monotone actions on finite chains through size four",
        "monotone_maps": map_count,
        "two_letter_action_pairs": machine_pairs,
        "accepted_length_bound_words": accepted_words,
        "one_sided_pump_checks": pump_checks,
        "deletion_counterexample": {"states": [0, 1], "zero_copy_rejected": True},
        "nonmonotone_counterexample": {"states": [0, 1, 0], "second_copy_rejected": True},
        "non_upward_acceptance_counterexample": {"states": [0, 1, 2], "second_copy_rejected": True},
        "does_not_verify": [
            "the infinite WQO recurrence argument",
            "a compatible WQO for unrestricted scaffolding automata",
            "an effective or elementary pumping-length bound",
            "zero-copy pumping from a strict comparison",
        ],
    }
    output = json.dumps(result, indent=2) + "\n"
    Path(__file__).with_name("wqo-pumping-checker-output.json").write_text(output)
    print(output, end="")


if __name__ == "__main__":
    main()