sign.py
Checks: REDUNDANT: The sign count theorem; REDUNDANT: The full width property; REDUNDANT: Comparison theorem.
Cited on: REDUNDANT.
To run it: save sign.py, with redundant.py beside it; standard library only.
"""
sign.py -- what the sign of a signed-digit string costs: the least
automaton that reads it, why no lookahead short of the whole string
decides it, and how comparison and the free comparator read the same
boxes.
QUESTION. Addition, scaling and every C^2 map of signed-digit streams
commit output digits at a bounded lookahead (redundant.py,
manystream.py), and max and min commit at lookahead 0
(comparators.py). The sign of the value, and so equality and
comparison, does not: it is a single verdict, not a stream of digits.
Three questions. What is the least finite-state reader of the sign,
and what sets its size? Why does no bounded lookahead decide it? And
max(x, y) must know which input is larger to select it, so why is
max free while the sign is not?
THE OBJECT. Radix b, digits D = {-a-, ..., a+}, |I| = a- + a+, with
|I| + 1 >= b, so every integer has a string (the slack
rho = |I| + 1 - b >= 0; the non-redundant rho = 0 is included). A
string d_1 ... d_n, top first, writes the integer
d_1 b^(n-1) + ... + d_n. The SIGN AUTOMATON reads it top first and
reports -1, 0 or +1. After a prefix of value u, an m-digit tail of
value t makes the whole string b^m u + t. Put M+- = a+-/(b - 1),
w = M- + M+, and call [u - M-, u + M+] the prefix's BOX: in units of
the prefix's last digit it is the closure of the values (b^m u + t)/b^m
over every tail. sigma = ceil(M-) + ceil(M+) is the count addition's
lookahead criterion spends (redundant.py::sigma). A prefix is LIVE
when its completions take more than one sign.
THE ARGUMENT (written before the engine).
(1) THE LIVE PREFIXES. Let a+- >= 1. The m-digit tails write exactly
the integers of [-a- R_m, a+ R_m], R_m = (b^m - 1)/(b - 1),
since |I| + 1 >= b. If u >= M-, every completion is at least
b^m u - a- R_m >= b^m M- - a- R_m = M- > 0; by the mirror every
completion of u <= -M+ is negative. If -M+ < u < M-: at u = 0
the completions 0, 1 and -1 exist; at u > 0 the empty tail is
positive and b^m u + t = 0 has a tail iff u <= M- (1 - b^-m),
true for large m since u < M- strictly; mirror at u < 0. So u
is live iff -M+ < u < M-, that is iff 0 lies strictly inside its
box, and every live prefix can still be driven to 0. The sides
CROSS: a positive prefix survives while u < M-, the NEGATIVE
reach, since only a negative tail pulls it back.
(2) THE SIGN COUNT. The least automaton's states are the classes of
prefixes with the same sign under every completion. The dead
prefixes make two classes. Live u < u' are separated by the
tail t with b^m u + t = 0, which leaves b^m (u' - u) > 0, and a
live prefix is separated from both dead classes by its tail to
0. Every integer of (-M+, M-) is a prefix value, the n-digit
prefixes writing every integer of [-a- R_n, a+ R_n]. So the
count is 2 plus the integers of (-M+, M-), which number
(ceil(M-) - 1) + (ceil(M+) - 1) + 1:
the sign automaton has sigma + 1 states,
2 ceil(a/(b - 1)) + 1 on the symmetric set. It is the number
addition spends: sigma counts the digits of D within M- of its
bottom and M+ of its top, the integers the box's two reaches
cover from an integer anchor, and the sign count counts the
same two reaches placed on either side of 0. With one reach 0
the numeration is unsigned: 0 is live (completions 0 and one
sign) and every other prefix is dead, 2 states.
(3) THE LEADING-NONZERO LAW. sigma + 1 = 3 iff a+- <= b - 1. Then
the only live prefix is 0: the automaton reads "zero so far"
until the first nonzero digit, whose sign is the string's, and a
string writes 0 iff every digit is 0. At a+ >= b the string
(-1, b) writes 0 with a nonzero lead, and at a- >= b so does
(1, -b).
(4) THE FULL WIDTH. At every width n >= 1 the strings 0^(n-1) 1
and 0^(n-1) (-1) share n - 1 leading digits and differ in sign,
so no k < n leading digits decide the sign of every width-n
string, at every D with a+- >= 1, rho = 0 included. The cost is
the prefix 0, whose box holds 0 at every depth; it is a signed
numeration's, not the redundancy's.
(5) THE FACTORIZATION. Each digit acts on the automaton's states as
a map, the sign is the output of the composite map at the start
state, and composition is associative. So the sign is a per-digit
map, read at lookahead 0, followed by a product a balanced tree
evaluates at depth ceil(log2 n). A zero-test factors the same
way: the per-digit predicate "d = 0" reads at lookahead 0 and
the conjunction over the digits is the full-width reduction; it
is the test only under (3). A digit-output map pays its cost in
lookahead, where a bounded carry chain and a bounded lookahead
are one condition; a reduction pays in states and depth.
(6) COMPARISON. x - y taken digit by digit is a string of
{-|I|, ..., |I|}, contiguous with both digit bounds |I| at the
same radix, so comparison is the sign automaton at (b, |I|, |I|):
2 ceil(w) + 1 states, reading a- and a+ only through their sum,
and never fewer than the sign's, ceil(w) being at least each
ceil(M+-). By (1) a difference u of prefixes is live iff
|u| < w, that is iff the two prefixes' boxes, each w long, have
interiors that meet.
(7) THE STITCH. max(x, y) has for its image over a pair of boxes the
higher box, since boxes of one depth share a width, and that is
a tile at L = 0 (comparators.py). Which box is higher is the
order of the prefix values, known exactly at every step. Which
value is higher is the order of two points of the boxes, open
by (6) exactly while the boxes' interiors meet. max reads the
first order and never the second: it commits a digit of the
higher box and is not wrong when the order of the boxes turns
later, the new higher box being a tile of the next depth. The
sign reads the second, and the prefix 0 keeps it open forever.
One box, two orders: the comparator selects by the order of the
boxes, which is always decided, and the verdict asks for the
order of the points, which is decided only when the boxes part.
THE SLATE, frozen before the engine ran.
SA THE CONTROLS. At every cell of both grids (symmetric: b = 2..12,
a = 1..12; asymmetric: b = 2..9, a+- = 0..8; each with
|I| + 1 >= b), the automaton minimised from the clamped prefix
machine reports the exact sign of every string whose length keeps
the cell's string count at most 4,000, and its count does not
move when the clamp widens by 3.
SB THE SIGN COUNT. At every cell with a+- >= 1: the count is
sigma + 1, redundant.py's sigma, and the live classes are exactly
the integers of (-M+, M-), one class each; at the cells with one
reach 0, the count is 2. Hand cells: (2,1,5) 7, (2,2,2) 5,
(3,2,2) 3, (3,1,1) 3 and (5,2,2) 3 at rho = 0.
SC THE LEADING-NONZERO LAW. The count is 3 exactly at a+- <= b - 1;
there the first nonzero digit's sign is the string's at every
string SA reads; elsewhere the two-digit witness of (3) writes 0
with a nonzero lead.
SD THE FULL WIDTH. At the cells of radices 2..4 with 1 <= a+- <= b,
at every width n >= 1 with at most 20,000 strings: the least k
whose k-digit prefixes fix the sign of every width-n string is n,
the rho = 0 cells included.
SE THE FACTORIZATION. At twelve cells, 200 seeded random strings of
lengths 1 to 64 each: the balanced product of the per-digit maps
gives the exact sign, as does the automaton run in sequence, at
tree depth ceil(log2 n).
SF COMPARISON. At every cell with a+- >= 1: the automaton at
(b, |I|, |I|) has 2 ceil(w) + 1 states, at least the sign's, and
its live differences are exactly the integers u whose box
[u - M-, u + M+] meets [-M-, M+] in interior points.
KILLS, as what the script prints.
K1 an SA line off: the automaton is not the sign's; nothing below is
read.
K2 an SB count off sigma + 1, or a live class off the interval: (1)
or (2) is wrong.
K3 an SC count of 3 off a+- <= b - 1, a misread first nonzero digit,
or a witness not writing 0: (3) is wrong.
K4 an SD width decided at k < n: (4) is wrong.
K5 an SE mismatch or a deeper tree: (5) is wrong.
K6 an SF count off 2 ceil(w) + 1 or below the sign's, or a live
difference off the box meet: (6) is wrong.
POSITIVE CONTROL: SA, read before any verdict line.
FINDINGS (entered after the run; every number is a print).
- SA holds over 583 distinct cells: 949,180 strings read, each sign
exact, and no count moved when the clamp widened by 3. K1 did not
fire.
- SB holds: the count is sigma + 1 at all 511 signed cells, the live
classes are the integers of (-M+, M-) one class each, and the 72
cells with one reach 0 have 2 states. The hand cells print (2,1,5)
7, (2,2,2) 5, (3,2,2) 3, (3,1,1) 3, (5,2,2) 3. K2 did not fire.
- SC holds: 165 cells have count 3 and they are exactly the 165 with
a+- <= b - 1; there the first nonzero digit is the sign at every
string read, and elsewhere the count is not 3. K3 did not fire.
- SD holds at 28 cells and 164 (cell, width) pairs, rho = 0 at
(3,1,1), (4,1,2) and (4,2,1): no width is decided by a shorter
prefix. K4 did not fire.
- SE holds at 12 cells and 2,400 strings. K5 did not fire.
- SF holds at 511 cells: 2 ceil(w) + 1 states, never fewer than the
sign's, the live differences exactly the meeting boxes. K6 did not
fire.
- One engine repair before the first run, not touching the slate: a
witness clause in SC that could never fire was removed. On audit
the other was too: (-1, b) writes -b + b = 0 at every radix, so
K3's witness could never fail; that the law fails above the line
is SC's count, 3 exactly at a+- <= b - 1. SE's depth is
ceil(log2 n) by the tree's halving and is no longer checked; SF's
automata, built at (b, I, I) past SA's grid, now read the exact
sign on random strings.
- (5)'s last sentence, that a bounded carry chain and a bounded
lookahead are one condition for a digit-output map, is framing:
no section checks it and no claim rests on it.
RUN RECORD: 14/14 checks, 0.9 s, peak commit 20.7 MB under a memory guard;
after an audit (SC's witness cut, SF's exact sign added), 14/14, 1.0 s,
20.7 MB.
"""
import math
import random
import time
from fractions import Fraction as Fr
import redundant as rd
CHECKS = []
CAP_SA = 4_000
CAP_SD = 20_000
def check(name, ok, detail=""):
CHECKS.append(bool(ok))
tail = f" ({detail})" if detail else ""
print(f" {'PASS' if ok else 'FAIL'} {name}{tail}")
def tag(c):
return f"({c[0]},{c[1]},{c[2]})"
def sgn(x):
return (x > 0) - (x < 0)
def ceil_frac(p, q):
return -(-p // q)
# ---- the cells ----
def covering(b, am, ap):
return am + ap + 1 >= b and am + ap >= 1
def sym_grid():
return [(b, a, a) for b in range(2, 13) for a in range(1, 13)
if covering(b, a, a)]
def asym_grid():
return [(b, am, ap) for b in range(2, 10) for am in range(9)
for ap in range(9) if covering(b, am, ap)]
def all_cells():
return sorted(set(sym_grid()) | set(asym_grid()))
def signed(c):
return c[1] >= 1 and c[2] >= 1
# ---- the engine ----
POS, NEG = "P", "N"
class Automaton:
"""The prefix machine u -> b u + d, clamped to [-B, B] with two
sinks, minimised by partition refinement from the start state 0."""
def __init__(self, b, am, ap, B):
self.b, self.D, self.B = b, list(range(-am, ap + 1)), B
states, todo = {0}, [0]
while todo:
s = todo.pop()
for d in self.D:
t = self.step(s, d)
if t not in states:
states.add(t)
todo.append(t)
self.states = sorted(states, key=str)
cls = {s: self.out(s) for s in self.states}
while True:
sig = {s: (cls[s],) + tuple(cls[self.step(s, d)]
for d in self.D)
for s in self.states}
ids = {v: i for i, v in enumerate(sorted(set(sig.values())))}
new = {s: ids[sig[s]] for s in self.states}
if len(set(new.values())) == len(set(cls.values())):
cls = new
break
cls = new
self.cls = cls
self.count = len(set(cls.values()))
dead = {cls[s] for s in (POS, NEG) if s in cls}
self.live = sorted(s for s in self.states
if s not in (POS, NEG) and cls[s] not in dead)
self.out_of = {cls[s]: self.out(s) for s in self.states}
self.trans = {}
for s in self.states:
for d in self.D:
self.trans[(cls[s], d)] = cls[self.step(s, d)]
def step(self, s, d):
if s in (POS, NEG):
return s
v = self.b * s + d
if v > self.B:
return POS
if v < -self.B:
return NEG
return v
@staticmethod
def out(s):
return 1 if s == POS else -1 if s == NEG else sgn(s)
def digit_map(self, d):
"""The class map of one digit, as a tuple over class ids."""
n = self.count
return tuple(self.trans[(k, d)] for k in range(n))
def run(self, digits):
k = self.cls[0]
for d in digits:
k = self.trans[(k, d)]
return self.out_of[k]
def build(c, extra=0):
b, am, ap = c
return Automaton(b, am, ap, max(am, ap) + 2 + extra)
def value(b, digits):
v = 0
for d in digits:
v = b * v + d
return v
def strings(D, n):
"""Every string of length n over D, as a digit tuple; its value at
radix b is left to the caller. A plain product."""
if n == 0:
yield ()
return
for s in strings(D, n - 1):
for d in D:
yield s + (d,)
def max_len(size, cap):
n, total = 0, 1
while total * size <= cap:
n += 1
total *= size
return n
def walk(A, b, nmax):
"""Depth-first over every string of length 1..nmax: yields
(digits, exact value, automaton class)."""
stack = [((), 0, A.cls[0])]
while stack:
s, v, k = stack.pop()
if s:
yield s, v, k
if len(s) < nmax:
for d in A.D:
stack.append((s + (d,), b * v + d, A.trans[(k, d)]))
def live_interval(c):
b, am, ap = c
Mm, Mp = Fr(am, b - 1), Fr(ap, b - 1)
lo, hi = math.floor(-Mp) + 1, math.ceil(Mm) - 1
return list(range(lo, hi + 1))
def first_nonzero(digits):
for d in digits:
if d:
return sgn(d)
return 0
def least_deciding_prefix(b, D, n):
"""The least k whose k-digit prefixes fix the sign of every width-n
string."""
signs = {}
for s in strings(D, n):
signs[s] = sgn(value(b, s))
for k in range(n + 1):
seen = {}
ok = True
for s, g in signs.items():
if seen.setdefault(s[:k], g) != g:
ok = False
break
if ok:
return k
return None
def compose(f, g):
"""First f, then g, as class maps."""
return tuple(g[x] for x in f)
def tree_product(maps):
depth = 0
while len(maps) > 1:
maps = [compose(maps[i], maps[i + 1]) if i + 1 < len(maps)
else maps[i] for i in range(0, len(maps), 2)]
depth += 1
return maps[0], depth
# ---- the sections ----
AUTOMATA = {}
def automaton(c):
if c not in AUTOMATA:
AUTOMATA[c] = build(c)
return AUTOMATA[c]
def section_sa():
print("SA the controls")
cells = all_cells()
misread, moved, strings_read = [], [], 0
for c in cells:
A = automaton(c)
nmax = max_len(len(A.D), CAP_SA)
for s, v, k in walk(A, c[0], nmax):
strings_read += 1
if A.out_of[k] != sgn(v):
misread.append((tag(c), s))
break
if build(c, extra=3).count != A.count:
moved.append(tag(c))
print(f" {len(cells)} cells, {strings_read} strings read")
check("SA the automaton reports the exact sign of every string read",
not misread, f"off {misread[:4]}")
check("SA the count does not move when the clamp widens by 3",
not moved, f"off {moved[:4]}")
def section_sb():
print("SB the sign count")
cells = all_cells()
sg = [c for c in cells if signed(c)]
un = [c for c in cells if not signed(c)]
off_count, off_live = [], []
for c in sg:
A = automaton(c)
if A.count != rd.sigma(*c) + 1:
off_count.append((tag(c), A.count, rd.sigma(*c) + 1))
classes = {A.cls[u] for u in A.live}
if A.live != live_interval(c) or len(classes) != len(A.live):
off_live.append((tag(c), A.live, live_interval(c)))
un_off = [(tag(c), automaton(c).count) for c in un
if automaton(c).count != 2]
print(f" {len(sg)} signed cells, {len(un)} with one reach 0")
check("SB count = sigma + 1 at every signed cell", not off_count,
f"off {off_count[:4]}")
check("SB live classes = the integers of (-M+, M-), one each",
not off_live, f"off {off_live[:3]}")
check("SB count 2 at every cell with one reach 0", not un_off,
f"off {un_off[:4]}")
hand = {(2, 1, 5): 7, (2, 2, 2): 5, (3, 2, 2): 3, (3, 1, 1): 3,
(5, 2, 2): 3}
got = {c: automaton(c).count for c in hand}
print(f" hand cells: " + ", ".join(f"{tag(c)} {got[c]}"
for c in hand))
check("SB the hand cells", got == hand, f"got {got}")
def section_sc():
print("SC the leading-nonzero law")
cells = [c for c in all_cells() if signed(c)]
three = [c for c in cells if automaton(c).count == 3]
below = [c for c in cells if c[1] <= c[0] - 1 and c[2] <= c[0] - 1]
misread = []
for c in below:
A = automaton(c)
nmax = max_len(len(A.D), CAP_SA)
for s, v, k in walk(A, c[0], nmax):
if first_nonzero(s) != sgn(v) or ((v == 0) != (not any(s))):
misread.append((tag(c), s))
break
print(f" {len(three)} cells of count 3, {len(below)} with "
f"a+- <= b - 1")
check("SC count 3 exactly at a+- <= b - 1",
sorted(three) == sorted(below))
check("SC there the first nonzero digit is the sign, and 0 iff all "
"digits are 0", not misread, f"off {misread[:4]}")
def section_sd():
print("SD the full width")
cells = [(b, am, ap) for b in range(2, 5) for am in range(1, b + 1)
for ap in range(1, b + 1) if covering(b, am, ap)]
off, read, zero = [], 0, []
for c in cells:
b, am, ap = c
D = list(range(-am, ap + 1))
if am + ap + 1 == b:
zero.append(tag(c))
for n in range(1, max_len(len(D), CAP_SD) + 1):
read += 1
k = least_deciding_prefix(b, D, n)
if k != n:
off.append((tag(c), n, k))
print(f" {len(cells)} cells, {read} (cell, width) pairs, "
f"rho = 0 at {zero}")
check("SD the least deciding prefix is the whole width", not off,
f"off {off[:4]}")
def section_se():
print("SE the factorization")
rng = random.Random(20260925)
cells = [(2, 1, 1), (2, 2, 2), (2, 1, 5), (3, 1, 1), (3, 2, 2),
(3, 4, 1), (4, 2, 3), (4, 5, 5), (5, 2, 2), (6, 4, 7),
(7, 3, 12), (9, 8, 8)]
off = []
for c in cells:
A = automaton(c)
for _ in range(200):
n = rng.randint(1, 64)
s = [rng.choice(A.D) for _ in range(n)]
prod, depth = tree_product([A.digit_map(d) for d in s])
tree = A.out_of[prod[A.cls[0]]]
exact = sgn(value(c[0], s))
if tree != exact or A.run(s) != exact:
off.append((tag(c), n))
print(f" {len(cells)} cells, {200 * len(cells)} strings")
check("SE the balanced product, the run and the exact sign agree",
not off, f"off {off[:4]}")
def section_sf():
print("SF comparison")
cells = [c for c in all_cells() if signed(c)]
off_count, below, off_live, off_sign = [], [], [], []
rng = random.Random(20261008)
for c in cells:
b, am, ap = c
I = am + ap
C = build((b, I, I))
for _ in range(20):
s = [rng.randint(-I, I) for _ in range(rng.randint(1, 10))]
if C.run(s) != sgn(value(b, s)):
off_sign.append((tag(c), s))
want = 2 * ceil_frac(I, b - 1) + 1
if C.count != want:
off_count.append((tag(c), C.count, want))
if C.count < automaton(c).count:
below.append(tag(c))
Mm, Mp = Fr(am, b - 1), Fr(ap, b - 1)
meet = [u for u in range(-2 * I - 2, 2 * I + 3)
if max(u - Mm, -Mm) < min(u + Mp, Mp)]
if C.live != meet:
off_live.append((tag(c), C.live, meet))
print(f" {len(cells)} cells")
check("SF comparison has 2 ceil(w) + 1 states", not off_count,
f"off {off_count[:4]}")
check("SF never fewer than the sign's", not below, f"off {below[:4]}")
check("SF live differences = the boxes whose interiors meet",
not off_live, f"off {off_live[:3]}")
check("SF the comparison automaton reads the exact sign, 20 random "
"strings a cell", not off_sign, f"off {off_sign[:3]}")
def main():
t0 = time.time()
section_sa()
if not all(CHECKS):
print("the controls failed; nothing below is read")
raise SystemExit(1)
for section in (section_sb, section_sc, section_sd, section_se,
section_sf):
t1 = time.time()
section()
print(f" ({time.time() - t1:.1f} s)")
print(f"{sum(CHECKS)}/{len(CHECKS)} checks passed, "
f"{time.time() - t0:.1f} s")
raise SystemExit(0 if all(CHECKS) else 1)
if __name__ == "__main__":
main()