Which.h File Reference

Which-provenance (lineage) m-semiring. More...

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

Include dependency graph for Which.h:

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

Go to the source code of this file.

Classes
class	semiring::Which
	Which-provenance (lineage) semiring. More...

Namespaces
namespace	semiring

Typedefs
using	semiring::which_provenance_t = std::optional<std::set<std::string> >
	Which-provenance value: a set of labels, or \(\bot\) (empty optional).

Detailed Description

Which-provenance (lineage) m-semiring.

The which-provenance semiring (also known as lineage) records, for each derivation of a result tuple, the set of base-tuple labels that contributed to it. Unlike why-provenance, only one such set is tracked per gate: the union of all witnesses across all derivations.

Formally, the carrier set is \(\mathcal{P}(\text{Labels}) \uplus \{\bot\}\), where \(\bot\) (the additive identity) represents "no derivation". Implemented as which_provenance_t = std::optional<std::set<std::string>> (an empty optional is \(\bot\)).

Operations:

• zero() → \(\bot\) (no derivations)
• one() → \(\emptyset\) (a derivation requiring no witnesses)
• plus() → union of witness sets; \(\bot\) acts as identity
• times() → union of witness sets; \(\bot\) is absorbing
• monus() → set difference, \(\bot\) when \(x \subseteq y\)
• delta() → identity ( \(\bot \mapsto \bot\), \(x \mapsto x\))

The semiring is idempotent (set union is idempotent: \(a \oplus a = a\)) but not absorptive in the \(\mathbb{1} \oplus a = \mathbb{1}\) sense used by absorptive(): \(\emptyset \oplus \{x\} = \{x\} \neq \emptyset\). Times also does not left-distribute over monus as long as the label universe is non-empty.

See also

https://provsql.org/lean-docs/Provenance/Semirings/Which.html Lean 4 verified instance: instSemiringWithMonusWhich, with proofs of Which.idempotent, Which.not_absorptive, and Which.not_mul_sub_left_distributive.

Definition in file Which.h.