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

Hi Michael,

Here are some comments on my comments...

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

Take: Schema-1 = (?X ?Y; ?X[foo->?Y])
 and: Schema-2 = (?Y ?X; ?X[foo->?Y])

According to what I quote above, as I (mis?)understand it, the frame
a[foo->a] is an instance of both Schema-1 and Schema-2. Thus, Schema-1
and Schema-2 form a coherent set of external schemas - does it not?
If so, this contradicts what is claimed in the text.

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

Not by me you weren't! I have myself voted consistently and repeatedly
against it.

> This requirement complicates BLD and PRD unnecessarily.

That has been my point from the start.

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

I was not aware that we were defining an interchange format between
F-logic and F-logic. ;-)

Be that as it may, this semantics conflicts with the freedom of using
frames for representing objects in the presence of multiple occurrences
of a given field. The most general approach is to define it using a
collection semantics over a commutative monoid. That monoid could very
well be idempotent to yield the equivalence you have built in (and which
could be the overridable default). However, it is less restrictive to
parametrize the semantics up to a consumer-specifiable function collecting
multiple values of a same field.

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

Fine. Then, why are the syntactic form of all other arguments to the
I(_) interpretation function given explicitly in this definition while
this one is not?

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

First of all, that would make the definition much *simpler* and easier to
read, and therefore to understand. Second, it does save space: \sigma(\phi)
need not be any further defined - it is the formula results after applying
the valuation \sigma\ to \phi.

Cheers,

-hak
--
Hassan Aït-Kaci  *  ILOG, Inc. - Product Division R&D
http://koala.ilog.fr/wiki/bin/view/Main/HassanAitKaci