verify_stack_wqo_obstruction.py

#!/usr/bin/env python3
"""Finite calibration for the exact-stack WQO obstruction."""

import itertools
import json
from pathlib import Path


EMPTY = "empty"


def words(alphabet, depth):
    result = [()]
    for length in range(1, depth + 1):
        result.extend(itertools.product(alphabet, repeat=length))
    return tuple(result)


def observation(stack):
    return EMPTY if not stack else stack[0]


def pop(stack):
    return stack[1:] if stack else stack


def distinguishing_depth(left, right):
    for depth in range(max(len(left), len(right)) + 1):
        if observation(left) != observation(right):
            return depth
        left, right = pop(left), pop(right)
    raise AssertionError("distinct stacks had identical complete pop traces")


def main():
    stacks_checked = ordered_pairs = off_diagonal_pairs = trace_checks = 0
    maximum_witness_depth = 0

    for alphabet_size in range(1, 4):
        alphabet = tuple(range(alphabet_size))
        stack_set = words(alphabet, 6)
        stacks_checked += len(stack_set)
        for left in stack_set:
            for right in stack_set:
                ordered_pairs += 1
                if left == right:
                    continue
                off_diagonal_pairs += 1
                depth = distinguishing_depth(left, right)
                maximum_witness_depth = max(maximum_witness_depth, depth)
                trace_checks += depth + 1

    # If observation preservation is dropped, the unary length order is
    # monotone under pop, but it compares empty with nonempty stacks.
    unary = words((0,), 6)
    for left in unary:
        for right in unary:
            if len(left) <= len(right):
                assert len(pop(left)) <= len(pop(right))
    assert len(()) <= len((0,))
    assert observation(()) != observation((0,))

    # If pop monotonicity is dropped, equality of the current observation is
    # a finite-class WQO. It relates stacks of heights one and two, but their
    # popped observations differ.
    short = (0,)
    tall = (0, 0)
    assert observation(short) == observation(tall)
    assert observation(pop(short)) != observation(pop(tall))

    result = {
        "status": "pass",
        "scope": "stack alphabets through size three and heights through six",
        "stacks_checked": stacks_checked,
        "ordered_stack_pairs": ordered_pairs,
        "off_diagonal_pairs": off_diagonal_pairs,
        "pop_trace_observation_checks": trace_checks,
        "maximum_distinguishing_depth": maximum_witness_depth,
        "sharpness": {
            "without_observation_preservation": "unary length order is pop-monotone",
            "without_pop_monotonicity": "current-top equivalence is a finite-class WQO",
        },
        "does_not_verify": [
            "that every infinite-state scaffold presentation lacks a useful WQO",
            "orders that deliberately abstract empty or top-of-stack observations",
            "the infinite proof beyond its finite pop-trace instances",
        ],
    }
    output = json.dumps(result, indent=2) + "\n"
    Path(__file__).with_name("stack-wqo-obstruction-checker-output.json").write_text(output)
    print(output, end="")


if __name__ == "__main__":
    main()