Re: Semantic Web Services Framwork v. 1.0

From: Michael Kifer (kifer@cs.sunysb.edu)
Date: 05/13/05

  • Next message: Benjamin Grosof: "courteous details Re: Semantic Web Services Framwork v. 1.0"
    > 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  
    


    This archive was generated by hypermail 2.1.4 : 05/13/05 EST