Re: [TED] CORE Pages on Positive Conditions and Horn Rules Edited: Slots & Constraints

Hello,

The attachment is in response to some comments by Michael and Harold
regarding the CLP proposal and using the OSF formalism as a means to
encode slotted terms. I am copying the rest of the RIF WG since I
believe that this discussion is relevant to more than the three of us ...

Cheers,

-hak

Michael Kifer wrote:

>>See attachment for the essence of this semantics using OSF constraints.

[HAK note - this is not included here but will be in the document that
  I am currently writing]

>>
>>>For instance, suppose we have this in the db:
>>>
>>>p(f{x->a,y->b}).
>>>
>>>and then the user asks the query
>>>
>>>?-  p(f{x->a}).
>>>
>>>Is it true or not?
>>
>>Yes. (Assuming 'x' is not a variable).
>>
>>
>>>Note that in unordered notation, if we have
>>>
>>>p(f{1->a,2->b}).
>>>
>>>then
>>>
>>>?- p(f{1->a}).
>>>
>>>is not true.
>>
>>It all depends on how you interpret this notation. If a, b, and f denote
>>singletons, then Rank(f) =3D {1,2} and also f must be in Dom(1) and Dom(2)
>>[see attachment for notation]. Therefore, using the 'partial feature' rule
>>and the 'weak extensionality' rule in addtion to the basic OSF rules entails
>>that p(f(1->a)) is true iff p(f(1->a,2->b)) is true.
>>
>>
>>>I am asking in order to see if we are seeing things the same way, since=
>>
>> I
>>
>>>have to write the semantics part for the syntax we agreed at the F2F.
>>I understand your concern. Please do not hesitate to call me  if you wish
>>to discuss these issues further.
>>
>>
>>>	regards
>>>	  --michael 
>>
>>Cheers,
>>
>>-hak
> 
> 
> 
> Hi Hasan,
> 
> For some reason our spam filter didn't like your attachment, so all msgs
> with it ended up among spam. I hope that the filter will "unlearn" the
> pattern it didn't like, but just in case I am copying to my gmail account.
> 
> Anyway, now that I found it, here are my thoughts.
> 
> One serious problem that I see is that this is not exactly compatible with
> the standard first-order logic (as Harold observed in a followup email).
> So, feature terms with subsumption are better suited for a dialect of RIF
> than its core.
> 
> The question in my mind really is whether slotted terms should be in the
> core at all because it seems that there is disagreement between the
> semantics that Harold has in mind (which is used in RuleML) and the one you
> have.
> 
> As far as I understand Harold's idea of slotted terms, they can be given
> this model theoretic semantics. A slotted terms is basically a thing of the form
> f{slot_1->val_1 ... slot_k->val_k} where the order of the slots doesn't matter.
> So, an interpretation I_sf (sf stands for slotted funcs) maps f to a function
> 
> I(f): Powerset(Domain^2) -> Domain
> 
> That is, I(f) takes a set of pairs of elements in the domain and returns an
> element of the domain. For instance, I(f{slot_1->val_1 ... slot_k->val_k})
> is I(f)({(I(slot_1) I(val_1)), ..., (I(slot_k) I(val_k))}).
> (In f{...} the braces are simply suggest that we are dealing with a set,
> while in I(f)({...}) they really mean a set.)
> This can be viewed as a generalization of the standard first-order terms
> where slot_i=i.
> 
> This semantics doesn't imply any subsumption. It can be implemented at
> reasonable cost provided that variables over slots are not allowed.
> The idea of sorts can also be extended to such terms.
> 
> A dialect can add subsumption to such terms, but the model theory for that
> is not quite clear to me. (I can see the operational semantics only.)
> 
> Another issue is the use of slotted atoms. They can be given a similar
> semantics (to that of slotted terms a la Harold/RuleML :). But there also is
> object notation a la F-logic, which has a different meaning from that of
> slotted atoms.
> 
> So, it is not clear what to include and at what level of RIF.
> Would like to hear about your thoughts on this.
> 
> 
> I am glad that you agree with the idea of using sorts for extensibility.
> I was pretty sure that you would like it :-)
> I was surprised that a number of people had difficulty understanding this
> simple thing.
> 
> 
> 	cheers
> 	  --michael  



