A Categorical Semantics of let and letrec

*Abstract:*

A general abstract theory for computation
involving shared resources is presented. We develop the models of
*sharing graphs*, also known as term graphs, in terms of both
syntax and semantics.

According to the complexity of the permitted form of sharing, we consider four situations of sharing graphs. The simplest is first-order acyclic sharing graphs represented by let-syntax, and others are extensions with higher-order constructs (lambda calculi) and/or cyclic sharing (recursive letrec binding). For each of four settings, we provide the equational theory for representing the sharing graphs, and identify the class of categorical models which are shown to be sound and complete for the theory. The emphasis is put on the algebraic nature of sharing graphs, which leads us to the semantic account of them.

We describe the models in terms of the notions of symmetric monoidal categories and functors, additionally with symmetric monoidal adjunctions and traced monoidal categories for interpreting higher-order and cyclic features. The models studied here are closely related to structures known as notions of computation, as well as models for intuitionistic linear type theory. As an interesting implication of the latter observation, for the acyclic settings, we show that our calculi conservatively embed into linear type theory. The models for higher-order cyclic sharing are of particular interest as they support a generalized form of recursive computation, and we look at this case in detail, together with the connection with cyclic lambda calculi.

We demonstrate that our framework can accommodate Milner's
*action calculi*, a proposed framework for general interactive
computation, by showing that our calculi, enriched with suitable
constructs for interpreting parameterized constants called
controls, are equivalent to the closed fragments of action calculi
and their higher-order/reflexive extensions. The dynamics, the
computational counterpart of action calculi, is then understood as
rewriting systems on our calculi, and interpreted as local
preorders on our models.

This report is available in the following formats:

- PDF file
- Gzipped PDF file
- PostScript file
- Gzipped PostScript file
- PostScript file with Type 1 fonts
- Gzipped PostScript file with Type 1 fonts