places.py
Checks: LEARNER: Under an income the rank is common theorem; LEARNER: The stream enters at a reversal theorem; rule.
Cited on: LEARNER.
To run it: save places.py, with forecast.py, learner.py, rationed.py beside it; standard library only.
"""places.py -- where a rationed reader's member sits against a greedy
spend-all reader's: equal, a reversal, in a layer, or incomparable at a
lower rank, and the last is a reversal over a member of the greedy
reader's layer, so the two places compose and there is no third.
QUESTION. rationed.py's greedy spend-all readers (both patiences 0,
delta = INF) share one rank trace, so two of them differ only inside a
layer; forecast.py found that without a resource limit a reader departs
from the greedy one only at a reversal, a member strictly containing
the greedy one's. A rationed reader that is patient, or draws a finite
delta, is covered by neither. Where can its committed member sit
against a greedy spend-all reader's, and does the side loss's stream
enter at a new place?
THE ARGUMENT (D1 to D3 written before the engine, D4 after the first
run).
(D1) RANK NEVER ABOVE THE GREEDY SPEND-ALL READER'S. Let X be any
rationed reader at income B and cap W and G a greedy spend-all
one. X's step spends s_n <= B + b_(n-1), its member holds J_n
(a patient move holds J_(n-p), which holds J_n, images nesting)
and so contains the bottom (learner.py's bottom lemma), whose
rank r*(J_n) bounds it by rationed.py's (A); at a step where no
member holds the image, an initial segment, r* = 0 and every
reader sits at the root. With P = rank + bank, b_n = min(W,
B + b_(n-1) - s_n) gives P^X_n = min(rho^X_n + W, P^X_(n-1) +
B). G follows
rho^G_n = min(r*(J_n), P^G_(n-1) + B) (rationed.py's (B)) and
the same P recursion. From 0, 0, by induction, rho^X_n <=
min(r*, P^X_(n-1) + B) <= rho^G_n, and then P^X_n <= P^G_n.
(D2) THE FOUR CLASSES. By (A) the inner member of a strictly nested
pair has the higher rank, so X's member is never strictly
inside G's: it is EQUAL, strictly CONTAINS it (a REVERSAL), or
is incomparable at G's rank (a LAYER) or below it (BELOW).
BELOW needs rho^X < rho^G, so no two greedy spend-all readers
make it.
(D3) BELOW EXISTS. Holders (T_i, k) and (T_j, k') of one image
with i < j <= i + k, k >= 1, are incomparable ((A)'s proof); the
tile (0, 1), rank 1, and the root's S_2, (2/3, 3/2), rank 2,
both hold (7/10, 9/10), and at its cut 4/5 the first forecasts
left and the second right.
(D4) BELOW IS A REVERSAL OVER A LAYER. Inside a holding member M =
(T_i, k), every rank from i + k + 1 to r*(J) carries a holding
member: the straddles (T_i, k'), k < k' <= k_i*, inside M as
straddles at one vertex nest; and, if T_i is not the bottom
tile, the path tiles T_j, j >= i + k + 1, and their straddles,
a straddle lying inside its own tile. Those tiles exist and lie
inside M: at k = 0 because M is T_i; at k >= 1 because J's
closure misses v_i, so by (A)'s path T_(i+k+1) = (l + k v_i,
v_i) holds J and shares S_k(v_i)'s left end. If T_i is the
bottom tile its straddles alone reach r*. So when rho^X <
rho^G, X's member strictly contains some member M' of G's rank,
M' != G's member when the pair is BELOW: X is a reversal against
M', a layer-mate of G's. Where members sit there is no third
kind of place: the two compose. The hand pair: (0, 1) contains
T_2 = (1/2, 1), rank 2, a layer-mate of S_2 of the root, and T_2
forecasts left at 4/5 (3/10 against 1/5) as (0, 1) does.
THE RUN. rationed.py's nine rows, N = 120, counted steps 8 .. 119, the
side truth by deepening to 320 (forecast.py). At each of the 16
settings (B = 1..4, W = 0, 2, 4, 8) every policy of space5(W) is run
and set beside each of the four greedy spend-all readers, step by
step, and classed EQUAL, REVERSAL, LAYER, BELOW, or BAD (strictly
inside G's member, or of higher rank).
PREDICTIONS AND KILLS (frozen before code).
K1 BAD = 0 at every setting; one BAD site kills (D1) or (D2) here.
K2 GAIN_BELOW, the sites (setting, row, step, policy) where the policy
hits the side and U = (1, 1, 0, 0, INF) misses and the pair is
BELOW, summed over the settings: predicted > 0, at most settings,
by patient readers and by greedy ones with delta finite. 0 kills
"met on the rows".
Printed beside them: the gain sites by class per setting; BELOW
sites split by patience and delta; the greedy spend-all policies
never BELOW.
Added after the first run, not frozen: D4's check at every BELOW site
against U, and F4's arm, whether a member of U's layer inside the
gaining reader's hits, with its null, the gains where those members
all forecast one side.
CONTROLS, read before any verdict: C0 the hand pair of (D3); C1 the
refuser against U, REVERSAL one way and BAD the other; C1b at no
income limit no LAYER and no BELOW; for D4, at the first 300 LAYER
sites against U no mate inside, and at the first 300 REVERSAL sites
below U's rank U's own member among them.
FINDINGS.
F0 The controls: the hand pair is BELOW, forecasting L and R; the
refuser against U at (2, 2) differs at 1008 sites, every one
REVERSAL one way and BAD the other (BAD's two arms, strictly inside
and rank above, coincide by (A), so they are not told apart); at
no income limit the 100,800 (policy, row, step) sites against U
are 17,844 EQUAL and 82,956 REVERSAL, no LAYER, BELOW or BAD.
F1 K1: BAD = 0 at all 16 settings, against all four greedy spend-all
readers; no greedy spend-all policy is BELOW one.
F2 K2: GAIN_BELOW = 3554, at 13 of the 16 settings (frozen as "> 0,
at most settings"); none at (4, 0), (4, 4), (4, 8), where no layer
gains either. Gains against U, reversal / layer / below, at six of
the 13 (the rest in the print): (1, 0) 24899 / 2887 / 237, (1, 2)
52349 / 9437 / 833, (1, 8) 66113 / 28709 / 335, (2, 8) 81944 / 3686
/ 19, (3, 8) 85471 / 1652 / 798, (4, 2) 53317 / 784 / 392; the
reversal leads at every setting.
F3 By (a patience other than 0, a refused kind counted; delta
finite): BELOW sites, all four G, (no, yes) 3220, (yes, no)
31035, (yes, yes) 66192; BELOW gains against U 319, 875, 2360.
Both frozen sources gain, so a reader of greedy patience drawing a
finite delta goes below too: the rank gap, which both make, is what
BELOW needs (necessary, not sufficient; reversals have it too).
F4 D4 holds at all 6575 BELOW sites against U (and at the 3554
gains), its controls clean (300 LAYER sites with no mate, 300
REVERSAL sites below U's rank holding U's member). Not frozen, a
count over the nine rows at the 16 settings, N = 120, against U
only: at all 3554 BELOW gains the members of U's layer inside
the gaining reader's forecast one side, and that side hits. So
there the gain is the layer-mate's, a choice inside U's layer, and
the reversal above it adds none; nothing derived forces it, a
forecast's side not being monotone in containment.
RUN RECORD. Bare, through the gate: 9 of 9 checks, 49.8 s, its peak
9.0 MB.
Exact integers in every decision. No frozen prediction was changed.
"""
import sys
from learner import (N0, INF, inside, holds, span, path_tiles,
index_max)
from rationed import ROWS9, images9, run_rationed, space5, rank, relation
from forecast import mediant, forecast, truth_deep
N_MAIN = 120
N_DEEP = 320
INCOMES = [1, 2, 3, 4]
CAPS = [0, 2, 4, 8]
QUARTET = [(a, b, 0, 0, INF) for a in (0, 1) for b in (0, 1)]
U = (1, 1, 0, 0, INF)
PLACES = ["EQUAL", "REVERSAL", "LAYER", "BELOW", "BAD"]
CHECKS = []
def check(name, ok, detail=""):
CHECKS.append(bool(ok))
print(f" {'PASS' if ok else 'FAIL'} {name}" +
(f" ({detail})" if detail else ""))
def place(cx, cg):
rel = relation(cx, cg)
rx, rg = rank(cx), rank(cg)
if rx > rg or rel == "inside":
return "BAD"
if rel == "equal":
return "EQUAL"
if rel == "contains":
return "REVERSAL"
return "LAYER" if rx == rg else "BELOW"
def layer_inside(J, rho, mx):
"""The members of rank rho holding J strictly inside mx (D4)."""
out = []
for t in path_tiles(J):
k = rho - t[3]
if 0 <= k <= index_max(t[0], t[1], J):
m = (t[0], t[1], k, t[3])
if m != mx and inside(m, mx):
out.append(m)
return out
def hits_of(trace, deep_row, truths_row):
return [int(forecast(trace[n], mediant(deep_row[n])) ==
truths_row[n - N0]) for n in range(N0, N_MAIN)]
def controls(imgs):
print("\nC CONTROLS")
tile01 = ((0, 1), (1, 1), 0, 1)
s2root = ((0, 1), (1, 0), 2, 0)
J = ((7, 10), (9, 10))
ok = (span(tile01) == ((0, 1), (1, 1)) and
span(s2root) == ((2, 3), (3, 2)) and
holds(tile01, J) and holds(s2root, J) and
relation(tile01, s2root) == "incomparable" and
rank(tile01) == 1 and rank(s2root) == 2 and
place(tile01, s2root) == "BELOW" and
forecast(tile01, mediant(J)) == "L" and
forecast(s2root, mediant(J)) == "R")
check("C0 the hand pair: a BELOW pair, forecasts L and R", ok)
# C1: orientation on real runs, the refuser against U at (2, 2)
ref = (0, 0, INF, INF, INF)
differ = wrong = 0
for row in ROWS9:
tu, _ = run_rationed(imgs[row], U, 2, 2)
tr, _ = run_rationed(imgs[row], ref, 2, 2)
for m in range(N0, N_MAIN):
if tu[m] != tr[m]:
differ += 1
wrong += not (place(tr[m], tu[m]) == "REVERSAL" and
place(tu[m], tr[m]) == "BAD")
check("C1 the refuser reads REVERSAL against U, U BAD against it",
differ > 0 and wrong == 0, f"{differ} differing, {wrong} wrong")
# C1b: unlimited readers, no LAYER and no BELOW
seen = {p: 0 for p in PLACES}
for row in ROWS9:
g, _ = run_rationed(imgs[row], U, None, 0)
for p in space5(0):
tr, _ = run_rationed(imgs[row], p, None, 0)
for m in range(N0, N_MAIN):
seen[place(tr[m], g[m])] += 1
check("C1b no income limit: only EQUAL and REVERSAL",
seen["LAYER"] == seen["BELOW"] == seen["BAD"] == 0 and
seen["REVERSAL"] > 0, f"{seen}")
def main():
imgs = images9(N_MAIN)
deep = images9(N_DEEP)
truths = {row: [truth_deep(deep[row], n) for n in range(N0, N_MAIN)]
for row in ROWS9}
if any(t is None for row in ROWS9 for t in truths[row]):
print("an unresolved truth: no verdict is read")
sys.exit(1)
controls(imgs)
if not all(CHECKS):
print("\nA CONTROL FAILED: nothing below is read.")
sys.exit(1)
print("\nK THE PLACES, per setting (B, W)")
print(" setting sites(all G) BAD BELOW LAYER REVERSAL"
" gain vs U: rev layer below")
bad_total = gain_below_total = 0
quartet_below = 0
split = {}
gsplit = {}
no_mate = carried = one_side = one_side_hit = 0
d4_sites = d4_miss = 0
ctl = {"LAYER": [0, 0], "REVERSAL": [0, 0]}
settings_with_gain_below = 0
for B in INCOMES:
for W in CAPS:
cnt = {p: 0 for p in PLACES}
gain = {p: 0 for p in PLACES}
for row in ROWS9:
gtr = {g: run_rationed(imgs[row], g, B, W)[0]
for g in QUARTET}
ghit = hits_of(gtr[U], deep[row], truths[row])
for p in space5(W):
tr = gtr[p] if p in gtr else \
run_rationed(imgs[row], p, B, W)[0]
xhit = hits_of(tr, deep[row], truths[row])
for g in QUARTET:
for j, n in enumerate(range(N0, N_MAIN)):
pl = place(tr[n], gtr[g][n])
cnt[pl] += 1
if g == U and (pl == "BELOW" or (
pl in ctl and ctl[pl][0] < 300 and
(pl == "LAYER" or
rank(tr[n]) < rank(gtr[g][n])))):
ms = layer_inside(imgs[row][n],
rank(gtr[g][n]), tr[n])
if pl == "BELOW":
d4_sites += 1
d4_miss += not ms
elif pl == "LAYER":
ctl[pl][0] += 1
ctl[pl][1] += bool(ms)
else:
ctl[pl][0] += 1
ctl[pl][1] += gtr[g][n] not in ms
if pl == "BELOW":
if p in QUARTET:
quartet_below += 1
key = ((p[2], p[3]) != (0, 0),
p[4] is not INF)
split[key] = split.get(key, 0) + 1
if g == U and xhit[j] and not ghit[j]:
gain[pl] += 1
if pl == "BELOW":
key = ((p[2], p[3]) != (0, 0),
p[4] is not INF)
gsplit[key] = gsplit.get(key, 0) + 1
J = imgs[row][n]
ms = layer_inside(J, rank(gtr[g][n]),
tr[n])
no_mate += not ms
cut = mediant(deep[row][n])
sides = {forecast(m, cut) for m in ms}
hit = truths[row][n - N0] in sides
carried += hit
if len(sides) == 1:
one_side += 1
one_side_hit += hit
bad_total += cnt["BAD"]
gain_below_total += gain["BELOW"]
settings_with_gain_below += gain["BELOW"] > 0
print(f" ({B}, {W}) {sum(cnt.values()):10d} "
f"{cnt['BAD']:3d} {cnt['BELOW']:8d} "
f"{cnt['LAYER']:5d} {cnt['REVERSAL']:8d} "
f"{gain['REVERSAL']:5d} {gain['LAYER']:5d} "
f"{gain['BELOW']:5d}")
print("\n below sites by (patient, delta finite):")
for key in sorted(split):
print(f" patient={key[0]!s:5s} finite_delta={key[1]!s:5s}"
f" {split[key]}")
print(" below gains against U by (patient, delta finite):")
for key in sorted(gsplit):
print(f" patient={key[0]!s:5s} finite_delta={key[1]!s:5s}"
f" {gsplit[key]}")
print(f" below gains with no layer-mate of U inside the reader's"
f" member: {no_mate}; with one that hits too: {carried}")
print(f" settings with a below gain: {settings_with_gain_below}"
f" of 16")
print(f" GAIN_BELOW = {gain_below_total}")
check("K1 BAD = 0 at every setting", bad_total == 0, f"{bad_total}")
check("D2 no greedy spend-all policy in a BELOW pair",
quartet_below == 0, f"{quartet_below}")
check("K2 GAIN_BELOW > 0 (BELOW met on the rows)",
gain_below_total > 0, f"{gain_below_total}")
print(f" of those, all layer-mates forecast one side at "
f"{one_side}, and hit there at {one_side_hit}")
print(f" D4 controls, the first 300 sites against U: LAYER "
f"{ctl['LAYER']} (sites, with a mate), REVERSAL below U's rank "
f"{ctl['REVERSAL']} (sites, U's member missing)")
check("D4 every below gain contains a member of U's layer",
no_mate == 0, f"{no_mate}")
check("D4 at every BELOW site against U: a layer-mate inside",
d4_sites > 0 and d4_miss == 0, f"{d4_sites} sites, {d4_miss}"
f" without")
check("D4 controls: no mate at a LAYER, U's member at a REVERSAL",
ctl["LAYER"][0] > 0 and ctl["LAYER"][1] == 0 and
ctl["REVERSAL"][0] > 0 and ctl["REVERSAL"][1] == 0,
f"{ctl}")
print()
print(f"{sum(CHECKS)} of {len(CHECKS)} checks pass")
sys.exit(0 if all(CHECKS) else 1)
if __name__ == "__main__":
main()