[PRD] PICK specification (round 3)

All,

Here is (what I think is) the result of the (kind of) PRD F2F we had in Orlando wrt the conflict resolution strategies we want to cover normatively in PRD 1.0.

Basically, we agreed on having only one normatively required behaviour, corresponding to option 1a in my previous summary (PICK specification, round 2 [1]), which was a refinement on Gary's initial proposal [2].

[1] http://lists.w3.org/Archives/Public/public-rif-wg/2008Oct/0127.html
[2] http://lists.w3.org/Archives/Public/public-rif-wg/2008Oct/0074.html

More precisely, the previous summary is amended as follows:

> The essential idea, as Gary puts it, is that an instance of a rule does not
> fire more than once in its lifetime, where the lifetime of an instance is the
> longest span of contiguous states where it is an instance.
> 
> Trying to capture that more precisely, now...
> 
> Lots of helper functions, first:
> 
> picked(c) returns the rule instance that was picked when in configuration c.
> 
> prior: C_RS x |N -> C_RS, where C_RS is the set of configurations and |N is the set
> of integers, is a helper function that, given a configuration, c, and a number of
> cycles, i, returns the i-th configuration prior to c in the systems history:
> prior(c, 0) returns c;
> prior(c', 1) returns c, where c' is the next configuration after c, as given by the
> overall PRD transition system, or c' if c' is the initial configuration;
> prior(c, age) = prior(prior(c, age - 1), 1).
> 
> Notice that, if i is greater than the number of cycle since the initial
> configuration, prior(c, i) always returns the initial configuration.
> So, let cycle: C_RS -> |N, be a helper function that return the numer of cycles
> between the input configuration and the initial configuration, that is:
> cycle(c) = min(i | forall j >= i, prior(c, j) = prior(c, i))
> 
> Let us now define an integer function age(c, ri, test), [...]

Definition of age changed to:
<<Let us now define an integer function age(c, ri), where c is a configuration and ri is a rule instance in instances(c):
age(c, ri) = min(cycle(c), max(i |forall j, 0=< j =< i, exists ri' in instances(priori(c, j)), such that sameInstances(ri, ri') is true)).

age(c, ri) tells us "how old" is a rule instance ri in a configuration c, based on how long it has been in c's predecessors, according to the sameInstances test, where, given two rule instances ri and ri', sameInstances(ri, ri') is defined as follows:
- sameInstance(ri, ri') is true iff rule(ri) = rule(ri') and, forall variables ?x_i in Var(rule(ri)), subst_ri(?x_i) = subst_ri'(?x_i), where subst_ri, resp. subst_ri' is the substitution associated with ri, resp. ri'.>>

(definition of "sameInstance" did not change).

> lastPicked(ri, c) is an integer that returns the number of cycle between c and the
>   last configuration when ri was last picked, where the test to checked if ri was
>   picked is [...]

...sameInstance:
- lastPicked(ri, c) = min(i | forall configurations c'=prior(c, i) such that sameInstance(picked(c'), ri) is true), if there is a configuration c'=prior(c,i), 0<=i<=cycle(c) that satisfies the condition;
- lastPicked(ri, c) = cycle(c)+1 is there is none.

(Definition of "lastPicked" changed to remove possibility to change the comparison test for rule instances).

> [...]

Definition of "sameRule" deleted.

> priority(r) returns a number, where r is a rule. Higher numbers mean higher priority.
> [...]

Definition of "repeatable" deleted.

> Given all that help, PICK(order, c) is defined as follows. First, we construct the
> agenda relation A(priority, age, ri) where ri is a rule instance and the other 2
> arguments are numbers.  The tuple (priority, age, ri) is in A iff both the following
> are true:
> 1. [...]

Condition that rule is repeatable deleted.

>    age(c, ri, sameInstance) < lastPicked(ri, c, sameInstance)
>    [...]

Case (b) where rule is not repeatable deleted.

> 2. priority = priority(rule(ri)).
> Second, we order A by (priority, age).  We order by decreasing priority, then by increasing or decreasing age, depending on whether PICK's order argument is LIFO or FIFO, respectively.  Ties are broken arbitrarily.
> Finally, we return the ri from the first tuple in A according to the ordering.
> 
> Condition 1 [...] says exactly that an instance cannot be fired twice in its life
> time, that is, that there has to be at least one configuration where it is not an
> instance, according to the sameInstance test, after it is fired, before it is
> fireable again: that corresponds to refraction.

"Condition 1.a" replaced by: "Condition 1".
 
> [...]
>
> Question 1: is the strategy with simple refraction+priority+recency prevalent
> enough that we include it in PRD (simple refraction=refraction with rule-level
> repeatability=1.a)?

We answer yes to that question. And we answer no to questions 2 (about rule-level non-repeatability) and question 3 (about object/property-level repeatability).

Cheers,

Christian

Received on Friday, 31 October 2008 00:26:42 UTC