Proj aware join

differential/corpus/programs/projection_cut.mm2

@@ -0,0 +1,52 @@
+;; @expect
+;; @steps  20
+;; @desc   Variables no template reads: the engines may answer them with one witness instead of
+;; @desc   enumerating their domain, but only where that cannot change the answer set. Each block
+;; @desc   below is a shape the projection cut must get right; the expected space pins all of them.
+
+;; --- 1. A trailing don't-care with fan-out. `$_` is mentioned once and no template reads it, so
+;; every value past the first re-derives `(out1 a)`. One row per `r`, whatever the fan-out.
+(r a)
+(r b)
+(s a p)
+(s a q)
+(s a t)
+(s b t)
+(exec 0 (, (r $x) (s $x $_)) (, (out1 $x)))
+
+;; --- 2. Schematic data. A don't-care may witness a term that itself contains variables; the
+;; answer must not depend on which witness the engine happened to reach first.
+(sv k plain)
+(sv k (f $z))
+(sv k (g $w $v))
+(exec 1 (, (sv $y $_) ) (, (out2 $y)))
+
+;; --- 3. A don't-care that is NOT trailing. `$m` decides which `(gg $m $n)` subtrie `$n` is drawn
+;; from, so pinning it would drop answers rather than duplicates: every `$n` must survive.
+(gg p 1)
+(gg p 2)
+(gg q 3)
+(exec 2 (, (gg $m $n)) (, (out3 $n)))
+
+;; --- 4. The same, one level down: the don't-care sits inside a compound, still not trailing.
+(hh (kk p 1))
+(hh (kk p 2))
+(hh (kk q 3))
+(exec 3 (, (hh (kk $mm $nn))) (, (out4 $nn)))
+
+;; --- 5. A repeated variable no template reads is a JOIN variable, not a don't-care: it still has
+;; to intersect, so `(out5 ...)` holds only the values `jl` and `jr` agree on.
+(jl 1)
+(jl 2)
+(jl 3)
+(jr 2)
+(jr 3)
+(jr 4)
+(je 2)
+(exec 4 (, (jl $p) (jr $p) (je $q)) (, (out5 $q)))
+
+;; --- 6. An O-form whose pattern carries a don't-care guard. The guard must keep gating: the
+;; counter decrements once per step while `(wanted t)` exists, and stops when it no longer does.
+(wanted t)
+(counter (S (S (Z))))
+(exec 5 (, (exec 5 $a $b) (wanted $c) (counter (S $d))) (O (+ (exec 5 $a $b)) (+ (counter $d)) (- (counter (S $d)))))

differential/corpus/programs/projection_cut_aliased.mm2

