Why.h File Reference

Why-provenance semiring (set of witness sets). More...

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

Include dependency graph for Why.h:

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

Go to the source code of this file.

Classes
class	semiring::Why
	Why-provenance semiring. More...

Namespaces
namespace	semiring

Typedefs
using	semiring::label_t = std::string
	A single label identifying a base tuple.
using	semiring::label_set = std::set<label_t>
	A witness: a set of labels that collectively justify one derivation.
using	semiring::why_provenance_t = std::set<label_set>
	Why-provenance value: the full set of all witnesses.

Detailed Description

Why-provenance semiring (set of witness sets).

The why-provenance semiring represents provenance as a set of witness sets. Each witness set is a set of base-tuple labels that together "witness" one derivation of the query result. The full provenance is the collection of all such witness sets.

Formally, the carrier type is \(\mathcal{P}(\mathcal{P}(\text{Labels}))\), implemented as why_provenance_t = std::set<std::set<std::string>>.

Operations:

• zero() → ∅ (no derivations)
• one() → {∅} (one derivation requiring no witnesses)
• plus() → union of input sets
• times() → pairwise concatenation (Cartesian product of witnesses)
• monus() → remove elements of \(y\) from \(x\)
• delta() → identity (returns \(x\) unchanged if non-empty)

This 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\}} \cup \{\{x\}\} = \{\emptyset, \{x\}\} \neq \{\emptyset\}\).

See also

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

Definition in file Why.h.