RE: [PRD] Action 659 (on hak) completed

> Hassan,
> 
> </chair><PRD editor>
> 
> Thanx for the valuable comments. Overall, I agree with them. We (PRD
> editors) had to make a couple decisions re what we could reasonably do
> about them before WD2, though.

Christian,

I understand that much and your efforts editing/writing and publishing
this document are most commendable. Reviewing it, I forced myself to read
it with an average "Java object-educated" Joe's working knowledge of a
production rule language who would hear about RIF-PRD and be curious to
get acquainted with it. With that sort of readership in mind, such a
document must ring some bells and not drown the reader in unmotivated
formalities that are hard to follow, let alone prove. The test of
publication is a severe one - one would hence be well-advised to ensure
that it be of use and meet some success.

> Below, our reply to your comment, per item (including the simple edits,
> but it makes easier to check that we replied to everything).

Below are some comments on (and interspersed among) some of yours.

> [...]
> 
> > 1. [...] Why can't we use (La)TeX in our Wiki documents?  (Sandro?) [...]
> 
> Would it help to use LaTeX for the draft, if the final document has to
> be HTML?

These systems generate HTML as well - the LaTeX formulas and glyphs appear
as bitmap pics in the text. Anyway, the comment is a general one to ease
(IMHO) reading of W3C technical documents that use math.

> > 2. Examples are too few and far between. The formal presentation should
> >    illustrate each newly defined formal concept on a simple example.
> 
> Right. Unfortunately, it is unlikely that we will have enough time to
> make that significantly better in the short time left bfore WD2: we will
> leave that at the bottom of the list, hoping that it will not be a
> showstopper.

I do not know the sort of "show" you have in mind, nor what you mean by
"stopping" it. All I am saying is that one can publish anything one wants
as long as one understands that the results might not necessarily be those
one expected. The expectation in publishing RIF-PRD, as I understand it,
it to explain and motivate a specific format of interchange among PR systems
to practitioners of PR systems. If that is the "show", then your may want to
have a wider audience than the few that will understand the current version.
I myself honestly do not, and so am not among those happy few.

> > 3. The section on Actions needs to be elaborated with motivating comments
> >    and explanations regard the oddities of some PRD constructs. Its formal
> >    contents has yet to be simplified in my view, but I would not make that
> >    a condition precluding publication.
> 
> Right. We tried to improve that (see detailled comments).
> 
> > 4. Perhaps a list of exemplars of actual production rule systems presumed
> >    to use the RIF-PRD should be given up front at the outset. In this way,
> >    the reader familiar with one of those will be able latch on the basic
> >    concepts being discussed and formalized. I strongly suggest giving
> >    small simple examples in some of these actual systems to illustrate a
> >    concept before giving its formal definition.
> 
> I agree, personnaly. This has been a recurring discussion and is
> unlikely to be solved before PRD WD2 is released (or so I hope. I mean,
> I hope that we will not have to wait that long for PRD WD2 :-)

I am talking about simple editing: adding prose - a few paragraphs -
overviewing common features of several systems (not that many - say 3 to
5 representative actual systems), and then an informal overview of the
RIF-PRD architecture abstracting those common features away. As it
stands, the document presents a format for an architecture it does not
even attempt to describe informally before definit it formally. The
reader simply has no precise idea what is talked about and is drowned in
formalities of little intutive relations to his/her familiar notions
(object, working memory, object pattern matching, etc., ...)

