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>

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, --michaelReceived 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
*