@@ -0,0 +1,53 @@
+;; @expect
+;; @steps  30
+;; @desc   Data-side aliasing: facts whose own variable ties the don't-care column to a column a
+;; @desc   template reads. The query-side rule (mentioned once, unread, trailing) says nothing
+;; @desc   about the DATA sharing a variable across those columns, so each shape is pinned here.
+;; @desc
+;; @desc   Why it is sound: a bare fresh singleton is an unconstrained position, so whichever
+;; @desc   stored subterm it meets, the binding is read by nothing and constrains nothing else.
+;; @desc   What could still discriminate is a LATER query position drawing from the subtrie the
+;; @desc   choice selected -- and the trailing condition is exactly what excludes that. The
+;; @desc   discriminating information in these shapes lives in the repeated column, which is a
+;; @desc   trie PREFIX of the don't-care column, so it is enumerated before the cut applies.
+
+;; 1. the tail aliases the first column; the facts differ at the REPEATED column, so `$a` must
+;;    still iterate over both A and B
+(f1 $x A $x)
+(f1 $x B $x)
+(exec (0 1) (, (f1 $a $a $_)) (, (o1 $a)))
+
+;; 2. the facts differ at the DON'T-CARE column instead, and `$a` stays free
+(f2 $x $x A)
+(f2 $x $x B)
+(exec (0 2) (, (f2 $a $a $_)) (, (o2 $a)))
+
+;; 3. the don't-care column mixes a back-reference with a ground term
+(f3 $x $x $x)
+(f3 $x $x A)
+(exec (0 3) (, (f3 $a $a $_)) (, (o3 $a)))
+
+;; 4. the read variable is pinned by the FIRST column, with an alias in the tail
+(f4 A $x $x)
+(f4 B $x $x)
+(exec (0 4) (, (f4 $a $a $_)) (, (o4 $a)))
+
+;; 5. two trailing don't-cares, both aliased to the read variable
+(f5 $x A $x $x)
+(f5 $x B $x $x)
+(exec (0 5) (, (f5 $a $a $_ $_2)) (, (o5 $a)))
+
+;; 6. the don't-care sits in the MIDDLE, so it is not cuttable at all
+(f6 $x A $x)
+(f6 $x B $x)
+(exec (0 6) (, (f6 $c $_ $c)) (, (o6 $c)))
+
+;; 7. the don't-care's subterm carries structure over the shared variable
+(f7 $x $x (g $x))
+(f7 $x $x (h $x))
+(exec (0 7) (, (f7 $a $a $_)) (, (o7 $a)))
+
+;; 8. a read variable pinned only via the repeated column, with the tail aliasing it
+(f8 $x $x A $x)
+(f8 $x $x B $x)
+(exec (0 8) (, (f8 $a $a $b $_)) (, (o8 $a $b)))

differential/corpus/programs/transform_decomposition.mm2

@@ -0,0 +1,70 @@
+;; @expect
+;; @steps  40
+;; @desc   Decomposition lowerings, each computed BOTH ways so the expected space pins the
+;; @desc   staged form equal to the naive one: a 6-cycle split into two bags, a 4-clique staged
+;; @desc   through triangles, and the wiki Reachability-P2 crafting join reduced per ingredient
+;; @desc   side. A divergence in any of them changes this program's space.
+
+;; ---------------------------------------------------------------- 6-cycle, ghw 2 < rho* 3
+(e a b)
+(e b c)
+(e c d)
+(e d f)
+(e f g)
+(e g a)
+(e a c)
+(e c f)
+(e f a)
+(exec (0 0) (, (e $a $b) (e $b $c) (e $c $d) (e $d $f) (e $f $g) (e $g $a)) (, (cycN $a)))
+;; two bags of three edges; the first is materialised as its PROJECTED endpoints, which is what
+;; shares the suffix across every binding of the discarded middle variables
+(exec (1 0) (, (e $a $b) (e $b $c) (e $c $d)) (, (p3 $a $d)))
+(exec (1 1) (, (p3 $a $d) (e $d $f) (e $f $g) (e $g $a)) (, (cycS $a)))
+
+;; ---------------------------------------------------------------- 4-clique
+(edge n0 n1)
+(edge n0 n2)
+(edge n0 n3)
+(edge n1 n2)
+(edge n1 n3)
+(edge n2 n3)
+(edge n1 n4)
+(edge n2 n4)
+(exec (2 0) (, (edge $x0 $x1) (edge $x0 $x2) (edge $x0 $x3)
+                (edge $x1 $x2) (edge $x1 $x3) (edge $x2 $x3))
+            (, (c4N $x0 $x1 $x2 $x3)))
+;; staged through the triangle bag. Every variable is named by the template, so nothing is
+;; projected away and leapfrog has nothing to share -- kept as the contrast to the 6-cycle.
+(exec (3 0) (, (edge $x0 $x1) (edge $x0 $x2) (edge $x1 $x2)) (, (tri $x0 $x1 $x2)))
+(exec (3 1) (, (tri $x0 $x1 $x2) (edge $x0 $x3) (edge $x1 $x3) (edge $x2 $x3))
+            (, (c4S $x0 $x1 $x2 $x3)))
+
+;; ---------------------------------------------------------------- crafting (wiki P2 exec (1 3))
+(recipe r0 (numIngredients 2))
+(recipe r0 (result (id itemA)))
+(recipe r0 (pattern 0 sx0))
+(recipe r0 (pattern 1 sy0))
+(recipe r0 (key (sx0 wood)))
+(recipe r0 (key (sx0 stone)))
+(recipe r0 (key (sy0 coal)))
+(recipe r1 (numIngredients 2))
+(recipe r1 (result (id itemB)))
+(recipe r1 (pattern 0 sx1))
+(recipe r1 (pattern 1 sy1))
+(recipe r1 (key (sx1 gold)))
+(recipe r1 (key (sy1 missing)))
+(inventory wood)
+(inventory stone)
+(inventory coal)
+(inventory gold)
+(exec (4 0) (, (recipe $p (numIngredients 2)) (recipe $p (result (id $n)))
+                (recipe $p (pattern 0 $x)) (recipe $p (key ($x $xi)))
+                (recipe $p (pattern 1 $y)) (recipe $p (key ($y $yi)))
+                (inventory $xi) (inventory $yi))
+            (, (craftN $n)))
+;; each ingredient side is satisfiable independently given the recipe, and everything but the
+;; product name is projected away: reduce each side to a witness on $p, then combine
+(exec (5 0) (, (recipe $p (pattern 0 $x)) (recipe $p (key ($x $xi))) (inventory $xi)) (, (ok0 $p)))
+(exec (5 1) (, (recipe $p (pattern 1 $y)) (recipe $p (key ($y $yi))) (inventory $yi)) (, (ok1 $p)))
+(exec (5 2) (, (recipe $p (numIngredients 2)) (ok0 $p) (ok1 $p) (recipe $p (result (id $n))))
+            (, (craftS $n)))

