Re: SUO: FW: What can Category Theory do that traditional logic and model theory cannot?
This is begining to sound very interesting.
Citeseer (http://citeseer.nj.nec.com/) lists 77 citations to
"F. William Lawvere. Functorial semantics of algebraic theories.
Proceedings, National Academy of Sciences, U.S.A., 50:869--872, 1963.
Summary of Ph.D.
Thesis, Columbia University,"
many quite recent. Google.com gives
103 hits for `lawvere "functorial semantics"'. I don't have time right
now to see which ones (if any) actually give an overview---if anyone else
does
I'd be interested in the reference.
For those who don't know anything about category theory the small book
Conceptual Mathematics; A First Introduction to Categories
By F. William Lawvere,Stephen H. Schanuel
Cambridge University Press; 05/1996
is very readable at undergrad level -- in fact it assumes almost no
mathematics at all.
John Velman
john.r.velman@boeing.com
"Uschold, Michael F" <Michael.Uschold@PSS.Boeing.com>@majordomo.ieee.org on
08/22/2001 04:16:32 PM
Please respond to "Uschold, Michael F" <Michael.Uschold@PSS.Boeing.com>
Sent by: owner-standard-upper-ontology@majordomo.ieee.org
To: "DLU SUO (E-mail)" <standard-upper-ontology@ieee.org>
cc: "Chris Menzel (E-mail)" <cmenzel@philebus.tamu.edu>, "Michael
Gruninger (E-mail)" <gruning@nist.gov>, "John Sowa (E-mail)"
<sowa@bestweb.net>, "Uschold, Michael F"
<Michael.Uschold@PSS.Boeing.com>
Subject: SUO: FW: What can Category Theory do that traditional logic and
model theory cannot?
Here is another message in my exchange with David Espinosa.
Mike
****************************************************************************
**
NB: If you send email to me
1. from outside the Boeing Company or
2. from inside the Boeing Company, but not using Exchange
Then, as of August 24 2001 you must use the following email
address: michael.f.uschold@boeing.com. Other addresses,
such as mfu@redwood.rt.cs.boeing.com or
michael.f.uschold@PSS.boeing.com won't work.
Please update your email address books accordingly.
****************************************************************************
**
-----Original Message-----
From: David Espinosa [mailto:davidespinosa@pacbell.net]
Sent: Tuesday, August 21, 2001 11:04 PM
To: Uschold, Michael F
Cc: Chris Menzel (E-mail)
Subject: Re: What CT can do that traditional logic and model thy
cannot?
> If you have no time/interest to to
> continue this, perhaps you could recommend to me people who I might
pursue
> this with.
Talking is always fun, but I really don't have much time! You're welcome
to
publish this message-it's a little dogmatic, but I'm sure no one will take
it as gospel. :)
> There is a real dearth on the Standard Upper Ontology list of any decent
> understanding of Category Theory (CT). I know almost nothing, but I know
a
> lot more than most of them, which is about zilch. I believe that CT
offers
a
> very powerful way to relate theories, and can be helpful both in creating
> larger theories from smaller ones, as well as providing a basis for
mapping
> and translation, but I cannot make the argument.
Looks like you need to study more if you think it's important. It's really
not voodoo, you know. Barr and Wells is pretty accessible.
It's also important to understand Lawvere's 1963 theory of functorial
semantics. That's not so hard, and it's one of the more beautiful theories
of the last century, if you like semantics. I'm trying to think where I
read it. Probably Pitts's paper and Crole's book are close enough. It's
basically this correspondence:
Category theory Logic
--------------- -----
category theory
functor interpretation
functor to Set model
natural transformation model homomorphism
Lawvere's theory unifies models of a theory and interpretations of one
theory into another by saying that a model is an interpretation into the
canonical theory of sets.
> If it is true, then the SUO effort could benefit greatly.
Category theory helps if you're trying to build a system that manipulates
and relates lots of theories. If you're working in subsets of one big
theory, it's not as useful. And inference (KR in the small) is more
important than theory (KR in the large) anyway.
As for the SUO effort, I don't believe in standardization, at least not if
it's difficult to achieve. Like-minded people should get together and
resolve minor differences. If there are major differences (category
theorists vs logicians would be pretty major), they need to split up and
make their own separate standards. I certainly don't believe in one group
or individual dictating to another.
I also don't believe in talking (bet that surprises you!). One of the nice
aspects of computer science is that we can build systems, not just talk
about them. It seems like standards bodies do more talking than building.
Similarly, a "standard ontology" is something of an oxymoron to me, again,
because of my preference for heterogeneity. How can you possibly tell me
how to see the world? Instead, give me some tools I can use to relate my
view to yours, in case I'm motivated to do so.
> There are some very very knowledgable people in traditional logic and
model
> theory who are not motivated to study CT because they have yet to see
> anything that the former cannot do that the latter does, though they are
> quite open to being shown. I am unable to articulate an argument, because
my
> CT understanding is so minimal.
The "many theories" view of the world is particularly well-adapted to
categorical methods. These theories are abstract data types, which are
useful in mathematics and some aspects of programming. I don't know how
useful they are in knowledge representation and reasoning.
The real action in any case, is in inference. Organizing the world in
terms
of theories does give you some leverage there, since you can push theorems
across theory interpretations, but it doesn't give you enough. Categorical
logic could give you more, but it's really just an alternative presentation
of standard logic. Mike Healey has been interested in building a
category-theory based theorem prover along these lines-why don't you give
it
a try? You could start with a very simple logic.
By the way, the Handbook of Automated Reasoning has just been published,
and
I'd advise you to read as much of it as you possibly can. I used to be
against formal logic in AI, but then I decided that if computers are going
to think, they may as well think clearly.
> On the off chance that this matter is of
> sufficient interest to you, I invite you to make such an argument and
pass
> it along to me for posting on the list.
I'm not sufficiently religious about it. I think they should build their
systems however they see the world, not how I see it.
> Here is a sample message from Chris Menzel, a philosopher and a logician
and
> a very very bright chap. It summarizes this situation fairly well. I
would
> love to motivate him to study CT, because there is noone active on the
SUO
> effort that understands both, and can clearly articulate the
relationship,
pros and cons.
Why not you? Where there is a will, there is a way. Again, category
theory
isn't voodoo. It's just a branch of abstract algebra (well, it's really
the
trunk of the tree, but never mind).
> Me, I don't care. I'm all for using whatever framework is most powerful
> and appropriate. But can you, or anyone, provide us with one concrete
> example of a shortcoming in the traditional framework of first-order
> syntax, proof theory, and model theory that would necessitate moving to
> a framework as abstract and (to most) unfamiliar as category theory?
As for KR in the small, no one has built a theorem prover based purely on
categories. But there are many provers based on FOL. So I'm afraid FOL
wins in terms of standards. A category-based prover is a subject for
reasearch, not standardization.
As for KR in the large, if you want to build a system based around theories
and theory interpretations, you are going to use some amount of category
theory whether you like it or not. But perhaps modular theories aren't
important to you, and you prefer one big theory (or subsets of it). Then
you have a lattice, which is still a category, but sufficiently degenerate
that category theory isn't that relevant.
But, again, the action is in inference. And better to be doing knowledge
representation and *reasoning* (automated, preferably) than talking about
it.
> There is another issue that arose recently. Claims are being made that it
> would be easy to build an interface to a knowledge representation system
> which used CT under the covers, but which did not require anyone to
learn
> any CT.
That claim is actually easier to prove than disprove: build one.
> This seems quite contray to the experience at Specware, but I do not
know.
Failure in one case doesn't prove impossibility. However, success in one
case *does* prove possibility. At least they are trying at Kestrel, not
just talking (well, some are doing, some are talking, like anywhere).
> Again, if you have interest in this and can respond, or put me in
> touch with others who might be interested, please do so.
If you write to Cordell and/or John Anton, I'm sure they can suggest
someone
at Kestrel.
Best wishes,
David