Semiring.h

Go to the documentation of this file.

/**
 * @file semiring/Semiring.h
 * @brief Abstract semiring interface for provenance evaluation.
 *
 * ProvSQL evaluates provenance circuits over arbitrary (m-)semirings.
 * This header defines the abstract base class @c semiring::Semiring<V>
 * that every concrete semiring must implement.
 *
 * A **semiring** @f$(S, \oplus, \otimes, \mathbb{0}, \mathbb{1})@f$
 * consists of:
 * - A carrier set @f$S@f$ (the @c value_type).
 * - An additive operation @f$\oplus@f$ with identity @f$\mathbb{0}@f$.
 * - A multiplicative operation @f$\otimes@f$ with identity @f$\mathbb{1}@f$.
 *
 * An **m-semiring** additionally provides:
 * - A monus operation @f$\ominus@f$ used for set-difference queries.
 * - A @f$\delta@f$ operator.
 *
 * Optional operations -- comparison, semimodule scalar multiplication,
 * aggregation, value literals, and the measure-carrier gates
 * (random-variable leaves, scalar arithmetic, mixtures, guarded
 * selection, observations, conditioning) -- are provided by subclasses
 * that support them; the base class throws @c SemiringException for all
 * of these.  Most carry no algebraic meaning in a general semiring and
 * are overridden only by @c Formula, whose carrier is a symbolic
 * rendering of the circuit rather than a semantic value.
 *
 * Concrete implementations live in the same @c semiring/ directory:
 * @c Boolean.h, @c Counting.h, @c Formula.h, @c Why.h, @c BoolExpr.h.
 *
 * @see https://provsql.org/lean-docs/Provenance/SemiringWithMonus.html
 *      Lean 4 formalization of the @c SemiringWithMonus typeclass and
 *      proofs of the key monus identities (@c monus_smallest,
 *      @c monus_self, @c zero_monus, @c monus_add, @c add_monus,
 *      @c idempotent_iff_add_monus).
 */
#ifndef SEMIRING_H
#define SEMIRING_H
 
#include <vector>
#include <string>
 
#include "../Aggregation.h"
 
