avalog
avalog copied to clipboard
Add support for time dimensions
A time dimension is a special optimization knowledge in the accelerator that increases monotonically. This knowledge can be referred to, but not accessed by value at the language level.
Time dimensions are used in rules to control combinatorics.
For example:
(A, B)[t] :- (B, A)[t++].
Only patterns of (B, A) added after fact index t is matched against. When (B, A) is matched against, the fact index is used to update the time dimension t.
One can think about time as a resource, which is consumed step by step.
Time dimensions introduces unsoundness, because when shared, it introduces concurrency.
The motivation for time dimensions is to be able to "collect" stuff from facts and put them into lists.
For example:
// Collect all agents.
(collect, agents(X))[j=0] :- (X, agent)[i=0].
(collect, agents(X, Y))[j] :- (collect, agents(..X))[j++], (Y, agent)[i++].
Without the time dimensions, any possible list will be constructed, which is not what I want.
I believe it is possible to infer termination of rules based on time dimensions.
This assigns a termination state to a pattern, given by the left-side expression.
When this state is true, no further facts will be generated of this form.
Later, this might be used to create closed-world assumptions.