avalog icon indicating copy to clipboard operation
avalog copied to clipboard

Add support for time dimensions

Open bvssvni opened this issue 5 years ago • 2 comments

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.

bvssvni avatar Oct 29 '20 01:10 bvssvni

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.

bvssvni avatar Oct 29 '20 01:10 bvssvni

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.

bvssvni avatar Oct 29 '20 02:10 bvssvni