verify_order_frontier.py

#!/usr/bin/env python3
"""Finite regression checks, not an unrestricted proof. Python 3.10+, stdlib only."""
import itertools as it
import json
import random


def frontier(order, processed):
    return tuple(j for j in range(1, len(order))
                 if (order[j-1] in processed) != (order[j] in processed))


def solve(order_a, maps_a, accept_a, order_b, maps_b, accept_b, width_b):
    """Complete leveled diagrams, start state 0; exact existential frontier DP."""
    b = len(order_a)
    assert set(order_a) == set(order_b) and len(set(order_a)) == b
    if not b:
        return 0 in accept_a and 0 in accept_b, 0
    processed, old, table, h = set(), (), {(0, ())}, 0
    for i, var in enumerate(order_a):
        j = order_b.index(var)
        processed.add(var)
        new = frontier(order_b, processed)
        h = max(h, len(new))
        following = set()
        for a, values in table:
            stored = dict(zip(old, values))
            incoming = [0] if j == 0 else ([stored[j]] if j in stored else range(width_b))
            for q in incoming:
                for bit in (0, 1):
                    r = maps_b[j][q][bit]
                    if j == b-1 and r not in accept_b:
                        continue
                    if j+1 in stored and stored[j+1] != r:
                        continue
                    extension = dict(stored)
                    extension[j], extension[j+1] = q, r
                    following.add((maps_a[i][a][bit], tuple(extension[e] for e in new)))
        table, old = following, new
        assert len(table) <= len(maps_a[i]) * width_b ** len(new)
    return any(a in accept_a for a, _ in table), h


def evaluate(order, maps, accepted, values):
    state = 0
    for var, transition in zip(order, maps):
        state = transition[state][values[var]]
    return state in accepted


def brute(oa, ma, aa, ob, mb, ab):
    return any(evaluate(oa, ma, aa, v) and evaluate(ob, mb, ab, v)
               for v in it.product((0, 1), repeat=len(oa)))


def compile_formula(clauses):
    occurrences = [(variable, positive) for clause in clauses for variable, positive in clause]
    b = len(occurrences)
    equal_order = sorted(range(b), key=lambda i: occurrences[i][0])
    equal_maps = []
    for p, var in enumerate(equal_order):
        first = p == 0 or occurrences[equal_order[p-1]][0] != occurrences[var][0]
        last = p == b-1 or occurrences[equal_order[p+1]][0] != occurrences[var][0]
        equal_maps.append([[2 if q == 2 or (not first and q != t)
                            else (0 if last else t) for t in (0, 1)] for q in range(3)])
    clause_maps = []
    for clause in clauses:
        assert clause
        for j, (_, positive) in enumerate(clause):
            last = j == len(clause)-1
            clause_maps.append([[2 if q == 2 else
                                 ((0 if q == 1 or t == positive else 2) if last
                                  else int(q == 1 or t == positive))
                                 for t in (0, 1)] for q in range(3)])
    return equal_order, equal_maps, {0}, list(range(b)), clause_maps, {0}


def main():
    rng = random.Random(9104)
    diagrams = reductions = 0
    max_h = 0
    for b in range(7):
        for ob in it.permutations(range(b)):
            oa = list(range(b))
            wa, wb = rng.randrange(1, 4), rng.randrange(1, 4)
            ma = [[[rng.randrange(wa) for _ in (0, 1)] for _ in range(wa)] for _ in oa]
            mb = [[[rng.randrange(wb) for _ in (0, 1)] for _ in range(wb)] for _ in ob]
            aa = {s for s in range(wa) if rng.randrange(2)}
            ab = {s for s in range(wb) if rng.randrange(2)}
            answer, h = solve(oa, ma, aa, ob, mb, ab, wb)
            assert answer == brute(oa, ma, aa, ob, mb, ab)
            if list(ob) == oa or list(ob) == oa[::-1]:
                assert h <= 1
            max_h = max(max_h, h)
            diagrams += 1
    formulas = [[], [[(0, True)]], [[(0, True)], [(0, False)]],
                [[(0, True)]*3, [(0, False)]*3]]
    for _ in range(150):
        formulas.append([[(rng.randrange(3), bool(rng.randrange(2))) for _ in range(3)]
                         for _ in range(rng.randrange(1, 4))])
    for clauses in formulas:
        oa, ma, aa, ob, mb, ab = compile_formula(clauses)
        expected = any(all(any(values[x] == pos for x, pos in clause) for clause in clauses)
                       for values in it.product((0, 1), repeat=3))
        answer, _ = solve(oa, ma, aa, ob, mb, ab, 3)
        assert answer == expected == brute(oa, ma, aa, ob, mb, ab)
        reductions += 1
    print(json.dumps({'seed': 9104, 'diagram_pairs': diagrams,
                      'all_second_orders_through_b': 6, 'max_frontier_tested': max_h,
                      'occurrence_reduction_cases': reductions, 'passed': True,
                      'status': 'finite regression checks; not formal verification'}, indent=2))


if __name__ == '__main__':
    main()