Re: Insights: adjunctions and languages

Re: Insights: adjunctions and languages

[categories]

Date: Fri, 30 Jan 1998 10:36:58 -0500 (EST)
From: F W Lawvere <wlawvere@acsu.buffalo.edu>


     Mathematicians and computer scientists who have developed
a clear vision of the relation between lambda calculus
and cartesian-closed categories, as Jonathan Burns evidently
has, may wish to consider the following PROBLEM:

     1.  There is a great deal of technical development of
the presentational machinery of lambda calculus.

     2.  Lately, there have been interesting advances in the
study of the algebraic theory of exponential rigs, which
Tarski called "the high school" theory. (See papers of
Stanley Burris et al. on counter examples by Wilkie et al.
to naive completeness conjectures.)
    
     3.  There are many objectively (or semantically)
arising examples of cartesian-closed categories in the form
of presheaf toposes, such as that of finite directed graphs
or of discrete dynamical systems (as explained in our recent
elementary book published by Cambridge).

     4.  The rich variety of models mentioned in 3. has apparently
NEVER BEEN DIRECTLY RELATED to the abstract theory of lambda
calculus, nor to the theory of exponential rigs.  In the latter
case, although specific models are of great interest, they
have been constructed by formal syntactical means, rather than
through the "objective number theory" means via Steiner-Cantor-
Burnside-Grothendieck-Schanuel abstraction from these concrete
categories of combinatorial structures, in which the exponent-
iation operation has a very explicit mathematical content and 
construction. Although the exponential rigs capture only
the "existence of isomorphisms" equations between objects
as opposed to the detailed knowledge of given morphisms
(usually not iso) between the combinatorial structures and
the detailed particular operations that lambda calculus 
eventually wants to apply to, nonetheless already at that
level nontrivial equational questions arise.  For example,
there are often "connected" objects A which satisfy equations
B^A + C^A = (B+C)^A, and there are sometimes sufficiently
separating "figures" or "elements" of connected shapes.
As another example, exponential objects occasionally are
actually polynomial in the sense that B^A is actually iso-
morphic to F(A,B) where F is a combination of products and
co-products;  two cases that I know of are, with B = A,
F = 2A^2 and F = 1+A.  The latter has a clear intuitive
interpretation that the only internally definable endomaps
are either identity or constant.  But it is an open PROBLEM
whether there are any other polynomials  F  for which there
exists a finite presheaf topos, in which there exist objects
A enjoying such isomorphisms.


				

Insights: adjunctions and languages

[categories]

Date: Thu, 29 Jan 1998 17:55:05 +1100 (AEDT)
From: Jonathan Burns <burns@latcs1.cs.latrobe.edu.au>


Hello and goodwill

Now that I have my PhD dissertation submitted, I've had a while to
stand back from the material, and consider the categorial territory
that I stumbled into in the last year or so. Although I'm acquainted
with a mere fraction of the crucial concepts here, what I have found
seems to contain really elegant insights into computer languages, and
I want to clarify these to myself, as a philosophical basis for
future study.

It may well be that it will all be old news here, but the introductory
texts don't spell things out in quite the way I perceive them. (My
reading started out wide, but narrowed down mainly to MacLane, Barr
and Wells, and articles by Ridenour in some S-V workshop proceedings
some years back. Asperti and Longo has been good too.)

To cut to the chase, consider Cartesian closure. If we leave out matters
of storage, scoping and other time-related resources, a Lisp-family
language is lambda-calculus with a reduction policy - that is, a set
of decisions that one expression form is to be replaced by another.
(For Lisp, the policy is to do beta- and eta-reduction in some order
until no more redexes can be found.) And lambda is a CCC with name
binding - as opposed to expressing everything with projectors.

But more: a CCC is defined by adjunctions: unique-terminal, diagonal-
product, product-exponential. These adjunctions define isomorphisms
between expression forms:

	f = n (F g)
	g = (G f) u

where u and n are unit and counit. In other words, the isomorphisms are
determined by natural transformations, of a very simple and intuitive
kind: if you can have one of a thing, you can have two of them; if you
can have one thing and another, you can have both together in a product;
if you have a product expression, then you can have a product expression
constructor (exponential) with one term curried out.

These natural transformations are universal structural operators;
inherently polymorphic or domain-free, in programming terms. And using
only a handful of them, you can define these isomorphisms, which then
constitute an equational theory for a language - in the sense that
lambda is the equational theory behind Lisp.

Whatever can be defined by adjunctions is what they call "referentially
transparent": equals are substituted only for equals. It's stronger than
that, in fact, because with an adjunctive system like this, an expression
can be substituted for another only when there is also a rule for the
reverse substitution. E.g.

	x * x = square x

The referentially-transparent equational theory stands by itself. But on
top of it, we may now impose reduction policies, ("games") of various kinds:

1. We can substitute equals for equals by hand: "just doing algebra".

2. We can specify an algorithm for substitutions: intepreters.

3. We can extend this to interpreters where we introduce new reduction
   rules as we go along: symbolic algebra systems.

4. We can specify a data-directed backtracking algorithm, which is allowed
   to apply a reduction rule in either order: equational logic systems.

5. We can specify a data-directed heuristic backtracking algorithm:
   dunno quite what we call these, maybe constraint systems.

6. We can specify systems which not only use backtracking and heuristics,
   but assert and retract additional rules as we go along: traditional AI.

"Extending the rules" is a dangerous game, of course; you have the
responsibility for maintaining referential transparency. Nobody I've
read has hinted at the possibility of automating the definition of
equational rules by adjunction. Even if such a thing could only be
done in a very restrained sense, though, it would still be very
powerful. Vaguely, I think the rubric has to be: OK, here's the kind
of data we want to work on - regular expressions, perms and coms,
machine code, whatever - now, what are the equivalences we see in
these domains, and are they isomorphisms? And if so, _why_ are they
isomorphisms, and what natural transformations might possibly define
them by adjunction?

The key insight for me, the thing that categories has revealed, is that
reduction polices for equational theories are _the_ bridge between the
declarative and the procedural; and equational theories can be built
by adjunction from universal constructors. It's so beautiful I just
want to sit and gaze at it. It's one of those obvious things that you
see side-on for years, and then suddenly you see it directly.

More later.



Jonathan Burns        |  
burns@latcs1.lat.oz.au|  A student approached Susskind, in hopes 
Computer Science Dept |   of understanding the lambda-nature...
La Trobe University   |