Regular expressions for provenance

As noted by Green et al. several provenance analyses can be considered a special case of the general problem of computing formal polynomials resp. power-series as solutions of an algebraic system. Specific provenance is then obtained by means of evaluating the formal polynomial under a suitable homomorphism. Recently, we presented the idea of approximating the least solution of such algebraic systems by means of unfolding the system into a sequence of simpler algebraic systems. Similar ideas are at the heart of the semi-naive evaluation algorithm for datalog. We apply these results to provenance problems: Semi-naive evaluation can be seen as a particular implementation of fixed point iteration which can only be used to compute (finite) provenance polynomials. Other unfolding schemes, e.g. based on Newton's method, allow us to compute a regular expression which yields a finite representation of (possibly infinite) provenance power series in the case of commutative and idempotent semirings. For specific semirings (e.g. Why(X)) we can then, in a second step, transform these regular expressions resp. power series into polynomials which capture the provenance. Using techniques like subterm sharing both the regular expressions and the polynomials can be succinctly represented.