Re: Semantic Web Services Framwork v. 1.0

From: Michael Kifer <kifer@cs.sunysb.edu>
Subject: Re: Semantic Web Services Framwork v. 1.0 
Date: Fri, 13 May 2005 18:58:59 -0400

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

> > I cannot find any transformation to define the
> > Courteous layer in Grosof2004a.
> 
> Strange. I do see it there. 

Benjamin appears to disagree with you.

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

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

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.  

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

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

[...]

> > Second, "substitution" has not been defined.
> 
> Yes, but this is a standard notion.

Is it?  Are infinite substitutions allowed?

> > 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.  What does "argument" mean here?  

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

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

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

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

> A lot of people happened to have read those papers, and for them
> such references are meaningful. 

Well, perhaps.  But, "show me"!

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

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

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

> All the best,
> 
> 
> 	--michael  


Peter F. Patel-Schneider

Received on Sunday, 15 May 2005 01:03:49 UTC