Non-final lattice results visible to downstream rules about ascent HOT 6 OPEN

@s-arash
I suppose rejection is fine, as long as the user is informed that the situation can be fixed by adding an intermediate relation (like b2 in my example)

from ascent.

An even more simplified repro, with less variables and generalized names:

use ascent::ascent_run;

fn main() {
    let prog = ascent_run! {
        relation a(usize,i64) = vec![(0,2),(1,2),(1,3)];
        lattice b(usize,i64);
        b(id,x) <-- a(id,x);
        relation b2(usize,i64);
        b2(id,x) <-- b(id,x);
        relation c(usize,usize,i64);
        c(id,id1,x2) <-- b(id,x2), b(id1,x2), if id1 < id;
        relation c2(usize,usize,i64);
        c2(id,id1,x2) <-- b2(id,x2), b2(id1,x2), if id1 < id;
    };
    println!(
        "1: {:?}\n2: {:?}",
        prog.c,
        prog.c2,
    );
}

produces:

1: [(1, 0, 2)]
2: []

on ascent 0.5.0

from ascent.

A similar case is if the lattice and a normal relation are mutually recursive:

use ascent::ascent_run;

fn main() {
    let prog = ascent_run! {
        relation a(i64) = vec![(0,)];

        lattice b(i64);
        b(i) <-- a(i);
        
        relation c(i64);
        c(i+1) <-- b(i);

        b(i) <-- c(i), if *i < 10;
    };
    println!(
        "b: {:?}\nc: {:?}",
        prog.b,
        prog.c,
    );
}

This produces:

b: [(9,)]
c: [(1,), (2,), (3,), (4,), (5,), (6,), (7,), (8,), (9,), (10,)]

Which is also 'wrong', in the sense that the set of tuples after convergence contains facts (such as c(3)) that are not implied by any other fact in the set of tuples after convergence. (as b(2) once existed, but was eliminated by lattice join).

This is actually a paradox, similar to writing mutually recursive relations with negation:

a(x) <-- !b(x);
b(x) <-- a(x)

as above if b(n) is in the result, c(n+1) is, but then b(n+1) is, but then b(n) can't due to lattice invariants.

I believe any relation depending on a lattice must go to a higher stratum, and only access the lattice after it was fully computed.

from ascent.

You identified an issue with lattices in Datalog, which is for the computation to be well defined, the rules need to be monotonic. In your last example, the following rule is not monotonic: c(i+1) <-- b(i);

Statically determining if rules are monotonic is very hard, and given the open nature of Ascent (you could invoke arbitrary Rust code in your rules) I'd say impossible in Ascent. The following papers discuss this issue in some depth:

https://cs.au.dk/~magnusm/papers/pldi16/paper.pdf
https://kmicinski.com/assets/byods.pdf

I believe any relation depending on a lattice must go to a higher stratum, and only access the lattice after it was fully computed.

Unfortunately, this doesn't guarantee monotonicity, as even rules involving a single lattice could be non-monotonic. What's more, this restriction precludes some sensible programs where relations and lattices are mutually-recursively defined. That is, one may be willing to pay the price of underdetermined semantics with non-monotonic rules and still get the benefits of lattices.

I'll leave this issue open for discussion for a bit longer, but I don't think there are any satisfactory solutions here that apply to Ascent.

from ascent.

@s-arash Thanks for the answer.
For the mutually recursive case (last example), I understand your explanation, that there may be programs that are sensible despite involving mutually recursive lattices, and we don't want to reject those, making it the users responsibility to provide only monotonic rules.

But are my first two examples non-monotonic too? Those don't involve any recursion or feeding back anything to the lattice...
I think those are well-defined (with the proper result being obstruct and c being empty relations), and demonstrate a bug, where the relations downstream are accessing non-final lattice elements.

from ascent.

@B-Lorentz Ah I see. I just looked at your second example. It indeed looks like a bug. The problem is that this rule requires an index on the lattice column: c(id,id1,x2) <-- b(id,x2), b(id1,x2), if id1 < id;, and the index collects intermediate results from the lattice.

One simple solution may be to reject programs that require indexes on lattice columns altogether. There are more complex solutions of course. But I'm not sure if they are worth the effort.

from ascent.