differential/corpus/programs/transform_process_calculus.mm2

@@ -0,0 +1,66 @@
+;; @expect
+;; @steps  60
+;; @desc   The process calculus lowered three ways over the same soup, so the expected space pins
+;; @desc   all three to the same final message: monotone naive, delta on the message side, and
+;; @desc   consuming (the reagents are retired). The naive rule never removes, so it re-derives
+;; @desc   every past communication on every round -- quadratic in the cascade length.
+
+;; a cascade: each receiver forwards to the next channel
+(pN (? c0 p0 (! c1 p1)))
+(pN (? c1 p1 (! c2 p2)))
+(pN (? c2 p2 (! c3 p3)))
+(pN (? c3 p3 (! r0 q0)))
+(pN (? r0 q0 (? r1 q1 (! deep ok))))
+(pN (? r1 q1 (! early seen)))
+(pN (! r1 q1))
+(pN (! c0 p0))
+(pD (? c0 p0 (! c1 p1)))
+(pD (? c1 p1 (! c2 p2)))
+(pD (? c2 p2 (! c3 p3)))
+(pD (? c3 p3 (! r0 q0)))
+(pD (? r0 q0 (? r1 q1 (! deep ok))))
+(pD (? r1 q1 (! early seen)))
+(pD (! r1 q1))
+(pD (! c0 p0))
+(dD (? c0 p0 (! c1 p1)))
+(dD (? c1 p1 (! c2 p2)))
+(dD (? c2 p2 (! c3 p3)))
+(dD (? c3 p3 (! r0 q0)))
+(dD (? r0 q0 (? r1 q1 (! deep ok))))
+(dD (? r1 q1 (! early seen)))
+(dD (! r1 q1))
+(dD (! c0 p0))
+(pC (? c0 p0 (! c1 p1)))
+(pC (? c1 p1 (! c2 p2)))
+(pC (? c2 p2 (! c3 p3)))
+(pC (? c3 p3 (! r0 q0)))
+(pC (? r0 q0 (? r1 q1 (! deep ok))))
+(pC (? r1 q1 (! early seen)))
+(pC (! r1 q1))
+(pC (! c0 p0))
+(fN (S (S (S (S (S (S Z)))))))
+(fD (S (S (S (S (S (S Z)))))))
+(fC (S (S (S (S (S (S Z)))))))
+
+;; (a) monotone: nothing retired, so round k re-derives all k-1 earlier communications
+(exec (1 Z) (, (exec (1 $l) $p $t) (fN (S $k)) (pN (? $c $pl $b)) (pN (! $c $pl)))
+            (O (+ (exec (1 (S $l)) $p $t)) (+ (pN $b)) (+ (fN $k)) (- (fN (S $k)))))
+
+;; (b) SYMMETRIC delta. A self-join over one relation needs both arms: new receivers against
+;; every message, and every receiver against new messages. With only the second, a communication
+;; that derives a RECEIVER never reacts with a message already in the soup -- which is what the
+;; (? r0 ..) pair above is here to catch.
+((armD 0) (, (dD (? $c $pl $b)) (pD (! $c $pl)))
+          (O (+ (pD $b)) (+ (dD $b)) (- (dD (? $c $pl $b)))))
+((armD 1) (, (pD (? $c $pl $b)) (dD (! $c $pl)))
+          (O (+ (pD $b)) (+ (dD $b)) (- (dD (! $c $pl)))))
+(exec (2 (IC 0 1 (S (S (S (S (S (S (S (S (S (S Z))))))))))))
+      (, (exec (2 (IC $x $y (S $c))) $sp $st) ((armD $x) $p $t))
+      (, (exec (2 (IC $y $x $c)) $sp $st) (exec (2 (R $x)) $p $t)))
+
+;; (c) consuming: the reagents are retired, so no intermediate is ever kept and the
+;; re-derivation is removed at its source rather than filtered afterwards
+(exec (3 Z) (, (exec (3 $l) $p $t) (fC (S $k)) (pC (? $c $pl $b)) (pC (! $c $pl)))
+            (O (+ (exec (3 (S $l)) $p $t)) (+ (pC $b))
+               (- (pC (? $c $pl $b))) (- (pC (! $c $pl)))
+               (+ (fC $k)) (- (fC (S $k)))))