-- 
Hassan Aït-Kaci
ILOG, Inc. - Product Division R&D
tel/fax: +1 (604) 930-5603 - email: hak @ ilog . com

> Hi Hasan,

Hi Michael,

Please (again): my name is spelled with two S's (Hassan).

> For some reason our spam filter didn't like your attachment, so all
> msgs with it ended up among spam. I hope that the filter will
> "unlearn" the pattern it didn't like, but just in case I am copying to
> my gmail account.

Your spam filter must be unusually smart, then! ... :-) However, if it
has taken the habit of discarding mail from me to you (including this
one!?)  this is unfortunate as far as easing our communication. Let us
hope that it may come to terms (!) with the fact (!) that if it takes
what I am sending you as de facto spam, at least it is not that I am not
trying to sell you anything related to your sex life! ;-)

> Anyway, now that I found it, here are my thoughts.

> One serious problem that I see is that this is not exactly compatible
> with the standard first-order logic (as Harold observed in a followup
> email).  So, feature terms with subsumption are better suited for a
> dialect of RIF than its core.

I am not sure I understand (and therefore cannot concur with) the "is
not exactly compatible with standard fol" part. The OSF formalism
that I summarized in my mail is all expressed in pure fol!

> The question in my mind really is whether slotted terms should be in
> the core at all because it seems that there is disagreement between
> the semantics that Harold has in mind (which is used in RuleML) and
> the one you have.

My response (which was perhaps too terse) to the question related to
having slotted atoms or terms is that if we use the CLP scheme whereby a
slotted term syntax is seen as sugaring of more basic constraints, then
the issue is not a semantic one, but a syntactic one. Indeed, the CLP
semantics factors out semantics once and for all. Once the semantic CLP
scheme is in place, *any* formalism describing the constraint part that
is capable of recognizing solved forms (e.g., FOT substitutions in the
case Prolog) can do. Since the OSF formalism is a flexible means for
representing varied syntactic data models *and*, to boot, is compatible
(since it generalizes FOTs). I contend that it is very adequate for
representing data through logical constraints, where constraint formulae
are a basic axiomatization of terms à la Michael Maher's [1].

Hence, the actual semantics of these constraints is *meta-logical* in
that they encode and describe in FOL data using a logic tailored to
represent rooted labelled graphs corresping to solved formulae. It is in
that regard (as a meta-formalism) that I have proposed the OSF
constraint formalism since it may be extended with any additional axioms
to fit positional functional terms or objects (i.e., arity constraints,
values), and even more powerful constraints (e.g., sort definition
schema checking, etc...).

> As far as I understand Harold's idea of slotted terms, they can be
> given this model theoretic semantics. A slotted terms is basically a
> thing of the form f{slot_1->val_1 ... slot_k->val_k} where the order
> of the slots doesn't matter.  So, an interpretation I_sf (sf stands
> for slotted funcs) maps f to a function
> 
> I(f): Powerset(Domain X Domain) -> Domain
> 
> That is, I(f) takes a set of pairs of elements in the domain and
> returns an element of the domain. For instance, I(f{slot_1->val_1
> ... slot_k->val_k}) is I(f)({(I(slot_1) I(val_1)), ..., (I(slot_k)
> I(val_k))}).  (In f{...} the braces are simply suggest that we are
> dealing with a set, while in I(f)({...}) they really mean a set.)
> This can be viewed as a generalization of the standard first-order
> terms where slot_i=i.

This is an interesting trick but:

 (1) it no more "standard FOL" than how OSF terms are interpreted (i.e.,
     as graphs axiomatized in FOL), and IMHO no more intuitive

 (2) it simply assimilate all function symbols to unary functions
     over sets of pairs of domain elements

 (3) it is *not* faithful to the data models of slotted terms in that it
     allows arbitrary deomain elements to figure as slots

 (4) it cannot be generalized easily or intuitionally to account for
     object features such as cycles, 

