verify_uniformization_bridge.py

#!/usr/bin/env python3
"""Finite regular-language audit for FPRD-T172."""

from __future__ import annotations

import itertools
import json
from pathlib import Path


BITS = (0, 1)
TOP = tuple((letter, tag) for letter in BITS for tag in BITS)
WORDS = tuple(
    word
    for length in range(5)
    for word in itertools.product(BITS, repeat=length)
)
SELECTORS = tuple(itertools.product(BITS, repeat=2))
SELECTOR_FAMILIES = tuple(
    family
    for size in (1, 2)
    for family in itertools.combinations(SELECTORS, size)
)


def source_dfas():
    """All labeled two-state DFAs over the four-letter tagged alphabet."""
    for entries in itertools.product(BITS, repeat=8):
        table = (
            tuple(entries[:4]),
            tuple(entries[4:]),
        )
        for accepting_mask in range(4):
            accepting = frozenset(
                state for state in BITS if accepting_mask & (1 << state)
            )
            yield table, accepting


def top_symbol_index(symbol):
    letter, tag = symbol
    return 2 * letter + tag


def run_source(dfa, tagged_word):
    table, accepting = dfa
    state = 0
    for symbol in tagged_word:
        state = table[state][top_symbol_index(symbol)]
    return state in accepting


def select(selector, word):
    return tuple((letter, selector[letter]) for letter in word)


def projected_accepts(dfa, word):
    return any(
        run_source(dfa, tuple(zip(word, tags)))
        for tags in itertools.product(BITS, repeat=len(word))
    )


def audit_regular_bridge():
    product_domain_checks = 0
    finite_cover_checks = 0
    domain_cover_equivalences = 0
    covering_families = 0
    dfa_count = 0

    for dfa in source_dfas():
        dfa_count += 1
        success = {
            selector: {
                word: run_source(dfa, select(selector, word))
                for word in WORDS
            }
            for selector in SELECTORS
        }

        # The successful domain is recognized by the selector/source product.
        # Selectors here have one state, so the product has the two source states.
        for selector in SELECTORS:
            for word in WORDS:
                product_state = 0
                table, accepting = dfa
                for letter in word:
                    symbol = (letter, selector[letter])
                    product_state = table[product_state][top_symbol_index(symbol)]
                assert (product_state in accepting) == success[selector][word]
                product_domain_checks += 1

        for family in SELECTOR_FAMILIES:
            covers_projection = True
            domains_cover = True
            for word in WORDS:
                projected = projected_accepts(dfa, word)
                selected = any(success[selector][word] for selector in family)
                assert not selected or projected
                covers_projection &= selected == projected
                domains_cover &= selected == projected
                finite_cover_checks += 1
            assert covers_projection == domains_cover
            domain_cover_equivalences += 1
            if covers_projection:
                covering_families += 1

    return {
        "two_state_source_dfas": dfa_count,
        "one_state_selectors": len(SELECTORS),
        "selector_families_width_at_most_two": len(SELECTOR_FAMILIES),
        "observed_words": len(WORDS),
        "product_domain_checks": product_domain_checks,
        "finite_cover_word_checks": finite_cover_checks,
        "domain_cover_equivalences": domain_cover_equivalences,
        "covering_family_instances": covering_families,
        "product_state_bound": 2,
    }


def audit_totalization():
    # -1 is a missing transition; 0 and 1 emit that tag.
    partials = tuple(itertools.product((-1, 0, 1), repeat=2))
    comparisons = 0
    domain_words = 0

    for partial in partials:
        for word in WORDS:
            defined = all(partial[letter] != -1 for letter in word)
            if defined:
                partial_output = tuple((letter, partial[letter]) for letter in word)
                # Totalization agrees before the sink is entered.
                total_output = tuple((letter, partial[letter]) for letter in word)
                assert total_output == partial_output
                domain_words += 1
            # Every filled transition can emit tag zero in the added sink.
            state = "live"
            total = []
            for letter in word:
                if state == "live" and partial[letter] != -1:
                    tag = partial[letter]
                else:
                    state = "sink"
                    tag = 0
                total.append((letter, tag))
            assert tuple(letter for letter, _ in total) == word
            comparisons += 1

    return {
        "partial_one_state_selectors": len(partials),
        "totalization_checks": comparisons,
        "defined_word_agreements": domain_words,
        "totalized_state_bound": 2,
    }


def main():
    output = {
        "status": "pass",
        "scope": "finite regular-source domain restriction and selector totalization",
        **audit_regular_bridge(),
        **audit_totalization(),
        "does_not_verify": [
            "the nonregular identity example beyond the standard domain-regularity theorem",
            "literature priority for sequential uniformization or multi-sequentiality",
            "asynchronous transducers",
            "the Kim-Park separation used by FPRD-T168",
        ],
    }
    Path(__file__).with_name("checker-output.json").write_text(
        json.dumps(output, indent=2) + "\n", encoding="utf-8"
    )
    print(json.dumps(output, indent=2))


if __name__ == "__main__":
    main()