ontolog-forum
[Top] [All Lists]

Re: [ontolog-forum] Ontologies and Algebraic Specifications

To: "Horning, Jim" <Jim.Horning@xxxxxxxxxx>
Cc: ontolog-forum@xxxxxxxxxxxxxxxx
From: Pat Hayes <phayes@xxxxxxx>
Date: Tue, 27 Feb 2007 09:37:02 -0600
Message-id: <p06230902c209f700632b@[10.100.0.26]>
>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.
>
>I suspect that I have now learned enough to be 
>dangerous.  I'd like to check my understanding 
>and solicit guidance.
>
>---
>
>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.*
>
>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.
>
>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.
>
>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.
>
>---
>
>I will sketch some apparent correspondences 
>between SAS and ONT below.  My main questions 
>are:
>
>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?]    (01)

I would be VERY leery of any such psychological claim.    (02)

>2. Can SAS and ONT really say roughly the same 
>things?  Or are they each only helpful in their 
>own (almost) disjoint domains?
>
>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.)
>
>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?
>
>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.
>
>---
>LSL, an SAS language
>http://www.cs.cmu.edu/afs/cs/usr/wing/www/publications/LarchBook.pdf
>---
>
>A *specification* is a related set of well-formed traits.
>
>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
>
>- *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.    (03)

That seems very odd to me, speaking from the ONT 
side. There are many things one wants to say that 
just can't be put into equational form.    (04)

>  (Part of the algebraic heritage.) [We also 
>concluded after great struggle that limiting 
>"exports" was a methodological and logical 
>nightmare.]
>
>- *sorts* [types/kinds/classes].
>
>- *operators* [polyadic function symbols/constants].
>
>- *variables*.
>
>Syntax: The syntax of LSL specifies how tokens 
>may be combined into well-formed *terms*, 
>*sentences*, and traits.
>
>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).
>
>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.
>
>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.
>
>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
>
>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.
>
>---
>An typical ONT language (TOL)
>[I'm going way out on a limb here to try to distill what I've been reading.]
>---
>
>An *ontology* is a related set of well-formed units.
>
>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
>
>- *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*.    (05)

Hmm. Im not sure what you mean by a 'unit' here. 
(Common Logic has a 'module' construction, but 
that has a special purpose of limiting the 
'local' universe of discourse.)    (06)

This seems to miss the central point, which is 
that an ontology is, at base, a theory; that is, 
a collection of sentences. Plus, maybe, some 
bells and whistles, but in many cases even those 
are re-understood as kinds of sentence (e.g. 
'imports'). Some languages have types which may 
in some cases require declarations, but these are 
not an essential part of the mix. Importing is a 
Web idea, and there is no such thing as 
"exporting" (AFAIK).    (07)

Also, one of the most central and salient aspects 
of an ONT language is how it handles quantifiers, 
and what it can quantify over. You don't mention 
this anywhere, which I also find odd. Does Larch 
have quantifiers? (It is possible to treat 
quantification in terms of implicit universal 
quantification of variables and handling 
existentials by the deft use of functions, 
avoiding any need for an explicit quantifier 
scoping mechanism in the syntax. I'll make a 
guess that this is how Larch does it also.)    (08)

>- *types* [classes/kinds/classes].    (09)

Be careful of terminology. "types" often is 
understood to imply that type membership is 
syntactically checkable or used to determine 
wellformedness. This is quite unusual in ontology 
languages. If you really do just mean classes, 
then yes, almost all ontology languages have this.    (010)

>- *unary/nullary function symbols* [slots/constants].    (011)

Again, slots are only one way to do this, not as 
widely used as binary properties. In general, 
there can be relations of arbitrary arity 
(possibly encoded by binary 'list' structures, as 
in OWL/RDF). And there can be function symbols or 
not: this is something of a toss-up. Function 
names are essentially syntactic sugar.    (012)

>- *variables* [?].    (013)

Matter of taste. Some folk like syntactically 
distinguished variables, others don't. Again a 
toss-up; there are pros and cons for either 
choice.    (014)

>Syntax: The syntax of TOL specifies how signs 
>may be combined into well-formed *terms*, 
>*sentences*, and units.
>
>Semantics:  Each well-formed unit has an 
>associated set of *models* that satisfy all of 
>its subtyping relations and constraints    (015)

That satisfy all the *sentences*, including those 
that specify typing relationships.    (016)

>and an associated *theory* (the set of all sentences true in all models).    (017)

That is the ontology itself (or its deductive closure.)    (018)

>  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).
>
>Inclusion: TOL has an isA relation between types 
>based on subsetting of their *instances*.    (019)

Not in all cases. For example, OWL-DL identifies 
subClassOf with subset of instances, but RDFS 
does not.    (020)

>  This is the predominant form of constraint. 
>Subtyping is usually either specified directly 
>or by transitivity [but could be entailed by 
>other axioms?].    (021)

Actually isA is usually understood as the 
relationship between an individual and its type; 
the relation between types is often called 
subClass. Yes, it may be entailed by other 
axioms. (Actually to be honest this varies 
between languages, and is a good hallmark of 
computational/deductive complexity.)    (022)

>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 __ ).]    (023)

That would be a matter to be handled by the language's syntax/grammar.    (024)

>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.
>
>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.    (025)

More usually, the TOL *is* the logical form. For 
example, OWL reasoners typically work directly 
with some form of OWL syntax.    (026)

Pat    (027)

>
>Example: See John F. Sowa's message to this list
>Sent: Monday, February 12, 2007 7:01 PM
>
>---
>
>What are the most important things I have misunderstood?
>
>What are your answers to my questions 1-4 above?
>
>Thanks,
>
>Jim H.
>
>* For your amusement, here are two paragraphs 
>from early in this message translated by Google 
>from English to Portuguese and back:
>
>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.*
>
>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.    (028)


-- 
---------------------------------------------------------------------
IHMC            (850)434 8903 or (650)494 3973   home
40 South Alcaniz St.    (850)202 4416   office
Pensacola                       (850)202 4440   fax
FL 32502                        (850)291 0667    cell
phayesAT-SIGNihmc.us       http://www.ihmc.us/users/phayes    (029)


_________________________________________________________________
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    (030)

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