ors.py
Checks: LATENCY: Trees of units property; rule; observation.
Cited on: LATENCY.
To run it: save ors.py, with chains.py, graphs.py, manystream.py, poles.py, redundant.py beside it; standard library only.
"""
ors.py -- can a unit's insets carry an OR of raises?
QUESTION. At (6, 2, 4) a VARIABLE is a head h = x y pinned at a delay s
in its window (floor 2, raised 3 to 5), read from outside the clause's
cone. A tree of product units over fresh streams and pinned heads,
each read once, every other unit free at 0 .. L* + 3: is the root's
aliveness at a latency T an OR of the settings? An OR at (tree, T):
settings a != b per variable, the root dead at a and alive at every
other corner of the box {a, b}^k (KILL 2 was frozen on the single
flips and the full flip only; a table closed under min and max has no
such OR either, two of three variables sharing a polarity). A
variable's polarity: + where b > a
(a raise helps), - where b < a.
BY HAND (the window). A root q at delay L is alive iff tau_V e_U +
tau_U e_V >= K(L) = Lam w - (w - 1) 6^L, each inset at most 1/5: at
L = 1 that wants Lam in (1, 6/5], at L = 0 Lam <= 1/5, beyond L = 1
Lam > 6. With tau = M^^n, n an input's fresh streams (a head's 2;
below, m counts a pinned head as one leaf), the pairs in (1, 6/5]
are (2, 3), (2, 4), (3, 3) and (1, 5..7): (2, 4) is always alive (a head hands at
least 11/75, 0.4096 * 11/75 > K = 0.0595); a 3-stream unit (z, head)
is dead at L = 1 and hands at least 0.152 above, past (3, 3)'s K =
0.0288; a fresh input carries nothing. So at the root only (A, (z, B))
at L = 1, K = 0.1824, the clause A or not-B (K2's numbers), and a
three-variable OR needs a deep input carrying three.
THE DESIGN (frozen before code). B tables by
graphs.step, a pinned head's B min(v_h(s), room) from t = s and None
before; memoized per (subtree, its marks' settings); T = 0 .. TMAX.
Trees of m leaves (T = 0 .. 34, frozen 0 .. 30; T = 34 asserted
alive at every setting) up to relabelling, marks A, B (C) each once, the
rest fresh, and up to a permutation of the marks.
CONTROLS. K1 every tree of the two-mark sweep, its marks freed
(alive at T for some setting) against graphs.build's B with each mark
a head; its plant, a pinned head arriving at s - 1 (scratch copy),
fails it. K2 the hand witness (A, (z, B)) at T = 6: alive except at
(2, 3); at L = 1 leftovers -37/30375, 391/151875, 403/151875,
979/151875 at (2, 3), (3, 3), (2, 2), (3, 2). K3 the detector on
synthetic tables: OR yes; AND, XOR, one variable no.
KILL 1 (frozen): two-mark ORs over m = 3..9, s in 2..5, = 0; predicted
not to fire, (+, -) only. KILL 2 (frozen): three-mark ORs over m =
4..8, s in 2..4, = 0; predicted to fire, weakly. Frozen after reading
both: KILL 3 tables not closed under componentwise min or max (a
sublattice of the settings' product order) > 0, predicted 0; its
control K4 on synthetic tables (a mixed OR and an AND closed, (+, +)
not min-closed, (-, -) not max-closed).
FINDINGS (copied from the run below). Literal tables: N = (z, h) at
arrival 5 hands 0.19254 at s 2, 0.15625 at s 3, dead at s 4; P =
(h, ((x y) z)) at arrival 5 is dead at s 2 and alive at s 3, 4
(0.00247, 0.00310): alive only raised. K1 1176 trees, 0 off (its plant,
a pinned head arriving at s - 1, run at m <= 5: 17 (tree, T) off over
23 trees); K2 to K4 green; the witness at T = 6 over s 2..5 is dead at
(2, 3), (2, 4), (2, 5) and wherever B >= 4.
X2, m = 3..9 (2, 6, 15, 41, 106, 280, 726 trees), T = 0..34: tables
constant 38316, one variable 1598, both 1246; ORs at 238 (tree, T),
every one (+, -), the least the hand witness (A, (z, B)) at T = 6.
KILL 1 does not fire; no (+, +) or (-, -) OR to 9 leaves. X3, m = 4..8
(4, 15, 49, 155, 469 trees): constant 22849, one 490, many 881; KILL 2
FIRES: no three-variable OR to 8 leaves. KILL 3 does not fire: every
table of X2 and X3 is closed under componentwise min and max, so a
cone's feasible head settings at a latency form a sublattice (verified
at (6, 2, 4), each head read once, m <= 9 with two heads at s 2..5,
m <= 8 with three at s 2..4). KILL 1's polarities and KILL 2 follow
from it: a same-polarity OR's two flips have the dead corner as their
min (+, +) or max (-, -), and of three variables two share a polarity.
The CSP of max-closed
relations is polynomial (Jeavons and Cooper 1995, known).
RUN RECORD. main: 4/4 checks, 46.5 s, peak commit 133.3 MB.
"""
import itertools
import sys
import time
from collections import Counter
from fractions import Fraction as Fr
import chains
import graphs
CELL = chains.ms.Cell(6, 2, 4)
TMAX = 34
MARKS = ("A", "B", "C")
CHECKS = []
LAG = 0 # the plant: a pinned head arriving at s - LAG
def check(name, ok, detail=""):
CHECKS.append(bool(ok))
tail = f" ({detail})" if detail else ""
print(f" {'PASS' if ok else 'FAIL'} {name}{tail}")
FRESH_RNG = (-CELL.Mm, CELL.Mp)
HEAD_RNG = graphs.iprod(FRESH_RNG, FRESH_RNG)
HEAD_ROOM = chains.room(CELL, HEAD_RNG)
def head_left(s):
r = graphs.v(CELL, 2 * CELL.Mh, s, CELL.Mh, CELL.Mh, 0, 0)
return min(r, HEAD_ROOM) if r >= 0 else None
def marks(node):
if node == "z":
return ()
if node in MARKS:
return (node,)
return tuple(sorted(set(marks(node[0]) + marks(node[1]))))
MEMO = {}
def build(node, st):
"""(tau, range, B, sat) of node under settings st (mark -> s); B
over t = 0..TMAX, constant from sat on."""
key = (node, tuple(st[m] for m in marks(node)))
if key in MEMO:
return MEMO[key]
if node == "z":
out = (CELL.Mh, FRESH_RNG, [Fr(0)] * (TMAX + 1), 0)
elif node in MARKS:
s = st[node]
e, t0 = head_left(s), s - LAG
out = (CELL.Mh ** 2, HEAD_RNG,
[e if t >= t0 else None for t in range(TMAX + 1)], t0)
else:
tu, ru, bu, su = build(node[0], st)
tv, rv, bv, sv = build(node[1], st)
rng = graphs.iprod(ru, rv)
room = chains.room(CELL, rng)
Ls = graphs.floor(CELL, tu, tv)
sat = max(su, sv) + Ls + 3
B = []
for t in range(TMAX + 1):
if t > sat:
B.append(B[-1])
continue
B.append(graphs.step(CELL, (tu, tv, bu, bv), t,
range(0, Ls + 4), room)[0])
out = (tu * tv, rng, B, sat)
MEMO[key] = out
return out
def key(node):
if node == "z" or node in MARKS:
return (0, node)
return (1, key(node[0]), key(node[1]))
def canon(node):
if node == "z" or node in MARKS:
return node
a, b = canon(node[0]), canon(node[1])
return (a, b) if key(a) <= key(b) else (b, a)
def relabel(node, f):
if node == "z":
return node
if node in MARKS:
return f[node]
return (relabel(node[0], f), relabel(node[1], f))
def shapes(m):
"""Unordered binary trees of m leaves, leaves 'z'."""
if m == 1:
return ["z"]
out = set()
for i in range(1, m // 2 + 1):
for a in shapes(i):
for b in shapes(m - i):
out.add(canon((a, b)))
return sorted(out, key=key)
def leaves_to(node, labels):
it = iter(labels)
def go(n):
if n == "z":
return next(it)
return (go(n[0]), go(n[1]))
return go(node)
def count_leaves(node):
return 1 if node == "z" or node in MARKS else (
count_leaves(node[0]) + count_leaves(node[1]))
def marked_trees(m, k):
"""Trees of m leaves, k of them the marks A.. each once, up to
relabelling and permutation of the marks."""
out = set()
ms = MARKS[:k]
for sh in shapes(m):
for pos in itertools.combinations(range(m), k):
lab = ["z"] * m
for p, mk in zip(pos, ms):
lab[p] = mk
t = leaves_to(sh, lab)
best = min((canon(relabel(t, dict(zip(ms, perm))))
for perm in itertools.permutations(ms)), key=key)
out.add(best)
return sorted(out, key=key)
def table(node, k, svals):
"""alive[T][settings] for the root."""
ms = MARKS[:k]
rows = {}
for st in itertools.product(svals, repeat=k):
B = build(node, dict(zip(ms, st)))[2]
rows[st] = B
return [{st: rows[st][T] is not None for st in rows}
for T in range(TMAX + 1)]
def ors(alive, k, svals):
"""Every OR (a, b) in one aliveness table: dead at a, alive at every
other corner of {a, b}^k; with its polarity."""
out = []
pairs = [(a, b) for a in svals for b in svals if a != b]
for ch in itertools.product(pairs, repeat=k):
a = tuple(c[0] for c in ch)
if alive[a]:
continue
ok = True
for pick in itertools.product((0, 1), repeat=k):
if not any(pick):
continue
st = tuple(c[p] for c, p in zip(ch, pick))
if not alive[st]:
ok = False
break
if ok:
pol = "".join(sorted("+" if b > a else "-" for a, b in ch))
out.append((ch, pol))
return out
def closed(alive):
"""(min-closed, max-closed): the alive settings under componentwise
min and max."""
on = [s for s, x in alive.items() if x]
lo = hi = True
for p in on:
for q in on:
lo = lo and alive[tuple(map(min, p, q))]
hi = hi and alive[tuple(map(max, p, q))]
return lo, hi
def kind(alive, k, svals):
"""constant, one (depends on one variable), or many."""
vals = set(alive.values())
if len(vals) == 1:
return "constant"
for i in range(k):
f = {}
good = True
for st, x in alive.items():
if f.setdefault(st[i], x) != x:
good = False
break
if good:
return "one"
return "many"
def free_shape(node):
if node in MARKS:
return ("z", "z")
if node == "z":
return node
return (free_shape(node[0]), free_shape(node[1]))
def literal_tables():
print("LT literal tables at (6, 2, 4): B(A | s), the best leftover at "
"arrival <= A, '-' dead")
d3 = (("z", "z"), "z")
d4 = (d3, "z")
for name, node in (("N = (z, h)", ("z", "A")),
("P = (h, D3), D3 = ((x y) z)", ("A", d3)),
("P = (h, D4), D4 = (((x y) z) z)", ("A", d4))):
print(f" {name}")
for s in (2, 3, 4, 5):
B = build(node, {"A": s})[2]
row = " ".join(" - " if x is None else f"{float(x):.5f}"
for x in B[:10])
print(f" s={s} A=0..9: {row}")
def controls():
print("K1..K3 the instrument")
ok = True
w = ("A", ("z", "B"))
alive = table(w, 2, (2, 3))[6]
st = {}
for sa, sb in ((2, 3), (3, 3), (2, 2), (3, 2)):
tu, ru, bu, _ = build("A", {"A": sa})
tv, rv, bv, _ = build(("z", "B"), {"B": sb})
room = chains.room(CELL, graphs.iprod(ru, rv))
r = graphs.v(CELL, tu + tv, 1, tu, tv, min(bu[5], CELL.w - 1),
min(bv[5], CELL.w - 1))
st[(sa, sb)] = r
want = {(2, 3): Fr(-37, 30375), (3, 3): Fr(391, 151875),
(2, 2): Fr(403, 151875), (3, 2): Fr(979, 151875)}
ok = st == want and alive == {(2, 3): False, (3, 3): True,
(2, 2): True, (3, 2): True}
check("K2 the hand witness (A, (z, B)) at T = 6", ok,
f"alive {alive}; L = 1 leftovers {[str(st[x]) for x in want]}")
full = table(w, 2, (2, 3, 4, 5))[6]
print(f" the witness at T = 6 over s 2..5, dead at "
f"{sorted(k for k, x in full.items() if not x)}")
sv = (2, 3, 4, 5)
grid = list(itertools.product(sv, repeat=2))
syn = {"OR": {s: s[0] > 2 or s[1] > 2 for s in grid},
"AND": {s: s[0] > 2 and s[1] > 2 for s in grid},
"XOR": {s: (s[0] > 2) != (s[1] > 2) for s in grid},
"one": {s: s[0] > 2 for s in grid}}
got = {k: bool(ors(t, 2, sv)) for k, t in syn.items()}
check("K3 the detector: OR yes; AND, XOR, one variable no",
got == {"OR": True, "AND": False, "XOR": False, "one": False},
f"{got}")
syn = {"mixed": {s: s[0] > 2 or s[1] < 4 for s in grid},
"AND": syn["AND"], "++": syn["OR"],
"--": {s: s[0] < 4 or s[1] < 4 for s in grid}}
got = {k: closed(t) for k, t in syn.items()}
check("K4 closure: mixed OR and AND closed; (+, +) not min-closed, "
"(-, -) not max-closed",
got == {"mixed": (True, True), "AND": (True, True),
"++": (False, True), "--": (True, False)}, f"{got}")
def k1(trees):
off = 0
for node in trees:
free = graphs.build(CELL, free_shape(node), None, TMAX)[2]
tab = table(node, 2, (2, 3, 4, 5))
for T in range(TMAX + 1):
off += (free[T] is not None) != any(tab[T].values())
return off
def sweep(tag, k, mrange, svals):
t0 = time.time()
n = Counter()
first = {}
ex = []
trees_all = []
for m in mrange:
trees = marked_trees(m, k)
trees_all += trees
n[f"trees m={m}"] = len(trees)
for node in trees:
tab = table(node, k, svals)
assert all(tab[TMAX].values()), "TMAX too small"
for T in range(TMAX + 1):
kd = kind(tab[T], k, svals)
n[kd] += 1
lo, hi = closed(tab[T])
n["not min-closed"] += not lo
n["not max-closed"] += not hi
if not (lo and hi) and "unclosed" not in first:
first["unclosed"] = (m, node, T, (lo, hi))
found = ors(tab[T], k, svals)
if found:
n["OR (tree, T)"] += 1
pols = sorted({p for _, p in found})
for p in pols:
n[f"OR {p}"] += 1
if p not in first:
first[p] = (m, node, T, [c for c, q in found
if q == p][:3])
if len(ex) < 4:
ex.append((m, node, T, found[:2]))
print(f"\n{tag} trees with {k} marks, m = {mrange[0]}..{mrange[-1]}, "
f"s in {svals}, T = 0..{TMAX}, {time.time() - t0:.1f} s, "
f"memo {len(MEMO)}")
for kk in sorted(n):
print(f" {kk:20s} {n[kk]}")
for p, e in sorted(first.items()):
print(f" least {p}: m {e[0]}, {e[1]}, T {e[2]}, {e[3]}")
return n, trees_all
def main(m2=9, m3=8):
t0 = time.time()
literal_tables()
controls()
n2, trees = sweep("X2", 2, list(range(3, m2 + 1)), (2, 3, 4, 5))
off = k1(trees)
check("K1 marks freed = graphs.build with heads, every tree, every T",
off == 0, f"{len(trees)} trees, {off} off")
if not all(CHECKS):
print("\nCONTROL FAILED: nothing below is read.")
return 1
print(f"\nKILL 1 two-mark ORs: {n2['OR (tree, T)']} (tree, T) pairs; "
f"population 'many' {n2['many']}")
n3, _ = sweep("X3", 3, list(range(4, m3 + 1)), (2, 3, 4))
print(f"\nKILL 2 three-mark ORs: {n3['OR (tree, T)']} (tree, T) pairs; "
f"population 'many' {n3['many']}")
bad = sum(n[k] for n in (n2, n3)
for k in ("not min-closed", "not max-closed"))
print(f"\nKILL 3 tables not min- or max-closed: X2 "
f"{n2['not min-closed']} / {n2['not max-closed']}, X3 "
f"{n3['not min-closed']} / {n3['not max-closed']} ({bad})")
print(f"\n{sum(CHECKS)}/{len(CHECKS)} checks, {time.time() - t0:.1f} s")
return 0
if __name__ == "__main__":
sys.exit(main(*(int(x) for x in sys.argv[1:])))