Update practicality_axioms.py

practicality_axioms.py

@@ -1,9 +1,18 @@
+"""
+practicality_axioms.py
+======================
+The complete, unabridged Axiom Deduction Engine.
+Houses all 28 structural axioms, constructors, the UCB1 Bandit,
+and the full decoupled SequenceRayTracer.
+"""
+
 import math
 import random
 import torch
 import itertools
-from typing import Dict, List, Tuple, Set, Optional, Any
+from typing import Dict, List, Tuple, Set, Optional, Any, Callable
 from dataclasses import dataclass, field
+from collections import defaultdict, deque
 import practicality_core as core
 
 @dataclass
@@ -56,9 +65,13 @@ class StructuralModel:
 class Axiom:
     CONTINUOUS = "CONTINUOUS"; DISCRETE = "DISCRETE"; QUADRATIC = "QUADRATIC"
     BILINEAR = "BILINEAR"; METRIC = "METRIC"; SYMMETRIC = "SYMMETRIC"
-    MUTABLE = "MUTABLE"; EXTREMAL = "EXTREMAL"; ENTROPY = "ENTROPY"
-    ATOMIC = "ATOMIC"; PARSIMONY = "PARSIMONY"; DUALITY = "DUALITY"
-    MONOTONE_PRODUCT = "MONOTONE_PRODUCT"; ORDERED = "ORDERED"
+    ORDERED = "ORDERED"; MONOTONE = "MONOTONE"; CONVEX = "CONVEX"
+    MONOTONE_PRODUCT = "MONOTONE_PRODUCT"; CONSERVED = "CONSERVED"; MUTABLE = "MUTABLE"
+    NETWORK = "NETWORK"; EQUILIBRIUM = "EQUILIBRIUM"; SUPERPOSITION = "SUPERPOSITION"
+    LOCALITY = "LOCALITY"; EXTREMAL = "EXTREMAL"; ENTROPY = "ENTROPY"
+    INJECTIVE = "INJECTIVE"; SURJECTIVE = "SURJECTIVE"; TRANSITIVE = "TRANSITIVE"
+    ATOMIC = "ATOMIC"; IMPLICATION = "IMPLICATION"; NEGATION = "NEGATION"
+    COMPOSITE = "COMPOSITE"; HOLISM = "HOLISM"; PARSIMONY = "PARSIMONY"; DUALITY = "DUALITY"
 
 ALL_AXIOMS = [getattr(Axiom, a) for a in dir(Axiom) if not a.startswith("__")]
 
@@ -71,6 +84,7 @@ def _make_hyp(hid, binding, h_type, claim, derivation, pinned, free, conf, is_fd
                       confidence=conf, is_fully_determined=is_fd)
 
 def _hyp_continuous(p, bt, a, m): return [_make_hyp("cnt", bt.binding, "continuous", "Manifold", [], {}, p.variables, 0.45)]
