[PRD] PRD Review By Example

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 Thursday, 16 October 2008 18:42:47 UTC