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

 Hi Hassan,
 here are my responses to your comments to my comments to your comments.

On Fri, 5 Dec 2008 09:32:09 -0800
"Hassan Ait-Kaci" <hak@ilog.com> wrote:

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

No. Schema1 and Schema 2 cannot be both in a coherent set precisely because
they have a common instance. I may still be missing something in your
argument...

Also, I just noticed that the formulation is missing a subphrase (both in BLD
and PRD). Instead of
     t must be an instance of the coherent set of external schemas ...
it should read
     t must be an instance of a schema in the coherent set of external schemas ...

This change must be done in two bullets in the definition.
Maybe this was the source of the confusion?
   
> > >   - 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.

There was only one vote, years ago, when it was decided to introduce this
restriction. At that time full implications of this decision were not obvious
(at least to me). In the past year I tried to raise this issue at least twice
in F2Fs, but nobody was interested.

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

This semantics was out there for all to see for some two years.

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

It is a set semantics. You cannot just parametrize the semantics.
You need to make this monoid explicit in the syntax, which would be an
extension of what we have.


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

Because it is not necessary. The statement that t is an instance of a schema
and the variables in that schema already gives all the info.
An alternative would be much more verbose: to list all the possible syntactic
forms of t.

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

I doubt it will save any space or is simpler. The definition used is a standard
one for these quantifiers (e.g., in Enderton or Mendelson).

Moreover, what you are proposing is also not quite correct: sigma should be a
function that maps v1,...,vn only. And then we would have to define not only
what TVal_I(\phi) is but also what TVal_I(\sigma(\phi)) is. Thinking of it
more, your proposal would have made the definitions much longer.


	regards
	  --michael

Received on Friday, 5 December 2008 18:10:27 UTC