Re: SWSL declarative semantics

Peter,
thanks for your comments. Some clarifications below.

> From: Bijan Parsia <bparsia@isr.umd.edu>
> Subject: Fwd: SWSL declarative semantics
> Date: Thu, 20 Nov 2003 21:47:48 -0500
> 
> > Hi folks,
> > 
> > I got permission from Michael Kifer to forward this to this list. It 
> > seems to fit in with some of our discussions. Hmm. at first glance, I 
> > thought it might support a "comments count" view, or my own point about 
> > the gensym fallacy fallacy, but i see that it might be more against 
> > axiomatic approaches.
> > 
> > Cheers,
> > Bijan Parsia.
> 
> 
> > Begin forwarded message:
> > 
> > > From: kifer@cs.stonybrook.edu (Michael Kifer)
> > > Date: Thu Nov 20, 2003  6:01:24 PM US/Eastern
> > > To: swsl-committee@daml.org (Semantic Web Services Language Committee)
> > > Subject: SWSL declarative semantics
> > >
> > > As promised, here is are a few thoughts on the nature of the
> > > declarative semantics that we need for SWSL. This is a summary of a
> > > discussion that we had with Karl at ODBASE-03 in Sicily 2wks ago.
> > >
> > > Currently, the General Requirements section states that SWSL should 
> > > have
> > >     "declarative semantics, in the typical sense used in knowledge
> > >     representation where the meaning may be expressed in a
> > >     logical framework that establishes overall principles of what
> > >     conclusions are sancitoned from a set of premises".
> 
> Hmm.  This requirement is rather ambiguous, as it could apply to a
> proof-theoretic semantics as well as a model-theoretic semantics.  
> Futher, establishing ``overall principles of what conclusions are
> sanctioned from a set of premises'' could be statisfied by exhibiting a
> program that actually performs the inferences.

Yes, it is ambiguous. Was intended to refer to both.


> > > We felt that in the SW environment, it is inadequate to have semantics
> > > that simply sanctions conclusions. 
> 
> Agreed.
> 
> > > The problem is that a
> > > model-theoretic semantics by itself doesn't guarantee that all users
> > > have shared understanding of the language constructs and thus use the
> > > language correctly, especially if the logic language at hand is not
> > > sufficiently high level and its semantics is given though a complex set
> > > of axioms.  
> 
> This doesn't seem right.  The purpose of model-theoretics is precisely to
> provide ``shared understanding of the language constructs'' and this is why
> a model-theoretic semantics is not, and is not supposed to look like, a
> ``complex set of axioms''.  Perhaps Michael meant to complain about
> proof-theoretic semantics, a complaint I whole-heartedly agree with.

I should have been more precise. What I meant to criticize was a
model-theoretic semantics provided via a translation to a different
language, like the first-order logic. It is not really a model theory, but
some people claim that they provide a model theory to a high-level
language by axiomatizing the language constructs in first-order logic or
some other formalism that was invented for a different purpose.


> > > So, we believe that there is a need for an informal conceptual model
> > > (not unlike conceptual modeling in databases) that closely corresponds
> > > to the human perception of objects, classification, processes,
> > > etc. (e.g., UML-like). 
> 
> Well, sure, there should be such an informal model.  This is what a
> model-theoretic semantics attempts to formalize.  (I would not, however,
> use UML as an exemplar here, except as an exemplar of what can go wrong
> when an informal conceptual model neither closely corresponds to human
> intuitions nor is backed up with a comprehensible formal semantics.)

I said UML-*like*. That is, a set of pictorial conventions and other notations,
which *could* have been done properly.


> > > The language should then have constructs to
> > > represent the concepts of that model directly and the formal
> > > model-theoretic semantics of these concepts should be natural. By
> > > "natural" we mean that a reasonable technically competent person should
> > > agree that the formalization seems to adequately reflect the informal
> > > semantics behind the conceptual model.
> 
> Agreed.  It is possible to create a model-theoretic semantics that diverges
> from intuitions, which is not a good idea.
> 
> > > In other words, we need to make sure that there is a path from informal
> > > human model of a particular task at hand down to the bowls of the
> > > formalism that underlies the reasoning engine. Human knowledge
> > > engineers are not going to verify their programs using formal
> > > semantics, and in most cases they won't even fully understand it. By
> > > providing a transition path from the informal to the formal we can gain
> > > some confidence that the users' informal use of the language is
> > > reasonably correct.
> 
> Agreed.  If the formal specifications don't match intuitions then they need
> to be changed.
> 
> > > This approach applies to Semantic Web in general, not just SWS.
> 
> Agreed.  
> 
> > > The above should probably be an objective rather than a requirement.
> > >
> > >
> > > 	--michael
> 
> Peter F. Patel-Schneider



	regards
	  --michael

Received on Friday, 21 November 2003 08:38:42 UTC