Non-final lattice results visible to downstream rules

[B-Lorentz]

In the following program, the relation stop2 is a copy of stop.
And then obstruct is derived from stop the same way as obstruct2 is from stop2.
Therefore one would expect that the two relations have the same output, but instead the following happens:

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

But stop(1,2) is not part of the final result, (even though it is implied by roll(1,6), block(2), because it undergoes lattice merge with stop(1,4) implied by roll(1,6), block(4).

Yet it appears stop(1,2) is still used in deriving obstruct, even though its value isn't final yet.

use ascent::ascent_run;

fn main() {
    let prog = ascent_run! {
        relation block(i64) = vec![(2,),(4,)];
        relation roll(usize,i64) = vec![(0,3),(1,6)];
        lattice stop(usize,i64);
        stop(id,x) <--roll(id,x_start), block(x), if x < x_start;
        relation stop2(usize,i64);
        stop2(id,x) <-- stop(id,x);
        relation obstruct(usize,usize,i64);
        obstruct(id,id1,x2) <-- stop(id,x2), stop(id1,x2), if id1 < id;
        relation obstruct2(usize,usize,i64);
        obstruct2(id,id1,x2) <-- stop2(id,x2), stop2(id1,x2), if id1 < id;
    };
    println!(
        "1: {:?}\n2: {:?}",
        prog.obstruct,
        prog.obstruct2,
    );
}

[B-Lorentz]

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

[B-Lorentz]

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.

[s-arash]

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.

[B-Lorentz]

@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.

[s-arash]

@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.

[B-Lorentz]

@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)