Re: [PRD] review of the frozen draft of Nov 25

Michael,

Responses to the rest of your (very useful) comments, below...

Michael Kifer wrote:
> 
>   12. Sec 2.1.2.3, definition of condition satisfaction.
>   13. Definition of matching substitution.

As I said, I will leave those to Adrian :-)

I have some questions about them, but that will be for another email.

>   14. Sec 2.2.1, Abstract syntax, last paragraph. This repeats the
>       sentence that already appears in Sec 2.1.1 (after the bullets).

Remnant for document organisations past... I removed it.

>   15. Sec 2.2.2, Operational semantics.
> 
>       Here the reader starts to run into notational problems. At least,
>       I did, especially trying to get through the definitions that use
>       symbols defined a page or two ago. For instance, L is used for
>       actions, W is used for ground condition formulas, T for terminal
>       states, etc. These sometimes occur with subscripts. At some point
>       it becomes hard to follow. I suggest that better mnemonic symbols
>       are used. For instance, gActions, FinalStates, gConds, etc.

Difficult to do at once. We will try to make the notation more palatable, but longer names for sets may make the notation heavier... 

I am thinking about re-organising the whole section to make it an easier reasing, too.

Probably not much we can do for WD2, though: is that ok?

>   16. Definition of the PRD transition relation (Sec 2.2.2).
>           * Here φ is a ground formula, right? Say this in the preamble
>             of the definition.

I repeated that alpha is a ground atomic action: is that sufficient, or do you think we should specifically repeated that phi is a ground atomic formula?

>           * In the assert and retract action bullets, why not simply say
>             that w' = w+φ and w' = w - φ, respectively? This is not only
>             simpler, but also correct. In contrast, the current
>             definitions are wrong because of the problem with |= in the
>             presence of negation, as mentioned previously.
>           * In item 3, why not simply write w' = w
>             -{f1,...,fn,m1,...,mn'}? (for the same reason)

It was indeed like that in an earlier version. I do not quite remember why we changed that, but I suspect that it might be because w' = w+phi looked to much like implementation for our comfort (at least for mine).

The point is that any condition that match phi must be satisfied after assert(phi), etc, and satisfaction and matching are defined in terms of entailment, so, defining the effect of the actions in terms of entailment seemed both safe and the right way to do.

But simpler is better, and if w' = w+phi defines the effect of asserting phi, in terms of what formula are satisfied, without making any assuption wrt how the action works, it is fine with me (unless I or somebody else remember why we did it the way it is).

I did not do the correction yet, waiting for your reply to the implicit question above...

>   17. Sec 2.3.1, last sentence: repeats the same sentence in Sec 2.1.1
>       for the third time.

Yes, indeed. Don't you like it? Oh, ok, I removed it :-)

>   18. Sec 2.3.1.1, Rules. Sentence after the bullets: replace "noted"
>       with "written as" and delete "logic programming" (just "RIF-BLD
>       notation" is good enough).

Done. The idea was to explain to the basic PRD implementer, why those BLD guys would use such a strange notation :-)

>   19. Last paragraph in Sec 2.3.1.1: "whenever they have the same XML
>       syntax."
> 
>       This is rather indirect and looks cryptic. I'd like to also add
>       that this happens when the only actions are asserts, and there is
>       no negation.

I rewrote the sentence.

Is it any better?

>   20. Sec 2.3.1.2, groups.
> 
>       Here the term "strategy" is used, but it was never defined, even
>       syntactically. I presume that here it must be a strategy
>       identifier. But what is its syntax? Is it a constant? a Unicode
>       string of chars? something else?

Ooops! Yes, the preamble seems to have been left out at some point, here. I added one.

>   21. Sec 2.3.1.3, def of well-formed rules: /...has a subclass atomic
>       as its target/.
> 
>       Cannot quite figure out what this is supposed to mean. An atomic
>       subclass formula? This is one of the cases where the use of
>       /atomic/ garbles the sentence. In other cases the use of this term
>       as a noun is just awkward.

Subclass atomic formula, indeed. Corrected.

>   22. Sec 2.3.2, 1st line: PRS. Make it bold italic so that people could
>       find its definition more easily.

I replaced PRS by 'production rule system' instead. And marked the definition of a RIF-PRD production rule system as a definition (I mean, with 'Definition' written in bold and all that).

>   23. /The idea of describing PRS as a labeled ... which execution
>       results ..."/
> 
>       Replace /which/ by /whose/.

Done. I thought that 'whose' was only for people.

>   24. Ex 3.1, 3d bullet.
> 
>       Not clear which Joe is meant: Joe the Hen or Joe the chicken.

Ooops! What happened to that example? There are 3 Joes in it now?!?

I removed one and I renamed another one. But I think that we wll get rid of that example anyway.

>   25. After the example: definition of rule instance.
> 
>       Mark it as a definition so that it would be easier to find.

Done.

>   26. In the rule instance definition: r^id .
> 
>       What is this thing that is uniquely identifying the rule? Is it
>       the rule itself? You never talked about these identifiers before.
>       Furthermore, why not define ground instances of the rules in the
>       usual way, i.e., as the result of substitution of ground terms for
>       variables?

I simplified that part and removed that unique identifier thing.

I have a more general question, however: supposing we could not have done without, who cares about what it is, anyway, if we only use its defining characteristic, which is to uniquely identify a specific rule?

>   27. Three paragraphs later: FORMULAE. This symbol has never been
>       defined. Why not just say "ground facts" here? The end of this
>       sentence is garbled: /... are fired, in some sense to be further
>       specified, in that state of facts/. Please rephrase.

FORMULAE, ATOMICS etc.. Remnants of versions past. Removed.

"firing" is commonly used for executing the action part of a rule instance. I rephrased the sentence: "all the instances of the rules in the considered ruleset ''RS'', whose action blocks are executed in that state of facts."

>   28. Two paragraphs down, the definition of history.
> 
>       It is confusing and unnecessary to write histories backwards.
>       There is no advantage in making them into stacks, and this
>       assumption does not seem to be used anywhere. So, it is just
>       another distraction for the reader in a place where it is already
>       hard to read.

No good reason, you are right. I changed that.

>   29. Definition of INSTANTIATE, end of sentence: / in a sense that is
>       determined by the specification of the function./
> 
>       Cannot understand what is meant here.

I rewrote it: "[...], where the detailled specification of ''INSTANTIATE'' will define what it means, precisely, for a rule instance, ri, to satisfy a set of facts, w."

>   30. Definition of PICK.
> 
>       What is "input strategy" (input to what?)? A conflict resolution
>       strategy?

The conflict resolution strategy passed as an input to the function. I rephrased it.

>       The last two lines in that definition are unclear. Please rephrase.

Done.

>   31. Paragraph after the FINAL bullet.
> 
>       The symbol ACTIONS has not been defined. Moreover, the definition
>       of extractActions is not clear to me.

Yes, it was underspecified in the version you reviewed. I hope the current specification is clearer: at least, it is more detailled :-)

