Date: Thu, 29 Jan 1998 16:17:03 -0400 (AST) Subject: Insights: adjunctions and languages Date: Thu, 29 Jan 1998 17:55:05 +1100 (AEDT) From: Jonathan Burns 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 | Date: Fri, 30 Jan 1998 15:55:14 -0400 (AST) Subject: Re: Insights: adjunctions and languages Date: Fri, 30 Jan 1998 10:36:58 -0500 (EST) From: F W Lawvere 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.