ProvSQL C/C++ API
Adding support for provenance and uncertainty management to PostgreSQL databases
Loading...
Searching...
No Matches
Formula.h
Go to the documentation of this file.
1/**
2 * @file semiring/Formula.h
3 * @brief Symbolic representation of provenance as a human-readable formula.
4 *
5 * The @c Formula pseudo-semiring (@c std::string, @f$\oplus@f$, @f$\otimes@f$,
6 * "šŸ˜", "šŸ™") produces a symbolic representation of provenance using
7 * Unicode semiring symbols. It is primarily used for debugging and
8 * testing.
9 *
10 * Each gate evaluates to a string:
11 * - @c zero() → "šŸ˜"
12 * - @c one() → "šŸ™"
13 * - @c plus() → "(a āŠ• b āŠ• …)" or just "a" for singletons
14 * - @c times() → "(a āŠ— b āŠ— …)" or just "a" for singletons
15 * - @c monus() → "(a āŠ– b)"
16 * - @c delta() → "Ī“(a)" or "Ī“a" if @c a starts with @c (
17 * - @c cmp() → "[s1 op s2]"
18 * - @c semimod()→ "x*s"
19 * - @c agg() → operator-specific notation (e.g., "min(a,b)")
20 * - @c value() → the literal string itself
21 * - @c unmapped_input() → the leaf's abbreviated UUID ("1361b50e…")
22 *
23 * It also renders the measure-carrier gates that carry no algebraic
24 * meaning, and that every proper semiring therefore refuses -- being a
25 * serialisation of the circuit rather than an evaluation of it,
26 * @c Formula has a faithful rendering for each and refuses nothing:
27 * - @c rv() → "normal(2.5, 0.5)" (wired parameters substituted)
28 * - @c arith() → ordinary arithmetic notation ("(a + b)", "ln(a)"…),
29 * kept visually distinct from the semiring's
30 * @f$\oplus@f$ / @f$\otimes@f$
31 * - @c mixture() → "(p ? x : y)"
32 * - @c categorical() → "categorical(Īŗ; 0.3: a, 0.7: b)"
33 * - @c guarded_case()→ "case(g → v; else d)"
34 * - @c observe() → "observe(x = 2.5)"
35 * - @c conditioned() → "(x | c)"
36 */
37#ifndef FORMULA_H
38#define FORMULA_H
39
40#include <numeric>
41#include <vector>
42#include <string>
43#include <sstream>
44#include <iomanip>
45#include <iterator>
46
47#include "Semiring.h"
48
49/**
50 * @brief Concatenate elements of a range with a delimiter.
51 *
52 * Used internally by @c Formula::plus(), @c Formula::times(), and
53 * @c Formula::agg() to build operator-separated strings.
54 *
55 * @tparam Range Any range type with a @c value_type typedef.
56 * @tparam Value Element type (defaults to @c Range::value_type).
57 * @param elements The range to join.
58 * @param delimiter String to insert between adjacent elements.
59 * @return All elements concatenated with @p delimiter between them.
60 */
61template <typename Range, typename Value = typename Range::value_type>
62static std::string join(Range const& elements, const char *const delimiter) {
63 std::ostringstream os;
64 auto b = begin(elements), e = end(elements);
65
66 if (b != e) {
67 std::copy(b, prev(e), std::ostream_iterator<Value>(os, delimiter));
68 b = prev(e);
69 }
70 if (b != e) {
71 os << *b;
72 }
73
74 return os.str();
75}
76
77/**
78 * @brief If @p s is wrapped in a single matched outer paren pair AND its
79 * top-level operator (depth 1, inside that pair) is @p op, return
80 * the inner content; otherwise return @p s unchanged.
81 *
82 * Used by @c Formula::plus() and @c Formula::times() to flatten same-op
83 * nested gates by associativity: a child @c "(a āŠ• b)" feeding into a
84 * parent @c plus is unwrapped to @c "a āŠ• b" so the join produces
85 * @c "a āŠ• b āŠ• c" instead of @c "(a āŠ• b) āŠ• c". A different top-level op
86 * (e.g., a @c times child) keeps its parens.
87 */
88static std::string strip_wrap_if_op(const std::string &s, const std::string &op) {
89 if(s.size() < 2 || s.front() != '(' || s.back() != ')')
90 return s;
91 // Verify the leading '(' closes only at the very end : if any earlier
92 // ')' brings depth back to 0, the outer pair isn't a single matched
93 // wrap (e.g., @c "(a) āŠ• (b)" must not be stripped).
94 int depth = 0;
95 for(size_t i = 0; i < s.size() - 1; ++i) {
96 if(s[i] == '(') ++depth;
97 else if(s[i] == ')') {
98 if(--depth == 0)
99 return s;
100 }
101 }
102 // Scan inner for a depth-0 occurrence of @p op. UTF-8 operators are
103 // multi-byte but @c compare on raw bytes is correct since we never
104 // straddle a UTF-8 char boundary at depth-0 positions outside parens.
105 const std::string inner = s.substr(1, s.size() - 2);
106 depth = 0;
107 for(size_t i = 0; i + op.size() <= inner.size(); ) {
108 if(inner[i] == '(') { ++depth; ++i; }
109 else if(inner[i] == ')') { --depth; ++i; }
110 else if(depth == 0 && inner.compare(i, op.size(), op) == 0)
111 return inner;
112 else
113 ++i;
114 }
115 return s;
116}
117
118/**
119 * @brief Render a probability for display in a symbolic formula.
120 *
121 * Enough significant digits that the usual decimal probabilities print
122 * back as themselves (@c 0.3, not @c 0.299999), without the full
123 * round-trip verbosity of @c setprecision(17).
124 */
125static std::string format_number(double v) {
126 std::ostringstream os;
127 os << std::setprecision(15) << v;
128 return os.str();
129}
130
131namespace semiring {
132/**
133 * @brief Symbolic provenance representation over @c std::string.
134 *
135 * Evaluates circuits to human-readable Unicode formulas.
136 * Supports all optional operations (@c cmp, @c semimod, @c agg,
137 * @c value) in addition to the mandatory ones.
138 */
139class Formula : public semiring::Semiring<std::string>
140{
141public:
142virtual value_type zero() const override {
143 return "šŸ˜";
144}
145virtual value_type one() const override {
146 return "šŸ™";
147}
148virtual value_type plus(const std::vector<value_type> &v) const override {
149 if(v.size()==0)
150 return zero();
151 else if(v.size()==1)
152 return v[0];
153 // Flatten same-op nesting by associativity: a child "(a āŠ• b)" is
154 // inlined as "a āŠ• b" so the join produces "a āŠ• b āŠ• c", not
155 // "(a āŠ• b) āŠ• c". Mixed-op children (e.g., a times subexpression)
156 // keep their parens.
157 std::vector<value_type> flat;
158 flat.reserve(v.size());
159 for(const auto &x : v)
160 flat.push_back(strip_wrap_if_op(x, "āŠ•"));
161 return "("+join(flat, " āŠ• ")+")";
162}
163virtual value_type times(const std::vector<value_type> &v) const override {
164 if(v.size()==0)
165 return one();
166 else if(v.size()==1)
167 return v[0];
168 std::vector<value_type> flat;
169 flat.reserve(v.size());
170 for(const auto &x : v)
171 flat.push_back(strip_wrap_if_op(x, "āŠ—"));
172 return "("+join(flat, " āŠ— ")+")";
173}
174virtual value_type monus(value_type x, value_type y) const override
175{
176 return "("+x+" āŠ– "+y+")";
177}
178virtual value_type delta(value_type x) const override
179{
180 if(x[0]=='(')
181 return "Ī“"+x;
182 else
183 return "Ī“("+x+")";
184}
185virtual value_type cmp(value_type s1, ComparisonOperator op, value_type s2) const override {
186 std::string result = "["+s1+" ";
187 switch(op) {
189 result+="=";
190 break;
192 result+="≠";
193 break;
195 result+="≤";
196 break;
198 result+="<";
199 break;
201 result+="≄";
202 break;
204 result+=">";
205 break;
206 }
207 return result+" "+s2+"]";
208}
209virtual value_type semimod(value_type x, value_type s) const override {
210 return x + "*" + s;
211}
212virtual value_type agg(AggregationOperator op, const std::vector<std::string> &s) override {
214 return "<>";
215
216 if(s.empty()) {
217 switch(op) {
220 return "0";
222 return "+āˆž";
224 return "-āˆž";
227 return "<>";
229 return "⊤";
231 return "⊄";
233 return "[]";
235 assert(false);
236 }
237 }
238
239 std::string result;
240 switch(op) {
242 result+="[";
243 break;
245 result+="min(";
246 break;
248 result+="max(";
249 break;
251 result+="avg(";
252 break;
254 result+="choose(";
255 break;
256 default:
257 ;
258 }
259
260 result += s[0];
261
262 for(size_t i = 1; i<s.size(); ++i) {
263 switch(op) {
266 result+="+";
267 break;
273 result+=",";
274 break;
276 result+="∨";
277 break;
279 result+="∧";
280 break;
282 assert(false);
283 }
284 result+=s[i];
285 }
287 result+="]";
288 else if(op==AggregationOperator::MIN ||
292 result+=")";
293 return result;
294}
295virtual value_type value(const std::string &s) const override {
296 return s;
297}
298/**
299 * @brief Render a random-variable leaf from its on-disk encoding.
300 *
301 * @c "normal:2.5,0.5" becomes @c "normal(2.5, 0.5)"; a wired parameter
302 * (written @c "$i", making the leaf a compound / latent one) is replaced
303 * by the rendering of the corresponding wire. Parsing here is
304 * deliberately textual: the rendering must survive any family the
305 * distribution registry gains, including one this build does not know.
306 */
307virtual value_type rv(const std::string &spec,
308 const std::vector<value_type> &params) const override {
309 const auto colon = spec.find(':');
310 if(colon == std::string::npos)
311 return spec;
312
313 std::vector<value_type> args;
314 size_t pos = colon + 1;
315 while(pos <= spec.size()) {
316 const auto comma = spec.find(',', pos);
317 const auto end = (comma == std::string::npos ? spec.size() : comma);
318 std::string arg = spec.substr(pos, end - pos);
319 if(arg.size() > 1 && arg[0] == '$') {
320 try {
321 const size_t slot = std::stoul(arg.substr(1));
322 if(slot < params.size())
323 arg = params[slot];
324 } catch(const std::exception &) {
325 // Malformed wire reference: keep the raw text.
326 }
327 }
328 args.push_back(arg);
329 if(comma == std::string::npos)
330 break;
331 pos = comma + 1;
332 }
333
334 return spec.substr(0, colon) + "(" + join(args, ", ") + ")";
335}
336/**
337 * @brief Render an arithmetic gate in ordinary arithmetic notation.
338 *
339 * Deliberately ASCII (@c +, @c *, @c -, @c /, @c ^) so that arithmetic
340 * over scalar children stays visually distinct from the semiring's
341 * @f$\oplus@f$ / @f$\otimes@f$ / @f$\ominus@f$. An operand count that
342 * does not match the operator's arity falls back to a functional
343 * rendering rather than misrepresenting the circuit.
344 */
346 const std::vector<value_type> &v,
347 const std::string &extra) const override {
348 const auto infix = [&v](const char *sep) {
349 return "(" + join(v, sep) + ")";
350 };
351 const auto functional = [&v](const char *name) {
352 return name + ("(" + join(v, ", ") + ")");
353 };
354
355 switch(op) {
357 if(v.empty()) return "0";
358 return v.size() == 1 ? v[0] : infix(" + ");
360 if(v.empty()) return "1";
361 return v.size() == 1 ? v[0] : infix(" * ");
363 return v.size() == 2 ? infix(" - ") : functional("minus");
365 return v.size() == 2 ? infix(" / ") : functional("div");
367 return v.size() == 1 ? "(-" + v[0] + ")" : functional("neg");
369 return functional("max");
371 return functional("min");
373 return v.size() == 2 ? infix(" ^ ") : functional("pow");
375 return functional("ln");
377 return functional("exp");
379 // Interleaved [indicator, value] wires; the fraction is in extra.
380 if(v.empty() || v.size() % 2 != 0)
381 return functional("percentile");
382 {
383 std::vector<value_type> rows;
384 for(size_t i = 0; i + 1 < v.size(); i += 2)
385 rows.push_back("[" + v[i] + "] " + v[i+1]);
386 return "percentile(" + extra + "; " + join(rows, ", ") + ")";
387 }
388 }
389 return functional("arith");
390}
391/** @brief Render a Bernoulli mixture as a conditional expression. */
393const override {
394 return "(" + p + " ? " + x + " : " + y + ")";
395}
396/**
397 * @brief Render a categorical mixture as its list of weighted outcomes,
398 * prefixed by the key that ties them to a single draw (two
399 * categoricals sharing a key share the draw).
400 */
402 const std::vector<double> &probs,
403 const std::vector<std::string> &outcomes)
404const override {
405 std::vector<value_type> arms;
406 for(size_t i = 0; i < probs.size() && i < outcomes.size(); ++i)
407 arms.push_back(format_number(probs[i]) + ": " + outcomes[i]);
408 return "categorical(" + key + "; " + join(arms, ", ") + ")";
409}
410/** @brief Render a guarded selection, first-match order preserved. */
411virtual value_type guarded_case(const std::vector<value_type> &v)
412const override {
413 if(v.empty() || v.size() % 2 == 0)
414 return "case(" + join(v, ", ") + ")";
415
416 std::vector<value_type> arms;
417 for(size_t i = 0; i + 1 < v.size(); i += 2)
418 arms.push_back(v[i] + " → " + v[i+1]);
419 arms.push_back("else " + v.back());
420 return "case(" + join(arms, "; ") + ")";
421}
422/** @brief Render a likelihood-weighting observation. */
423virtual value_type observe(value_type child, const std::string &datum)
424const override {
425 return "observe(" + child + " = " + datum + ")";
426}
427/**
428 * @brief Render a conditioning marker as @c "(target | evidence)".
429 *
430 * A three-wire (Boolean-event) conditioned gate also carries the
431 * materialised joint @c times(target, evidence) as its third wire; it
432 * is redundant with the first two and left out of the rendering.
433 */
434virtual value_type conditioned(const std::vector<value_type> &v)
435const override {
436 if(v.size() < 2)
437 return "cond(" + join(v, ", ") + ")";
438 return "(" + v[0] + " | " + v[1] + ")";
439}
440/**
441 * @brief Identify a variable leaf the provenance mapping does not name
442 * by an abbreviated form of its UUID.
443 *
444 * @c Formula serialises the circuit, so the base class's
445 * @f$\mathbb{1}@f$ would be doubly wrong here: it makes every unnamed
446 * leaf look alike, and -- being the multiplicative identity -- it is
447 * dropped by the enclosing @c times(), collapsing a whole join to
448 * @c "šŸ™". An abbreviated UUID keeps the structure and stays
449 * recognisable against what ProvSQL Studio prints on the circuit's
450 * nodes. The first UUID group is kept: 32 bits, enough to tell the
451 * leaves of one circuit apart at a glance, with the full value one
452 * @c get_children / Studio click away.
453 */
454virtual value_type unmapped_input(const std::string &uuid) const override {
455 return uuid.size() > 8 ? uuid.substr(0, 8) + "…" : uuid;
456}
457value_type parse_leaf(const char *v) const {
458 return std::string(v);
459}
460/**
461 * @brief Special case: @c Formula serialises the circuit structure as
462 * a string rather than computing a semantic value, so a
463 * safe-query-rewritten circuit renders to its (rewritten)
464 * structural formula and remains a faithful description. The
465 * homomorphism question does not arise.
466 */
467virtual bool compatibleWithBooleanRewrite() const override {
468 return true;
469}
470/**
471 * @brief Serialise a Formula evaluation as text.
472 *
473 * Drops the cosmetic outer paren pair that @c plus / @c times / @c monus
474 * always produce: at the root there is no enclosing context, so the
475 * outer parens carry no disambiguation value.
476 */
477std::string to_text(const value_type &s) const {
478 if(s.size() < 2 || s.front() != '(' || s.back() != ')')
479 return s;
480 int depth = 0;
481 for(size_t i = 0; i < s.size() - 1; ++i) {
482 if(s[i] == '(') ++depth;
483 else if(s[i] == ')') {
484 if(--depth == 0)
485 return s;
486 }
487 }
488 return s.substr(1, s.size() - 2);
489}
490};
491}
492
493#endif /* FORMULA_H */
AggregationOperator
SQL aggregation functions tracked by ProvSQL.
Definition Aggregation.h:51
@ OR
Boolean OR aggregate.
Definition Aggregation.h:58
@ MAX
MAX → input type.
Definition Aggregation.h:55
@ COUNT
COUNT(*) or COUNT(expr) → integer.
Definition Aggregation.h:52
@ AND
Boolean AND aggregate.
Definition Aggregation.h:57
@ SUM
SUM → integer or float.
Definition Aggregation.h:53
@ ARRAY_AGG
Array aggregation.
Definition Aggregation.h:60
@ NONE
No aggregation (returns NULL).
Definition Aggregation.h:61
@ MIN
MIN → input type.
Definition Aggregation.h:54
@ CHOOSE
Arbitrary selection (pick one element).
Definition Aggregation.h:59
@ AVG
AVG → float.
Definition Aggregation.h:56
ComparisonOperator
SQL comparison operators used in gate_cmp circuit gates.
Definition Aggregation.h:39
@ LT
Less than (<).
Definition Aggregation.h:43
@ GT
Greater than (>).
Definition Aggregation.h:45
@ LE
Less than or equal (<=).
Definition Aggregation.h:42
@ NE
Not equal (<>).
Definition Aggregation.h:41
@ GE
Greater than or equal (>=).
Definition Aggregation.h:44
ArithmeticOperator
Arithmetic operations carried by gate_arith circuit gates.
Definition Aggregation.h:74
@ POW
binary power
Definition Aggregation.h:82
@ MAX
n-ary maximum (order statistic)
Definition Aggregation.h:80
@ DIV
binary quotient
Definition Aggregation.h:78
@ PERCENTILE
continuous percentile over interleaved [indicator, value] wires
Definition Aggregation.h:85
@ NEG
unary negation
Definition Aggregation.h:79
@ EXP
unary exponential
Definition Aggregation.h:84
@ TIMES
n-ary product
Definition Aggregation.h:76
@ MIN
n-ary minimum (order statistic)
Definition Aggregation.h:81
@ LN
unary natural logarithm
Definition Aggregation.h:83
@ MINUS
binary difference
Definition Aggregation.h:77
static std::string join(Range const &elements, const char *const delimiter)
Concatenate elements of a range with a delimiter.
Definition Formula.h:62
static std::string format_number(double v)
Render a probability for display in a symbolic formula.
Definition Formula.h:125
static std::string strip_wrap_if_op(const std::string &s, const std::string &op)
If s is wrapped in a single matched outer paren pair AND its top-level operator (depth 1,...
Definition Formula.h:88
Abstract semiring interface for provenance evaluation.
Symbolic provenance representation over std::string.
Definition Formula.h:140
virtual value_type zero() const override
Return the additive identity .
Definition Formula.h:142
virtual bool compatibleWithBooleanRewrite() const override
Special case: Formula serialises the circuit structure as a string rather than computing a semantic v...
Definition Formula.h:467
virtual value_type cmp(value_type s1, ComparisonOperator op, value_type s2) const override
Evaluate a comparison gate.
Definition Formula.h:185
virtual value_type semimod(value_type x, value_type s) const override
Apply a semimodule scalar multiplication.
Definition Formula.h:209
virtual value_type agg(AggregationOperator op, const std::vector< std::string > &s) override
Evaluate an aggregation gate.
Definition Formula.h:212
virtual value_type times(const std::vector< value_type > &v) const override
Apply the multiplicative operation to a list of values.
Definition Formula.h:163
virtual value_type guarded_case(const std::vector< value_type > &v) const override
Render a guarded selection, first-match order preserved.
Definition Formula.h:411
value_type parse_leaf(const char *v) const
Definition Formula.h:457
virtual value_type arith(ArithmeticOperator op, const std::vector< value_type > &v, const std::string &extra) const override
Render an arithmetic gate in ordinary arithmetic notation.
Definition Formula.h:345
std::string to_text(const value_type &s) const
Serialise a Formula evaluation as text.
Definition Formula.h:477
virtual value_type unmapped_input(const std::string &uuid) const override
Identify a variable leaf the provenance mapping does not name by an abbreviated form of its UUID.
Definition Formula.h:454
virtual value_type monus(value_type x, value_type y) const override
Apply the monus (m-semiring difference) operation.
Definition Formula.h:174
virtual value_type observe(value_type child, const std::string &datum) const override
Render a likelihood-weighting observation.
Definition Formula.h:423
virtual value_type one() const override
Return the multiplicative identity .
Definition Formula.h:145
virtual value_type delta(value_type x) const override
Apply the operator.
Definition Formula.h:178
virtual value_type mixture(value_type p, value_type x, value_type y) const override
Render a Bernoulli mixture as a conditional expression.
Definition Formula.h:392
virtual value_type categorical(value_type key, const std::vector< double > &probs, const std::vector< std::string > &outcomes) const override
Render a categorical mixture as its list of weighted outcomes, prefixed by the key that ties them to ...
Definition Formula.h:401
virtual value_type value(const std::string &s) const override
Interpret a literal string as a semiring value.
Definition Formula.h:295
virtual value_type conditioned(const std::vector< value_type > &v) const override
Render a conditioning marker as "(target | evidence)".
Definition Formula.h:434
virtual value_type plus(const std::vector< value_type > &v) const override
Apply the additive operation to a list of values.
Definition Formula.h:148
virtual value_type rv(const std::string &spec, const std::vector< value_type > &params) const override
Render a random-variable leaf from its on-disk encoding.
Definition Formula.h:307
Abstract base class for (m-)semirings.
Definition Semiring.h:97