Models of Sharing Graphs A Categorical Semantics of let and letrec

Models of Sharing Graphs presents a sound mathematical basis for reasoning about models of computation involving shared resources, including graph rewriting systems, denotational semantics and concurrency theory. An algebraic approach, based on the language of category theory, is taken throughout this work, which enables the author to describe several aspects of the notion of sharing in a systematic way. In particular, a novel account of recursive computation created from cyclic sharing is developed using this framework.

1 Introduction.- 1.1 Computation Involving Shared Resources.- 1.2 Sharing Graphs as Models of Sharing.- 1.3 Sharing Graphs and Their Presentation.- 1.4 Categorical Models for Sharing Graphs.- 1.5 Relating Models.- 1.6 Recursion from Cyclic Sharing.- 1.7 Action Calculi as Graph Rewriting.- 1.8 Overview.- 2 Sharing Graphs and Equational Presentation.- 2.1 Sharing Graphs.- 2.2 Acyclic Sharing Theory.- 2.3 Cyclic Sharing Theory.- 2.4 Rewriting on Sharing Graphs.- 2.5 Equational Term Graph Rewriting.- 3 Models of Acyclic Sharing Theory.- 3.1 Preliminaries from Category Theory.- 3.2 Acyclic Sharing Models.- 3.3 The Classifying Category.- 3.4 Theory-Model Correspondence.- 3.5 Modeling Rewriting via Local Preorders.- 4 Higher-Order Extension.- 4.1 Higher-Order Acyclic Sharing Theory.- 4.2 Higher-Order Acyclic Sharing Models.- 4.3 The Classifying Category.- 5 Relating Models.- 5.1 Preliminaries from Category Theory.- 5.2 Higher-Order Extension.- 5.3 Notions of Computation.- 5.4 Models of Intuitionistic Linear Logic.- 6 Models of Cyclic Sharing Theory.- 6.1 Traced Monoidal Categories.- 6.2 Cyclic Sharing Models.- 6.3 The Classifying Category.- 7 Recursion from Cyclic Sharing.- 7.1 Fixed Points in Traced Cartesian Categories.- 7.2 Generalized Fixed Points.- 7.3 Higher-Order Cyclic Sharing Theory.- 7.4 Cyclic Lambda Calculi.- 7.5 Analyzing Fixed Points.- 8 Action Calculi.- 8.1 Action Calculi: Definitions, Basics.- 8.2 Action Calculi as Sharing Theories.- 8.3 Extensions.- 9 Conclusion.- A Proofs.- A.1 Proof of Proposition 6.1.5.- A.2 Proof of Theorem 7.1.1.- A.3 Proof of Theorem 7.2.1.- A.4 Proof of Proposition 7.1.4.- A.5 Proof of Proposition 7.2.2.