Models of sharing graphs. A categorical semantics of \(let\) and \(letrec\) (Q4936346)

Shared resources are an important concept in computer science, with several different meanings and purposes. This dissertation uses sharing graphs (term graphs) as models of sharing: graphs are used for representing the sharing relations of resources, computations on them are realized as rewriting systems. A Graph Rewriting Theory (combining these two parts) is then a canonical and practically useful instance of such models for implementers of programming languages. The efficiency of computations, the investigation of side-effects and the relation between cyclic sharing and recursion are important topics to be dealt with. Chapter 2 defines sharing graphs as directed graphs with extra conditions and information. Additionally, an equational (i.e. algebraic) presentation of finite sharing graphs is given; sharing graphs are represented as term expressions of mildly relaxed algebraic theories enriched with constructs for sharing (let/letrec bindings). The equivalence between the graph-theoretical description and the equational presentation of finite sharing graphs is established for both cyclic and acyclic cases. Chapter 3 studies the category-theoretic models of acyclic sharing theories. The class of models is described in terms of symmetric monoidal categories and functors, the soundness and completeness could be shown similarly to the standard categorical type theory. Chapter 4 develops a higher-order extension of acyclic sharing theories (with lambda abstractions and applications). It is followed by a few case studies (chapter 5) where the first-order acyclic sharing theories and the higher-order ones are related. The relations to Moggi's notions of computation and to the intuitionistic linear type theory are considered as well. Chapter 6 introduces the models for cyclic sharing graphs which are based on traced monoidal categories and establishes the expected properties of these models. Chapter 7 is the most interesting part of the thesis. It combines the higher-order extensions with cyclic sharing. This results in a wider class of models of recursive computation which can be taken as an explanation of recursive computation from resource-sensitive cyclic computation. Furthermore, the theory is closely related to cyclic lambda calculi which have been studied as a foundation for implementations of functional recursive computations. Chapter 8 covers, as a special application, the representation of Milner's action calculi within the given framework. This thesis is part of the series of ``Distinguished Dissertations'' -- it is excellently written and gives very interesting results on a rather small space. Everybody who is interested in the theory of computing and its mathematical foundations will have a great pleasure to read this thesis. Naturally, it is not easy to read and requires a lot of formal training.