Adrian, Joel, Ed, Dick, and Randall, (01)
AW> Or, consider that SQL never had a model theory. Now we have
> two major commercial implementations of SQL that produce
> different results from the same query over the same data. (02)
I agree that compatibility among different implementations of
what is supposed to be "the same" language is an extremely strong
reason for having a formal model theory as part of the standard.
French chefs (at least at top restaurants) have a slogan: (03)
Il faut honorer le menu. (04)
In other words, if it's on the menu, you have an obligation to
serve it upon request. (05)
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. (06)
JB> So rather than attempting to map L1 <-> L2, L1 <-> L3, etc.,
> what is the chance that the champions of each language can define
> a mapping from Ln <-> SKOS? Is SKOS rich enough by itself, or
> combined with RDFS/OWL/Prolog/OPS-5 better, or is it primitive
> enough, to express the same statement or theorem that you could
> state in Ln? (07)
There is already an ISO standard for Common Logic, which can support
a semantics-preserving mapping from RDFS, OWL, and the Horn clause
subset, which defines the pure logic aspects of rule-based languages
such as Prolog, OPS-5, and others. CL supports everything that SKOS
would support plus much, much more. (08)
JB> All men have an aspect which is called 'height'.
> The height of a man is quantifiable...
>
> I've attempted to write these statements in every language I've
> seen, with some success, but I am not convinced that any of my
> translations of those statements would be interoperable with
> anyone else's, even if we both used the same language. (09)
The major problems here are not in logic, but ontology. The
most difficult words to define in that passage are 'aspect'
and 'quantifiable', which raise an enormous number of logical,
linguistic, and philosophical issues. (010)
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. (011)
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. (012)
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. (013)
EB> And if L1 is short on formal semantics in the first place,
> how would you go about such a proof? (014)
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. (015)
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. (016)
EB> And, like Chris, I would argue just the opposite. (017)
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. (018)
EB> The basic concepts in a Tarski-style semantic model are
> clear, and they are not that hard to do for your language. (019)
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. I would
not recommend the alternative of trying to prove that n
independently defined model theories are compatible. (020)
RHM>> I hereby resolve to stop talking and return to my task
>> of translating mKR to IKL. (021)
RS> How will you do that? How will you _define_ it? (022)
The obvious answer is to *define* the semantics of mKR by its
translation to the target language (CL or IKL). That's one
of the primary purposes of CL: provide a common semantics
for an open-ended family of logic-based languages. (023)
John (024)
_________________________________________________________________
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 (025)
|