differential/corpus/programs/transform_staging.mm2

@@ -0,0 +1,65 @@
+;; @expect
+;; @steps  60
+;; @desc   The two source-level transforms, each computed BOTH ways in one program so the
+;; @desc   expected space pins them equal: a chain query naively and Yannakakis-staged, and a
+;; @desc   transitive closure naively and semi-naively. If a staging ever stops agreeing with the
+;; @desc   form it replaces, this program's space changes.
+
+;; ---------------------------------------------------------------- the chain query R-S-T
+(R a p)
+(R b p)
+(R c q)
+(R d r)
+(S p u)
+(S p v)
+(S q u)
+(S r dead)
+(T u m)
+(T v n)
+
+;; naive: one join over all three relations
+(exec (0 0) (, (R $x $y) (S $y $z) (T $z $w)) (, (outN $x $w)))
+
+;; Yannakakis-staged: project, semi-join bottom-up, semi-join top-down, then join the reduced
+;; relations. Every projection is `(, (Rel $key $_))` -- the shape the projection cut answers
+;; with one witness per key -- which is why the reduced relations are emitted KEY-FIRST: a
+;; projection off a key-last relation would be `(, (Rel $_ $key))`, where the don't-care is not
+;; trailing and must keep enumerating.
+(exec (1 0) (, (T $z $_))            (, (Tz $z)))
+(exec (1 1) (, (S $y $z) (Tz $z))    (, (S1 $y $z)))
+(exec (1 2) (, (S1 $y $_))           (, (S1y $y)))
+(exec (1 3) (, (R $x $y) (S1y $y))   (, (R1 $y $x)))
+(exec (1 4) (, (R1 $y $_))           (, (R1y $y)))
+(exec (1 5) (, (S1 $y $z) (R1y $y))  (, (S2 $z $y)))
+(exec (1 6) (, (S2 $z $_))           (, (S2z $z)))
+(exec (1 7) (, (T $z $w) (S2z $z))   (, (T1 $z $w)))
+(exec (1 8) (, (R1 $y $x) (S2 $z $y) (T1 $z $w)) (, (outS $x $w)))
+
+;; ---------------------------------------------------------------- transitive closure
+(edge g0 g1)
+(edge g1 g2)
+(edge g2 g3)
+(edge g3 g4)
+
+;; NOTE on loc ordering: execs run in byte order of the whole atom, and a SYMBOL loc sorts
+;; above a COMPOUND one -- `(exec (2 0) ..)` would run AFTER `(exec (2 (1 Z)) ..)`, so the seed
+;; would fire after the loop and the loop would see an empty relation. Every loc here is the
+;; same shape so the intended order is the numeric one.
+;;
+;; Both loops carry Peano fuel. A self-reproducing exec has no termination condition of its own,
+;; so an unbounded one would monopolise every remaining step and the family after it would never
+;; run at all.
+(fuelN (S (S (S (S (S Z))))))
+(fuelD (S (S (S (S (S Z))))))
+
+;; naive: every iteration re-joins the WHOLE path relation with edge
+(exec (2 (0 0)) (, (edge $x $y)) (, (pathN $x $y)))
+(exec (2 (1 Z)) (, (exec (2 (1 $l)) $p $t) (fuelN (S $k)) (pathN $x $y) (edge $y $z))
+                (O (+ (exec (2 (1 (S $l))) $p $t)) (+ (pathN $x $z))
+                   (+ (fuelN $k)) (- (fuelN (S $k)))))
+
+;; semi-naive: every iteration joins only the frontier the previous one produced
+(exec (3 (0 0)) (, (edge $x $y)) (, (front Z $x $y) (pathD $x $y)))
+(exec (3 (1 Z)) (, (exec (3 (1 $l)) $p $t) (fuelD (S $k)) (front $l $x $y) (edge $y $z))
+                (O (+ (exec (3 (1 (S $l))) $p $t)) (+ (front (S $l) $x $z)) (+ (pathD $x $z))
+                   (+ (fuelD $k)) (- (fuelD (S $k)))))