Another unclear question is the compatibility of the conventional
semantics of f(t1,...,tn) and its set-function encoding version
f{1->t1,...,n->tn} and how to reconcile them formally. Indeed, since the
RIF also wants to have the predefined syntax f(t1,...,tn), is "f"
denoting a function from D^n -> D or from P(DxX) -> D?

Finally, the "dotted" notation for slotted terms proposed by Harold
(viz,, f{s1->t1,...,sn->tn} ==> f.s1 = t1 & ... & f.sn = tn) is
inconsistent with your pairset-function trick (i.e., what does exactly
f.s mean?). In the OSF formalism, the dotted notation is between
*variables* (i.e., X.s = Y).

> This semantics doesn't imply any subsumption. It can be implemented at
> reasonable cost provided that variables over slots are not allowed.
> The idea of sorts can also be extended to such terms.

In a way it does in the way FOTs imply subsumption by matching (where a
term t1 subsumes a term t2 iff the set of all instances of t1 contains
those fo t2 - e.g., "person{age->10, name->Y}" is subsumed by
"person{age->10, name->"Doe"}".

> A dialect can add subsumption to such terms, but the model theory for
> that is not quite clear to me. (I can see the operational semantics
> only.)

This is the whole point: your set-pair functions encoding trick is just
a syntactic encoding - not a semantic one. Therefore, unlike the oSF
constraint formalism, it does not fare very far for describing arbitrary
data models in a general and flexible way with *both* a model semantics
and a provably correct operational semantics.

> Another issue is the use of slotted atoms. They can be given a similar
> semantics (to that of slotted terms a la Harold/RuleML :) . But there
> also is object notation a la F-logic, which has a different meaning
> from that of slotted atoms.

Let me extrapoloate from your slotted term "semantics" here. If your
pair-set function trick is to be applied to predicates, this means that
p{a1->t1, ..., an->tn} denotes a monadic relation on the set of pairs of
domain values. In other words, all predicates denote sets of pairs of
domain values. Again the comments above apply on this being unfaithful
to the intended semantics (i.e., "slots" may not be arbitrary domain
value). On the other hand, the OSF formalism (as a simple FIL
meta-formalism for describing graphs) can be used for atoms as well
since these are graphs.

It is precisely because there many "slotted term" notations out there
with varied semantics that I am suggestind the CLP scheme as the means
to encode their semantics. It should be the responsibility of whoever
wants to use the RIF for rules using slots to express one's data model
as contraints. Building in any specific syntax should only have meta
logical semantics at this level - viz., how to encode *faithfully*
the intended semantics using constraints.

> So, it is not clear what to include and at what level of RIF.  Would
> like to hear about your thoughts on this.

I am not at all trying to sell the OSF formalism to RIF. I am trying to
show that the CLP scheme is the best abstraction level for formalizing
Horn clauses over arbitrary data models seen as constraints. Whether a
particular syntax for "slotted" terms is provided in the RIF is ok as
long as (1) it can be desugared as a formal constraint system thereby
inheriting its semantics from the CLP scheme's for free; (2) and it
corresponds *faithfully* to the user's intended semantics. I contend
that OSF terms fit the bill.

As icing on the cake, mapping a slooted term to an OSF constraint is
*isomorphic* to expressing it as an set of RDF triples, thus meeting
an important requirement for the RIF to accept the RDF data model!

> I am glad that you agree with the idea of using sorts for extensibility.
> I was pretty sure that you would like it :-) I was surprised that a
> number of people had difficulty understanding this simple thing.

I agree with you.

> 	cheers
> 	  --michael  

Best,

-hak

REFERENCES:

[1] @TECHREPORT{maher:axiomatizations:ibm:88
	, AUTHOR = {Michael J.~Maher}
	, TITLE = {Complete Axiomatizations of the Algebras of Finite
		 Rational and Infinite Trees}
	, INSTITUTION = {IBM T.J.~Watson Research Center}
	, YEAR = {1988}
	, TYPE = {Technical Report}
	, ADDRESS = {Yorktown Heights, NY, USA}
	, NOTE = {\online{http://www.cse.unsw.edu.au/~mmaher/pubs/trees/axiomatizations.pdf}}
	}