Paul, (01)
A lattice of theories is *not* developed. It is
like the integers: it has resided for all eternity
in a Platonic heaven of mathematical structures. (02)
It imposes no restrictions whatever on how anybody
does or should or might think or act. It's like the
integers: they don't tell you how many people do or
should or might be counted in the next census. But
they provide us some assurance that there will exist
an appropriate integer in that Platonic heaven to
count whatever number of people might exist at the
time the census counting is done. (03)
> So how are lattice of theories developed? (04)
What are developed are particular statements of
theories that people or computers write (or type). (05)
When a theory is developed, an integer can be plucked
out of that Platonic heaven, such as #17, and be
pasted as a label on that theory. (06)
Instead of using integers to label the theories, I am
proposing that we adopt that lattice from the Platonic
heaven. The reason why a lattice is better than the
integers is that the integers are linearly ordered,
but a lattice has a partial order, which allows more
options in the way one theory is related to any other. (07)
Then whenever anybody writes a theory, we may be able to
show where it fits in the lattice in relation to any other
theory that has been developed or the infinitely many
other potential slots for theories that nobody has yet
developed (or written or typed). (08)
There is one qualification that I haven't mentioned: to
show whether theory A is a generalization, a specialization,
a sibling, or a distant cousin of another theory B requires
a theorem prover. Sometimes that theorem prover will give
us an answer very, very quickly. But other times, it might
take a long time -- perhaps it might never come back with an
answer. (09)
But not to fear: this limitation is exactly the same limitation
that programmers face every day: proving that any given program
is correct or even that it will eventually stop is undecidable. (010)
Yet programmers live with that undecidability every day, and
they even take *advantage* of the insights from the idea to
adopt *structured* methods for designing programs so that it
is possible to guarantee, in advance, that they will stop or
that they will have certain desirable properties. (011)
That is my fundamental reason for recommending a lattice: it
suggests certain *structured methods* for designing a theory
so that it is determined *in advance* where it will fit in the
lattice -- sometimes the exact place and sometimes within the
right ballpark -- i.e., there may be cases where it is unknown
whether two apparent siblings happen to be identical twins. (012)
There is more to be said about structured methods, but the
main point I want to make is that they are like structured
programming: lattices don't restrict the subject matter of
the ontologies you write, but they provide guidelines that
make them easier to analyze, understand, debug, and test. (013)
John (014)
_________________________________________________________________
Message Archives: http://colab.cim3.net/forum/ontac-forum/
To Post: mailto:ontac-forum@xxxxxxxxxxxxxx
Subscribe/Unsubscribe/Config:
http://colab.cim3.net/mailman/listinfo/ontac-forum/
Shared Files: http://colab.cim3.net/file/work/SICoP/ontac/
Community Wiki:
http://colab.cim3.net/cgi-bin/wiki.pl?SICoP/OntologyTaxonomyCoordinatingWG (015)
|