> > 2.1.1.1 Terms
> >
> > 2.1.1.2 Atomics
> >
> >   - The English word "atomic" is an adjective, not a noun. Why not
> >     simply call these constructs "atoms" as they commonly are in Formal
> >     Logic?  Namely, the enumeration defining this notion should read:
> 
> We used "atomic formula" everywhere in the document, instead, following
> Michael's suggestion.
> 
> "Atomic formula" rather than "atom", because that saves us one
> definition (that is, that atoms are also atomic formulas" :-)

Since an atom is indeed defined as an atomic formula, using simply
"atom" is better - one substantive instead of a nominal locution. In
addition, it is the common term in Formal Logic for that sort of
objects.

> > 2.1.2.3 Satisfaction of a condition
> >
> >   - Quoting: "Definition (Logical entailment). Let \phi\ and \psi\ be
> >     formulas. We say that \phi\ entails \psi, written as \phi\ |= \psi\,
> >     if and only if for every semantic structure, I, for which both
> >     TVal_I(\phi) and TVal_I(\psi) are defined, I |= \phi\ implies I |=
> >     \psi."
> >
> >     This defines a notion (viz., "entails") using another one
> >     (viz. "implies") - but what does "implies" mean? I propose to
> >     rephrase this to, "I |= \psi\ HOLDS WHENEVER I |= \phi\ does."
> >
> >     Same remark for the paragraph following the above quote.
> 
> Makes sense to me.
> 
> However, Adrian rewrote that section, based on Michael's comment, and
> the part that this comment addresses disappeared.
> 
> Adrian's rewriting has to be reviewed, btw (easy to say, when I did not
> even read it myself yet :-)

Where is this rewriting? Can you point out to the exact section, its
length, in what document's version?

> >     Again, this definition is overly complicated and confusing. I would
> >     rephrase it much more simply and as formally (and as correctly) as:
> >
> >        Definition (Matching Substitution). Let \psi\ be a condition
> >        formula, and \phi\ be a set of ground formulas that satisfies
> >        \psi. We say that \psi\ matches \phi\ with substitution \sigma :
> >        Var -> Terms if an only if there is a syntactic interpretation I
> >        such that for all ?xi in Var(\sigma), I(?xi) = I(\sigma(?xi)).
> >
> >     Such a substitution is necessarily ground because all the \phi_i's are
> >     ground. A syntactic interpretation is one where the semantic domain
> >     for D_ind is the set of ground terms.
> 
> It seems that that section still needs to be updated by Adrian, so, we
> will leave that one open for now.

When/where will the new version be ready?

> >     Note that I left out the the subscripts for I; i.e., I wrote "I(?xi) =
> >     I(\sigma(?xi))" instead of I_V(?xi) = I_C(\sigma(?xi))". This is
> >     because they should be clear from the context, and also that I do not
> >     agree that it shound be "I_C" (and with this document's definition of
> >     ground terms) because for me (contrary to the RIF-PRD document's
> >     editors), a ground substitution may map variables to ground terms, not
> >     just constants.
> 
> See above.
> 
> >     In the last paragraph starting with "In other words, ...", a reference
> >     is missing. Also, I do not understand "in the usual sense of pattern
> >     matching algorithms, e.g. [REFERENCE]" - there is no such "usual
> >     sense" - which is why we need to make our definitions clear and simple.
> 
> Hmmm. This sentence was meant to make what precedes less frightening,
> that is, to tell the lay PR-oriented reader that everything that was
> defined before was only what he was used to, in different words.

Oh yeah? Like, "Trust in me! This obscure stuff really makes all what
you know much clearer..."?  Remember my quote of Goethe's opinion of
mathematicians and Frenchmen? ;-)

> We realize that such a warning should rather come before the frightening
> part than after: we will repair that mistake before WD2 publication if
> times permit, hoping that it is not a showstopper...

Again, depends on what your "show" is...

> Re the missing reference: would you have one to suggest?

Since I have no idea the sort of "usual" pattern matching algorithm you
have in mind, I can suggest none. There are many not so usual notions of
pattern matching: off the top of my head, I can think of at least four
distinct such classes of PM - as in (1) FOT-Rewriting system's PM
(one-way FOT unification), (2) RETE-style object PM, (3) F-logic style
object PM, (4) OSF object OM. Of these, (2) has never been formalized
nor formally related to Logic (and surely not to BLD). IMHO, the whole
issue of PRD's PM is that it *IS* highly unusual and *must* be precisely
defined, not hand-waved away.

> > 2.2 Actions
> >
> > 2.2.1 Abstract Syntax
> >
> >   - Section title should be "Abstract syntax" (no capital "S").
> 
> Corrected.
> 
> >   - Quoting: "For a production rule language to be able to interchange
> >     [...]"
> >
> >     At this point the reader has no clue of what an assertion/retraction
> >     or an addition/removal is (of what into/from what?), nor what the
> >     difference is between the two, nor what justifies that they act on the
> >     listed sorts of items and not others.
> 
> Here, again, the fact that the current version of PRD sits on frames,
> which are only a (probably inadequate) approximation when used to
> represent objects, does not help.
> 
> We will add an editors' note to explain (i) that this is only a first
> basic set of actions, and (ii) why they are different from what would be
> expected as the basic set in a directly object-oriented
> representation. We are currently drafting that editors' note and we will
> include it later today or tomorrow (hopefully, before the RIF telecon).

