check_name_weighted_classes.py

#!/usr/bin/env python3
"""Finite semantic checks for assessment 177; not a native implementation."""
from collections import deque
from fractions import Fraction
from itertools import product
import json


def words(n):
    return [''.join(bits) for bits in product('01', repeat=n)]


def weight(v):
    return Fraction(1, 2 ** (2 * len(v) + 1))


def code(v):
    return ''.join('00' if b == '0' else '01' for b in v) + '11'


def clause(v, w):
    return f'(-01{v},+1{w});'


def gaps(rows):
    occupied = sorted({len(ws) for ws in rows.values()})
    nxt = dict(zip(occupied, occupied[1:]))
    return {v: nxt.get(len(ws)) == len(ws) + 1 for v, ws in rows.items()}


def prefix_masks(n):
    names = words(n)
    return sorted({sum(1 << i for i, v in enumerate(names) if v.startswith(p))
                   for length in range(n + 1) for p in words(length)})


def shortest_costs(n):
    """Independent BFS over all answer vectors and one-prefix XOR edges."""
    masks = prefix_masks(n)
    dist = {0: 0}
    todo = deque([0])
    while todo:
        x = todo.popleft()
        for p in masks:
            y = x ^ p
            if y not in dist:
                dist[y] = dist[x] + 1
                todo.append(y)
    return dist


def tree_cost(bits, inherited=0):
    """Optimize the root tag, then independently optimize its children."""
    if len(bits) == 1:
        return bits[0] ^ inherited
    middle = len(bits) // 2
    return min(t + tree_cost(bits[:middle], inherited ^ t)
               + tree_cost(bits[middle:], inherited ^ t) for t in (0, 1))


def main():
    report = dict(relation_states=0, gap_queries=0, prefix_vectors=0,
                  monotone_histories=0, partitions=0, static_codes=0,
                  abandoned_classes=0)
    targets = words(2)
    for k in range(9):
        h = 2 ** k
        rows = {'0': set(targets[:2])}
        stream = [clause('0', w) for w in targets[:2]]
        for u in words(k):
            rows['1' + u + '0'] = set(targets)
            rows['1' + u + '1'] = {targets[0]}
            stream += [clause('1' + u + '0', w) for w in targets]
            stream.append(clause('1' + u + '1', targets[0]))
        assert sum(map(len, stream)) == 5 * h * (k + 13) + 24
        trigger = clause('0', '10')
        assert len(trigger) == 12
        before = {v: set(ws) for v, ws in rows.items()}
        for z in (0, 1):
            if z:
                rows['0'].add('10')
            answers = gaps(rows)
            for v, ans in answers.items():
                expected = bool(z) if v == '0' else v[-1] == '1' and not z
                assert ans == expected
                report['gap_queries'] += 1
            completed = {v: ws | set(targets) for v, ws in rows.items()}
            assert len({frozenset(ws) for ws in completed.values()}) == 1
            report['relation_states'] += 1
        old = gaps(before)
        new = gaps(rows)
        long_delta = [int(old['1' + u + b] != new['1' + u + b])
                      for u in words(k) for b in '01']
        assert long_delta == [0, 1] * h
        assert sum(long_delta[2 * i] ^ long_delta[2 * i + 1]
                   for i in range(h)) == h
        if k <= 5:
            assert tree_cost(long_delta) == h
        rows['0'].add('10')
        assert gaps(rows) == new  # duplicate identity
        assert gaps(before) == old  # retained semantic version
    for depth in range(4):
        dist = shortest_costs(depth)
        for mask, cost in dist.items():
            bits = [(mask >> i) & 1 for i in range(2 ** depth)]
            assert tree_cost(bits) == cost
            report['prefix_vectors'] += 1
    names = ['0', '10', '111']
    for moves in product(range(3), repeat=6):
        counts = [0] * 3
        visits = {0: set(names)}
        visited = {v: {0} for v in names}
        for i in moves:
            counts[i] += 1
            c = counts[i]
            assert c not in visited[names[i]]
            visited[names[i]].add(c)
            visits.setdefault(c, set()).add(names[i])
            assert all(sum((weight(v) for v in vs), Fraction()) <= Fraction(1, 2)
                       for vs in visits.values())
        report['monotone_histories'] += 1
    names = ['0', '1', '00', '01', '10', '11']
    for labels in product(range(3), repeat=len(names)):
        blocks = {}
        for v, label in zip(names, labels):
            blocks.setdefault(label, []).append(v)
        reps = [min(vs, key=lambda v: (len(v), v)) for vs in blocks.values()]
        codes = list(map(code, reps))
        assert all(not a.startswith(b) for a in codes for b in codes if a != b)
        assert len(set(codes)) == len(codes)
        total = Fraction()
        for vs in blocks.values():
            rep = min(vs, key=lambda v: (len(v), v))
            mass = sum((weight(v) for v in vs), Fraction())
            total += mass
            for v in vs:
                assert len(code(rep)) <= 2 * len(v) + 2
                assert mass >= weight(v)
                report['static_codes'] += 1
        assert total <= Fraction(1, 2)
        report['partitions'] += 1
    for h in range(1, 33):
        counts = {f'1{i:06b}': i for i in range(1, h + 1)}
        counts['0'] = 0
        abandoned = set()
        for c in range(1, h + 2):
            previous = counts['0']
            counts['0'] = c
            if previous:
                assert previous in counts.values()
                abandoned.add(previous)
        assert len(abandoned) == h
        assert sum((weight('0') for _ in abandoned), Fraction()) == Fraction(h, 8)
        report['abandoned_classes'] += h
    print(json.dumps(report, sort_keys=True))


if __name__ == '__main__':
    main()