Lattice support

[vlad-arista]

Our use case (complex event processing/event calculus) would benefit from lattice support because in many cases we only need the minimal/maximal interval for which certain conditions hold (for instance when we compute the complete interval for the complex event) and generating the intermediate facts are not needed (and take up memory). Would you be open to us contributing a design and implementation for it?

[burakemir]

Absolutely! I need lattice support for my use cases, too (just yesterday in fact) and was planning to start work on it. The capability fits very well in the Mangle philosophy of creating a reference spec and implementation of well-known datalog extensions.

About the terminology, FWIW, I know the specific capability of retaining only a minimum/maximum under the name "subsumption" or "subsumptive rule" in the context of datalog literature. Lattice support could more generally mean computing fixpoints in other lattices (as demonstrated in Datafun). "subsumption" is not a great name either since it is used with different means, just calling it out since we will need to figure out how we call this in the documentation.

Looking forward to your proposal!

[burakemir]

Thinking about lattice support and "subsumption" some more. Sharing my notes here, in case they are helpful:

• custom lattice support applies to intensional predicates only.

• the "usual" lattice is the powerset(R) lattice where R is the relation (set of tuples / facts) that is expressed by predicate rules.

• we want to define a join-semilattice, that is a poset with joins. A simple but not most general way to do this is to stick to powerset(R) but instead of plain inclusion as the partial order, we also relate subsets A <: B when B contains elements that "covers" elements from A.

• with custom lattice, the idea is that join lets us remove elements that are "covered" by others, which is more economical in terms of space, should save evaluation cycles, while remainining fully declarative.

• specifying the partial order could happen in a variety of ways: for a particular argument, or for whole tuples. One could even imagine calling an external function, or applying a mapping (lattice homomorphism) to a lattice S and doing the comparison/joining in S.

• some ways of defining partial order may introduce potential for mistakes (things that are supposed to be partial order relations but aren't).

• for maximum, minimum, there is currently a way to get maxima/minima of a column: using |> fn:group_by() we can specify a process that takes a preliminary result relation and aggregates. Currently, the implementation computes the entire result relation and reduces it afterwards. Custom lattice support can yield alternative implementation strategy for aggregation queries, too.

[burakemir]

The paper "Bring your own datastructures to datalog" is very nicely written https://dl.acm.org/doi/pdf/10.1145/3622840 It describes the flix approach (I'm very open to any proposal here, sharing just in case it helps:)

• you can have a relation R(X1 ,..., Xn, V) and when it is defined as (map) lattice, then by convention a relation is a map m: (domain(X1),...,domain(Xn)) --> domain(V)
• when a new tuple is inserted, a join is performed in domain(V). so if m1 is the relation before insertion and m2 the relation after insertion (m1 v m2)(x1,...xn) = m1(x1,...,xn) v m2(x1,...,xn) so to figure out the join you only look up if there is something for the x tuple... and you retain the result.
• the join is an lattice-theoretic operation, defined in terms of a partial order, and that order needs to be user-definable. It must be monotonic (which cannot be checked), and then everything will work, e.g. shortest paths etc.

We could support this by making a smart FactStore, that can internally represent maps and can call the user-defined order operations. It would be good if at initialization time there was a check that the expected capability is supported by the FactStore.

[kamahen]

There's been quite a bit of work in the Prolog world on "tabling" (a kind of memo-ization), including lattices. The original work was done by David S Warren at SUNY, on XSB Prolog; and this has been incorporated into SWI-Prolog. I think that Picat also has this, and other Prolog implementations (e.g., Ciao Prolog).

[burakemir]

Yes, this is very related. Many behaviors can be exposed by configuring storage, and it seems this is what was chosen for PROLOG, see "mode-directed tabling" https://www.swi-prolog.org/pldoc/man?section=tabling-mode-directed

I think a noteworthy difference is that in Mangle, we'd like to consider support for non-powerset lattices as something that concerns the engine, not the storage. In Mangle, everything around fact storage is happening through the FactStore interface, and implementations of that interface need not know about engine matters. They could be applying joins for non-powerset lattices behind the scenes today! But this request is about a user-configurable way that is part of the Mangle program.

There is a minimal piece of functionality that a fact store implementation must provide to collaborate with engine, and that is fact removal. I'll make some changes to support it.

[burakemir]

I have an implementation of this now which I plan to get reviewed and submit. Then you can take a look and see if it works for your use case, or whether you'd prefer a different approach.