Can you point out to the rewritten section(s).

> >     I strongly recommend that the whole section on Actions start with a
> >     description of what global structure PR actions act upon (i.e.,
> >     working memory, agenda, object base, ...) and what sort of items
> >     populates such structures. It should be a synopsis describing the
> >     abstract architecture common to most PR systems.
> 
> Good point. Shouldn't tht rather be in the overview, though?

Wherever - but it should be there.

> We will work on both (an introduction in the Oversiew section, and a
> preamble refering to that intro in the Actions section).
> 
> > 2.2.1.1 Atomic actions
> >
> >   - Quoting: "Definition (Atomic action). An atomic action can have
> >     several different forms and is defined as follows:
> >
> >     1. Assert: If \phi\ is a positional atom, an atom with named
> >        arguments, a frame, a membership atomic, or a subclass atomic in
> >        the RIF-PRD condition language, then Assert(\phi) is an atomic
> >        action. \phi\ is called the target of the action.
> >     2. Retract: If \phi\ is a positional atom, an atom with named arguments,
> >        or a frame in the RIF-PRD condition language, then Retract(\phi) is
> >        an atomic action. \phi\ is called the target of the action. 
> >     3. Retract object: If t is a term in the RIF-PRD condition language,
> >        then Retract(t) is an atomic action. t is called the target of the
> >        action."
> >
> >     Again: asserting/retracting into/from what? No notion of working
> >     memory, object or knowledge base has been defined at this stage.
> >
> >     Use examples to introduce new notions *before* their giving formal
> >     defintions. A good systematic editorial strategy to follow is first to
> >     give an informal example, then define the notion formally, then
> >     related the just-given formal definition to the example given before
> >     it.
> 
> I fully agree, of course. I have been told that this was not a tutorial,
> but I still fully agree with you :-)

You were told by whom? I beg to differ - it *IS* a tutorial - big time!
You are explaining stuff to people. You are teaching them something they
need to understand. You want to define all notions that you use and not
make your reader go guess for him/herself what you have implicitly in
your mind.

> We will add examples asap. And informal introductions as well, where
> useful.

Good. When?

> >     BTW, I would not "retract" an object, but "remove" it.
> 
> A more complete set of the actions that should be covered by PRD, and
> how they should be labeled, is an open issue (issue-62).
> 
> We (the PRD TF) prefered not to address that issue for WD2, though.

I am not speaking of any technical issue. I am simply speaking about
plain English here.

> > 2.2.1.2 Action variable bindings
> >
> >   - This section will be puzzling to many readers in its current form.
> >     [...] It is just a form of
> >     the familiar (let ((?x1 t1) ... (?xn tn)) body) and New(_) is
> >     (gensym).
> 
> That section has been partly rewritten. Hopefully, the new version makes
> the intent more obvious. And examples will be added asap; but,
> hopefully, the rewriting makes the intent clear enough that the lack of
> example is not a showstopper.

Again, point to (or quote) the new text. It is hard enough reviewing
moving targets, it would help if you could show how the new version
addresses the raised concern(s).

> > 2.2.1.3 Action blocks
> >
> >   - Quoting: "[...]"
> >
> >     Question: Why are actions ai's constrained to be *atomic* only?  Why
> >     disallow nesting of actions that might share common contexts of
> >     variables and bindings?
> 
> The definition has been rewritten, but the question remains
> valid. Allowing only atomic actions is a simplification, but the
> possibility to nest actions/action blocks should definitely considered.
> 
> Do you want us to raise an issue to keep track of the question?

Whatever. (It is a feature of the latest JRules engine, BTW.)

> >   - The definition of a "well-formed action block" is baffling, pulled out
> >     of a hat, and unmotivated. The reader ponders, "why?" and "where's an
> >     example?". Show some ill-formed blocks and explain informally why they
> >     should be declared ill-formed.
> 
> Has been rewritten.

