Re: [PRD] New version of RIF-PRD on the wiki

This is not an exhaustive review of PRD, but a list of comments on things
that I managed to spot.


	--michael  


1. The overall impression is that this document is ... a bit raw and
   disconnected.

   There are numerous references to "informal" semantics, but no actual
   semantics.
   There is also a section, 1/2 page long, titled "Operational Semantics",
   but it contains neither semantics nor is it operational :-)

2. There is reference to Naf as if this is not controvercial in PR.

   First, most PR systems, including ILOG (AFAIK), Jess, Drools, and
   whatnot, DO NOT USE NAF.  What they use is called "inflational negation"
   - a thingie investigated by Kolaitis and Co.
      
    @inproceedings{kolaitis-pods-88,
    author = "P.G. Kolaitis and C.H. Papadimitriou",
    title = "Why not Negation by Fixpoint",
    booktitle = PODS,
    publisher = "ACM",
    address = "New York",
    pages = {231--239},
    year = 1988
    }

   There were also later works.

   In most PR systems, if you assume that something is false and keep deriving
   things, you may later derive the very thing that you earlier assumed to
   be false. So, the derivations based on that assumption are unfounded,
   but the PR systems will happily plow ahead.

   However, there are smarter PR systems. For instance, the Haley engine will
   reconsider its earlier decision and will undo unfounded derivations.
   This is not based on any model theory, but it feels "smarter". It is
   also sound with respect to the well-founded semantics (if no delete
   actions in the head).

   What I am driving at is that the inclusion of the inflationary negation
   into the core PR dialect is a bad idea, as it precludes other
   (&semantically better) engines to join.

   You might say that Kolaitis & Papadimitriou will not do things that make
   no sense, but one point of their paper was to find conditions
   when inflationary negation does not run into the problems that many
   production engines run into.

3. The doc introduces ExtTerms, but keeps Uniterms "for compatibility".
   Not clear why  a new kind of terms is needed and what "compatibility"
   here means.

4. Universal quantification.
   You mean in the rule body, right? I wonder what that means in PR.
   You cannot get away with "informal semantics" here.

   If you mean that the rules themselves are universally quantified, then
   this has no meaning for PR, AFAIK.

   The following statement, apart from being self-contradictory, seems to
   indicate that you mean the latter option, which has no meaning.

       The QUANTIFICATION class is used to represent any quantified formula
       that is allowed in rules covered by RIF-PRD. In rule languages
       covered by RIF-PRD, only existential quantification, represented by
       the Exists construct, is allowed in the condition language. RIF-PRD
       allows universal quantification, represented by the Forall
       construct, only at the rule level [ Rule section].

   Then, in the Rules section, you say:

       The Forall construct is used to represent universally quantified
       conditional statements and rules.

   That is, forall can occur in conditions. This requires serious explaining.

5. Aggregation.

   It is understandable that you want to rush something useful into the
   specification, but it is better to fix numerous problems with the core
   language of PRD first. 

   When it comes to aggregation, we might want to use the same concepts for
   the logic rules and for PRD. One important issue in aggregation, 
   is grouping-by, and this needs to be carefully defined.
   Your "informal semantics" for that is really badly explained. It does
   raise even to the level of an informal description, but in this matter
   "informal" is not even good enough.

6. Const ::= LITERAL '^^' TYPE [ '@' LANGUAGE_ID ]
   diverges from BLD.

7. You do not need to say anything about signatures, since BLD does not
   have them. If you work out a framework for PR dialects, like FLD, then
   you might want to talk about signatures there, but probably not, and I
   doubt that they will appear explicitly in any concrete dialect.

8. The section on actions is very tentative, so I will not comment much,
   but it seems that the action of updating is ill-defined.

9. In the compatibility section, you say:

       Based on Fitting's paper on fixpoint semantics of rule language, it
       should be easy that the result set of RIF-Core rules has the same
       semantics as the original set of RIF-PRD rules;

   This is true, but has nothing to do with Fitting's paper. You probably
   meant Kowalski & van Emden.

Received on Saturday, 16 February 2008 07:46:23 UTC