[Top] [All Lists]

Re: [ontolog-forum] Requirements of computer language semantics

To: "[ontolog-forum]" <ontolog-forum@xxxxxxxxxxxxxxxx>
From: Ed Barkmeyer <edbark@xxxxxxxx>
Date: Thu, 19 Mar 2009 17:23:31 -0400
Message-id: <49C2B7D3.6040602@xxxxxxxx>
John F. Sowa wrote:    (01)

> The major reasons for incompatibility between IBM and Oracle (or
> between Microsoft and Mozilla) is that they do not implement the
> standards exactly as stated.  The reasons for that are political
> and often futile attempts to "lock in" their installed user base.
> The user's groups have to fight back by refusing to purchase any
> software that does not honor the standards.    (02)

There is some truth in this, but
  (a) most of the lock-in technology is added features that the standard 
doesn't specify at all; and
  (b) some of the departures are a consequence of important features of 
the underlying software design (which may predate the standard, or 
predate understanding it, or predate understanding the need to conform 
to it) that make it impossible to implement some fine detail properly 
without rewriting half of the software; and
  (c) many incompatibilities are just different implementations of a 
specified behavior with different side effects the standard doesn't 
actually address.    (03)

John will doubtless remember the effort of a misguided professor and his 
numerical analysis cronies to require that the order of evaluation of 
the terms of an arithmetic expression in Fortran must always be what 
John Backus' original compiler did, so that their careful syntax for 
controlling the machine rounding errors on the IBM 704 would work when 
the programs were moved to 1970s hardware.  With respect to SQL, 
constructs involving multiway joins have multiple possible 
implementations that produce equivalent, but not identical, results. 
There are some situations in which different optimization algorithms 
produce different orderings of the results, even though the standard 
nominally specifies a particular one.  The brute force cross-product 
model described in the standard produces a known result, but no one 
actually implements that, because of the performance penalty.  And there 
are cases involving null values that are an endless source of 
controversy (one of many instances of "Much Ado about Nothing").    (04)

[Conformance to the SQL standard is one of the real standards success 
stories, in terms of overall impact on users (and NIST prides itself on 
having contributed to that).  I wish John had not chosen SQL as an 
example of deliberate vendor variance.  But I also wish the SQL 
committee had stopped when they were done.  (And if wishes were horses...)]    (05)

> EB> In general, when the mapping is not semantically 1-to-1 at
>  > the language element level, it is very difficult to determine
>  > the relationship between the semantics of L1 and the semantics
>  > of L2 -- you are now talking about proving the equivalence
>  > of the systems.
> I certainly agree.  That is why my recommended approach is to
> start with one very general language, such as Common Logic,
> which is a superset of first-order logic *and* of the very
> thorny aspects of RDF and OWL full.  With CL as the target
> language, all the SemWeb languages and most other logic
> based languages can be mapped into CL by 1-to-1 mappings.    (06)

OK.  If you are mapping a declarative knowledge representation language 
to an axiomatic first-order language, then I agree.  Those are strong 
constraints on L1 and L2 that won't generalize much.  For example, they 
don't generalize to L1 condition-action languages, even though most of 
the actions may be:  conclude <S>.    (07)

> The major reason why I recommended *not* having a separate
> model theory for the source languages is the difficulty of
> proving equivalence.  It is far easier to use the mapping
> from a subset language Ln into CL as the *definition* of
> the semantics of Ln.    (08)

Into CL, yes.  Into Ln (unspecified) is quite another thing entirely.    (09)

> EB> And if L1 is short on formal semantics in the first place,
>  > how would you go about such a proof?
> That's the easy case.  Instead of proving equivalence, you
> *define* L1 to be equivalent to that subset of CL into
> which L1 is mapped.    (010)

Absolutely.  Yes, translating language constructs to equivalent 
axiomatic formulations is a good semantic model.  (I didn't see the part 
where you said that L2 was CLIF, or some other well-defined FOL language.)    (011)

> JFS>> Other things being equal, it makes more sense to try
>  >>    to map a new language L1 to some previously defined
>  >>    and analyzed language than to try to define the
>  >>    semantics for L1 from scratch.
> EB> And, like Chris, I would argue just the opposite.
> If you do, you are forced to prove that two independently
> define model theories are equivalent.  In some cases,
> that is easy, but in others it can be very difficult.    (012)

That is not true at all.  The problem as stated was to define the 
semantics of a given language L1.  ISO 24707 does exactly that, where 
L1=CLIF, using the Tarski approach without reference to any other 
language.  And the RDF and OWL Recommendations do something very similar.    (013)

> EB> The basic concepts in a Tarski-style semantic model are
>  > clear, and they are not that hard to do for your language.
> Yes, but the basic primitives of core CL are very simple
> and very general.  Defining multiple logics by the mapping
> to one standard logic with a solid model theory automatically
> insures that all of them are mutually compatible.     (014)

This is certainly a laudable goal, but
(1) it wasn't the topic I thought we were discussing, and
(2) it only works for FOL languages.  For logic programming languages, 
you just don't have all the necessary semantic concepts in CL.  (And I 
don't know what kind of language mKR really is.)    (015)

> I would
> not recommend the alternative of trying to prove that n
> independently defined model theories are compatible.    (016)

Nor would I.  Nor do I see how it is relevant to the issue of providing 
formal semantics for a given language.  This is ignoratio elenchi.    (017)

-Ed    (018)

Edward J. Barkmeyer                        Email: edbark@xxxxxxxx
National Institute of Standards & Technology
Manufacturing Systems Integration Division
100 Bureau Drive, Stop 8263                Tel: +1 301-975-3528
Gaithersburg, MD 20899-8263                FAX: +1 301-975-4694    (019)

"The opinions expressed above do not reflect consensus of NIST,
  and have not been reviewed by any Government authority."    (020)

Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/  
Config Subscr: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/  
Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/ 
To join: http://ontolog.cim3.net/cgi-bin/wiki.pl?WikiHomePage#nid1J
To Post: mailto:ontolog-forum@xxxxxxxxxxxxxxxx    (021)

<Prev in Thread] Current Thread [Next in Thread>