Re: SWSL declarative semantics

Peter F. Patel-Schneider writes:
>
> From: Michael Kifer <kifer@cs.sunysb.edu>
> Subject: Re: SWSL declarative semantics
> Date: Fri, 21 Nov 2003 08:35:22 -0500
> 
> > 
> > Peter,
> > thanks for your comments. Some clarifications below.
> 
> [...]
> 
> > > > > 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.
> 
> Agreed.  However, this is not really a model-theoretic semantics at all.
> Instead it is a translation to some other formalism that may or may not
> have a model-theoretic semantics.  If the translation is intuitive (and
> simple and ...) then, sometimes, a model-theoretic semantics for the other
> formalism may induce a decent model-theoretic semantics for the initial
> formalism.  (But then why not take the easy step of writing down this
> induced model-thoeretic semantics directly?) However, such translations are
> usually not very simple and thus any benefits of a model-theoretic
> semantics of the other formalism do not accrue to the original formalism.

This is exactly what I said above:
   "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 translation for DAML+OIL, for example, does NOT provide this benefit.
> Even the simple translation from SKIF to FOL is rather suspect in this
> regards.


Did you mean HiLog? What is SKIF? :-)


> > > > > 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.
> 
> Hmm.  It would be interesting to see a pictorial formalism where this
> really works.  Pictures are worth a thousand words, of course, and thus it
> is usually the case that it takes more than a thousand words to really
> tease out what is going on in a pictorial formalism, which does not
> generally lead to nice logical formalisms.  Formalisms that start out
> pictorially usually end up abandoning the pictures except for
> non-authoritative display purposes.  (Semantic Networks, Frames, and
> Brachman's original structural inheritance diagrams have all gone this
> route.)  I remember arguments about what was really going on in KLONE-talk,
> a graphical interface to KL-ONE that was abandonded, largely because its
> manipulations of KL-ONE graphs did not correspond to reasonable
> modifications of the underlying formalism.

Note that I said "pictorial conventions *and other* notations".  And, second,
I said that this is needed for an *informal* conceptual model. That is,
this is not supposed to be the formalism itself, but a way to convey the
intuition behind the formalism to ordinary folks (knowledge engineers).
I think it is a mistake to think that programmers appeal to
model-theoretic semantics when they specify something in a logic-based
formalism. I believe that programmers need "rules of
thumb" that are natural enough to enable the programmers write correct
programs. This is where I see the role of the informal conceptual model.

I don't believe that model-theoretic semantics by itself is sufficient
to make sure that people use the language constructs correctly.
Its role is to serve as a yardstick for correct implementation of the
language itself and as an arbiter in hairy cases. In both uses, it is a
took for an expert, not for an average Joe-knowledge-engineer.
(Even experts use the formal semantics in their day-to-day work
only when they get stuck.)

Also, not that in my message I said that such a conceptual model is an
objective and not a requirement. In our slang this means that it is
something desirable, but we aren't sure that it is achievable in full.
However, this is achievable to some degree. To cite a trivial case, E-R
diagram is such a tool (for a very simple case). Another successful example 
is Query by Example as it is implemented in, say, MS Access.


	--michael  


> [...]
> 
> > 	regards
> > 	  --michael  
> 
> peter
>

Received on Friday, 21 November 2003 10:20:51 UTC