Comments (6)
@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.
Related Issues (20)
- Private type `…` in public interface (error E0446) HOT 3
- Compiling ascent at runtime HOT 2
- New release with parallel Ascent HOT 2
- ascent_macro: Upgrade syn to >= v2 HOT 1
- MISP computation HOT 8
- ascent_macro: Fix minimal versions (by upgrading syn to v1.0.109, itertools to v0.12) HOT 5
- Ascent should omit trait bounds on the generated program's type declaration HOT 5
- Project's current formatting makes it hard to contribute non-trivial changes HOT 4
- Lattice constrains not enforced on input in ascent_run HOT 2
- Incorrect result? HOT 2
- Calling run() multiple times HOT 6
- Please add a license HOT 1
- Macro limitations HOT 1
- WASM compatibility: `std::time` HOT 3
- Unsoundness in `util::update` HOT 1
- Arash's current email address? HOT 1
- Composition Feature
- ascent = "0.2" broke? HOT 4
- Comparison to Crepe? HOT 4
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from ascent.