\set ECHO none
add_provenance

(1 row)
# plain sum(x) > 15  /  >= 15
ha_probs

(1 row)
g|round
A|0.500
B|0.500
(2 rows)
ha_probs

(1 row)
g|round
A|0.500
B|0.500
(2 rows)
# additive forms (== sum(x) > 15, sum(x) >= 15)
ha_probs

(1 row)
g|round
A|0.500
B|0.500
(2 rows)
ha_probs

(1 row)
g|round
A|0.500
B|0.500
(2 rows)
ha_probs

(1 row)
g|round
A|0.500
B|0.500
(2 rows)
# multiplicative forms (positive, negative-with-flip, division)
ha_probs

(1 row)
g|round
A|0.500
B|0.500
(2 rows)
ha_probs

(1 row)
g|round
A|0.500
B|0.500
(2 rows)
ha_probs

(1 row)
g|round
A|0.500
B|0.500
(2 rows)
ha_probs

(1 row)
g|round
A|0.750
B|0.500
(2 rows)
# integer division floors (SQL truncation toward zero): NOT foldable into the
# threshold, resolved by possible-worlds enumeration with integer semantics.
#   sum(x)/2 >= 5  (floor(sum/2) >= 5  <=>  sum >= 10)
ha_probs

(1 row)
g|round
A|0.750
B|0.500
(2 rows)
#   sum(x)/7 = 1  (floor: only the worlds with 7 <= sum < 14 qualify)
ha_probs

(1 row)
g|round
A|0.250
B|0.000
(2 rows)
# unary minus (with flip) and a nested combination, both == sum(x) > 15
ha_probs

(1 row)
g|round
A|0.500
B|0.500
(2 rows)
ha_probs

(1 row)
g|round
A|0.500
B|0.500
(2 rows)
# non-exact / non-terminating multipliers (fractional thresholds)
ha_probs

(1 row)
g|round
A|0.500
B|0.500
(2 rows)
ha_probs

(1 row)
g|round
A|0.500
B|0.500
(2 rows)
ha_probs

(1 row)
g|round
A|0.750
B|0.750
(2 rows)
# threshold robustness: trailing-zero high scale, and a large magnitude
#   sum(x) > 15.0000000000000000  ==  sum(x) > 15  (scale trimmed)
ha_probs

(1 row)
g|round
A|0.500
B|0.500
(2 rows)
#   sum(x) > 1000000000  (large threshold -> exact-enumeration fallback)
ha_probs

(1 row)
g|round
A|0.000
B|0.000
(2 rows)
# min/max arithmetic (different evaluator) folds the same way
ha_probs

(1 row)
g|round
A|0.000
B|0.000
(2 rows)
ha_probs

(1 row)
g|round
A|0.000
B|0.000
(2 rows)
ha_probs

(1 row)
g|round
A|0.500
B|0.500
(2 rows)
ha_probs

(1 row)
g|round
A|0.500
B|0.500
(2 rows)
# count(*) arithmetic
ha_probs

(1 row)
g|round
A|0.250
B|0.250
(2 rows)
ha_probs

(1 row)
g|round
A|0.250
B|0.250
(2 rows)
ha_probs

(1 row)
g|round
A|0.250
B|0.250
(2 rows)
# distributive arithmetic is pushed into the aggregate: sum(x)*2 is a clean
# agg gate (not arith), so a materialised column stays comparable later
#   gate type of the pushed sum(x)*2 column (expect agg, not arith)
g|gate
A|agg
B|agg
(2 rows)
#   WHERE s2 > 30 over the materialised pushed column (== sum(x) > 15)
remove_provenance

(1 row)
g|round
A|0.500
B|0.500
(2 rows)
har_probs

(1 row)
g|round
A|0.500
B|0.500
(2 rows)
har_probs

(1 row)
g|round
A|0.500
B|0.500
(2 rows)
har_probs

(1 row)
g|round
A|0.500
B|0.500
(2 rows)
har_probs

(1 row)
g|round
A|0.250
B|0.250
(2 rows)
add_provenance

(1 row)
create_provenance_mapping

(1 row)
# probabilities by exact possible-worlds enumeration
#   sum(x) > sum(y)  (only world {t1}: 10>5)  -> 0.25
remove_provenance

(1 row)
round
0.2500
(1 row)
#   sum(x)*sum(y) > 200  (worlds {t2},{t1,t2})  -> 0.5
remove_provenance

(1 row)
round
0.5000
(1 row)
#   100.0/sum(x) > 5  (numeric c/agg; only world {t1}: 100/10>5)  -> 0.25
remove_provenance

(1 row)
round
0.2500
(1 row)
#   100/sum(x) >= 5  (integer c/agg, floor: worlds {t1}:100/10=10, {t2}:100/20=5
#   qualify; {t1,t2}:100/30=3 does not)  -> 0.5
remove_provenance

(1 row)
round
0.5000
(1 row)
# m-semiring genericity: the formula semiring gives the valid-world expression
#   sum(x) > sum(y): the single world {t1} -> t1 with t2 absent
remove_provenance

(1 row)
f
t1 ⊗ (𝟙 ⊖ t2)
(1 row)
# further operators and aggregates resolved by the same enumeration.  The
# three non-empty worlds {t1},{t2},{t1,t2} (each 0.25) have aggregates
#   {t1}:  sum_x 10 sum_y 5  count 1  min_x 10 max_x 10 avg_x 10
#   {t2}:  sum_x 20 sum_y 30 count 1  min_x 20 max_x 20 avg_x 20
#   both:  sum_x 30 sum_y 35 count 2  min_x 10 max_x 20 avg_x 15
#   sum(x)-sum(y) > 0   (subtraction; only {t1}: 10-5>0)         -> 0.25
remove_provenance

(1 row)
round
0.2500
(1 row)
#   -sum(x) > -sum(y)   (unary minus both sides; == sum(x)<sum(y)) -> 0.5
remove_provenance

(1 row)
round
0.5000
(1 row)
#   sum(x) < sum(y)     (LT; {t2},{t1,t2})                        -> 0.5
remove_provenance

(1 row)
round
0.5000
(1 row)
#   sum(x) <= sum(y)    (LE; same worlds)                         -> 0.5
remove_provenance

(1 row)
round
0.5000
(1 row)
#   sum(x) <> sum(y)    (NE; all three worlds differ)             -> 0.75
remove_provenance

(1 row)
round
0.7500
(1 row)
#   count(*) > sum(y)-sum(x)  (count aggregate; only {t1}: 1>-5)  -> 0.25
remove_provenance

(1 row)
round
0.2500
(1 row)
#   avg(x) > min(x)     (avg vs min; only {t1,t2}: 15>10)         -> 0.25
remove_provenance

(1 row)
round
0.2500
(1 row)
#   max(x) <> min(x)    (max vs min; only {t1,t2}: 20<>10)        -> 0.25
remove_provenance

(1 row)
round
0.2500
(1 row)
# correlated contributors: joining every row against a shared one-row table
# makes each provenance a conjunction (row AND switch), no longer a set of
# independent literals, so the worlds combine in the non-certified m-semiring.
# sum(x) > sum(y) now also needs the switch present: the 0.25 above times
# P(switch) = 0.5.
add_provenance

(1 row)
#   sum(x) > sum(y) over tt, ttsw                                -> 0.125
remove_provenance

(1 row)
round
0.1250
(1 row)