Re: [PRD] PRD Review By Example

Gary and all,

I just browsed through your comments, yet, so this is only a quick comment re the subject: trying the semantics with examples is a very good thing, indeed. But I suggest that you try the semantics in the July FPWD, or wait a couple more days for the current wiki version to be updated.

Just as a reminder: although there is no specific warning in the current draft on the wiki, the "rules and ruleset" section is not uptodate, as I said during the PRD telecon (but maybe not clearly enough).

It is mostly the version that was published in July, with a couple ad hoc changes, but not aligned with the remainder of the document anymore. E.g., as Gary notices, the notion of an instance of a rule is still used, but it is not defined anymore, etc.

My understanding was that that part (the semantics of rulesets, including conflict resolution) would be the main subject of our discussion in Orlando, and I planned to have it tidied by next Tuesday.

Gary, actually, I think that it would be interesting if you could try your example on the smenatics as it is described in the FPWD, since I do not plan to change anything re the content, only align the form to the editorial changes in the other parts of the document.

Cheers,

Christian

Gary Hallmark wrote:

> 
> 
> This is a case-oriented review of the current PRD spec on the wiki. It 
> attempts to use the spec to give meaning to
> the following simple ruleset, and identifies a number of issues 
> uncovered. Overall, I'm encouraged that the spec
> generally seems to "work" -- many of the issues are largely editorial 
> (save for the problems with PICK, which I address
> somewhat here and in detail in a seperate email.
> 
> Prefix(p someIRI)
> p:A(0)
> (* r1 *)Forall ?x (p:A(?x) :- p:A(External(func:numeric-minus(?x 1))))
> 
> 
> Issue 1: We must state that all "initial facts" in the ruleset RS (here, 
> p:A(0)) are removed from RS and become the initial working memory 
> w<sub>0</sub>
> 
> so, after this step, we have
> 
> w = {p:A(0)}
> RS = (* r1 *)Forall ?x (p:A(?x) :- p:A(External(func:numeric-minus(?x 1))))
> c = (w, {}, nil, nil) i.e. the initial configuration is the initial 
> facts and an empty set of rule instances.
> We have added a third component to the configuration: the rule instance 
> that is picked.
> 
> Now, we execute the first cycle of the transistion system.
> 
> s = {} because instances(c) is {}
> c' = (w, INSTANTIATE(w, RS), PICK(LIFO, c))
> 
> Issue 2: INSTANTIATE returns a set of Inst(R). This is undefined.
> I guess it is a pair (rule-id, consistent-substitution), and that 
> furthermore it must return *all* such pairs.
> 
> Issue 3: picked(c) from my new PICK specification should be changed to 
> mean the rule instance picked
> from the prior configuration to arrive at the current configuration. And 
> the transistion system that calls PICK must
> save the returned rule instance as picked(c').
> 
> So,
> 
> c' = (w, (r1, {?x->1}), nil)
> 
> Now, the second cycle
> 
> s = extractActions((r1, {?x->1})) because PICK is trivial - only 1 rule 
> instance exists
> 
> Issue 4: extractActions seems a bit underspecified as to how it 
> "grounds" the actions in the rules,
> which may have variables. Also, its argument should be a single rule 
> instance, not a list.
> I guess it is supposed to "plug in" the substitutions, so
> 
> s = {p:A(1)}
> 
> Now, the RIF-PRD transition system says
> 
> ({p:A(0)}, p:A(1), w') →RIF-PRD if and only if, for every ground formula 
> φ in W,
> w' |= φ if and only if And({p:A(0)} p:A(1)) |= φ
> 
> Issue 5: And(...) is undefined. We must define the PS before the 
> semantics if we use the PS in the semantics.
> Also, this And takes a set as its first argument. I'll replace the set 
> with its member:
> 
> ({p:A(0)}, p:A(1), w') →RIF-PRD if and only if, for every ground formula 
> φ in W,
> w' |= φ if and only if And(p:A(0) p:A(1)) |= φ
> 
> w' = {p:A(0) p:A(1)}
> 
> Note: w' is not uniquely determined. E.g. w' = {And(1=1 p:A(0) p:A(1))} 
> is ok, too. I guess this is fine.
> 
> c' = (w', INSTANTIATE(w', RS), (r1, {?x->1})) = ({p:A(0) p:A(1)}, {(r1, 
> {?x->1}), (r1, {?x->2})}, (r1, {?x->1}))
> 
> Now, the third cycle. Interesting because we need to pick one of the two 
> rule instances.
> 
> Issue 6: PICK is ill-defined.
> See my email proposal. According to the new specification, assuming the 
> rule is declared as repeatable, the agenda is:
> 
> {(0, 0, (r1, {?x->2}))}
> and thus its only rule instance is returned.
> 
> s = {p:A(2)}
> w' = {p:A(0) p:A(1) p:A(2)}
> c' = ({p:A(0) p:A(1) p:A(2)}, {(r1, {?x->1}), (r1, {?x->2}), (r1, 
> {?x->3})}, (r1, {?x->2}))
> 
> Note that if r1 is declared *not* repeatable, then the agenda would be 
> empty in the third cycle and the system terminates.
> 
> 
> 
>

Received on Friday, 17 October 2008 08:29:17 UTC