From: Michael Kifer (kifer@cs.sunysb.edu)
Date: 05/14/05
> > > 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 might be able to write down some semantics by myself. I have no > confidence that this would be the same semantics as the authors of the > document intend, nor even that the authors even have a single intended > semantics. If you familiarize yourself with the papers that we reference then you will have the needed confidence. > > > I cannot find any transformation to define the > > > Courteous layer in Grosof2004a. > > > > Strange. I do see it there. > > Benjamin appears to disagree with you. Not at all. This paper is incremental and deals with a new syntactic feature. It defines the transformation for that feature and refers to a previous paper for the transformations related to other syntactic features. I did say that this is not satisfactory, but if you had sufficient interest in the matter than you would have had no difficulty reconstructing the full transformation. > > 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. > > I do not see any mention of the = and != operators in VanGelder91. So what? It is a simple exercise to extend VG91 not only to the identity relation, but to any number of relations with fixed interpretations. This has been known for years. I don't know if the authors thought about this issue, but if I were writing this paper I would have argued to leave this trivial extension out in order to avoid distracting the reader. > > = is the identity relation with fixed interpretation. > > Of course, he would not mention this because it is trivial and is not worth > > mentioning. > > I don't view it as trivial at all. I would find it extremely strange if a > text on FOL with equality didn't mention equality, for example. This is NOT equality. It is the identity relation. > In essence you are saying that the NAF layer is an extension of > VanGelder91. Yes, it might be easy to define this extension. Yes, this > extension might have the same properties as those proved in VanGelder91. > However, this needs to be shown. This is left as an easy exercise to you. > > 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 :-) > > Well, there may also be a problem that the texts mentioned as semantic > sources don't handle real equality. I haven't investigated this issue yet. > However, I was indeed referring to = and !=. > > > 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. > > Well, yes, this might work well, and almost certainly does work for some > rule formalisms. Does it provide the right results all rule formalisms? Define the "right" results. One can define what's a "right result" with respect to a given semantics. I don't know what you mean by a semantics producing the right results. Is the well-founded semantics right? Stable model semantics? There were several extensions of WFS. Are they all "right"? Perhaps you meant "intended" results with respect to some set of "benchmarks"? Then the answer is "yes". If you find a program where this semantics doesn't produce an intended result (and we agree that our intuitions agree) THEN you will have shown that the above semantics doesn't match the intuition. There is no other measure by which a semantics can be judged. > > > 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. > > From the document: > > A first-order term is either a constant, a variable, or an > expression of the form t(t1,...,tn), where t is a constant and > t1,...,tn are first-order terms. Here the constant t is said to be > used as a function symbol and t1,...,tn are used as > arguments. Variable-free terms are also called ground. > > [...] > > A first-order atomic formula has the same form as first-order terms > except that a variable cannot be a first-order atomic formula. > > I took this as allowing n=0, as this seems reasonable. > > [...] It is arguable whether n=0 applies here (since you already have t1), but the point is well-taken. > > > Second, "substitution" has not been defined. > > > > Yes, but this is a standard notion. > > Is it? Are infinite substitutions allowed? A substitution is a mapping from the set of variables to terms. Then it is extended to terms and wff's in a standard way. I don't know what you mean by an infinite substitution here and why it is important. > > > > 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. > > "formula" is not a syntactic category. "Formula" is a short for "well-formed formula". It is certainly a syntactic category. > What does "argument" mean here? An argument to a function? > > > 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. > > Umm, getting the syntax unambiguous seems like a good first step. > > > 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. > > Which semantics? There are several. Like, for example? > > What do you mean by "illegal syntax"? > > Upside down A's and backward E's are not part of the syntax, as far as I > can tell. Are you saying that they are allowed? As I said, this was informal discussion preceding formal definitions. The symbols for quantifiers were specifically chosen so that this point would be clear. > > 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? > > Arbitrary first-order formulae have quite a number of well-known > characterizations. I don't see that the situation is any better for Horn > rules. As I said, many people find that the semantic characterizations of Horn clauses are particularly elegant. If you are not among those people, it is your problem. Some people don't like sports, while others do. Some don't like music. What was your point again? > > > 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. > > But not yet. I worry about the semantics depending on a circular > definition. Don't worry about that. > > A lot of people happened to have read those papers, and for them > > such references are meaningful. > > Well, perhaps. But, "show me"! You have two choices: wait or read the papers. > > 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. > > Well, I see lots of possibilities for confusion. Particularly as the > examples given in this section include explicit quantifiers, which I don't > remember being part of logic programming. Depends what you call "logic programming". If you mean ISO Prolog, then yes. If you mean LP as a discipline then you are dead wrong. LT extensions have been well-known for over 20 years and some LP systems have explicit quantifiers based on the LT transformation. > > > 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. > > Well-known for the particular languages you are defining? > > The > > transformation itself is the definition of the extended syntax. Which > > properties are you talking about here? > > Well, if they are the *definition*, then no problem. But then you have to > be very careful in making any semantic or intuitive claims. If you don't have a problem with this then what are we discussing? The document clearly states that the semantics of explicit quantifiers is defined through the LT transformation. > > 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. > > I am not convinced of this. Your conviction carries little weight until you actually read the papers, which you prefer to ignore. mk
This archive was generated by hypermail 2.1.4 : 05/14/05 EST