SUO: Re: IFF LOT Glossary
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
Robert,
I will try to work through this next part piece by piece.
| We extend this terminology to categories in place of sets
| and functors in place of functions. There is a functor
|
| base : Theory --> Language
|
| from the category of theories to the category of languages.
I still can't see a theory T as anything but a subset of a language L.
It helps me a little bit to write the names of categories in the plural,
so as not to confuse them with individuals. It also helps if I treat the
arrows of Arr(C) as the primary entities in the category C, recovering the
objects of Obj(C) as secondary entities by collecting all the entities that
appear in s(f) = Source(f) and t(f) = Target(f) as one ranges over all of the
arrows f in Arr(C). The last time that I tried to do "categories by computer",
I was using the following shapes of data structures, and so I still have these
sorts of pictures in my head:
Category C o
/|\
/ | \
... | ...
|
Arrow f o
/ \
s t
/ \
s(f) o o t(f)
A functor, then, is something that I picture like this:
Functor F o
. | .
. | .
. | .
. | .
Category C o o o Category D = CF
| ./ \. |
| . / \ . |
| . / \ . |
| . / \ . |
Arrow f o o o o Arrow fF
/ \ . . . . / \
/ .\ . . /. \
s . t . . s . t
/. \ . . / .\
o o o o
u v uF vF
This is a rough sketch of the actual data structures that I used to represent
a functor F as a "matching" between the parallel items of categories C and D.
NB. I will have to revert to the convention that I was accustomed to using
then, where all operators are applied on the right of their arguments.
What the picture says is that the functor F : C -> CF takes each arrow f in C
to an arrow fF in CF, and each object u in C to an object uF in CF, in such a
manner that (fs)F = (fF)s and (ft)F = (fF)t. To be a functor, F must satisfy
the following two system of equations:
(1_u)F = 1_(uF), for all u in Obj(C).
(f o g)F = fF o gF, for all composable f, g in Arr(C).
That was just how I kept track of things on the computer.
It is, of course, more usual to draw a "functor square" like this,
where we get one such picture for each object u and arrow f in C.
F
u o-------->o uF
| |
| |
f | | fF
| |
v v
v o-------->o vF
F
Okay, let me see if I have refreshed my memory
enough to tackle what you've been saying here.
There's a functor called "base" from the category of theories
to the category of languages, base : Theories -> Languages.
base
Theories o------------>o Languages
/|\ /|\
/ | \ / | \
... | ... ... | ...
| |
| base |
Theory U o------------>o Language L = base(Theory U)
| |
| |
Th-Arr f | | Lang-Arr g = base(Th-Arr f)
| |
| base |
Theory V o------------>o Language M = base(Theory V)
Okay, I think I'll rest here. Let me know if
I've got the structural aspects right so far,
and then I can try to move on to the content.
Jon Awbrey
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
| Consider the object function
|
| obj(base) : obj(Language) --> obj(Theory)
|
| of the base functor. Given any theory, this returns the underlying base FOL
| language consisting of the sets of relation, function and sort symbols used
| in the axioms and relational arities of the theory. The "base language fiber"
| refers to the "fiber of obj(base)"; that is, to the fiber of the function
| fib(obj(base)). For any language L in obj(Language), this returns the
| subclass
|
| fib(obj(base))(L) = {T in obj(Theory) | obj(base)(T) = L}
|
| of all theories of whose underlying base language is L.
| Here, fib(obj(base))(L), or fib(base)(L) for short, is
| called "the base fiber over L". This is the underlying
| set of the lattice of theories over L: LOT(L) = fib(base)(L).
|
| The morphic aspect of the base functor also comes into this picture.
| First of all, when the lattice of theories LOT(L) is regarded as part
| of the category of theories, there is a morphism g : T1 --> T2 between
| two theories in LOT(L) precisely when base(g) L --> L is the identity
| and T1 >= T2 in the lattice entailment order (T2 entails any axiom of T1).
| Secondly, for any morphism of languages f : L1 --> L2 in the category of
| languages, there are direct and inverse image functions
|
| dir(f) : LOT(L1) --> LOT(L2)
| inv(f) : LOT(L2) --> LOT(L1)
|
| that are adjoint monotonic functions. These are important for
| moving theories around, as the following paragraph indicates.
|
| A *diagram of theories* is the IFF representation for
| either an "unpopulated modular object-level ontology"
| or a "library of modules". Using the base functor,
| every diagram of theories T has an underlying base
| diagram of languages L = base(T). Take the colimit
| col(L) of this base diagram. Then the colimit of the
| diagram of theories col(T) is the direct image (flow)
| dir(inj_n) along the base diagram colimit injections
| followed by the meet in LOT(col(L)), the lattice of
| theories over col(L). Moreover, using the direct
| image (flow) dir(inj_n) moves the theories in T to
| the lattice of theories LOT(col(L)). Also, recall
| that we defined the notions of "monocosmic" and
| "polycosmic" in terms of the colimit of theories.
|
| RK: http://suo.ieee.org/email/msg10123.html
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o