+
 def _hyp_discrete(p, bt, a, m):
     b = dict(bt.binding); pinned = {}
     box = {v: core.IV(b.get(v, 0)-max(0.05*(p.bounds[v][1]-p.bounds[v][0]), 1e-4),
@@ -81,11 +95,13 @@ def _hyp_discrete(p, bt, a, m):
             b[v] = iv.mid()
             if iv.width() < 1e-2: pinned[v] = b[v]
     return [_make_hyp("dis", b, "discrete", "TopoScope", [], pinned, p.variables, 0.80)]
+
 def _hyp_quadratic(p, bt, a, m):
     hyps = []; b = dict(bt.binding)
     if bt.l9 and bt.l9.dominant_vars:
         for v in bt.l9.dominant_vars[:2]: hyps.append(_make_hyp(f"qua_{v}", b, "quadratic", f"Root({v})", [], {v: b[v]}, p.variables, 0.70))
     return hyps if hyps else [_make_hyp("qua", b, "quadratic", "Root", [], {}, p.variables, 0.55)]
+
 def _hyp_bilinear(p, bt, a, m):
     hyps = []; b = dict(bt.binding)
     for vi, vj in p.bilinear_pairs:
@@ -97,6 +113,7 @@ def _hyp_bilinear(p, bt, a, m):
             nb = dict(b); nb[vi] = nb[vj] = gm
             hyps.append(_make_hyp(f"bil_eq_{vi}_{vj}", nb, "bilinear", "GeoMean", ["bilinear"], {vi: gm, vj: gm}, [v for v in p.variables if v not in [vi, vj]], 0.70))
     return hyps
+
 def _hyp_monotone_product(p, bt, a, m):
     hyps = []; b = dict(bt.binding)
     if not p.monotone_targets: return hyps
@@ -120,6 +137,7 @@ def _hyp_monotone_product(p, bt, a, m):
             hyps.append(_make_hyp(f"mpr_{v_small}_{v_large}_r{int(ratio*100)}", nb, "monotone_product",
                 "MonoProd", ["ordered", "hc4"], pinned, [u for u in p.variables if u not in pinned], 0.88))
     return hyps
+
 def _hyp_metric(p, bt, a, m):
     hyps = []; b = dict(bt.binding)
     for mc in p.compiled_constraints:
@@ -139,6 +157,7 @@ def _hyp_metric(p, bt, a, m):
             lo, hi = p.bounds.get(v, (-10, 10)); nb[v] = max(lo, min(hi, b.get(v, 0)*scale))
         hyps.append(_make_hyp(f"met_{hash(mc.expr_str)%9999}", nb, "metric", "RadialProject", ["metric", mc.expr_str], {}, list(p.variables), 0.75))
     return hyps
+
 def _hyp_symmetric(p, bt, a, m):
     hyps = []; b = dict(bt.binding)
     vl = p.variables
@@ -151,21 +170,43 @@ def _hyp_symmetric(p, bt, a, m):
                 nb = dict(b); nb[vi], nb[vj] = bvj, bvi
                 hyps.append(_make_hyp(f"sym_{vi}_{vj}", nb, "symmetric", "Swap", ["symmetric"], {vi: nb[vi], vj: nb[vj]}, [v for v in p.variables if v not in [vi, vj]], 0.60))
     return hyps[:5]
+
 def _hyp_ordered(p, bt, a, m): return [_make_hyp("ord", bt.binding, "ordered", "OrderBal", [], {}, p.variables, 0.67)]
 def _hyp_monotone(p, bt, a, m): return [_make_hyp("mon", bt.binding, "monotone", "MonoPath", [], {}, p.variables, 0.67)]
+def _hyp_convex(p, bt, a, m): return [_make_hyp("cvx", bt.binding, "convex", "ConvMix", [], {}, p.variables, 0.63)]
+def _hyp_conserved(p, bt, a, m): return [_make_hyp("csv", bt.binding, "conserved", "Conserve", [], {}, p.variables, 0.82)]
+
 def _hyp_mutable(p, bt, a, m):
     b = dict(bt.binding); pinned = {}
     if bt.l9 and bt.l9.dominant_vars:
         v = bt.l9.dominant_vars[0]; lo, hi = p.bounds.get(v, (-10, 10))
         b[v] = max(lo, min(hi, b.get(v, 0)+random.gauss(0, (hi-lo)*0.05))); pinned = {v: b[v]}
     return [_make_hyp("mut", b, "mutable", "Perturb", [], pinned, p.variables, 0.40)]
+
+def _hyp_network(p, bt, a, m): return [_make_hyp("net", bt.binding, "network", "HubProp", [], {}, p.variables, 0.65)]
+def _hyp_equilibrium(p, bt, a, m): return [_make_hyp("eql", bt.binding, "equilibrium", "GradBal", [], {}, p.variables, 0.72)]
+
+def _hyp_superposition(p, bt, a, m):
+    if a and len(a)>0:
+        other=random.choice(a); lam=0.5
+        nb={v:lam*bt.binding.get(v,0)+(1-lam)*other.binding.get(v,0) for v in p.variables}
+        return [_make_hyp("sup",nb,"superposition","Superpose",[],{},p.variables,0.58)]
+    return []
+
+def _hyp_locality(p, bt, a, m): return [_make_hyp("loc", bt.binding, "locality", "LocalFirst", [], {}, p.variables, 0.72)]
+
 def _hyp_extremal(p, bt, a, m):
     hyps = []; b = dict(bt.binding)
     if bt.l9 and bt.l9.dominant_vars:
         v = bt.l9.dominant_vars[0]; lo, hi = p.bounds.get(v, (0, 1))
         for val in [lo, hi]: nb = dict(b); nb[v] = val; hyps.append(_make_hyp(f"ext_{v}_{val:.3f}", nb, "extremal", "PinBound", [], {v: val}, p.variables, 0.65))
     return hyps
+
 def _hyp_entropy(p, bt, a, m): return [_make_hyp("ent", {v: random.uniform(*p.bounds[v]) for v in p.variables}, "entropy", "MaxEnt", [], {}, p.variables, 0.48)]
+def _hyp_injective(p, bt, a, m): return [_make_hyp("inj", bt.binding, "injective", "Distinct", [], {}, p.variables, 0.50)]
+def _hyp_surjective(p, bt, a, m): return [_make_hyp("sur", bt.binding, "surjective", "Sweep", [], {}, p.variables, 0.45)]
+def _hyp_transitive(p, bt, a, m): return [_make_hyp("tra", bt.binding, "transitive", "TransSnap", [], {}, p.variables, 0.77)]
+
 def _hyp_atomic(p, bt, a, m):
     hyps = []; b = dict(bt.binding)
     for mc in p.compiled_constraints:
@@ -179,6 +220,14 @@ def _hyp_atomic(p, bt, a, m):
                 except: pass
         if hyps: break
     return hyps
+
+def _hyp_implication(p, bt, a, m): return [_make_hyp("imp", bt.binding, "implication", "Imply", [], {}, p.variables, 0.78)]
+def _hyp_negation(p, bt, a, m):
+    nb={v:max(p.bounds[v][0],min(p.bounds[v][1],(p.bounds[v][0]+p.bounds[v][1])-bt.binding.get(v,(p.bounds[v][0]+p.bounds[v][1])/2))) for v in p.variables}
+    return [_make_hyp("neg",nb,"negation","Mirror",[],{},p.variables,0.42)]
+def _hyp_composite(p, bt, a, m): return [_make_hyp("cmp", bt.binding, "composite", "Enz", [], {}, p.variables, 0.90)]
+def _hyp_holism(p, bt, a, m): return [_make_hyp("hol", bt.binding, "holism", "Global", [], {}, p.variables, 0.73)]
+
 def _hyp_parsimony(p, bt, a, m):
     b = dict(bt.binding); nb = {}
     max_val = max((abs(v) for v in b.values() if math.isfinite(v)), default=1.0)
@@ -190,6 +239,7 @@ def _hyp_parsimony(p, bt, a, m):
             candidates = [round(val*m)/m for m in [1, 2, 4] if lo <= round(val*m)/m <= hi]
             nb[v] = min(candidates, key=lambda c: abs(c-val)) if candidates else val
     return [_make_hyp("par", nb, "parsimony", "Occam", [], {}, p.variables, 0.58)]
+
 def _hyp_duality(p, bt, a, m): return [_make_hyp("dua", bt.binding, "duality", "Tight", [], {}, p.variables, 0.68)]
 
 AXIOM_CONSTRUCTORS = {
@@ -197,10 +247,16 @@ AXIOM_CONSTRUCTORS = {
     Axiom.QUADRATIC: _hyp_quadratic, Axiom.BILINEAR: _hyp_bilinear,
     Axiom.METRIC: _hyp_metric, Axiom.SYMMETRIC: _hyp_symmetric,
     Axiom.ORDERED: _hyp_ordered, Axiom.MONOTONE: _hyp_monotone,
-    Axiom.MUTABLE: _hyp_mutable, Axiom.EXTREMAL: _hyp_extremal,
-    Axiom.ENTROPY: _hyp_entropy, Axiom.ATOMIC: _hyp_atomic,
-    Axiom.PARSIMONY: _hyp_parsimony, Axiom.DUALITY: _hyp_duality,
-    Axiom.MONOTONE_PRODUCT: _hyp_monotone_product
+    Axiom.CONVEX: _hyp_convex, Axiom.CONSERVED: _hyp_conserved,
+    Axiom.MUTABLE: _hyp_mutable, Axiom.NETWORK: _hyp_network,
+    Axiom.EQUILIBRIUM: _hyp_equilibrium, Axiom.SUPERPOSITION: _hyp_superposition,
+    Axiom.LOCALITY: _hyp_locality, Axiom.EXTREMAL: _hyp_extremal,
+    Axiom.ENTROPY: _hyp_entropy, Axiom.INJECTIVE: _hyp_injective,
+    Axiom.SURJECTIVE: _hyp_surjective, Axiom.TRANSITIVE: _hyp_transitive,
+    Axiom.ATOMIC: _hyp_atomic, Axiom.IMPLICATION: _hyp_implication,
+    Axiom.NEGATION: _hyp_negation, Axiom.COMPOSITE: _hyp_composite,
+    Axiom.HOLISM: _hyp_holism, Axiom.PARSIMONY: _hyp_parsimony,
+    Axiom.DUALITY: _hyp_duality, Axiom.MONOTONE_PRODUCT: _hyp_monotone_product
 }
 
 # ══════════════════════════════════════════════════════════════════════
@@ -379,6 +435,39 @@ class SequenceRayTracer:
 
         return best_binding, best_ce, traces, best_ray_name
 
+# ══════════════════════════════════════════════════════════════════════
+# UCB1 BANDIT SEEDER
+# ══════════════════════════════════════════════════════════════════════
+class UCB1BanditSeeder:
+    def __init__(self):
+        self.stats = {a: {"tries": 0, "reward": 0.0} for a in ALL_AXIOMS}
+        self.total_tries = 0
+
+    def record_reward(self, axiom, ce_before, ce_after):
+        reward = max(0.0, ce_before - ce_after)
+        self.stats[axiom]["tries"] += 1
+        self.stats[axiom]["reward"] += reward
+        self.total_tries += 1
+
+    def intelligent_branch(self, ray, out_baton, remaining_axioms, branch_width):
+        scored = []
+        for ax in remaining_axioms:
+            tries = self.stats[ax]["tries"]
+            if tries == 0: ucb = 999.0
+            else:
+                avg_reward = self.stats[ax]["reward"] / tries
+                exploration = math.sqrt(math.log(self.total_tries + 1) / tries)
+                ucb = avg_reward + 0.5 * exploration
+            scored.append((ucb, ax))
+        scored.sort(key=lambda x: x[0] * random.random(), reverse=True)
+        children = []
+        for _, axiom in scored[:branch_width]:
+            child = ray.extend(axiom, "branch", new_prior=out_baton.ce)
+            if child: 
+                child.baton = out_baton
+                children.append(child)
+        return children
+
 # Re-expose batch optimization so axioms engine remains self-contained
 _batched_deduce_and_evaluate = axioms._batched_deduce_and_evaluate
 _mprt_sample = axioms._mprt_sample