I've quite a lot to ask, but for this post I'll explain what I've
been about. It's PhD research, but I came to category theory only
in the last year, so let me lay out my background.
1. Context.
The goal is to formulate coordinate systems as first-class entities
in programming languages. But what is a coordinate system, in
computational terms? Some more or less equivalent answers:
Operationally:
* The initial node, or any derived node, in a directed graph where the
edges are coordinate transformation functions.
Denotationally:
* A chart mapping from an open set into a vector space. (Manifold
theory.)
* A signature or ADT (where it appears as type F):
Types:
X ; coordinate tuples
T ; coordinate transformations
F ; coordinate systems
P ; points
Operations:
compose: T x T -> T
invert: T -> T
apply: T x X -> X
plot: F x X -> P
measure : F x P -> X
step: T x F -> F
Identities:
plot(step(t,f),apply(t,x)) = plot(f,x)
measure(f,plot(f,x)) = x
plot(f,measure(f,p)) = p
+ group identities for T
* A functor on a Cartesian closed category with additive structure,
preserving biproducts (vector bases); or more ambitiously, preserving
a set of invariant relations axiomatizing Euclidean geometry.
It's the simple linear case of this last, which I want to develop here.
2. Background.
I got this stuff originally from Arbib & Manes, Freyd, Barr & Wells,
and Pierce; while I bounced off Eilenberg and Asperti & Longo. What
I found I was stubbornly keeping out of the library was MacLane,
_Categories for the Working Mathematican_, and the 1985 _Category
Theory and Computer Programming_, with its nice essays by Rydehard,
Poigne, Pitt et al.
3. Essentials.
The foundations are Cartesian closed categories and abelian categories.
Briefly, CCCs have values, products and powers; while ACs have
abelian group structure on Hom-sets, a common zero, and biproducts;
as well as kernels and stuff which I'm not up with yet.
(I'm also still lost with limits and adjunctions. It's frustrating that
I can work through examples, and still miss the principle. I imagine
I really understood adjoints, a whole lot would snap into focus.)
4. Sketch Synopsis.
(Terminology:
domain = type = object
arrow = morphism
power domain = exponential = Hom-set (in CCCs)
)
4.1. CCC Isomorphisms.
CCC's are held together by domain constructors: 1, x, and [->],
with corresponding isomorphisms:
A =~= [1->A] ; domains have values
[M->A] x [M->B] =~= [M -> AxB] ; there are finite products
[MxA -> B] =~= [M -> [A->B]] ; Hom-sets are power domains
[NB! I get the impression that writers use "power domain" in a different
sense. "Hom domain", "arrow domain", "function domain" might all be
better.)
Also
A x B =~= B x A
for products in general. Products are associative, powers aren't.
4.2. The Field Domain.
To put it to work, assume primitive domains:
I stands for a finite index set
R stands for the reals, with the ring structure:
(+) : R x R -> R
(.) : R x R -> R
0 : 1 -> R
1 : 1 -> R
(-) : R -> R
(To turn R into a field, we have to break it up as a coproduct:
R = {0} + R-{0}
so that we can define
(^-1) : R-{0} -> R-{0}
but this complication can be left until kernels are opened up.)
R is a module, with a one-element basis {1}, and it's also its
own linear automorphism set,
R =~= L[R->R]
r <-> (lambda(.)) r
The vectorial properties, addition and scalar multiplication,
carry over to any domain [A->R]. For [A->R] to be a module,
there must be a finite basis for it. As far as I can tell,
being "finite" only requires that operations (e.g. sum) over
all elements are defined.
4.3. Biproduct from CCC.
Now bring in domain I. Equip it with an equality mapping, the
Kronecker delta:
(=) : I x I -> R : (i,j) |-> if (i = j) 1, else 0
With the CCC isomorphisms, plus R =~= L[R->R], this can be
expressed as:
delta : I x R x I -> R : (i,r,j) |-> if (i = j) r , else 0
and we use the usual exponential curry-eval diagram, and a bit of
extra currying, to resolve it to:
eta : I -> [R -> [I->R]] : i |-> (r |-> (j |-> if(i=j) r,else 0))
pi : I -> [[I->R] -> R] : i |-> ((j |-> x[j]) |-> x[i])
This expresses the biproduct (sketch diagram here)
eta i pi i
R -> [I->R] -> R
with (eta i) and (pi i) as injection and projection sets. The eta's
produce vectors, the pi's take components. In effect they are a
vector basis and a covector basis for [I->R].
We want a name for this category; I don't know what the standard is,
so I'll refer to the domain [I->R] as X within the category, and
X(I) for the category itself.
4.4. Duality Functor
The contravariant hom-functor X(I)(-,R) gives the dual category,
which we could call X*(I) = Xop(I). The hom-functor action is:
X(I)(-,R):
A |=> [A->R]
f: A ->B |=> f#: [B->R] -> [A->R]
In particular, this gives:
(pi* i) = (eta i)# : [X->R] -> R : x* |-> x* eta i
(eta* i) = (pi i)# : R -> [X->R] : r |-> r pi i
and
(eta** i) = (eta i)##
(pi** i) = (pi i)##
after some fiddling around with [1-> ]'s.
4.5. Chart and Transformation Functors.
Next, suppose we have another category, say P, with its own
copies of I and R as well as a domain E. And suppose there is
an isomorphism:
f : E -> X
~f : X -> E
then (as far as I can tell), it defines an invertible functor:
Chart(f): P -> X(I)
with the action:
R |=> R
I |=> I
E |=> X
eta i |=> ~f eta i : R -> E
pi i |=> (pi i) f : E -> R
and Chart(f), at last, is what we mean by a coordinate system!
Thirdly, if we have a matrix:
m : I x I -> R
and require its adjoint to be defined (i.e. it's non-singular),
then
t(m) = Sum(i,j) ( t<i,j> (eta i) (pi j) ) : X -> X
defines a functor as above:
Trans(t(m)) : X(I) -> X(I)
The adjoint matrix has to be defined, to preserve the biproduct.
If it isn't, the dual functor won't define a surjection.
4.6 Category: XTFP(I)?
Now let me put together what I think I've got. (If I'm qualifying
assertions a lot, that is because the concept is clear enough for
making assertions, but the hard work is only half done.)
Overall, we have a collection of categories which we can denote
{Trans(t)(X), I, Trans(t) eta(X), Trans(t) pi(X)}
including the structure
X(I) = {[I->R], I, eta, pi}
which we first made up (and which remains somewhat special, because
it's the only one for which the eta's and pi's are the columns and
rows of the identity matrix, i.e. Kronecker delta for I).
Make a category of this collection. Its domains will be the categories
in the collection, and its arrows will be the transformation functors
Trans(t(m)). Call this XT(I); perhaps a nicer name would be
Bases(I).
But more, we can include XT(I) in a larger category, of images of
the whole thing. This will be a category of domains P, with associated
chart functors Chart(f): P -> X.
It would be reasonable to call the the category containing XT(I)
and the image of it defined by a single P and F, XTF(I,P) or
Altas(I,P). And the whole gazoo, comprising as many of these as
we care to make up P's, we can call XTFP(I), or LinearGeometry(I).
4.7 Back to ADT's.
One test of whether the construction has gelled, is to match it
against the ADT signature at the beginning. That signature is
what I was originally calling "XTFP", before I started using
categories, and the reason I've gone in for categories was to
impose on it a discipline of function domains and ranges.
The core of the signature is:
Operations:
compose: T x T -> T
invert: T -> T
apply: T x X -> X
plot: F x X -> P
measure : F x P -> X
step: T x F -> F
With the categorial development, write this as:
compose : (t1,t2) |-> t1 t2
invert : t |-> ~t
apply : (t,x) |-> t x
plot: (f, x) |-> ~f x
measure: (f,p) |-> f p
step: (t,f) |-> t f
But also requiring:
invert: f -> ~f
The ADT is thus included in XTFP(I); but the latter now has a good
deal more structure, because it also contains R, with addition and
scalar multiplication defined on I x I x ... x I -> R, and all arrow
domains which are isomorphic to it via the CCC and R <-> L[R->R]
isomorphisms.
What's more, if we extend still further, to a category containing
XTFP(I) for all indices I, this larger category (XTFP) is exactly
Vect.
4.8 In Practice
The categorial version of the ADT is nice in some basic ways.
The identities, such as
plot(step(t,f),apply(t,x)) = plot(f,x)
come out like
~(t f) (t x) = ~f ~t t x = ~f x
with the cancellation being obvious, where the original is
rather ad hoc.
Considering this as an expression syntax, it's pretty readable.
In fact, this form is what I have, in an implementation of the
original ADT in Mathematica 2.2. I extend the types to lists
or arrays in the types, and the expression syntax then works
for regular hierarchic figures. I build small models in this
XTFP implementation: 3D stick-figure bicycles, fractals, etc.
I think of it as a more elaborate version of LOGO.
Part of what I'm wrestling with, is a way to use Mathematica's
substitution rules to make the t's and f's work _as_ Trans
and Chart functors. This is application of categories (to the
definition of functional programming languages) with a vengeance.
I haven't seen it done quite like this in the literature, but
then I may be missing something in denotational semantics or
typed-lambda, which states it all but states it obscurely.
4.9 Geometric Semantics
A big concern of mine, is that programming languages for graphics
and geometry lack geometric meaning. Because the conventions of
numerical representation are settled _during_ the analysis of a
modelling problem, and _before_ programming begins, the actual
code does not support any shifting between alternate representations;
that is, there's no such thing as change of variable, re-solving
equations for a different variable set, etc.
Bringing coordinate systems into a programming as first-class entities
is supposed to be a first step towards improving the state of affairs.
Now we can see coordinate systems and transformations as functors,
the problem can be seen as, how to keep the language in a form to
which functors can be applied.
The immediate successes in geometric semantics with XTFP(I), are
1. Points and their coordinates are distinguished.
2. Covariant and contravariant vectors are distinguished.
3. Active and passive coordinate transformations are distinguished.
4.10 The Further Prospect.
The basic operation in XTFP(I) turns out to be: substitute for the
eta i and pi i, any equivalent set of basis vectors.
Looking back, it impresses me that we can get all this from:
1. Field structure on R
2. Equality on I
The next thing to go for, is the remainder of tensor analysis.
The compounds
eta i pi j
pi i eta j
are arrow-successive; but there is no tensor product defined,
to make
eta i eta j
meaningful, for instance.
Further, up til now we have made minimal use of structure on I.
But there are some obvious morphisms between XTFP(I)'s, for
different I's.
In particular, if we have I, then we have the lattice of subsets
of I; and these subsets index related spaces, with related vector
bases. E.g. if
I = (1,2,3,4)
indexes vectors in R^4 = [I->R], then
I<I = ((1,2),(1,3),(1,4),(2,3),(2,4),(3,4))
indexes bivectors. The combinatorics of the I's implies the
form of the cross-product function, that is, how to arrange the
2x2 minors of a matrix {x1,x2} with x1,x2 in X(I). So to speak.
I'm working on a smooth way to formalize this in general. The
essential concept is that there must be some _functor_ from the
category of I's and combinatorial operations, to the category
of the graded subspaces (scalar, vector, bivector,..,(n-1)-vector,
determinant) of X(I). It's one of those cases where one is sure
that someone must have done such a thing already, but one can't
find it in the literature.
4.11 Thanks for Listening.
That's the state of play.
I guess my conclusion on categorial development, is that you can
spend a lot of effort getting to the elements of the area you want
to model; but when you've done it, you have a formalism that's
pretty well purged of ad-hoc assumptions. It's done with the
absolute minimum.
Now, everyone wants feedback on their ideas, and I'm no exception;
but I'm not expecting anyone to review this in detail. What would
help me a lot is any indication that others have gone up the same
route, of combining CCCs or lambda-calculus with arithmetic, to
define vector analysis in the same sort of way.
That's all. Now I'll be hoping to gain some enlightenment from
listening in to your discussions.
-------------------------------------------------------------------
Jonathan Burns |
burns(a)latcs1.lat.oz.au| I don't care what the Dark Matter is
Dept.Computer Science | as long as it's not spiders.
LaTrobe University | - The Classic .sigs
-------------------------------------------------------------------
