I've been following the messages to this list for about six months now, hoping
to learn how modern ontologies, and related methodologies and tools, can help
in building reasoning tools to improve the performance of computer networks. (01)
I suspect that I have now learned enough to be dangerous. I'd like to check my
understanding and solicit guidance. (02)
--- (03)
Disclaimer: I have no expertise in NLP. I know just enough about it to
remember how promising a technology it has been since I entered the field in
1959, and how poorly widely-available systems like Google's do today.* (04)
Much of my background is in programming methodology and formal methods for
digital systems. In the 70s and 80s, I did quite a lot of work in structured
algebraic specifications (SAS), which seem to me to present a number of
analogies with the approaches being discussed on this list (ONT), some of which
I will discuss presently. If the analogies are valid, they will strengthen my
confidence. If not, they are probably going to lead me astray. (05)
I will couch my discussion of SAS in terms of the Larch Shared Language (LSL),
because I am most familiar with it, not because of any superiority over more
recent algebraic specification languages like CASL. I doubt that the details
of the differences among SAS languages are any more important for discussion at
this level than are the differences among ONT languages. (06)
When I say something about SAS, I feel confident about my grasp. However, when
I assert something about ONT, it is to test my understanding, not to advance an
argument. (07)
--- (08)
I will sketch some apparent correspondences between SAS and ONT below. My main
questions are: (09)
1. Are these correspondences real, or have I missed something important?
[1a. If they are real, is that a coincidence,
or a reflection of some deep property of the way
our minds organize our perception of reality?] (010)
2. Can SAS and ONT really say roughly the same things? Or are they each only
helpful in their own (almost) disjoint domains? (011)
3. What can be expressed in ONT, but not in SAS? How important is it to be
able to express these things? In what circumstances does the extra power
justify the cost? (There is always a cost.) (012)
4. What can be expressed in SAS, but not in ONT? How important is it to be
able to express these things? In what circumstances does the extra power
justify the cost? (013)
I think that's enough to start a free-for-all, so I will save for later my
further questions, like how ONT languages deal with the things that we saw as
critical design issues in LSL. (014)
---
LSL, an SAS language
http://www.cs.cmu.edu/afs/cs/usr/wing/www/publications/LarchBook.pdf
--- (015)
A *specification* is a related set of well-formed traits. (016)
Vocabulary: LSL has an open-ended set of *tokens*
[signs/symbols/signifiers/identifiers/names], a few of which are *reserved* for
structural purposes. The remainder can be used to denote (017)
- *traits* [modules/units/components] that are the concrete elements of
discourse. The body of a trait may refer to other traits and include
*declarations*, *axioms*, and *consequences*. Axioms are mostly, but not
exclusively, equations. (Part of the algebraic heritage.) [We also concluded
after great struggle that limiting "exports" was a methodological and logical
nightmare.] (018)
- *sorts* [types/kinds/classes]. (019)
- *operators* [polyadic function symbols/constants]. (020)
- *variables*. (021)
Syntax: The syntax of LSL specifies how tokens may be combined into well-formed
*terms*, *sentences*, and traits. (022)
Semantics: Each well-formed trait has an associated set of *models* (the
algebras that satisfy all of its axioms) and an associated *theory* (the set of
all sentences true in all models/entailed by the axioms). The semantics
defines the association of well-formed traits with theories and sets of models.
Tokens are not given meaning in isolation, only their relations to other
tokens are fixed (by the set of true sentences). (023)
Inclusion: LSL has an isA relation between traits determined by theory
inclusion, rather than on sorts, representing class inclusion. However, many
traits have a "principal sort," so the pragmatic difference is not large.
E.g., trait Rational *includes* trait Integer and *implies* trait Field.
Inclusion can either be specified directly or entailed by other axioms. (024)
Redundancy: Not every arrangement of tokens constitutes a well-formed trait.
As well as syntactic redundancy (e.g., mandatory declaration of operators and
variables), there are special language constructs (e.g., *assumes*, *implies*,
and *converts*) whose primary purposes are a) to raise the chance that an error
will cause a mechanically-detectable inconsistency, and b) to give human
readers ways to grow and check their understanding. (025)
Tool support: The Larch Prover (LP) was designed to check LSL traits for
consistency, and to prove theorems in their associated theories--interactively,
under human supervision.
http://www.cs.cmu.edu/afs/cs.cmu.edu/project/larch/.alpha_osf20/lp/html/news/distribution.html (026)
Examples: See the Larch Shared Language Handbook:
http://nms.lcs.mit.edu/Larch/handbook/toc.html
I would suggest using the index to pick out some domain that you are reasonably
familiar with, and focusing on the includes/assumes/implies structure, rather
than the details of the axioms. (027)
---
An typical ONT language (TOL)
[I'm going way out on a limb here to try to distill what I've been reading.]
--- (028)
An *ontology* is a related set of well-formed units. (029)
Vocabulary: TOL has an open-ended set of *signs*
[symbols/signifiers/identifiers/names/shapes], a few of which are *reserved*
for structural purposes. Others can be used to denote (030)
- *units* [modules/units/component] that are the concrete elements of
discourse. The body of a unit may *import* from, and *export* to, other units
and will include *type declarations* and possibly some *constraints*. (031)
- *types* [classes/kinds/classes]. (032)
- *unary/nullary function symbols* [slots/constants]. (033)
- *variables* [?]. (034)
Syntax: The syntax of TOL specifies how signs may be combined into well-formed
*terms*, *sentences*, and units. (035)
Semantics: Each well-formed unit has an associated set of *models* that
satisfy all of its subtyping relations and constraints and an associated
*theory* (the set of all sentences true in all models). The semantics defines
the associations of theories and sets of models to well-formed units. Signs
are not given meaning in isolation, only their relations to other signs are
fixed (by the set of true sentences). (036)
Inclusion: TOL has an isA relation between types based on subsetting of their
*instances*. This is the predominant form of constraint. Subtyping is usually
either specified directly or by transitivity [but could be entailed by other
axioms?]. (037)
Patterns: Syntactic patterns that show how the words are used in sentences.
[I don't see a direct correspondence to SAS, although there seems to be some
relation to LSL's provision for "mixfix" operators (like if __ then __ else __
).] (038)
Redundancy: Not every arrangement of tokens constitutes a well-formed unit.
There is syntactic redundancy as well as some semantic constraints that can be
the basis of mechanical checking. (039)
Tool support: There are a couple of forms of tool support:
- Tools for entering and viewing related sets of units.
- Tools for converting from TOL to the logical forms appropriate to various
available theorem provers, that support both checking for logical consistency
and proving theorems entailed by the ontology. (040)
Example: See John F. Sowa's message to this list
Sent: Monday, February 12, 2007 7:01 PM (041)
--- (042)
What are the most important things I have misunderstood? (043)
What are your answers to my questions 1-4 above? (044)
Thanks, (045)
Jim H. (046)
* For your amusement, here are two paragraphs from early in this message
translated by Google from English to Portuguese and back: (047)
Disclaimer: I do not have no skill in NLP. I only know sufficiently on it to
remember as to promise to a technology I was since that I incorporated the
field the 1959, and as the badly plaza-available systems as Google they make
today.* (048)
of deep mine Very is in the methodology of programming and formal methods for
digital systems. In 70 ' s and in 80s, I made completely many of work in
specifications algebraic structuralized (SAS), that me they seem to present a
number of analogies with the approaches that are being argued in this list
(Ontário), some of that I will argue presently. If the analogies will be valid,
strengthen my confidence. If not, they are going probably to lead me astray. (049)
_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/
Subscribe/Config: 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 Post: mailto:ontolog-forum@xxxxxxxxxxxxxxxx (050)
|