# Is it possible to recover the set of derivation trees of a fact from its semiring provenance in Datalog?

Background: In the context of Datalog, Green et. al (2007) introduce the notion of the Datalog provenance semiring, a generalization of why-provenance as well as bag and probabilistic database semantics in which each EDB tuple is tagged with a symbolic value and combined via the operations of a commutative semiring. They call this form of provenance "how-provenance" because it shows how each EDB contributes to a derived fact.

Sometimes, though, the "how-provenance" of a derived fact is defined as its set of derivation trees, for example by Deutch et. al (2015).

When the number of derivation trees is finite, the semiring provenance of a derived fact is the sum over all its derivation trees of the product of the tags of the leaves of the tree.

Question: Is it possible to go in the other direction—that is, to recover the set of derivation trees from the semiring provenance? And does the answer change if there are a finite or infinite number of derivation trees?

To do so, I think you would need to modify the Datalog program so that each relation is tagged with an EDB that represents an identifier for that rule. But even then, the commutativity of the provenance semiring seems to make it difficult to reconstruct proof trees because you lose the order of derivations and leaves.

• What is the precise input, just an element of the semiring? With the derived fact? With the entire program? If you give yourself too much input you'll be able to just compute the derivation trees. Dec 2, 2023 at 8:59
• Ah, that's a really good point, thanks @AndrejBauer! The one I had in mind was just an element of the semiring (symmetric to the case where we can compute the semiring provenance from only the set of derivation trees), but I'm interested in any case where the semiring provenance could help compute the set of derivation trees more efficiently than simply throwing the provenance away and computing the derivation trees from scratch. Dec 2, 2023 at 17:29
• @JustinLubin: when the set of derivation trees is infinite, how is it represented as input? Also, even when it is finite, I'm not sure how to formally specify the problem. Probably you could just ignore the input and naively recompute all the derivation trees. Is your question whether, for a Datalog query Q, the complexity of the problem "Given a database D and the how-provenance of Q on D, compute all derivations trees of Q on D" could be higher than "Given a database D, compute all derivation trees of Q on D"? But the set of derivation trees would be large, so this can mess up the complexity
– a3nm
Dec 7, 2023 at 22:16
• @a3nm Ahh, the set of derivation trees being so large that it messes up the complexity is a really good point. I hadn't considered that, but that makes perfect sense. I think that means that what I'd be looking for is something along the lines of enumerating derivation trees given an enumeration of the semiring provenance (which would also handle the infinite case). But that's a fuzzy notion I don't know how to formalize :) I think my underlying question is whether the two definitions of how-provenance are, in some sense, "equivalent" to each other (which I know is also a fuzzy one). Thanks! Dec 15, 2023 at 23:05
• @JustinLubin: Yes, I think the problem should be better formalized: how is the semiring provenance enumerated? Also, does the question depend on the semiring?
– a3nm
Dec 17, 2023 at 4:21