borrow.py
Checks: MACHINE: Clearing a place decides and dividing once does not theorem; MACHINE: A blind read decides and a sighted read is universal theorem.
Cited on: MACHINE.
To run it: save borrow.py; standard library only.
"""borrow.py -- which moves that lower a depth keep a program's halting
decidable: a move that clears a place whole, or one that divides once.
QUESTION. machine.py decides every program over pushes and presence
reads: the depths v_p(M) only rise, and (instruction, zero-pattern) is
a finite quotient. Give the program a move that LOWERS a depth. Two
come to hand at a place p: CLEAR p, M -> M / p^(v_p(M)), which drops
the place whole, and DIVIDE p, M -> M / p when p | M, which drops one, M left
alone otherwise.
Both lower a depth, and both make a tested depth fall back to zero, so
"a down-move" does not separate them. What does?
THE OBJECT. States M = 2^a 3^b, so the counters are the depths a and b.
A PROGRAM is a finite list of instructions, each PUSH p (M -> Mp),
CLEAR p, DIVIDE p, or TEST p t (does p^t divide M?) with two targets,
plus HALT. T is the largest t a program tests. For a set O of maps of
N (the moves on one depth) and a set of tests on N, the COARSEST
CONGRUENCE is the coarsest equivalence on N that refines every test
and is carried into itself by every map in O; its CLASS COUNT is its
number of classes.
THE ARGUMENT (written before the engine).
(C) CLEARING DECIDES. With moves PUSH and CLEAR and tests t <= T,
the map v -> min(v, T) respects all three: min(v + 1, T) is a
function of min(v, T), CLEAR sends every v to 0, and v >= t iff
min(v, T) >= t for t <= T. So (q, min(a, T), min(b, T)) is a
bisimulation onto a finite set of |Q| (T + 1)^2 states, the run
halts iff its projection reaches HALT, and otherwise it loops;
halting decides. machine.py's depth machine is the CLEAR-free
T = 1 case.
(I) THE CLASS COUNT IS THE GRADE. The argument in (C) is the statement
that the coarsest congruence of {PUSH, CLEAR} refining the tests
t <= T has T + 1 classes. Replace CLEAR by DIVIDE: v and w > v are
separated by DIVIDE^v followed by the test t = 1, so the coarsest
congruence is equality, one class per depth; with two depths
and the zero-test this is Minsky's machine (Minsky 1967), cited,
and halting is undecidable. Both moves lower a depth to zero; the
one that decides is the one whose congruence is finite. A
down-move no test reads cannot steer a run, and a test of depths
that only rise flips once; the damage is the pair's class count. The program "at q0: if 2 does not
divide M halt, else divide by 2; at q1: if 2 does not divide M
loop, else divide by 2 and go to q0" halts from 4 and loops from
8, both from the class (q0, (1, 0)).
(R) THE READ VARIES THE SAME COUNT. Hold the move fixed and vary the
test. At an odd prime l seated in M the push l lowers the
headroom counter c = v_l(lambda(M)) + 1 - v_l(M) by one,
truncated at zero (machine.py, the headroom counters). Under a
blind test of the push l (independence, new idempotents,
semisimplicity, which see the support and the squarefree bit)
the states 3.7, 3.19 and 3.163 answer alike at every depth of
the orbit; under dynamics (does the push raise lambda?) they are
told apart by how many pushes pass before lambda rises, which is
c = 1, 2 and 4. So machine.py's "the price is a read" and this
file's "the price is the move" are one invariant with a
different coordinate held fixed.
THE PREDICTIONS (fixed before the engine ran).
P1 section_clear: on every program of up to two instructions with
T = 2 and of three instructions with T = 1, over PUSH, CLEAR and
TEST at the places 2 and 3, from every start (a, b) in {0, 1,
2}^2, the quotient decider's verdict matches a direct run of
4 |Q| (T + 1)^2 + 1 steps; runs from starts sharing a class
project to the same (q, min(a, T), min(b, T)) trace for that
many steps.
P2 section_classes: over v in 0..30 and every word of length at most
L, the classes the tests separate number exactly T + 1 for
{PUSH, CLEAR}, T = 1, 2, 3, at every L in {4, 6, 8}; and exactly
L + 2 for {PUSH, DIVIDE} with the zero-test (v <= L each alone,
the rest together), rising with L.
P3 section_divide: the halve-twice program halts from M = 1, 4, 16
and loops from 2, 8, 32; the runs from 4 and 8 start at one
class (q0, (1, 0)), by construction (cap sends both depths to
1), printed, so the decider of P1 is wrong on one of them.
P4 section_clear (the positive control on the down-flip): a program
that pushes and clears 2 forever flips its test from yes to no
at least 100 times in 400 steps, and the decider settles it LOOP.
P5 section_read: from 3.7, 3.19 and 3.163 the number of transparent
pushes of 3 before lambda rises is 1, 2 and 4. The three blind
demands answer the push 3 alike at every state of the three
orbits by construction, 3 dividing every state; printed, not
checked.
P6 section_divide (added after the first green run, which had no
check able to see the decider wrong): P1's decider gives the
halve-twice starts 4 and 8 one verdict, and their fates differ.
P7 section_classes (added after the first green run, when the
erasure reading was carried here): over v in 0..30, push and
division restricted to v >= 1 merge no two depths, clear merges
all 31 into one value and truncated division merges exactly the
pair 0, 1; so erasing and not erasing each occur on both sides of
the class-count line. The counts follow from the definitions; the
check prints them beside the class counts.
THE KILLS (observables, fixed before the engine ran).
K1 any disagreement printed by P1 kills (C).
K2 any {PUSH, CLEAR} class count other than T + 1 at any L >= T
kills (I)'s finite row; a {PUSH, DIVIDE} count that does not
rise with L kills its infinite row.
K3 P3 printing the same fate from 4 and 8 kills the positive
control, and no verdict of P1 is read.
THE DESIGN. Pure Python. The engine holds the depths (a, b), not M:
PUSH, CLEAR and DIVIDE at a place act on its depth alone and TEST p t
reads v_p(M) >= t, so the counter run is the run on M exactly. P5
works on M through its factorization with lambda from prime powers.
FINDINGS (entered after the run, from its printed output).
1. P1 hit: the quotient decider agrees with a direct run on 1016280
(program, start) cases, 0 disagreements, and the 463320 start
classes each project to one trace, 331776 of them holding two
starts or more (the rest, singletons, pass trivially).
2. P2 hit: push/clear prints [2, 3, 4] classes at T = 1, 2, 3 for L
= 4, 6 and 8; push/divide prints 6, 8, 10, which is L + 2.
3. P3 hit: halve-twice halts from 1, 4, 16 and loops from 2, 8, 32;
the runs from 4 and 8 start at the class (q0, (1, 0)).
4. P4 hit at the edge of its band: the pump flips its test from yes
to no exactly 100 times in 400 steps, one flip per four-step
cycle (the estimate on paper had been about 133, reading the
cycle as three steps), and the decider settles it LOOP.
5. P5 hit: 1, 2 and 4 transparent pushes of 3 from 21, 57 and 489,
and one blind answer, (False, False, False), throughout.
6. P6 (added after the first green run, which had no check able to
see the decider wrong): run on halve-twice, P1's decider answers
LOOP from both 4 and 8, where 4 halts.
7. P7 hit (added after the first green run): over 0..30 push merges
0 depths, clear 30, division on v >= 1 0, truncated division 1.
Tiers: (C) and (I) are theorems, proved above, with undecidability
given Minsky's theorem; the engine checks instances. SETTLED ON
AUDIT: (I)'s title reads the class count as the grade, and it is a
sufficient condition only: a vector addition system keeps one class
per value and still decides reachability (Mayr 1981, Kosaraju 1982).
RUN RECORD. 11 checks, 18 s, peak 12 MB; 10 once P3's
by-construction class check became a print.
"""
import sys
from itertools import product
from math import gcd
CHECKS = []
def check(name, ok, detail=""):
CHECKS.append(bool(ok))
print(f" {'PASS' if ok else 'FAIL'} {name}" +
(f" ({detail})" if detail else ""))
def section(title):
print()
print(title)
# ----------------------------------------------------------------------
# the counter engine: the depths (a, b) at the places 2 and 3
def step(ins, v):
"""One instruction on the depth vector v; returns (next, v)."""
op = ins[0]
if op == "TEST":
return (ins[3] if v[ins[1]] >= ins[2] else ins[4]), v
v = list(v)
if op == "PUSH":
v[ins[1]] += 1
elif op == "CLEAR":
v[ins[1]] = 0
elif v[ins[1]] > 0:
v[ins[1]] -= 1
return ins[2], tuple(v)
def run_direct(prog, v, steps):
"""Returns ('HALT'|'LOOP'|'OPEN', trace of (q, v))."""
q, trace = 0, []
for _ in range(steps):
ins = prog[q]
trace.append((q, v))
if ins[0] == "HALT":
return "HALT", trace
if ins[0] == "LOOP":
return "LOOP", trace
q, v = step(ins, v)
return "OPEN", trace
def cap(v, T):
return tuple(min(x, T) for x in v)
def decide(prog, v, T):
"""The quotient decider on (q, min(v, T)); PUSH/CLEAR/TEST only."""
q, z, seen = 0, cap(v, T), set()
while (q, z) not in seen:
seen.add((q, z))
ins = prog[q]
if ins[0] == "HALT":
return "HALT"
if ins[0] == "LOOP":
return "LOOP"
q, z = step(ins, z)
z = cap(z, T)
return "LOOP"
def programs(n, T):
"""Every PUSH/CLEAR/TEST program of n instructions over the two
places with tests t <= T, HALT at index n; targets 0..n."""
opts = []
for i in (0, 1):
for x in range(n + 1):
opts.append(("PUSH", i, x))
opts.append(("CLEAR", i, x))
for t in range(1, T + 1):
for x in range(n + 1):
for y in range(n + 1):
opts.append(("TEST", i, t, x, y))
for body in product(opts, repeat=n):
yield list(body) + [("HALT",)]
# ----------------------------------------------------------------------
# section_clear
PUMP = [("PUSH", 0, 1), ("TEST", 0, 1, 2, 0), ("CLEAR", 0, 1), ("HALT",)]
def section_clear():
section("CLEAR -- push, clear and bounded tests decide")
total = agree = nclass = same = multi = 0
starts = list(product(range(3), repeat=2))
for n, T in ((1, 2), (2, 2), (3, 1)):
for prog in programs(n, T):
steps = 4 * len(prog) * (T + 1) ** 2 + 1
proj = {}
for v in starts:
total += 1
d = decide(prog, v, T)
r, trace = run_direct(prog, v, steps)
agree += (d == "HALT") == (r == "HALT")
p = tuple((q, cap(x, T)) for q, x in trace)
proj.setdefault(cap(v, T), []).append(p)
for ps in proj.values():
nclass += 1
multi += len(ps) > 1
same += all(p == ps[0] for p in ps)
print(f" {total} (program, start) cases; {nclass} start classes, "
f"{multi} holding two starts or more")
check("P1 the quotient decider matches a direct run everywhere",
agree == total, f"{total - agree} disagreements")
check("P1 starts in one class project to one trace",
same == nclass, f"{nclass - same} classes split")
r, trace = run_direct(PUMP, (0, 0), 400)
outs = [x[0] >= 1 for q, x in trace if q == 1]
down = sum(1 for u, w in zip(outs, outs[1:]) if u and not w)
d = decide(PUMP, (0, 0), 1)
print(f" push-and-clear: {down} yes-to-no flips in 400 steps; "
f"decider {d}, direct {r}")
check("P4 clearing flips the test down at least 100 times",
down >= 100)
check("P4 and the decider settles the pump LOOP", d == "LOOP")
# ----------------------------------------------------------------------
# section_classes: the coarsest congruence, read through words
def classes(ops, tests, L, top=30):
words = [()]
for n in range(1, L + 1):
words += list(product(range(len(ops)), repeat=n))
sig = {}
for v in range(top + 1):
s = []
for w in words:
x = v
for i in w:
x = ops[i](x)
s.append(tuple(x >= t for t in tests))
sig.setdefault(tuple(s), []).append(v)
return len(sig)
def section_classes():
section("CLASSES -- the coarsest congruence refining the tests")
push = lambda x: x + 1
clear = lambda x: 0
divide = lambda x: max(0, x - 1)
ok_clear = ok_div = True
for L in (4, 6, 8):
row = []
for T in (1, 2, 3):
c = classes([push, clear], range(1, T + 1), L)
row.append(c)
ok_clear &= c == T + 1
d = classes([push, divide], (1,), L)
ok_div &= d == L + 2
print(f" L = {L}: push/clear at T = 1, 2, 3 -> {row}; "
f"push/divide at T = 1 -> {d}")
check("P2 push/clear has T + 1 classes at every L", ok_clear)
check("P2 push/divide separates 0..L alone: L + 2 classes", ok_div)
moves = {"push": (push, range(31)), "clear": (clear, range(31)),
"divide, v >= 1": (divide, range(1, 31)),
"divide, truncated": (divide, range(31))}
merged = {}
for name, (f, dom) in moves.items():
dom = list(dom)
merged[name] = len(dom) - len({f(v) for v in dom})
print(" depths merged over 0..30: " + ", ".join(
f"{k} {v}" for k, v in merged.items()))
check("P7 erasure falls on both sides of the class-count line",
merged == {"push": 0, "clear": 30, "divide, v >= 1": 0,
"divide, truncated": 1})
# ----------------------------------------------------------------------
# section_divide
HALVE_TWICE = [("TEST", 0, 1, 1, 4), ("DIVIDE", 0, 2),
("TEST", 0, 1, 3, 5), ("DIVIDE", 0, 0), ("HALT",),
("LOOP",)]
def section_divide():
section("DIVIDE -- one division breaks the quotient")
out = {a: run_direct(HALVE_TWICE, (a, 0), 100) for a in range(6)}
print(" halve-twice from M = 2^a: " + " ".join(
f"{2 ** a}:{out[a][0]}" for a in range(6)))
check("P3 halts from 1, 4, 16 and loops from 2, 8, 32",
all(out[a][0] == ("HALT" if a % 2 == 0 else "LOOP")
for a in range(6)))
n4 = (out[2][1][0][0], cap(out[2][1][0][1], 1))
n8 = (out[3][1][0][0], cap(out[3][1][0][1], 1))
print(f" the runs from 4 and 8 start at the classes {n4} and "
f"{n8}")
d4, d8 = decide(HALVE_TWICE, (2, 0), 1), decide(HALVE_TWICE, (3, 0), 1)
print(f" P1's decider on halve-twice: 4 -> {d4}, 8 -> {d8}")
check("P6 P1's comparison can fail: one verdict, two fates",
d4 == d8 and out[2][0] != out[3][0])
# ----------------------------------------------------------------------
# section_read: the push 3 on the headroom, blind and sighted
def factor(n):
f, p = {}, 2
while p * p <= n:
while n % p == 0:
f[p] = f.get(p, 0) + 1
n //= p
p += 1
if n > 1:
f[n] = f.get(n, 0) + 1
return f
def lam(f):
out = 1
for p, a in f.items():
if p == 2:
x = 1 if a == 1 else 2 if a == 2 else 2 ** (a - 2)
else:
x = p ** (a - 1) * (p - 1)
out = out * x // gcd(out, x)
return out
def blind(f, m):
fm = factor(m)
g = dict(f)
for p, a in fm.items():
g[p] = g.get(p, 0) + a
return (all(p not in f for p in fm), any(p not in f for p in fm),
all(a == 1 for a in g.values()))
def section_read():
section("READ -- the same push under a blind and a sighted test")
counts, blinds = [], set()
for M in (21, 57, 489):
f, n = factor(M), 0
while True:
blinds.add(blind(f, 3))
g = dict(f)
g[3] += 1
if lam(g) != lam(f):
break
n, f = n + 1, g
counts.append(n)
print(f" transparent pushes of 3 from 21, 57, 489: {counts}; "
f"blind answers seen: {sorted(blinds)}")
check("P5 the sighted test counts 1, 2, 4", counts == [1, 2, 4])
def main():
section_divide()
section_classes()
section_read()
section_clear()
print()
print(f"{sum(CHECKS)}/{len(CHECKS)} checks passed")
sys.exit(0 if all(CHECKS) else 1)
if __name__ == "__main__":
main()