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).
