verify_reversible_summary_congruence.py

#!/usr/bin/env python3
"""Finite certificates for the reversible-summary residual theorem.

The script minimizes supplied deterministic Moore machines, checks whether
every generator acts as a permutation on the reachable minimal quotient, and
exhaustively corroborates the common-pop collapse for state sets of size at
most four. It does not prove the general theorem or analyze pushdown systems.
"""

from collections import deque
from dataclasses import dataclass
from itertools import permutations, product
import json
from pathlib import Path


@dataclass(frozen=True)
class Moore:
    states: tuple
    alphabet: tuple
    start: object
    output: dict
    delta: dict


def reachable(machine):
    seen = {machine.start}
    queue = deque([machine.start])
    while queue:
        state = queue.popleft()
        for letter in machine.alphabet:
            target = machine.delta[state, letter]
            if target not in seen:
                seen.add(target)
                queue.append(target)
    return seen


def minimize(machine):
    states = reachable(machine)
    blocks = {}
    for state in states:
        blocks.setdefault(machine.output[state], set()).add(state)
    partition = list(blocks.values())

    while True:
        owner = {state: index for index, block in enumerate(partition) for state in block}
        refined = {}
        for state in states:
            signature = (
                machine.output[state],
                tuple(owner[machine.delta[state, letter]] for letter in machine.alphabet),
            )
            refined.setdefault(signature, set()).add(state)
        next_partition = list(refined.values())
        if {frozenset(block) for block in next_partition} == {
            frozenset(block) for block in partition
        }:
            partition = next_partition
            break
        partition = next_partition

    owner = {state: index for index, block in enumerate(partition) for state in block}
    quotient_delta = {
        (index, letter): owner[machine.delta[next(iter(block)), letter]]
        for index, block in enumerate(partition)
        for letter in machine.alphabet
    }
    quotient_output = {
        index: machine.output[next(iter(block))]
        for index, block in enumerate(partition)
    }
    return Moore(
        tuple(range(len(partition))),
        machine.alphabet,
        owner[machine.start],
        quotient_output,
        quotient_delta,
    )


def analyze(name, machine):
    minimal = minimize(machine)
    transitions = {}
    failures = []
    for letter in minimal.alphabet:
        image = tuple(minimal.delta[state, letter] for state in minimal.states)
        injective = len(set(image)) == len(minimal.states)
        transitions[letter] = {"image": image, "injective": injective}
        if not injective:
            witness = None
            for left in minimal.states:
                for right in minimal.states:
                    if left < right and minimal.delta[left, letter] == minimal.delta[right, letter]:
                        witness = [left, right, minimal.delta[left, letter]]
                        break
                if witness:
                    break
            failures.append({"letter": letter, "merge": witness})
    return {
        "name": name,
        "minimal_states": len(minimal.states),
        "permutation_summary": not failures,
        "transitions": transitions,
        "failures": failures,
    }


def parity_machine():
    return Moore(
        (0, 1), ("X",), 0,
        {0: 0, 1: 1},
        {(0, "X"): 1, (1, "X"): 0},
    )


def mod_three_machine():
    return Moore(
        (0, 1, 2), ("A",), 0,
        {0: 0, 1: 1, 2: 2},
        {(0, "A"): 1, (1, "A"): 2, (2, "A"): 0},
    )


def presence_machine():
    return Moore(
        (0, 1), ("X", "A"), 0,
        {0: False, 1: True},
        {
            (0, "X"): 1, (1, "X"): 1,
            (0, "A"): 0, (1, "A"): 1,
        },
    )


def emptiness_machine():
    return Moore(
        (0, 1), ("X",), 0,
        {0: True, 1: False},
        {(0, "X"): 1, (1, "X"): 1},
    )


def rightmost_tag_machine():
    states = ("e", "0", "1")
    alphabet = ("B0", "B1", "A")
    delta = {}
    for state in states:
        delta[state, "A"] = state
        delta[state, "B0"] = "0" if state == "e" else state
        delta[state, "B1"] = "1" if state == "e" else state
    return Moore(states, alphabet, "e", {state: state for state in states}, delta)


def common_pop_exhaustive(max_size=4):
    records = []
    for size in range(1, max_size + 1):
        states = tuple(range(size))
        perms = tuple(permutations(states))
        functions = product(states, repeat=size)
        solutions = 0
        unequal_push_solutions = 0
        checked = 0
        for down in functions:
            left_inverses = []
            for up in perms:
                checked += 1
                if all(down[up[state]] == state for state in states):
                    left_inverses.append(up)
            solutions += len(left_inverses) ** 2
            unequal_push_solutions += sum(
                1 for first in left_inverses for second in left_inverses if first != second
            )
        assert unequal_push_solutions == 0
        records.append({
            "states": size,
            "down_tables_times_permutations_checked": checked,
            "ordered_two_push_solutions": solutions,
            "unequal_push_solutions": unequal_push_solutions,
        })
    return records


def main():
    cases = [
        analyze("parity of hidden height", parity_machine()),
        analyze("hidden height modulo three", mod_three_machine()),
        analyze("presence of X", presence_machine()),
        analyze("exact emptiness", emptiness_machine()),
        analyze("rightmost B0/B1 tag", rightmost_tag_machine()),
    ]
    assert cases[0]["permutation_summary"]
    assert cases[1]["permutation_summary"]
    assert not cases[2]["permutation_summary"]
    assert not cases[3]["permutation_summary"]
    assert not cases[4]["permutation_summary"]

    result = {
        "status": "passed",
        "residual_examples": cases,
        "common_untyped_pop": common_pop_exhaustive(),
        "assurance": (
            "Exact minimization and injectivity checks for the finite examples; "
            "bounded exhaustive corroboration of common-pop collapse through four states."
        ),
        "not_verified": [
            "the general residual theorem",
            "unrestricted pushdown reachability",
            "automatic synthesis from source programs",
            "scaffold generation",
            "proof assistant formalization",
        ],
    }
    output = Path(__file__).with_name("reversible-summary-congruence-output.json")
    output.write_text(json.dumps(result, indent=2, sort_keys=True) + "\n")
    print(json.dumps(result, indent=2, sort_keys=True))


if __name__ == "__main__":
    main()