 |
ProvSQL C/C++ API
Adding support for provenance and uncertainty management to PostgreSQL databases
|
|
ProvSQL C/C++ API
Adding support for provenance and uncertainty management to PostgreSQL databases
|
Tropical (min-plus) m-semiring restricted to nonnegative costs. More...
#include "Tropical.h"
Public Member Functions | |
| virtual bool | absorptive () const override |
Return true if this semiring is absorptive ( \(\mathbb{1} \oplus a = \mathbb{1}\) for all \(a\)). | |
| value_type | parse_leaf (const char *v) const |
| Public Member Functions inherited from semiring::Tropical | |
| virtual value_type | zero () const override |
| Return the additive identity \(\mathbb{0}\). | |
| virtual value_type | one () const override |
| Return the multiplicative identity \(\mathbb{1}\). | |
| virtual value_type | plus (const std::vector< value_type > &v) const override |
| Apply the additive operation to a list of values. | |
| virtual value_type | times (const std::vector< value_type > &v) const override |
| Apply the multiplicative operation to a list of values. | |
| virtual value_type | monus (value_type x, value_type y) const override |
| Apply the monus (m-semiring difference) operation. | |
| virtual value_type | delta (value_type x) const override |
| Apply the \(\delta\) operator. | |
| virtual bool | compatibleWithBooleanRewrite () const override |
No semiring homomorphism BoolFunc(Y) →+* Tropical exists (the min-plus structure cannot be made Boolean-functions compatible), so the safe-query Boolean rewrite is unsound under the tropical semiring. | |
| value_type | parse_leaf (const char *v) const |
| Public Member Functions inherited from semiring::Semiring< double > | |
| virtual value_type | cmp (value_type s1, ComparisonOperator op, value_type s2) const |
| Evaluate a comparison gate. | |
| virtual value_type | semimod (value_type x, value_type s) const |
| Apply a semimodule scalar multiplication. | |
| virtual value_type | agg (AggregationOperator op, const std::vector< value_type > &s) |
| Evaluate an aggregation gate. | |
| virtual value_type | value (const std::string &s) const |
| Interpret a literal string as a semiring value. | |
| virtual | ~Semiring ()=default |
| virtual bool | certifying () const |
| Whether this semiring builds certified exclusive enumerations (see the three hooks below). | |
| virtual bool | independent_literal (const value_type &) const |
Whether v is an independent literal for certification purposes: a base Bernoulli variable (or a constant), so that distinct literals have disjoint supports and an AND over them is decomposable. | |
| virtual value_type | certified_world_term (const std::vector< value_type > &, const std::vector< value_type > &) const |
Build one complete world term: the conjunction of the present literals and the negations of the missing literals, certified decomposable. | |
| virtual value_type | certified_exclusive_plus (const std::vector< value_type > &) const |
Build the disjunction of pairwise-exclusive disjuncts, certified deterministic. | |
Additional Inherited Members | |
| Public Types inherited from semiring::Semiring< double > | |
| typedef double | value_type |
| The carrier type of this semiring. | |
Tropical (min-plus) m-semiring restricted to nonnegative costs.
Over \(\mathbb{R}_{\ge 0} \cup \{+\infty\}\) the tropical semiring is absorptive ( \(\min(0, a) = 0\) for \(a \ge 0\)) – the canonically-ordered case the Lean formalisation proves (Tropical.absorptive under CanonicallyOrderedAdd). Declaring it lets min-plus evaluation accept circuits carrying the 'absorptive' assumption marker – notably cyclic recursive queries truncated at the absorptive value fixpoint, whose minimal derivations determine the min-cost exactly (negative costs would make cyclic min-cost genuinely unbounded, which is why the unrestricted Tropical declines). Negative input costs are rejected at leaf-parsing time.
Definition at line 110 of file Tropical.h.
|
inlineoverridevirtual |
Return true if this semiring is absorptive ( \(\mathbb{1} \oplus a = \mathbb{1}\) for all \(a\)).
When true, the circuit evaluator and HAVING-semantics machinery may exploit the resulting idempotency ( \(a \oplus a = a\), implied by absorptivity) to deduplicate children of plus gates and to short-circuit over the multiplicative identity.
false by default; override to return true. Reimplemented from semiring::Semiring< double >.
Definition at line 112 of file Tropical.h.
|
inline |
Definition at line 115 of file Tropical.h.