differential/expected/programs/projection_cut.expected

@@ -0,0 +1,34 @@
+(r a)
+(r b)
+(hh (kk p 1))
+(hh (kk p 2))
+(hh (kk q 3))
+(je 2)
+(jl 1)
+(jl 2)
+(jl 3)
+(jr 2)
+(jr 3)
+(jr 4)
+(out1 a)
+(out1 b)
+(out2 k)
+(out3 1)
+(out3 2)
+(out3 3)
+(out4 1)
+(out4 2)
+(out4 3)
+(out5 2)
+(wanted t)
+(counter (Z))
+(s a p)
+(s a q)
+(s a t)
+(s b t)
+(gg p 1)
+(gg p 2)
+(gg q 3)
+(sv k (f $a))
+(sv k (g $a $b))
+(sv k plain)

differential/expected/programs/projection_cut_aliased.expected

@@ -0,0 +1,28 @@
+(o1 A)
+(o1 B)
+(o2 $a)
+(o3 $a)
+(o4 A)
+(o4 B)
+(o5 A)
+(o5 B)
+(o6 $a)
+(o7 $a)
+(o8 $a A)
+(o8 $a B)
+(f1 $a A $a)
+(f1 $a B $a)
+(f2 $a $a A)
+(f2 $a $a B)
+(f3 $a $a $a)
+(f3 $a $a A)
+(f4 A $a $a)
+(f4 B $a $a)
+(f6 $a A $a)
+(f6 $a B $a)
+(f7 $a $a (g $a))
+(f7 $a $a (h $a))
+(f5 $a A $a $a)
+(f5 $a B $a $a)
+(f8 $a $a A $a)
+(f8 $a $a B $a)