To what?

> >   - Quoting: "Definition (Ground atomic action). An atomic action with
> >     target t is a ground atomic action (or, simply, a ground action) if
> >     and only if Var(t) ? bv, where bv is the set of variables declared in
> >     an enclosing action block, if any."
> >
> >     Is the ending "if any" needed? A binding may not occur outside a
> >     block, right?
> 
> Has been rewritten.

To what?

> > 2.2.1.4 RIFBLD compatibility
> >
> >   - I think this "compatibility" is misleading since the PRD rule:
> >
> >        IF \psi\ THEN DO(ASSERT(\phi_1),...,ASSERT(\phi_n))
> >
> >     could then be written:
> >
> >        IF \psi\ THEN AND(\phi_1,...,\phi_n)
> >
> >     which has a different reading in logic. The former asserts new facts
> >     conditionally on the truth of a guard, while the latter tests whether
> >     a set of facts hold conjointly conditionally on the truth of a guard.
> 
> Good point. That section has been moved to the definition of Rule, and
> we have to consider whether the BLD-like notation should be allowed
> anywhere (with the problem you raise) or only for rules that are
> equivalent under a PRD and a BLD semantics; and whether it should be
> mandatory or optional. Do you want us to raise an issue?

I would like an explanation, indeed. This looks dangerous - nay, insane.

> > 2.2.1.5 Wellformed actions
> >
> >   - Section title should be "Well-formed actions".
> >
> >   - Again: missing motivating examples illustrating why ill-formed actions
> >     pose problems.
> 
> The section has been rewrittent. Hopefully, again, the rewriting makes
> the intent clear enough that the lack of examples is not a showstopper
> for WD2 publication.

Again point out the changed parts - I have littel time to go and reread
entire chunks to find what has been changed.

> >   - The definition of the "RIF-PRD transition relation" is giving me
> >     headaches every time I try to understand it - even with the informal
> >     comments following it. Why is this correct as a definition? Could we
> >     have any justification that it does cover the type of PR systems in
> >     the RIF family?
> 
> Doesn't it quite obviously, with the restriction that this version has
> essentially only two actions, and that frame are not exactly object.

No it it *NOT* obvious - not to me. Why, I can't even read it - nay -
*PARSE* it - before the pain in my head becomes too unbearable!

> >   - Quoting: "... 1. for every constant k in W, w |/= c_i#k and ...".
> >
> >     What does this "c_i#k" denote?
> 
> This part has been rewritten. Do not the "informal" explanation of the
> three rules, below, clarify the meaning and intent, at least a little?

None whatsoever. What is the new formulation?