>   32. Definition of PRS_RS,LS
> 
>       Please remind what T_RS,LS is. (Earlier I suggested to use better
>       mnemonics, which would have made such reminders less important.)

Done.

>       Same definition, bullet 3: (h,s h') - a missing comma.

Done.

>   33. Sec 2.3.2.1, INSTANTIATE.
> 
>       Here you are talking about rule instances as things obtained from
>       rules by substituting terms for variables. This is how I also
>       suggested to define rule instances before. However, your
>       definition is different, and so here you are using the term /rule
>       instance/ in a possibly different sense. This is confusing and
>       most likely is unnecessary.

Changed that, see comment 26.

 
>   34. Later in the same section: using the symbols ACTION and FORMULA,
>       which were not defined previously.

I rewrote with reference to the definition of rule.

>   35. Definition of instantiateRULE.
> 
>       Here you are using the construct rule(r^ri ). What is this?
>       Earlier you defined only rule(ri).

Typo. Corrected.

>   36. A few lines below: a state is a triple (w,rs,ri).
> 
>       Earlier you defined states to be pairs.
> 
>   37. A few lines below, right above Example 3.4.
> 
>       What are these "input" and "output" functions?

Oh, ok: that part must be very unclear, then! The semantics of the function INSTANTIATE was specified operationally as a transition system of its own: hence a different definition of state, transition relation, input and output functions etc...

But all the semantics of INSTANTIATE has been embedded in instantiateRULE, over time, so that INSTANTIATE can now be specified more simply without requiring the definition of a specific transition system. Which I did.

> At this point I
>       felt that it does not make sense to continue reading until all the
>       above issues are resolved.

I think that we should be done by tomorrow night.

Cheers,

Christian

Received on Thursday, 4 December 2008 16:52:09 UTC