How.h File Reference

How-provenance m-semiring (canonical polynomial provenance ℕ[X]). More...

#include <cstring>
#include <map>
#include <sstream>
#include <string>
#include <vector>
#include "Semiring.h"

Include dependency graph for How.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
class	semiring::How
	How-provenance m-semiring over \(\mathbb{N}[X]\). More...

Namespaces
namespace	semiring

Typedefs
using	semiring::how_label_t = std::string
	A single label identifying a base tuple.
using	semiring::how_monomial_t = std::map<how_label_t, unsigned>
	A monomial: each variable mapped to its (positive) exponent.
using	semiring::how_provenance_t = std::map<how_monomial_t, unsigned>
	How-provenance value: each monomial mapped to its (positive) coefficient.

Detailed Description

How-provenance m-semiring (canonical polynomial provenance ℕ[X]).

The how-provenance semiring is the universal commutative semiring for provenance [Green, Karvounarakis, Tannen, Provenance Semirings, PODS'07]: every commutative-semiring provenance value can be obtained from the how-provenance polynomial by the unique homomorphism that substitutes each input label with its semiring image.

The carrier is the multivariate polynomial semiring \(\mathbb{N}[X]\) over the set \(X\) of base-tuple labels: each value is a multiset of multisets of labels, equivalently a sum of monomials with non-negative integer coefficients. We store it in canonical sum-of-products form as std::map<std::map<std::string,unsigned>,unsigned>: the outer map sends a monomial (variable→exponent) to its coefficient, and ordered containers give canonical equality on semantically-equal polynomials, which is the value-add over sr_formula.

Operations:

• zero() → \(0\) (empty polynomial)
• one() → \(1\) (the constant 1, monomial of degree 0)
• plus() → polynomial addition (coefficient-wise sum)
• times() → polynomial multiplication (Cauchy product)
• monus() → coefficient-wise truncated subtraction (per the Lean coeff_sub theorem)
• delta() → \(0\) if \(x = 0\), else \(1\) (support indicator, mirroring Counting::delta)

This semiring is not idempotent and not absorptive (absorptive() returns false), so the evaluator does not deduplicate plus operands. It also does not satisfy left-distributivity of multiplication over monus, contradicting an earlier claim in the literature; see Lean How.not_idempotent, How.not_absorptive, and How.not_mul_sub_left_distributive.

See also

https://provsql.org/lean-docs/Provenance/Semirings/How.html Lean 4 verified instance: the MvPolynomial X ℕ SemiringWithMonus instance, with proofs of How.universal, How.not_idempotent, How.not_absorptive, and How.not_mul_sub_left_distributive.

Definition in file How.h.