> >   - This definition is way too complex and impossible to comprehend - at
> >     least by this reader. It is so because it is not abstract enough.
> >     Basically, the formalism used is describing a particular - nay,
> >     peculiar - operational semantics aiming at rigor without motivating
> >     that rigor (Is it used in proofs? What sort of proofs? What sort of
> >     formal reasoning does this enable? Have you proven these rules to be
> >     confluent (Church-Rosser)? Terminating? What are the formal properties
> >     of the arrow you are defining (i.e., your labeled-transition relation)?
> >     In other words, what does all this formalism allow us to do that we
> >     couldn't do before - or not as easily? These are the questions the
> >     editors ought to ask themselves because they are indeed those that the
> >     readers of their document will ask themselves.
> 
> I am not quite sure which definition your are talking about, because
> that has been rather unstable lately. The current one (which is
> essentially, I think, the first three bullets of the one you did
> review), seems rather straightforward to me.

I am referring to the section starting with, "In the remainder of this
section, as in the section on the operational semantics of actions,
...".  (It comes right after your whimsical chicken example in Section
2.3.2 Operational semantics of rules and rule sets.

If this is your idea of straightforward, I then do not considen myself
competent. Can anyone else in this WF take a look and explain it to me?
(Do not worry - as CSMA wrote it, it is straightforward - to him!)

> Of course, it can certainly be improved and simplified.

X^(

> Re whether it needs to be based on entailment or whether, e.g. w' = w
> +/- phi is enough for, e.g., assert/retract, is something I need to
> understand better (I did not yet really go into Michael's answer to my
> question). We will use the simple version for WD2 (edits still to be
> done).

Isn't just this fact "a showstopper"?

> Re "what does all this formalism allow us to do that we couldn't do
> before - or not as easily?"  The objective is to specify the semantics
> of PRD completely and unambiguously (and in a way that is powerful
> enough to be extended to future dialects if required) and to specify it
> in a such a way that it can be compared as easily as possible to that of
> Core and, more generally, to the BLD/FLD branc hof RIF. I am not aware
> of another proposal that allowed us to do it before (as easily or not).

Then, obviously, your stated objective has not been reached by the
current document - not by a long shot.

> Re whether or not we need the formalism: yes, the idea is to be able to
> prove things, and, essentially, that PRD extends Core. If it allows to
> prove more, the better, but formally establishing the relationships with
> the logical side of RIF is the raison d'être of the formalisation (that
> says nothing wrt the correctness of the proposed formalization; just
> motivates it).

Before I buy a tool, I generally make sure that it will do the job I
intend it for by trying it. Can you please prove anything intereseting
to me with your paraphernalia?

Plotkin-style semantics is a wonderful tool, but one can to know how to
use it. When giving such a semantics, each rule is given separately in a
crisp declarative manner such that a system may be built incrementally
by adding more rules capturing more functionality so that it may be
easier to prove commutation and termination. Giving a Plotkin-style
semantics as a massive procedure calling on sub-procedures does not
allow one to do that. It makes it as difficult as the raw system it
purports to model, with the added burden of having to establish that it
is correct as a computation model of PRs.

> Re confluence etc: some properties need be proven, indeed (as part of
> proving that the operational semantics is correct). Is it a showstopper
> for the publication of WD2?

Again, what sort of "show" do have in mind? Regarding my own criteria,
yes - I am afraid it is a "showstopper". I, as a rule, will not publish
things I know to be incorrect, incomplete, or useless. But this is your
"show".

> >     Formalizing should *clarify* complex things, not *complexify* simple
> >     things. It should not be an exercise for the sake of making things
> >     look mathematical; it's only worth is if it gives one confidence that
> >     it captures simply and precisely what one can understand intuitively.
> >     In other words, it should follow the precept of the well-known maxim:
> >
> >                   Ce que l'on conçoit bien s'énonce clairement
> >                   Et les mots pour le dire arrivent aisément.
> >                   -- Nicolas Boileau
> >
> >     Lest some readers may relate to the following quip:
> >
> >                     Mathematicians are like Frenchmen: whatever you say
> >                     to them they translate into their own language and
> >                     forthwith it is something entirely different.
> >                   -- Johann Wolfgang von Goethe
> >
> >     One can only imagine, then, how a French mathematician might have
> >     sounded to Goethe! ;-)
> 
> Very true, indeed. So are also:
> 
> "L'enfer est pavé de bonnes intentions."
> "On ne fait pas d'omelette sans casser d'oeufs."
> "Qui ne tente rien n'a rien."
> "La critique est aisée, mais l'art est difficile."
> Etc, etc.

All agreed and understood. Mind you, I did not volunteer my "critique"
but was drafted for it (by you if I recall). Regarding how difficult the
"art" may be - again, I agree. But one may also ponder:

« À l'impossible, nul n'est tenu. »
« Errare humanum est ... Perseverare diabolicum! »
« À Bon entendeur, salut. »

Etc., etc., ...

> >   - Quoting: "A rule If condition, Then action can be equivalently noted
> >     action :- condition, that is, using RIF-BLD logic programming
> >     notation. Indeed, the normative XML syntax is the same for a
> >     conditional assertion in RIF-BLD and for a conditional action in
> >     RIF-PRD. The use of RIF-BLD notation is especially useful if the
> >     condition formula, condition, contains no negation, and if action is
> >     an atomic conclusion or a conclusion block, to emphasize that such a
> >     rule has the same semantics in RIF-PRD and RIF-BLD."
> >
> >     Does it? Have you proved it? Can you prove it? (See my comment above
> >     in Section 2.2.1.4 on RIFBLD compatibility.)
> 
> It does not completely, and it has to be proven yet: by the way, if you
> want to try...
>
> :-)

