CINXE.COM

<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.1 plus MathML 2.0 plus SVG 1.1//EN" "http://www.w3.org/2002/04/xhtml-math-svg/xhtml-math-svg-flat.dtd" > <html xmlns="http://www.w3.org/1999/xhtml"> <head> <title> sharing graph in nLab </title> <meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /> <meta name="robots" content="index,follow" /> <meta name="viewport" content="width=device-width, initial-scale=1" /> <link href="/stylesheets/instiki.css?1676280126" media="all" rel="stylesheet" type="text/css" /> <link href="/stylesheets/mathematics.css?1660229990" media="all" rel="stylesheet" type="text/css" /> <link href="/stylesheets/syntax.css?1660229990" media="all" rel="stylesheet" type="text/css" /> <link href="/stylesheets/nlab.css?1676280126" media="all" rel="stylesheet" type="text/css" /> <link rel="stylesheet" type="text/css" href="https://cdn.jsdelivr.net/gh/dreampulse/computer-modern-web-font@master/fonts.css"/> <style type="text/css"> h1#pageName, div.info, .newWikiWord a, a.existingWikiWord, .newWikiWord a:hover, [actiontype="toggle"]:hover, #TextileHelp h3 { color: #226622; } a:visited.existingWikiWord { color: #164416; } </style> <style type="text/css"><![CDATA[/*></style> <script src="/javascripts/prototype.js?1660229990" type="text/javascript"></script> <script src="/javascripts/effects.js?1660229990" type="text/javascript"></script> <script src="/javascripts/dragdrop.js?1660229990" type="text/javascript"></script> <script src="/javascripts/controls.js?1660229990" type="text/javascript"></script> <script src="/javascripts/application.js?1660229990" type="text/javascript"></script> <script src="/javascripts/page_helper.js?1660229990" type="text/javascript"></script> <script src="/javascripts/thm_numbering.js?1660229990" type="text/javascript"></script> <script type="text/x-mathjax-config"> <![CDATA[//><!]]> </script> <script type="text/javascript"> <![CDATA[//><!]]> </script> <link href="https://ncatlab.org/nlab/atom_with_headlines" rel="alternate" title="Atom with headlines" type="application/atom+xml" /> <link href="https://ncatlab.org/nlab/atom_with_content" rel="alternate" title="Atom with full content" type="application/atom+xml" /> <script type="text/javascript"> document.observe("dom:loaded", function() { generateThmNumbers(); }); </script> </head> <body> <div id="Container"> <div id="Content"> <h1 id="pageName"> <span style="float: left; margin: 0.5em 0.25em -0.25em 0"> <svg xmlns="http://www.w3.org/2000/svg" width="1.872em" height="1.8em" viewBox="0 0 190 181"> <path fill="#226622" d="M72.8 145c-1.6 17.3-15.7 10-23.6 20.2-5.6 7.3 4.8 15 11.4 15 11.5-.2 19-13.4 26.4-20.3 3.3-3 8.2-4 11.2-7.2a14 14 0 0 0 2.9-11.1c-1.4-9.6-12.4-18.6-16.9-27.2-5-9.6-10.7-27.4-24.1-27.7-17.4-.3-.4 26 4.7 30.7 2.4 2.3 5.4 4.1 7.3 6.9 1.6 2.3 2.1 5.8-1 7.2-5.9 2.6-12.4-6.3-15.5-10-8.8-10.6-15.5-23-26.2-31.8-5.2-4.3-11.8-8-18-3.7-7.3 4.9-4.2 12.9.2 18.5a81 81 0 0 0 30.7 23c3.3 1.5 12.8 5.6 10 10.7-2.5 5.2-11.7 3-15.6 1.1-8.4-3.8-24.3-21.3-34.4-13.7-3.5 2.6-2.3 7.6-1.2 11.1 2.8 9 12.2 17.2 20.9 20.5 17.3 6.7 34.3-8 50.8-12.1z"/> <path fill="#a41e32" d="M145.9 121.3c-.2-7.5 0-19.6-4.5-26-5.4-7.5-12.9-1-14.1 5.8-1.4 7.8 2.7 14.1 4.8 21.3 3.4 12 5.8 29-.8 40.1-3.6-6.7-5.2-13-7-20.4-2.1-8.2-12.8-13.2-15.1-1.9-2 9.7 9 21.2 12 30.1 1.2 4 2 8.8 6.4 10.3 6.9 2.3 13.3-4.7 17.7-8.8 12.2-11.5 36.6-20.7 43.4-36.4 6.7-15.7-13.7-14-21.3-7.2-9.1 8-11.9 20.5-23.6 25.1 7.5-23.7 31.8-37.6 38.4-61.4 2-7.3-.8-29.6-13-19.8-14.5 11.6-6.6 37.6-23.3 49.2z"/> <path fill="#193c78" d="M86.3 47.5c0-13-10.2-27.6-5.8-40.4 2.8-8.4 14.1-10.1 17-1 3.8 11.6-.3 26.3-1.8 38 11.7-.7 10.5-16 14.8-24.3 2.1-4.2 5.7-9.1 11-6.7 6 2.7 7.4 9.2 6.6 15.1-2.2 14-12.2 18.8-22.4 27-3.4 2.7-8 6.6-5.9 11.6 2 4.4 7 4.5 10.7 2.8 7.4-3.3 13.4-16.5 21.7-16 14.6.7 12 21.9.9 26.2-5 1.9-10.2 2.3-15.2 3.9-5.8 1.8-9.4 8.7-15.7 8.9-6.1.1-9-6.9-14.3-9-14.4-6-33.3-2-44.7-14.7-3.7-4.2-9.6-12-4.9-17.4 9.3-10.7 28 7.2 35.7 12 2 1.1 11 6.9 11.4 1.1.4-5.2-10-8.2-13.5-10-11.1-5.2-30-15.3-35-27.3-2.5-6 2.8-13.8 9.4-13.6 6.9.2 13.4 7 17.5 12C70.9 34 75 43.8 86.3 47.4z"/> </svg> </span> <span class="webName">nLab</span> sharing graph </h1> <div class="navigation"> <span class="skipNav"><a href='#navEnd'>Skip the Navigation Links</a> | </span> <span style="display:inline-block; width: 0.3em;"></span> <a href="/nlab/show/HomePage" accesskey="H" title="Home page">Home Page</a> | <a href="/nlab/all_pages" accesskey="A" title="List of all pages">All Pages</a> | <a href="/nlab/latest_revisions" accesskey="U" title="Latest edits and page creations">Latest Revisions</a> | <a href="https://nforum.ncatlab.org/discussions/?CategoryID=0" title="Discuss this page on the nForum. It does not yet have a dedicated thread; feel free to create one, giving it the same name as the title of this page" style="color:black">Discuss this page</a> | <form accept-charset="utf-8" action="/nlab/search" id="navigationSearchForm" method="get"> <fieldset class="search"><input type="text" id="searchField" name="query" value="Search" style="display:inline-block; float: left;" onfocus="this.value == 'Search' ? this.value = '' : true" onblur="this.value == '' ? this.value = 'Search' : true" /></fieldset> </form> <span id='navEnd'></span> </div> <div id="revision"> <html xmlns="http://www.w3.org/1999/xhtml" xmlns:svg="http://www.w3.org/2000/svg" xml:lang="en" lang="en"> <head><meta http-equiv="Content-type" content="application/xhtml+xml;charset=utf-8" /><title></title></head> <body> <p><em>Sharing graphs</em> are another kind of <a class="existingWikiWord" href="/nlab/show/string+diagram">string diagram</a> which focuses on the syntax of a language. Given a <a href="http://en.wikipedia.org/wiki/Backus-Naur_form">BNF</a> description of a <a class="existingWikiWord" href="/nlab/show/context-free+grammar">context-free grammar</a>, we get a category whose objects are (roughly) lists of subterms and whose morphisms are rules for composing the subterms into terms.</p> <h1 id="example_untyped_lambda_calculus">Example: Untyped lambda calculus</h1> <dl> <dt>Lambda calculus terms are recursively defined as follows:</dt> <dd> <p><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>t</mi></mrow><annotation encoding="application/x-tex">t</annotation></semantics></math> ::= <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>v</mi><mo stretchy="false">|</mo><mi>t</mi><mo stretchy="false">(</mo><mi>t</mi><mo stretchy="false">)</mo><mo stretchy="false">|</mo><mi>λ</mi><mi>v</mi><mo>.</mo><mi>t</mi></mrow><annotation encoding="application/x-tex">v | t(t) | \lambda v.t</annotation></semantics></math></p> </dd> </dl> <p>where <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>v</mi></mrow><annotation encoding="application/x-tex">v</annotation></semantics></math> is a countably infinite set of variables. (That is, a term is either a given variable, a given term applied to a given term, or the <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>λ</mi></mrow><annotation encoding="application/x-tex">\lambda</annotation></semantics></math>-abstraction of a given term as a function of a given variable.) There are three equivalences on terms, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>α</mi></mrow><annotation encoding="application/x-tex">\alpha</annotation></semantics></math> (for handling dummy variables), <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>β</mi></mrow><annotation encoding="application/x-tex">\beta</annotation></semantics></math> (substitution of terms), and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>η</mi></mrow><annotation encoding="application/x-tex">\eta</annotation></semantics></math> (extensionality). The corresponding category has</p> <ul> <li> <p>two generating types, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>V</mi></mrow><annotation encoding="application/x-tex">V</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>T</mi></mrow><annotation encoding="application/x-tex">T</annotation></semantics></math></p> </li> <li> <p>six function symbols</p> <ul> <li><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>λ</mi><mo>:</mo><msup><mi>V</mi> <mo>*</mo></msup><mo>×</mo><mi>T</mi><mo>→</mo><mi>T</mi></mrow><annotation encoding="application/x-tex">\lambda:V^* \times T \to T</annotation></semantics></math>. Lambda takes an antivariable and a term that may use the corresponding variable.</li> <li><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>∩</mo><mo>:</mo><mn>1</mn><mo>→</mo><msup><mi>V</mi> <mo>*</mo></msup><mo>×</mo><mi>T</mi></mrow><annotation encoding="application/x-tex">\cap:1 \to V^* \times T</annotation></semantics></math>. This turns an antivariable <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi></mrow><annotation encoding="application/x-tex">x</annotation></semantics></math> introduced by lambda into the term <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi></mrow><annotation encoding="application/x-tex">x</annotation></semantics></math>.</li> <li><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>:</mo><mi>T</mi><mo>×</mo><mi>T</mi><mo>→</mo><mi>T</mi></mrow><annotation encoding="application/x-tex">A:T \times T \to T</annotation></semantics></math>. (Application) This takes <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi></mrow><annotation encoding="application/x-tex">f</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>g</mi></mrow><annotation encoding="application/x-tex">g</annotation></semantics></math> and produces <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo stretchy="false">(</mo><mi>g</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">f(g)</annotation></semantics></math>.</li> <li><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>swap</mi><mo>:</mo><mi>T</mi><mo>×</mo><mi>T</mi><mo>→</mo><mi>T</mi><mo>×</mo><mi>T</mi></mrow><annotation encoding="application/x-tex">swap:T \times T \to T \times T</annotation></semantics></math>.</li> <li><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>!</mo><mo>:</mo><mi>T</mi><mo>→</mo><mn>1</mn></mrow><annotation encoding="application/x-tex">!:T \to 1</annotation></semantics></math>.</li> <li><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Δ</mi><mo>:</mo><mi>T</mi><mo>→</mo><mi>T</mi><mo>×</mo><mi>T</mi></mrow><annotation encoding="application/x-tex">\Delta:T \to T \times T</annotation></semantics></math>.</li> </ul> </li> <li> <p>relations</p> <ul> <li> <p>The last three function symbols come with relations that make the category cartesian (and justify the use of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>×</mo></mrow><annotation encoding="application/x-tex">\times</annotation></semantics></math> above). Leaving off the last two would give linear lambda calculus.</p> </li> <li> <p><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>β</mi><mi>η</mi><mo>:</mo><mi>A</mi><mo>∘</mo><mo stretchy="false">(</mo><mi>λ</mi><mo>×</mo><msub><mn>1</mn> <mi>T</mi></msub><mo stretchy="false">)</mo><mo>∘</mo><mo stretchy="false">(</mo><msub><mn>1</mn> <mrow><msup><mi>V</mi> <mo>*</mo></msup></mrow></msub><mo>×</mo><mi>P</mi><mo>×</mo><msub><mn>1</mn> <mi>T</mi></msub><mo stretchy="false">)</mo><mo>∘</mo><mo stretchy="false">(</mo><mo>∩</mo><mo>×</mo><msub><mn>1</mn> <mrow><msup><mi>T</mi> <mi>n</mi></msup></mrow></msub><mo>×</mo><msub><mn>1</mn> <mi>T</mi></msub><mo stretchy="false">)</mo><mo>⇔</mo><mi>P</mi><mo>∘</mo><msub><mi>swap</mi> <mrow><msub><mn>1</mn> <mrow><msup><mi>T</mi> <mi>n</mi></msup></mrow></msub><mo>,</mo><msub><mn>1</mn> <mi>T</mi></msub></mrow></msub></mrow><annotation encoding="application/x-tex">\beta\eta: A \circ (\lambda \times 1_T) \circ (1_{V^*} \times P \times 1_T) \circ (\cap \times 1_{T^n} \times 1_T) \Leftrightarrow P \circ swap_{1_{T^n}, 1_T}</annotation></semantics></math></p> <p>This is the categorical encoding of</p> <p><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>λ</mi><mi>x</mi><mo>.</mo><mi>P</mi><mo stretchy="false">)</mo><mo stretchy="false">(</mo><mi>y</mi><mo stretchy="false">)</mo><mo>⇔</mo><mi>P</mi><mo stretchy="false">[</mo><mi>y</mi><mo stretchy="false">/</mo><mi>x</mi><mo stretchy="false">]</mo></mrow><annotation encoding="application/x-tex">(\lambda x.P)(y) \Leftrightarrow P[y/x]</annotation></semantics></math></p> <p>where the free variables of the term <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi></mrow><annotation encoding="application/x-tex">P</annotation></semantics></math> are <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">{</mo><mi>x</mi><mo>,</mo><msub><mi>x</mi> <mn>1</mn></msub><mo>,</mo><mi>…</mi><mo>,</mo><msub><mi>x</mi> <mi>n</mi></msub><mo stretchy="false">}</mo></mrow><annotation encoding="application/x-tex">\{x, x_1, \ldots, x_n\}</annotation></semantics></math>.</p> </li> </ul> </li> </ul> <p>The string diagrams corresponding to this category are called sharing graphs.</p> <h1 id="discussion">Discussion</h1> <p>Peter Selinger <a href="https://golem.ph.utexas.edu/category/2006/08/categorifying_cccs_seeing_comp.html#c021631">said</a> of this example:</p> <p>“Sharing graphs” are extremely well-studied. See e.g.</p> <p>(1) <a href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.52.530">Stefano Guerrini, A general theory of sharing graphs (1997)</a></p> <p>There is a reduction strategy on sharing graphs that is provably the most efficient possible reduction strategy for lambda calculus; this goes back to the work of Levy and Lamping (both cited in the above paper).</p> <p>Guerrini also gives an algebraic semantics of these sharing graphs, see section 7. I don’t know whether it is related to your categorical view.</p> <p>I also like the book by Peyton-Jones:</p> <p>(2) <a href="http://research.microsoft.com/en-us/um/people/simonpj/papers/slpj-book-1987/">Simon Peyton Jones, The Implementation of Functional Programming Languages (1987)</a></p> <p>It shows how to use sharing graphs as the basis for a practical implementation of lazy programming languages. As far as I know, this is still state-of-the-art and is used in the implementation of Haskell. In keeping with the practical nature of the book, the sharing graphs are represented in slightly different form (with syntactic variables rather than backpointers), but this is of course equivalent.</p> <p>As for the categorical semantics, what you have in mind is a kind of abstract syntax with variable binding. To put this into perspective, the semantics of ordinary abstract syntax (i.e., without variable binding), is given by an object <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> in a cartesian category, together with interpretations for each <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>n</mi></mrow><annotation encoding="application/x-tex">n</annotation></semantics></math>-ary function symbol <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>:</mo><msup><mi>A</mi> <mi>n</mi></msup><mo>→</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">f : A^n \to A</annotation></semantics></math>. One can then inductively define the interpretation of terms, speak of the free such object, etc.</p> <p>Things get slightly more complicated if one adds variable binding to this picture. This has also been studied, though perhaps not in the same form as you are proposing. Perhaps the closest to your approach is</p> <p>(3) <a href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.46.4082">Martin Hofmann, Semantical analysis of higher-order abstract syntax (1999)</a></p> <p>Here one has <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>var</mi><mo>:</mo><mi>V</mi><mo>→</mo><mi>T</mi></mrow><annotation encoding="application/x-tex">var : V \to T</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>app</mi><mo>:</mo><mi>T</mi><mo>×</mo><mi>T</mi><mo>→</mo><mi>T</mi></mrow><annotation encoding="application/x-tex">app : T \times T \to T</annotation></semantics></math>, and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>lam</mi><mo>:</mo><mo stretchy="false">(</mo><mi>V</mi><mo>⇒</mo><mi>T</mi><mo stretchy="false">)</mo><mo>→</mo><mi>T</mi></mrow><annotation encoding="application/x-tex">lam : (V \Rightarrow T) \to T</annotation></semantics></math> (see top of p.9, with the obvious changes in notation). You will note the use of a function space <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>V</mi><mo>⇒</mo><mi>T</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(V \Rightarrow T)</annotation></semantics></math> in place of your cartesian product <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>V</mi> <mo>*</mo></msup><mo>×</mo><mi>T</mi></mrow><annotation encoding="application/x-tex">V^* \times T</annotation></semantics></math>.</p> <p>Another very similar paper is</p> <p>(4) <a href="http://citeseerx.ist.psu.edu/showciting?cid=198434">M.P.Fiore, G.D.Plotkin and D.Turi. Abstract syntax and variable binding (1999)</a> (Also available <a href="http://www.cl.cam.ac.uk/~mpf23/papers/Types/Types.html">here</a>.)</p> <p>Here, one has <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>var</mi><mo>:</mo><mi>V</mi><mo>→</mo><mi>T</mi></mrow><annotation encoding="application/x-tex">var : V \to T</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>app</mi><mo>:</mo><mi>T</mi><mo>×</mo><mi>T</mi><mo>→</mo><mi>T</mi></mrow><annotation encoding="application/x-tex">app : T \times T \to T</annotation></semantics></math>, and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>lam</mi><mo>:</mo><mi>δ</mi><mi>T</mi><mo>→</mo><mi>T</mi></mrow><annotation encoding="application/x-tex">lam : \delta T \to T</annotation></semantics></math> (as contained e.g. in the commutative diagram on p.6). Again, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>δ</mi><mi>T</mi></mrow><annotation encoding="application/x-tex">\delta T</annotation></semantics></math> is something akin to the function space <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>V</mi><mo>⇒</mo><mi>T</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(V \Rightarrow T)</annotation></semantics></math>, but is also isomorphic, in a suitable sense, to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>T</mi><mo>⇒</mo><mi>T</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(T \Rightarrow T)</annotation></semantics></math>, as far as I remember (this is important for substitution, see below).</p> <p>A third, technically slightly different (but conceptually similar) approach to abstract syntax with variable binders is:</p> <p>(5) <a href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.38.9383">Murdoch J. Gabbay, Andrew M. Pitts: A new approach to abstract syntax with variable binding (1999)</a></p> <p>(6) <a href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.62.9845">Murdoch J. Gabbay, Andrew M. Pitts: A new approach to abstract syntax with variable binding (2002)</a></p> <p>See especially the second-to-last line of [6, p.356], and you immediately see the similarity. Their <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">[</mo><mi>A</mi><mo stretchy="false">]</mo><mi>T</mi></mrow><annotation encoding="application/x-tex">[A]T</annotation></semantics></math> operation is akin to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>V</mi><mo>⇒</mo><mi>T</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(V \Rightarrow T)</annotation></semantics></math> in [3] and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>δ</mi><mi>T</mi></mrow><annotation encoding="application/x-tex">\delta T</annotation></semantics></math> in [4].</p> <p>It is fun to note that [3–5] all appeared (independently) in the same conference in 1999. Semantics of variable binders was clearly a pressing problem that year.</p> <p>I can comment briefly on the main difference between these works and what you are proposing. One thing that is important in syntax is substitution (of a term for a variable). In fact, in the usual abstract syntax (without binders), a term with <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>n</mi></mrow><annotation encoding="application/x-tex">n</annotation></semantics></math> variables is represented as a morphism <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>A</mi> <mi>n</mi></msup><mo>→</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">A^n \to A</annotation></semantics></math>. This is useful for substitution: namely, if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>:</mo><mi>A</mi><mo>×</mo><msup><mi>A</mi> <mi>n</mi></msup><mo>→</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">f : A \times A^n \to A</annotation></semantics></math> represents the term <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>t</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><msub><mi>y</mi> <mn>1</mn></msub><mo>,</mo><mo>.</mo><mo>.</mo><mo>.</mo><mo>,</mo><msub><mi>y</mi> <mi>n</mi></msub><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">t(x,y_1,...,y_n)</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>g</mi><mo>:</mo><msup><mi>A</mi> <mi>n</mi></msup><mo>→</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">g : A^n \to A</annotation></semantics></math> represents <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>s</mi><mo stretchy="false">(</mo><msub><mi>y</mi> <mn>1</mn></msub><mo>,</mo><mo>.</mo><mo>.</mo><mo>.</mo><mo>,</mo><msub><mi>y</mi> <mi>n</mi></msub><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">s(y_1,...,y_n)</annotation></semantics></math>, then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>∘</mo><mo stretchy="false">⟨</mo><mi>g</mi><mo>,</mo><mi>id</mi><mo stretchy="false">⟩</mo></mrow><annotation encoding="application/x-tex">f \circ \langle g, id \rangle</annotation></semantics></math> represents <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>t</mi><mo stretchy="false">[</mo><mi>s</mi><mo stretchy="false">/</mo><mi>x</mi><mo stretchy="false">]</mo></mrow><annotation encoding="application/x-tex">t[s/x]</annotation></semantics></math>.</p> <p>In the presence of variables, a term with <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>n</mi></mrow><annotation encoding="application/x-tex">n</annotation></semantics></math> variables is represented as <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>1</mn><mo>→</mo><msup><mi>V</mi> <mrow><mo>*</mo><mi>n</mi></mrow></msup><mo>×</mo><mi>T</mi></mrow><annotation encoding="application/x-tex">1 \to V^{*n} \times T</annotation></semantics></math> (in your notation). However, for reasons of substitution, one would still like this hom-set to be in 1-1 correspondence with <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>T</mi> <mi>n</mi></msup><mo>→</mo><mi>T</mi></mrow><annotation encoding="application/x-tex">T^n \to T</annotation></semantics></math>. Somehow this is what the papers [3–6] manage to do, each in their own way.</p> <p>I hope these references will be useful. It would be great if you had a more abstract monoidal framework of which the particular constructions in [3–6] are concrete examples. I have always wondered about the precise connection between [3–6], and whether there is a bigger picture.</p> </body></html> </div> <div class="revisedby"> <p> Last revised on July 6, 2019 at 19:22:19. See the <a href="/nlab/history/sharing+graph" style="color: #005c19">history</a> of this page for a list of all contributions to it. </p> </div> <div class="navigation navfoot"> <a href="/nlab/edit/sharing+graph" accesskey="E" class="navlink" id="edit" rel="nofollow">Edit</a><a href="https://nforum.ncatlab.org/discussions/?CategoryID=0">Discuss</a><span class="backintime"><a href="/nlab/revision/sharing+graph/3" accesskey="B" class="navlinkbackintime" id="to_previous_revision" rel="nofollow">Previous revision</a></span><a href="/nlab/show/diff/sharing+graph" accesskey="C" class="navlink" id="see_changes" rel="nofollow">Changes from previous revision</a><a href="/nlab/history/sharing+graph" accesskey="S" class="navlink" id="history" rel="nofollow">History (3 revisions)</a> <a href="/nlab/show/sharing+graph/cite" style="color: black">Cite</a> <a href="/nlab/print/sharing+graph" accesskey="p" id="view_print" rel="nofollow">Print</a> <a href="/nlab/source/sharing+graph" id="view_source" rel="nofollow">Source</a> </div> </div>  </div>  </body> </html>