Review of PRD of 25 Nov 2008

This is my review of the PRD document the 2008-12-25 PRD document snapshot.

General

The present version is a significant improvement on an earlier version, which I read. The new document is much more rigorous and better organized. I have several substantive comments, which are elaborated upon later, and a few editorial comments.

Substantive comments

• There are problems with the semantics of conditional formulas.
• I got bogged down in Section 2.3.2. It is very hard to read due to the poor choice of notation and the fact that definitions of some of the concepts are missing or are poorly explained.

Editorial comments

• The nesting level of sections is 4 - too deep compared to BLD, which has only a few level-3 sections. I suggest to get rid of "Abstract Syntax & Semantics" and make "Conditions", "Actions", and "Production Rules" into top level sections 2, 3, and 4, respectively.
• It would be very helpful to put the square sign ☐, character #9744, at the end of every definition and example.
• When referring to other RIF documents, put appropriate references in the bibliography and use the [...] style of reference. E.g., [RIF-BLD]. This would be consistent with BLD and other documents. Right now HTML links are used instead, which might not be correct when the documents are finally published outside of the wiki system.
• There are also broken references such as [ref. Plotkin], which should be [PLO04].
• References should be split into normative and other, like in BLD.
• In a number of places the following style is used: In the section Operational semantics .... This style should be avoided, as it is stylistically awkward and often results in broken sentences (as above). A better style is: In Section Operational .... Note that the word section is capitalized. The same holds true for references to examples. For instance, In Example 1.1, ... rather than in the example 1.1 or in example 1.1.

Specific Comments

1. Sec 1, above Ex 1.1: Actions can modify the facts, not only the knowledgebase

   Usually facts are considered part of the knowledge base, so this remark can be confusing to some readers.

2. Same page: 2. Conflict resolution.

   Would be appropriate to briefly explain this notion here.

3. Right above Example 1.2: Here both numeric and named section references are used. Since our wiki system does not support automatic maintenance of section numbers when references are made, I suggest that numeric references are not used.
4. Sentence right after Ex 1.2: RIF-PRD and RIF-BLD ... in both dialects.

   This is an awkward and unclear sentence. Please use something like this instead:

   The condition sublanguages of RIF-PRD and RIF-BLD have much in common. However, the presentation syntaxes for the rules are different, largely due to the different traditions in production rules and logic programing communities. Nevertheless, XML serializations of these syntaxes, again, have much in common, so many XML documents are valid in both dialects and have the same meaning.
5. Sec 2.1.1, Abstract syntax: parenthesis is missing at the end of the 2nd bullet.
6. 2nd sentence after the bullets: That notation is not ... XML syntax.

   Please replace with: This notation is not intended to be a concrete syntax, and so it leaves out many details. The only concrete syntax for RIF-PRD is its XML syntax.

7. Next paragraph, last sentence: This is one of two points ... languages also use.

   An unclear sentences. Please rephrase.

8. Sec 2.1.1.2 Atomics: The terms atomics and atomic are awkward when used as nouns. This often leads to awkward, ungrammatical, or unclear sentences. Worse yet, it seems to me that atomics and atomic formulas are the same, so you introduce two terms for one notion.
9. Section 2.1.1.4, well-formed formulas.

   This section was copied from BLD at the time when it had a problem. The context of individuals was not defined at the time, and there was an inconsistency in the definition of the context for the nullary symbols of the form f(). This has now been fixed in BLD, so please transfer the changes from there.

10. Section 2.1.2.1, Semantic structures.

    For production rules you need to use Herbrand domains. Otherwise, the definition of the models would be broken (as it is right now). PRD uses inflationary semantics for negation, and using general domains is problematic in this context.

    Since BLD's semantics maps everything into the domain (including predicate formulas), the domain for PRD's semantic structures should consist of all terms, all atomic formulas, plus all the domains for the data types.

11. Definition of truth valuation, the equality bullet. In the line that defines I_truth replace "if and only if" with "if" (because of the "otherwise" clause that follows).
12. Sec 2.1.2.3, definition of condition satisfaction.

    This definition is incorrect, if you have PRD negation. If Ψ has negation, for instance, And(p not q) then this definition is not strong enough to ensure that, say, p |= And(p not q).

    What production systems do is different from logical entailment. You are constructing semantic Herbrand structures instead. You start with the Herbrand semantic structure that satisfies all the facts and nothing else, find a rule whose premises are all true in that structure, and then you fire the head of the rule. This creates a new structure, and so on. In fact, I do not think that you need the motion of logical entailment in the first place. You do need the notion of condition satisfaction, but it should be satisfaction in particular Herbrand structures, not the notion that you are defining. (The current document defines entailment of conditions by ground facts, not the notion of satisfaction in semantic structures.)

13. Definition of matching substitution.

    This definition seems broken, and is an overkill in any case. Why not simply define it as σ(Ψ) ⊆ Φ?

14. Sec 2.2.1, Abstract syntax, last paragraph. This repeats the sentence that already appears in Sec 2.1.1 (after the bullets).
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.

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.
    • 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)
17. Sec 2.3.1, last sentence: repeats the same sentence in Sec 2.1.1 for the third time.
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).
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.

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?

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.

22. Sec 2.3.2, 1st line: PRS. Make it bold italic so that people could find its definition more easily.
23. The idea of describing PRS as a labeled ... which execution results ..."

    Replace which by whose.

24. Ex 3.1, 3d bullet.

    Not clear which Joe is meant: Joe the Hen or Joe the chicken.

25. After the example: definition of rule instance.

    Mark it as a definition so that it would be easier to find.

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?

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.
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.

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.

30. Definition of PICK.

    What is "input strategy" (input to what?)? A conflict resolution strategy?

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

31. Paragraph after the FINAL bullet.

    The symbol ACTIONS has not been defined. Moreover, the definition of extractActions is not clear to me.

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.)

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

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.

34. Later in the same section: using the symbols ACTION and FORMULA, which were not defined previously.
35. Definition of instantiateRULE.

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

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? At this point I felt that it does not make sense to continue reading until all the above issues are resolved.