Are you kidding me? I am telling you that your apparatus is precisely
unfit (for me - and for many I bet) to do such things, and you are
asking me to prove something using it? I must be dreaming. Besides,
the onus is on you, is it not? You are offering a formal system. What
formal things can you do with it? (Beside presenting it?)

BTW, I already told you that it is not true and why! Re-quoting myself:
  - I think this "compatibility" is misleading since the PRD rule:

       IF \psi\ THEN DO(ASSERT(\phi_1),...,ASSERT(\phi_n))

    could then be written:

       IF \psi\ THEN AND(\phi_1,...,\phi_n)

    which has a different reading in logic. The former asserts new facts
    conditionally on the truth of a guard, while the latter tests whether
    a set of facts hold conjointly conditionally on the truth of a guard.

> We added an editor's note to the effect that this was, at this stage, an
> unproven approximation, and that this aspect would be more completely
> addressed in a future version.

Quite a challenge as things stand IMHO. Good luck.

> >     Does your (Plotkin-style) formal operational semantics allow you to
> >     make such a strong statement formally? Is the semantics of 'do/assert'
> >     consistent with that of 'and'? Hard for me to see such a fact from
> >     what I have read.
> 
> Yes, it does, basically. But the devil is in the details and I did not
> check the details yet...

The details are all that matter. All else in hand-waving approximation.

> >     Quoting: "Notice that the notation for a rule with bound variables
> >     uses the keyword Forall for the same reasons, that is, to emphasize
> >     the overlap with RIF-BLD. Indeed, although Forall does not indicate
> >     the universal quantification of the declared variables, in RIF-PRD,
> >     but merely that the execution of the rule must be considered for all
> >     their bindings as constrained by the binding patterns, the semantics
> >     of a RIF-PRD rule with bound variables and the semantics of a RIF-BLD
> >     universally quantified rule coincide whenever they have the same RIF
> >     XML syntax."
> >
> >     This is yet another misleading notation. Forall means something very
> >     specify in logic to 9.99999% of the potential readers of these specs.
> 
> Absolutely. Using "Forall" in PRD is misleading; hence the explanation.

So why use it????

> Or do you mean that the explanation is misleading?

The "explanation" makes a statement to the effect that it acknowledges a
misleading choice of word in a formal notation but still persists in
using it. Makes no sense to this reader.

> > 2.3.1.3 Wellformed rules and groups
> >
> >   - Section title should be "Well-formed rules and groups".
> 
> it is, isn't it?

No it isn't: the hyphen os missing between "Well" and "formed".

> Yes, the example does not make sense anymore (assuming it ever did :-)
> now that we removed the explanation from the introduction.
> 
> The intention is, indeed, to replace it by a more meaningful one.
> 
> Hopefully in time for WD2.

Not just one big example after pages of formal stuff; but rather, many
small ones (related through a common simple object data-model), each
illustrating a specific notion being formally defined as it is being
defined.

> >   - Quoting: "In the remainder of this section, as in the section on the
> >     operational semantics of actions, ..."
> >
> >     The link associated to "operational semantics of actions" is stale:
> >     http://www.w3.org/2005/rules/wg/draft/rif-prd/#sect-semactions
> 
> 
> Corrected. We have to check all the links, anyway...
> 
> >   - Quoting: "For the purpose of this section, an instance of a rule, r
> >     \in\ R, is defined as a couple (rid, \sigma), where rid uniquely
> >     identifies r and \sigma\ is a ground substitution ..."
> >
> >     More precisely, this is a *ground* instance of a rule.
> 
> No, this is what is defined as an instance of a rule in this document. I
> am not aware of a different acceptation that would be usual enough to be
> a problem. Pointer?

In logic, an instance of a term is not necessarily ground. For example,
f(g(X),h(k(Y))) is an instance of f(U,h(V)) with substitution {g(X)/U,
k(Y))/V}, though not a ground one. On the other hand, f(g(a),h(k(a))) is
a *ground* instance with *ground* substitution {g(a)/U, k(h(a)))/V}.

> No, really, we appreciate the thorough comments. Adn we hope that you
> are not that disgusted that you will not try and read the remainder
> (once we will have improved its readability, of course :-)

I am not disgusted in the least bit, I am more worried that this work
may be missing its intended target.

> Cheers,
> </PRD editor><chair>
> 
> Christian

Cheers,

-hak