Re: Computer language and category theory

From: Alfred Einstead (whopkins_at_csd.uwm.edu)
Date: 11/24/04 

Date: 23 Nov 2004 15:51:44 -0800

Jon Haugsand <jonhaug@ifi.uio.no> wrote:
> Is there any work done one computer languages and category theory?
[...]
> However, I don't like such animals. So I wonder if there is some use
> of category theory or something else that have been used to model
> language like constructs.

Any formalism for transition systems generalizes to something involving
categories. Suppose G = (Q,s,M,P) is a grammar; i.e., s is in Q,
Q is a set of variables, M is a monoid (the standard formalism admits
only free monoids M = X*, where X is then deemed the 'alphabet', but
everything works in the general case), and P is a subset of Q x M[Q],
where M[Q] is the free extension of M over the set Q (note then that
(X*)[Q] is just (X union Q)*).

A transition relation -> can be defined over M[Q] recursively by the
following conditions:
      (a) a -> a, for any a in M[Q]
      (b) if a -> b, b -> c, then a -> c, where a, b, c are in M[Q]
      (c) if (q,b) is in P then aqc -> abc, where a, c are in M[Q]

This has the following properties:
    * Let [a] = { m in M: a -> m }
      then
            [m] = {m} for all m in M
            Context freeness: [ab] = [a][b] for all a, b in M[Q]
            [q] = union {[a]: (q,a) in P}
    * if a -> b, c -> d then ac -> bd
    * the set { q = [q]: q in Q } is the least solution to the
      set-theoretic system defined from the grammar
          (i.e., where a rule q -> xry becomes the inequality
           [q] superseet of {x}[r]{y} for q,r in Q, x,y in M
           similarly for the other rules).

The morphisms are defined recursively by:
         I: a -> a
         if f: a -> b, g: b -> c then gf: a -> c
         (q,b): aqc -> abc

Alternatively, one can restrict the last family of morphisms
only to the following: (q,b): q -> b and then add another family
of the form
          if f: a -> b, g: c -> d then f x g: ac -> bd
given the property just cited above.

When the grammar is not cyclic then s is an initial object.
All the elements m of M are terminal objects. The language
L(G) is just [s] which is the set of elements m of M for
which morphisms f: s -> m exist. Each morphism corresponds
roughly to a derivation sequence.