<p>I do not have a proper answer, but you might want to have a look at <a href="https://content.iospress.com/articles/fundamenta-informaticae/fi22-1-2-1" rel="nofollow noreferrer">this paper by Asperti</a> where there is a study of sharing graphs inspired by category theory.</p>

CC BY-SA 4.0
2021-11-05T17:32:07.970Z
2021-11-05T17:32:07.970Z
Beniamino Accattoli
<p>A "sharing graph" is a representation of a <span class="math-container">$\lambda$</span>-term that modifies an abstract syntax tree by adding edges connecting each variable use to the place where that variable is bound.  They are used in Lamping's "optimal" reduction algorithm to do <span class="math-container">$\beta$</span>-reduction by local edits, not duplicating any terms until necessary.  My understanding is that this works very directly for linear <span class="math-container">$\lambda$</span>-calculus (and is more or less a different representation of proof-nets for linear logic with <span class="math-container">$\multimap$</span> only), but in the nonlinear case one has to introduce (as with proof-nets) explicit multiplexing (i.e. contraction) nodes and some kind of "level marker" (i.e. the linear <span class="math-container">$!$</span> modality).  The initial encoding of a <span class="math-container">$\lambda$</span>-term as a sharing graph corresponds to the embedding of intuitionistic logic into linear logic as <span class="math-container">$(P\to Q) = (!P\multimap Q)$</span>, and once the optimal reduction is complete, one then has to perform a "read-back" to obtain an ordinary <span class="math-container">$\lambda$</span>-term in normal form since not every sharing graph is itself the translation of any <span class="math-container">$\lambda$</span>-term.  (Please correct me if I said anything wrong.)</p>

<p>Now, linear logic has categorical semantics, depending on the kind of linear logic under consideration.  Intuitionistic linear logic corresponds to symmetric monoidal categories (or multicategories), classical linear logic to linearly distributive categories (or polycategories),  the modality <span class="math-container">$!$</span> to a "Seely comonad", etc.  In particular, it seems to me that we could regard sharing graphs (<em>qua</em> proof nets) as the terms in some linear logic, with the rewrites of Lamping's algorithm as axioms, and thereby interpret sharing graphs modulo optimal rewrites into any monoidal category with the appropriate structure and axioms.</p>

<p>My question is whether there is any such monoidal category providing a "semantics of sharing graphs" that performs the read-back into <span class="math-container">$\lambda$</span>-calculus.  In other words, is read-back defined "inductively" over the structure of sharing graphs in a sufficient sense that it can be characterized by their categorical universal property?  It feels as though some kind of Chu or Int construction might do the trick, perhaps applied to a presheaf model of HOAS, but I haven't been able to make anything come out.</p>

<p>I'm getting to the edge of my linguistic competence here, but I suspect that a related question would be whether Lamping's algorithm can be written in a "normalization by evaluation" style (e.g. if the category performing the read-back consisted only of normal forms).</p>

<lambda-calculus><semantics><interaction-nets>
Semantic read-back of sharing graphs
Mike Shulman
# Semantic read-back of sharing graphs

(Asked by: username_0 on 2019-10-03)

A "sharing graph" is a representation of a $\lambda$-term that modifies an abstract syntax tree by adding edges connecting each variable use to the place where that variable is bound. They are used in Lamping's "optimal" reduction algorithm to do $\beta$-reduction by local edits, not duplicating any terms until necessary. My understanding is that this works very directly for linear $\lambda$-calculus (and is more or less a different representation of proof-nets for linear logic with $\multimap$ only), but in the nonlinear case one has to introduce (as with proof-nets) explicit multiplexing (i.e. contraction) nodes and some kind of "level marker" (i.e. the linear $!$ modality). The initial encoding of a $\lambda$-term as a sharing graph corresponds to the embedding of intuitionistic logic into linear logic as $(P\to Q) = (!P\multimap Q)$, and once the optimal reduction is complete, one then has to perform a "read-back" to obtain an ordinary $\lambda$-term in normal form since not every sharing graph is itself the translation of any $\lambda$-term. (Please correct me if I said anything wrong.)

Now, linear logic has categorical semantics, depending on the kind of linear logic under consideration. Intuitionistic linear logic corresponds to symmetric monoidal categories (or multicategories), classical linear logic to linearly distributive categories (or polycategories), the modality $!$ to a "Seely comonad", etc. In particular, it seems to me that we could regard sharing graphs (*qua* proof nets) as the terms in some linear logic, with the rewrites of Lamping's algorithm as axioms, and thereby interpret sharing graphs modulo optimal rewrites into any monoidal category with the appropriate structure and axioms.

My question is whether there is any such monoidal category providing a "semantics of sharing graphs" that performs the read-back into $\lambda$-calculus. In other words, is read-back defined "inductively" over the structure of sharing graphs in a sufficient sense that it can be characterized by their categorical universal property? It feels as though some kind of Chu or Int construction might do the trick, perhaps applied to a presheaf model of HOAS, but I haven't been able to make anything come out.

I'm getting to the edge of my linguistic competence here, but I suspect that a related question would be whether Lamping's algorithm can be written in a "normalization by evaluation" style (e.g. if the category performing the read-back consisted only of normal forms).

**Tags:** lambda-calculus, semantics, interaction-nets


---

## 1 answers

### Answer by username_1 on 2021-11-05. Score: 2

I do not have a proper answer, but you might want to have a look at [this paper by Asperti](https://content.iospress.com/articles/fundamenta-informaticae/fi22-1-2-1) where there is a study of sharing graphs inspired by category theory.


---

