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

From: Michael Kifer <kifer@cs.sunysb.edu>
Date: Thu, 4 Dec 2008 14:14:20 -0500
To: "Hassan Ait-Kaci" <hak@ilog.com>
Cc: "rif-wg" <public-rif-wg@w3.org>
Message-ID: <20081204141420.295deaaf@kiferserv>

On Thu, 4 Dec 2008 09:11:48 -0800
"Hassan Ait-Kaci" <hak@ilog.com> wrote:

> Attached is my review of the  RIF Production Rule Dialect's Editor's
> Draft of 25 November 2008:
>
>     http://www.w3.org/2005/rules/wg/draft/ED-rif-prd-20081125/

Hassan,
here are some comments on the PRD issues, which are related to BLD.

>   - Quoting: "... Definition (Well-formed formula). A formula  \phi\ is
>     well-formed iff:
>       * every constant symbol mentioned in \phi\ occurs in exactly one
>         context.
>       * ..."
>
>     Question: Does this make sense? What about the constant "a" in a
>     formula such as, e.g., "And(p(a),q(a))"? Doesn't it occur in two
>     separate contexts (namely, those of predicates "p" and "q")?

The notion of a context is defined right after that in the text (although it is
an older, broken version of what is now in BLD).
The context of "a" is "individual" in both cases.

>   - Quoting: "Whenever a formula contains a function term t or an
>     external atomic formula External(t), t must be an instance of the
>     coherent set of external schemas (Section Schemas for Externally
>     Defined Terms of [RIF-DTB]) associated with the language of
>     RIF-PRD."
>
>     I looked up the reference section in [RIF-DTB]
>     (http://www.w3.org/2005/rules/wg/draft/ED-rif-dtb-20081125/#app-external-schema)
>     and I read this:
>
>        "Definition (Coherent set of external schemas). A set of external
>        schemas is coherent if there is no term, t, that is an instance
>        of two distinct schemas in the set.  ?
>
>        The intuition behind this notion is to ensure that any use of an
>        external term is associated with at most one external
>        schema. This assumption is relied upon in the definition of the
>        semantics of externally defined terms. Note that the coherence
>        condition is easy to verify syntactically and that it implies
>        that schemas like (?X ?Y; ?X[foo->?Y]) and (?Y ?X; ?X[foo->?Y]),
>        which differ only in the order of their variables, cannot be in
>        the same coherent set."
>
>     I am not sure I understand this: what about t = a (i.e., a[foo->a])?
>     I do not see either that, "...  it implies that schemas ...  which
>     differ only in the order of their variables, cannot be in the same
>     coherent set." Can anyone enlighten me?

I do not understand how t = a is related to a[foo->a] in your understanding,
and how it is an instance of two different schemas in a coherent set.
Which set? Which schemas?

>   - General comment: This notion of WFF is highly uncommon and deserve
>     some elaboration and explanation in lay terms. Many a reader (like
>     me) are baffled at this point with so many technical requirements to
>     define such a simple notion.

I agree here. The problem is that some WG members insisted on forcing every
symbol to appear in at most one context. I tried to rebel against this as late
as at the last F2F, but was put down.

This requirement complicates BLD and PRD unnecessarily.

>   - Quoting: "(We shall see later that o[a->b a->b] is equivalent to
>     o[a->b];)".
>
>     Why should it be so? For example, a collection semantics might
>     interpret this as o[a->list(b,b)].

The BLD semantics for frames is that o[b1->c1 b2->c2] == o[b1->c1] /\ o[b2->c2].
The above is a special case when b1=b2=a.
Why is this so? Because this is how it was defined (after F-logic) and nobody
objected.

>   - Quoting: "I(External(t)) = I_external(\sigma)(I(s1), ..., I(sn)), if
>     t is an instance of the external schema \sigma\ = (?X1 ... ?Xn;
>     \tau) by substitution ?X1/s1 ... ?Xn/s1.  Note that, by definition,
>     External(t) is well-formed only if t is an instance of an external
>     schema. Furthermore, by the definition of coherent sets of external
>     schemas, t can be an instance of at most one such schema, so
>     I(External(t)) is well-defined."
>
>     The form of the term "t" is nowhere defined - its arguments must be
>     s1, ... sn.

It does not need to be. It is said to be an instance of the specified external
schema by the specified substitution.

> 2.1.2.2 Interpretation of condition formulas
>
>   - Quoting: "Existence: TVal_I(Exists ?v1 ... ?vn (\phi)) = t if and
>     only if for some I*, described below, TVal_I*(?) = t.  Here I* is a
>     semantic structure of the form <TV, DTS, D, D_ind, D_pred, I_C,
>     I*_V, I_P, I_frame, I_NP, I_sub, I_isa, I_=, I_external, I_truth>,
>     which is exactly like I, except that the mapping I*_V, is used
>     instead of I_V.  I*_V is defined to coincide with I_V on all
>     variables except, possibly, on ?v1,...,?vn."
>
>     Why so complicated? Why not simply rephrase that as, "Existence:
>     TVal_I(Exists ?v1 ... ?vn (\phi)) = t iff TVal_I(\sigma(\phi)) = t
>     for some variable valuation \sigma\ : Var -> D_ind.

This is also possible. But then the notion of \sigma(\phi) has to be defined
somewhere earlier. Does not save any space (although with some refactoring of
the text it might be possible to save some).
Received on Thursday, 4 December 2008 19:26:02 UTC

This archive was generated by hypermail 2.3.1 : Tuesday, 6 January 2015 21:47:54 UTC