W3C home > Mailing lists > Public > public-sws-ig@w3.org > May 2005

Re: Semantic Web Services Framwork v. 1.0

From: Michael Kifer <kifer@cs.sunysb.edu>
Date: Fri, 13 May 2005 18:58:59 -0400
To: "Peter F. Patel-Schneider" <pfps@research.bell-labs.com>
Cc: public-sws-ig@w3.org, martin@ai.sri.com, daml-all@daml.org, bgrosof@mit.edu (Benjamin Grosof)
Message-Id: <20050513225900.CDBB519E75F@kiferdesk.lmc.cs.sunysb.edu>


> I have a number of comments and questions concerning the document "Semantic
> Web Services Language (SWSL) - Version 1.0".  Most of these questions have
> to do with the SWSL-Rules language.
> 
> Note that this is by no means a complete catalog of my concerns concerning
> the document.  Answers to these questions, particularly my fundamental
> concern about semantics, may give rise to many other concerns.

Hi Peter,
Thank you very much for your comments. This was an exceptionally 
fast turnaround! :-)

> 
> Section 2.14
> 
> I am disappointed that the semantics for SWSL-Rules is not included in this
> document.


Yes, and we are aware of this. The document does say that the
single-point-of-reference semantics will be provided in a separate document.


> Pointing to external documents is not a substitute.  I believe
> that the external documents do not provide a semantics for the various
> SWSL-Rules subsets.

Well, it *is* a substitute for the time being. If you are sufficiently
curious and read the referenced papers then you will get a complete picture.
I believe that then you would be able to write down the semantics by
yourself. :-)

> I cannot find any transformation to define the
> Courteous layer in Grosof2004a.

Strange. I do see it there. Unfortunately, this paper describes the
algorithm in a manner that one may not be able to spot it by just skimming
through the text. Will harp on Benjamin to describe the transform
explicitly in a following edition of SWSL-Rules.

> VanGelder91 does not provide a semantics
> for the = and != operators.  Without semantic definitions, it is hard to
> determine just what is going on in the language.

You are wrong. = is the identity relation with fixed interpretation.
Of course, he would not mention this because it is trivial and is not worth
mentioning.

Perhaps, you meant the :=: relation, which is the real equality?
Yes, this is not mentioned, but it has been a "folk theorem" in the right
circles for some time now :-)

The idea is very simple. :=: is treated as a normal relation with
equivalence and congruence properties. The equivalence properties are
expressed using Horn rules (left as an exercise :-). The congruence
property is expressed as an infinite axiom schema where each rule is also
Horn. For instance, here are some rules in this schema:


    p(V,Y) :- p(X,Y) and X :=: V.
    p(X,V) :- p(X,Y) and Y :=: V.
    V[M -> Y] :- X[M -> Y] and X :=: V.
    X[M -> V] :- X[M -> Y] and Y :=: V.
    X[V -> Y] :- X[M -> Y] and M :=: V.
    ....
    f(V,Y,Z) :=: f(X,Y,Z)  :- X :=: V.
    ....

Then you compute the WF model for the original theory augmented with the
above schema.


> Section 2.2
> 
> Is there any difference between f and f() as first-order atomic formulae?

We didn't actually define f(), but the two could be defined as denoting the
same term.


> The unification (=) and disunification (!=) operators are not appropriately
> handled.   First, what does "identical" mean here?  Is it before or after
> prefix expansion, for example?

The intent was, of course, that prefix expansion happens first. Thanks for
pointing this out. Prefixes are treated as macros, and they are expanded
before the actual theory is looked upon.

Could have been stated better - yes.

> Second, "substitution" has not been defined.

Yes, but this is a standard notion.

> Third, what is the scope of the subsitution?  For example,
> consider 
> 	p(?x) = q(f(?y)) and p(f(?x)) = q(?y).

You apply substitutions to formulas, which are given as arguments.


> 
> And/or formulae are ambiguous.  Consider
>        p1 and p2 or p3
> Is this the conjunction of an atom and a disjunction or the disjunction of
> a conjunction and an atom?

Sure. We didn't want to distract the reader, but we should have said
something here.  I hope that you realize that this is a first more or less
complete version of the document and not a "proposed standard."

> Section 2.3
> 
> Any appeal to semantically-related notions (like "equivalently") is suspect
> here, as no semantics has yet been defined.  This is particularly true for
> illegal syntax.

Semantics of Horn rules is well-known.
What do you mean by "illegal syntax"?
I think you are confusing informal motivating discussions that preceded
formal definitions with the definitions themselves. It could be a problem
with our writing style - will try to separate the two more clearly.

> 
> I don't understand the stated allure of Horn rules.  Couldn't I make a
> similar statement about arbitrary first-order formulae being independently
> characterized by entailment, models, and deductive consequences?  How is
> this in any way less desirable than being characterized by entailment,
> a minimal model, and deductive consequences?

Horn rules have 4 different well-known characterizations. Arbitrary
formulas have two.  If you don't care about this - fine. A lot of people
find this elegant.  What is your point?


> Section 2.4
> 
> The appeal to semantic reductions is not appropriate here.  First, no
> semantics has been given yet.  Second, which semantics is to be used?

We are referring to the semantics that is defined in other papers, which we
reference. A lot of people happened to have read those papers, and for them
such references are meaningful. As I said, this is a living document and a
separate document is planned as a single point of reference for the
SWSL-Rules semantics.


> Section 2.5
> 
> No syntactic characterization of the extended syntax for this layer is
> given.  

Yes, the language could have been tightened here.
But the syntactic characterization is certainly clear to anyone who is
even minimally familiar with logic programming.

> Transformations into a syntax which is not defined do not provide useful
> information. 
> 
> Section 2.6
> 
> There is no definition of "equivalent" to use here, nor is the syntax
> legal.


This part was informal discussion to motivate the formal definition that
follows. It could be tightened - yes.


> Without any proofs that the transformations preserve any useful
> characteristics of the formulae, they should be treated very suspiciously.  


We describe here the *well-known* Lloyd-Topor transformation. The
transformation itself is the definition of the extended syntax.  Which
properties are you talking about here?


Thanks again for your comments. We'll incorporate them in the next
reincarnation of the document. The semantics document is, of course,
a big piece of prose and should not be expected tomorrow.
But all the components are well known and have been rigorously defined in
other papers.

All the best,


	--michael  
Received on Friday, 13 May 2005 22:59:31 UTC

This archive was generated by hypermail 2.3.1 : Tuesday, 6 January 2015 20:54:14 UTC