namespace semiring {
 
/**
 * @brief Exception thrown when a semiring operation is not supported.
 *
 * Raised by the default implementations of optional operations
 * (@c cmp, @c semimod, @c agg, @c value) when a subclass does not
 * override them.
 */
class SemiringException : public std::exception
{
std::string message; ///< Human-readable description of the error
 
public:
/**
 * @brief Construct with a descriptive error message.
 * @param m  Error message.
 */
SemiringException(const std::string &m) : message(m) {
}
/**
 * @brief Return the error message as a C-string.
 * @return Null-terminated error description.
 */
virtual char const * what() const noexcept {
  return message.c_str();
}
};
 
/**
 * @brief A gate kind this semiring does not interpret (a comparison, a
 *        semimodule multiplication, an aggregation, a value).
 *
 * Thrown by the defaults of the methods below.  In the measure
 * interpretation, which interprets them all, it means that the resolution
 * passes left a comparison of aggregate results unresolved: a shape ProvSQL
 * does not support, which @c probability_evaluate reports as such.
 */
class SemiringGateException : public SemiringException
{
public:
/** @brief Construct with a descriptive error message. */
SemiringGateException(const std::string &m) : SemiringException(m) {
}
};
 
/**
 * @brief Abstract base class for (m-)semirings.
 *
 * @tparam V  The carrier type (e.g. @c bool, @c unsigned, @c std::string).
 *
 * ### Required operations
 * All pure-virtual methods must be implemented by concrete subclasses.
 *
 * ### Optional operations
 * @c cmp(), @c semimod(), @c agg(), and @c value() have default
 * implementations that throw @c SemiringException.  Override them in
 * subclasses that support these circuit gate types.
 *
 * ### Absorptive semirings
 * A semiring is *absorptive* (i.e.,
 * @f$\mathbb{1} \oplus a = \mathbb{1}@f$ for all @f$a@f$) iff
 * @c absorptive() returns @c true.  Absorptivity implies idempotency
 * (@f$a \oplus a = a@f$), which lets the circuit evaluator and the
 * HAVING-semantics machinery deduplicate operands and short-circuit
 * over the multiplicative identity.  An absorptive semiring gets its
 * existential @c MIN / @c MAX HAVING comparisons (@c MIN below,
 * @c MAX above a constant) in a single scan instead of a world
 * enumeration; when its @f$\otimes@f$ also distributes over
 * @f$\ominus@f$ (@c mul_sub_left_distributive()), so do the other
 * @c MIN / @c MAX comparisons.
 */
template<typename V>
class Semiring
{
public:
/** @brief The carrier type of this semiring. */
typedef V value_type;
 
/**
 * @brief Return the additive identity @f$\mathbb{0}@f$.
 * @return The zero element of the semiring.
 */
virtual value_type zero() const = 0;
 
/**
 * @brief Return the multiplicative identity @f$\mathbb{1}@f$.
 * @return The one element of the semiring.
 */
virtual value_type one() const = 0;
 
/**
 * @brief Apply the additive operation to a list of values.
 *
 * @param v  Ordered list of operands (empty list should return @c zero()).
 * @return   @f$v_0 \oplus v_1 \oplus \cdots@f$.
 */
virtual value_type plus(const std::vector<value_type> &v) const = 0;
 
/**
 * @brief Apply the multiplicative operation to a list of values.
 *
 * @param v  Ordered list of operands (empty list should return @c one()).
 * @return   @f$v_0 \otimes v_1 \otimes \cdots@f$.
 */
virtual value_type times(const std::vector<value_type> &v) const = 0;
 
/**
 * @brief Apply the monus (m-semiring difference) operation.
 *
 * @param x  Minuend.
 * @param y  Subtrahend.
 * @return   @f$x \ominus y@f$.
 */
virtual value_type monus(value_type x, value_type y) const = 0;
 
/**
 * @brief Apply the @f$\delta@f$ operator.
 *
 * @param x  Input value.
 * @return   @f$\delta(x)@f$.
 */
virtual value_type delta(value_type x) const = 0;
 
/**
 * @brief Evaluate a comparison gate.
 *
 * @param s1  Left operand.
 * @param op  Comparison operator.
 * @param s2  Right operand.
 * @return    Result of the comparison in this semiring.
 * @throws SemiringException if not overridden.
 */
virtual value_type cmp(value_type s1, ComparisonOperator op, value_type s2) const {
  throw SemiringGateException("This semiring does not support cmp gates.");
}
 
/**
 * @brief Apply a semimodule scalar multiplication.
 *
 * @param x  Provenance value.
 * @param s  Scalar value.
 * @return   @f$x * s@f$ in the semimodule.
 * @throws SemiringException if not overridden.
 */
virtual value_type semimod(value_type x, value_type s) const {
  throw SemiringGateException("This semiring does not support semimod gates.");
}
 
/**
 * @brief Evaluate an aggregation gate.
 *
 * @param op  The aggregation function (COUNT, SUM, MIN…).
 * @param s   List of child semiring values to aggregate.
 * @return    The aggregated value.
 * @throws SemiringException if not overridden.
 */
virtual value_type agg(AggregationOperator op, const std::vector<value_type> &s) {
  throw SemiringGateException("This semiring does not support agg gates.");
}
 
/**
 * @brief Interpret a literal string as a semiring value.
 *
 * Used for @c gate_value gates whose payload is a string.
 *
 * @param s  Literal string.
 * @return   The corresponding semiring value.
 * @throws SemiringException if not overridden.
 */
virtual value_type value(const std::string &s) const {
  throw SemiringGateException("This semiring does not support value gates.");
}
 
/**
 * @brief Value of a variable leaf (@c gate_input / @c gate_mulinput)
 *        that the provenance mapping does not name.
 *
 * The absent-mapping convention: such a leaf contributes no provenance,
 * i.e. the multiplicative identity, which is what every proper semiring
 * wants and what this default returns.  A semiring that *renders* the
 * circuit rather than evaluating it overrides this to identify the leaf
 * instead -- @f$\mathbb{1}@f$ would not merely be anonymous there, it
 * would be absorbed by the enclosing @c times and take the structure
 * with it.  @c BooleanCircuit::toString does the same for the
 * Boolean-expression rendering (its @c x@<id@> fallback).
 *
 * @param uuid  The leaf gate's UUID, in canonical text form.
 */
virtual value_type unmapped_input(const std::string &uuid) const {
  return one();
}
 
/**
 * @brief Evaluate a continuous random-variable leaf (@c gate_rv).
 *
 * @param spec    The gate's distribution encoding (@c "normal:2.5,0.5"),
 *                where a parameter written @c "$i" is wired rather than
 *                literal (a latent / compound leaf).
 * @param params  The values of the gate's wires, indexed as the @c "$i"
 *                references; empty for an all-literal leaf.
 * @return        The leaf's value in this semiring.
 * @throws SemiringException if not overridden.
 */
virtual value_type rv(const std::string &spec,
                      const std::vector<value_type> &params) const {
  throw SemiringException(
          "This semiring does not support rv gates: a continuous "
          "distribution is not a semiring value.  Query a "
          "random-variable token through the measure surface "
          "(expected / variance / quantile / support / sample), or use "
          "the formula pseudo-semiring for a symbolic rendering.");
}
 
/**
 * @brief Evaluate an arithmetic gate over scalar children (@c gate_arith).
 *
 * @param op        The arithmetic operation.
 * @param children  The values of the gate's wires (for @c PERCENTILE,
 *                  interleaved @c [indicator, value] pairs).
 * @param extra     The gate's payload (the fraction for @c PERCENTILE,
 *                  empty otherwise).
 * @return          The result of the operation in this semiring.
 * @throws SemiringException if not overridden.
 */
virtual value_type arith(ArithmeticOperator op,
                         const std::vector<value_type> &children,
                         const std::string &extra) const {
  throw SemiringException(
          "This semiring does not support arith gates: arithmetic over "
          "scalar (random-variable) children is not a semiring "
          "operation.  Query such a token through the measure surface "
          "(expected / variance / quantile / support / sample), or use "
          "the formula pseudo-semiring for a symbolic rendering.");
}
 
/**
 * @brief Evaluate a Bernoulli mixture (@c gate_mixture, three wires).
 *
 * @param p  The Bernoulli event's value.
 * @param x  The value taken when the event holds.
 * @param y  The value taken otherwise.
 * @throws SemiringException if not overridden.
 */
virtual value_type mixture(value_type p, value_type x, value_type y) const {
  throw SemiringException(
          "This semiring does not support mixture gates: a probabilistic "
          "mixture is not a semiring operation.  Query such a token "
          "through the measure surface (expected / variance / quantile / "
          "support / sample), or use the formula pseudo-semiring for a "
          "symbolic rendering.");
}
 
/**
 * @brief Evaluate a categorical mixture (@c gate_mixture over
 *        @c gate_mulinput outcomes).
 *
 * @param key       The value of the mixture's key (its @c gate_input wire).
 * @param probs     Probability of each outcome.
 * @param outcomes  Textual payload of each outcome, parallel to @p probs.
 * @throws SemiringException if not overridden.
 */
virtual value_type categorical(value_type key,
                               const std::vector<double> &probs,
                               const std::vector<std::string> &outcomes) const {
  throw SemiringException(
          "This semiring does not support categorical mixture gates: a "
          "distribution over outcomes is not a semiring value.  Query "
          "such a token through the measure surface (expected / "
          "variance / quantile / support / sample), or use the formula "
          "pseudo-semiring for a symbolic rendering.");
}
 
/**
 * @brief Evaluate a guarded selection (@c gate_case).
 *
 * @param children  The gate's wires, @c [guard_1, value_1, …,
 *                  guard_k, value_k, default] (odd length), with
 *                  first-match semantics.
 * @throws SemiringException if not overridden.
 */
virtual value_type guarded_case(const std::vector<value_type> &children) const {
  throw SemiringException(
          "The requested semiring does not support a CASE / guarded "
          "selection over random variables (gate_case): it is evaluable "
          "only through the random-variable / measure surface "
          "(expected / variance / support / probability / sample).");
}
 
/**
 * @brief Evaluate a latent-variable observation (@c gate_observe).
 *
 * @param child  The observed leaf's value.
 * @param datum  The observed value, as text.
 * @throws SemiringException if not overridden.
 */
virtual value_type observe(value_type child, const std::string &datum) const {
  throw SemiringException(
          "This semiring does not support observe gates: the density "
          "factor of a likelihood-weighting observation is not a "
          "semiring value.  Such a token is evaluated by the "
          "importance-sampling surface, or rendered symbolically by the "
          "formula pseudo-semiring.");
}
 
/**
 * @brief Evaluate a conditioning marker (@c gate_conditioned).
 *
 * @param children  The gate's wires: @c [target, evidence] for the
 *                  value-level (random-variable) form, @c [target,
 *                  evidence, joint] for the Boolean-event one, where
 *                  @c joint is the materialised @c times(target, evidence).
 * @throws SemiringException if not overridden.
 */
virtual value_type conditioned(const std::vector<value_type> &children) const {
  throw SemiringException(
          "The requested semiring does not support conditioning: "
          "P(·|C) = P(·∧C)/P(C) needs a normalising division "
          "no general semiring provides.  A conditioned token is "
          "evaluable only in the measure interpretation "
          "(probability_evaluate, or the random-variable / agg_token "
          "distribution evaluators).");
}
 
virtual ~Semiring() = default;
 
/**
 * @brief Return @c true if this semiring is absorptive
 *        (@f$\mathbb{1} \oplus a = \mathbb{1}@f$ for all @f$a@f$).
 *
 * When @c true, the circuit evaluator and HAVING-semantics machinery
 * may exploit the resulting idempotency (@f$a \oplus a = a@f$, implied
 * by absorptivity) to deduplicate children of @c plus gates and to
 * short-circuit over the multiplicative identity.
 *
 * @return @c false by default; override to return @c true.
 */
virtual bool absorptive() const {
  return false;
}
 
/**
 * @brief Return @c true if this semiring is idempotent
 *        (@f$a \oplus a = a@f$ for all @f$a@f$).
 *
 * Absorptivity implies idempotence, so the default forwards to
 * @c absorptive(); override to return @c true in a semiring that is
 * idempotent without being absorptive (why- and which-provenance,
 * where @f$\oplus@f$ is set union).
 *
 * The HAVING machinery (@c provsql_having in @c having_semantics.hpp)
 * uses it for the *monotone* comparisons, those whose valid worlds are
 * closed under supersets (@c MIN below, @c MAX above a constant,
 * @c COUNT above a constant, @c SUM above a constant over non-negative
 * values, @c bool_or @c = @c true, @c bool_and @c = @c false): over
 * such a family the monus factors cancel from the possible-world sum,
 * which is then the plain @f$\oplus@f$-sum of the products of the
 * present annotations (Lean @c Having.witness_identity in
 * provenance-lean/Provenance/Having.lean, which assumes idempotence
 * only).  The enumeration stays exhaustive; absorptivity is what
 * further collapses it to the minimal worlds.
 *
 * @return @c absorptive() by default; override to return @c true only
 *         with a proof (the Lean @c *.idempotent lemmas).
 */
virtual bool idempotent() const {
  return absorptive();
}
 
/**
 * @brief Return @c true if @f$\otimes@f$ distributes over the monus
 *        on the left: @f$a \otimes (b \ominus c) = (a \otimes b) \ominus
 *        (a \otimes c)@f$ for all @f$a, b, c@f$.
 *
 * Together with absorptivity, this is the hypothesis under which the
 * HAVING machinery (@c provsql_having in @c having_semantics.hpp) may
 * replace the possible-world enumeration of a non-existential @c MIN /
 * @c MAX comparison (@c MIN above, @c MAX below a constant, or either
 * equal to one) by its single-scan closed form (Lean
 * @c Having.minScan_correct / @c Having.maxScan_correct in
 * provenance-lean/Provenance/HavingMinMax.lean); the existential
 * comparisons need absorptivity alone (Lean @c Having.sum_ann_meet in
 * provenance-lean/Provenance/Having.lean).  Holds in the Boolean,
 * counting, tropical, Viterbi, Łukasiewicz and interval-union
 * semirings; fails in the security (min-max) semiring, which is
 * absorptive but not distributive, and in Why / Which / How.
 *
 * @return @c false by default; override to return @c true only with a
 *         proof (the Lean @c *.mul_sub_left_distributive lemmas).
 */
virtual bool mul_sub_left_distributive() const {
  return false;
}
 
/**
 * @brief Return @c true if a semiring homomorphism @c BoolFunc(X)
 *        →+* @c S exists, so the safe-query (Boolean-rewrite)
 *        optimisation produces circuits that are semantically faithful
 *        when evaluated under this semiring.
 *
 * The compiled-semiring dispatcher consults this predicate before
 * evaluating a circuit whose root gate carries
 * @c PROVSQL_ROOT_TAG_BOOLEAN_REWRITE.  Returning @c false on a tagged
 * circuit raises @c CircuitException.
 *
 * Defaults to @c false: a new semiring whose author has not yet
 * verified the homomorphism is fail-closed by construction.
 * Subclasses with a verified homomorphism (currently @c Boolean,
 * @c BoolExpr, @c Formula, and @c IntervalUnion) override to return
 * @c true.  The justification (Lean-proof reference) belongs in a
 * comment next to each override; see the @c src/semiring/ headers.
 */
virtual bool compatibleWithBooleanRewrite() const {
  return false;
}
 
/**
 * @brief Whether this semiring builds *certified* exclusive
 *        enumerations (see the three hooks below).
 *
 * The HAVING possible-worlds machinery (@c provsql_having) enumerates,
 * for a comparison over a group aggregate, the complete valuations of
 * the group's contributors that satisfy the predicate.  Those
 * disjuncts partition the worlds -- the OR is *deterministic* and each
 * world term an AND of literals over distinct contributors,
 * *decomposable* -- i.e., the enumeration is a d-DNNF by construction.
 * A circuit-building semiring can persist that knowledge as the d-DNNF
 * certificate (the same mark the bounded-treewidth reachability route
 * emits), letting the linear certificate-aware evaluators handle the
 * result; scalar semirings have nothing to mark.
 *
 * @return @c false by default (the hooks below then go unused and the
 *         default constructions are used).
 */
virtual bool certifying() const {
  return false;
}
 
/**
 * @brief Whether @p 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.
 *
 * Only consulted when @c certifying() is @c true.
 *
 * @return @c false by default.
 */
virtual bool independent_literal(const value_type &) const {
  return false;
}
 
/**
 * @brief Build one complete world term: the conjunction of the
 *        @p present literals and the *negations* of the @p missing
 *        literals, certified decomposable.
 *
 * Only called when @c certifying() is @c true; the default throws.
 */
virtual value_type certified_world_term(
  const std::vector<value_type> &,
  const std::vector<value_type> &) const {
  throw SemiringException("This semiring does not certify enumerations.");
}
 
/**
 * @brief Build the disjunction of pairwise-exclusive @p disjuncts,
 *        certified deterministic.
 *
 * Only called when @c certifying() is @c true; the default throws.
 */
virtual value_type certified_exclusive_plus(
  const std::vector<value_type> &) const {
  throw SemiringException("This semiring does not certify enumerations.");
}
};
 
 
}
 
#endif /* SEMIRING_H */