SUO: Catagory Theory languages and translations
I sent the following message to David Espinosa, who worked at Kestral on Specware for a number of years. His response follows.
David,
> During our visit to Kestrel in summer 98 (with Rob Jasper), I remember you
> making a comment to the effect that the hub-and-spokes model for translation is
> passe, and the wave of the future is point to point translation between
> logics.
> As I understood you, the idea was to use category theory to formally
> define the relationship between two well defined logics, and to use that as the
> basis for defining a semantics-preserving translator which would convert
> sentences from one logic to another.
> Is this based on the General Logics paper by Meseguer?
> I wondered if you knew of any references to work along these
> lines by you or anyone else?
> Also, do you know how it compares to the work
> described in the following paper by Ciocoiu and Nau?
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 10:12 PM
To: Uschold, Michael F
Subject: Re: languages and translations
Heterogeneity vs homogeneity
----------------------------
However how we try to define standards, the world is heterogeneous.
Sooner or later someone makes a new, incompatible variation. Homogeneity is pretty unstable. So we'll definitely need translations between systems.
As for how to build them, sure, it's nice if you can find a common language, but that language probably won't capture every feature of every language. It's nice for translating a subset, but sooner or later you think of a nice way to map construct C1 of L1 into construct C2 of L2, and it won't go through the common language. So you have to revert back to individual translations, which are the general case.
The real point is that we shouldn't get stuck on the idea of a common language-if it emerges naturally, great, but there's nothing wrong with a big collection of translations. The same goes for any collection of format or datatypes or whatever. Look at how we program these days:
C, Lisp, Java, Perl, Python, a bunch of Unix tools, MS Excel, whatever gets the job done.
What's a language?
------------------
For the moment, I take a language to be a category (of specifications and morphisms, but we don't go into detail about those-it's just a category). And a language translation is a functor-again, we don't go into any more detail.
> Are your ideas based on the General Logics paper by Meseguer?
They are certainly inspired by it. But I think Meseguer's notion of entailment system yields the wrong category of specifications. He writes that m = m' if for all source symbols f, m(f) = m'(f). What you really want is that m = m' if m(f) is provably equal to m'(f) for all f. As far as I can see, to repair the definition, you either need to open up the category of signatures, so you can get at the individual symbols, or close up the category of specifications and say it's just a category, which is what I prefer.
Gluing languages: a formal construction
---------------------------------------
In fact, we can view the collection of languages and translations as a universal language. I'll give the formal construction (called the Grothendieck construction), but the concept is simple: we simply throw them together and call the result a language. I apologize for my bad description of the construction; as with all mathematical constructions you have to study the details to really get it, and I'm not providing the full set of details here (although I come close). But I'm hoping there is some intuition here that will be valuable to you.
Here's how the construction works on sets. Given a bunch of sets and functions between them, we erase the boundaries between the sets (i.e. take a disjoint union). We also erase the boundaries between the functions.
So instead of having a squaring function as an arrow, we have each of its actions as an arrow: 5 maps to 25, 3 maps to 9, etc.
You can read about in the first edition of Barr and Wells' Category Theory for Computing Science. I think it's also in the electronic supplement to the second edition, which is available online. I strongly encourage you to read about it, since it's simple once you get the concept, and then you see it everywhere. This is true of a lot of categorical notions.
Anyway, here's how it works in the case of specifications and translations.
The specifications of the universal language are the disjoint union of the specifications of the individual languages; that is, each is tagged with the logic that it's written in. Given a spec S1 in language L1 and a spec S2 in L2, the morphisms from S1 to S2 are pairs of a translation from L1 to L2 and an L2 specification morphism from t(S1) to S2.
As for composing the morphisms, here's the picture. Check the references for the full details.
S3
^
|
| m2
|
|
S2 - - - - -> t'(S2)
^ ^
| |
m1 | | t'(m1)
| |
| |
S1 - - - - -> t(S1) - - - -> t'(t(S1))
L1 ----t----> L2 -----t'-----> L3
The composition of (t, m1) and (t', m2) is the pair (t' o t, m2 o t'(m1)). You can think of each specification as "lying over" the logic it's written in; that's why I drew it that way.
One point worth noting is that the Grothendieck construction is a very weak gluing-I think it actually produces a "lax colimit" (whatever that is!). It doesn't really identify a spec with it's translation- they both exist, and there's a spec morphism from one to the other given by (t, id).
If you want the models of this synthetic universal language, I think you'll also have to glue the models of the original languages together in the same formal way. I've never thought about that. Meseguer may have written about this in the last couple years-check his colimit of diagrams paper.
Can you use category theory to build translations?
--------------------------------------------------
> As I understood you, the idea was to use category theory to formally
> define the relationship between two well defined logics, and to use that as the
> basis for defining a semantics-preserving translator which would convert
> sentences from one logic to another.
To build a translation other than by composition, you have to open up the languages and see what's going on inside them. Categorical logic could help you do that, but more likely, it will help you formalize what you already know. Here are some references, but this is quite technical stuff:
Andrew Pitts, Categorical Logic, handbook chapter.
Roy Crole, Categories for Types
Bart Jacobs, Categorical Logic and Type Theory
You could try Pitts, and some of Crole. Jacobs is for specialists.
References
----------
> I wondered if you knew of any references to work along these
> lines by you or anyone else?
There are also many papers about gluing logics. I've seen some papers by Gillian Hill, and also the book "Fibring Logics" by Dov Gabbay (Oxford University Press). But I haven't read enough of this literature. Keep looking-you'll find a lot.
> Also, do you know how it compares to the work
> described in the following paper by Ciocoiu and Nau?
I don't, but looking at that paper, it seems quite clearly written (and short). So you should be able to come to conclusions yourself (sorry I haven't time to read it!).
Keep up the good thoughts!
David