\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)