Re: SWSL declarative semantics

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.

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.

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

[...]

> 	regards
> 	  --michael  

peter

Received on Friday, 21 November 2003 08:50:09 UTC