<p>This is reminiscent of <em>sharing graphs</em>, introduced by Lamping (<a href="https://dl.acm.org/doi/10.1145/96709.96711" rel="nofollow noreferrer">POPL 1990</a>).  More recently, Willem Heijltjes and coauthors introduced the <em>atomic <span class="math-container">$\lambda$</span>-calculus</em> (<a href="https://researchportal.bath.ac.uk/en/publications/atomic-lambda-calculus-a-typed-lambda-calculus-with-explicit-shar" rel="nofollow noreferrer">LICS 2013</a>, <a href="https://link.springer.com/chapter/10.1007/978-3-030-45231-5_30#preview" rel="nofollow noreferrer">FOSSACS 2020</a>), which provides a <span class="math-container">$\lambda$</span>-calculus syntax for (something similar to) sharing graphs.  It is based on <em>deep inference</em>, a proof system introduced by Alessio Guglielmi as an alternative to sequent calculus, natural deduction, etc. whose cut-elimination procedure suggests &quot;atomic&quot; duplication of terms.</p>
<p>The syntax is not as straightforward as the one you originally suggested (with just <code>dup</code> and <code>annih</code>), but you realized yourself pretty quickly that it can't work that simply.  However, it is definitely linear and related to your naive calculus with <code>dup</code> and <code>annih</code>: in fact, pretty much that very same calculus is introduced in Definition 1 of the FOSSACS 2020 paper I linked above, under the name <em>sharing calculus</em>.  It has a general sharing construct <span class="math-container">$t[x_1,\ldots,x_n\leftarrow s]$</span>, of which the cases <span class="math-container">$n=2$</span> and <span class="math-container">$n=0$</span> are your <code>dup</code> and <code>annih</code>, respectively.</p>

CC BY-SA 4.0
2024-06-26T07:24:26.267Z
2024-06-26T07:24:26.267Z
Damiano Mazza
<p>(This is a comment turned into an answer, given that apparently it is a very pertinent answer)</p>
<p>Kesner and Lengrand's &quot;Resource operators for λ-calculus&quot; might be what you are looking for.</p>
<p>The basic idea is to have explicit weakening and contraction in the calculus, plus explicit substitutions.</p>
<p>Note, however, that having explicit weakening and contractions in proof terms nowadays is not really considered the way to go, because the calculus becomes too heavy to manage.</p>

CC BY-SA 4.0
2024-06-26T16:36:41.863Z
2024-06-26T16:36:41.863Z
Beniamino Accattoli
<p>I am trying to find resources on a lambda calculus one would use for explicit memory management, assuming there is such a calculus.</p>
<p>The concept is as follows: one takes untyped lambda calculus, restricts variable use to linear-only and adds two primitives: one for explicit term duplication:</p>
<p><code>let x, y = dup t in e</code></p>
<p>and one for explicit term annihilation:</p>
<p><code>let _ = annih t in e</code></p>
<p><code>dup</code> duplicates the operand in memory.
<code>annih</code> cleans up the memory used by the operand.</p>
<p>Has someone come across a lambda calculus (or perhaps other model of computation) that tries to achieve the same goal?</p>
<p>EDIT:
<code>dup</code> computes on all constructors, including lambda, on contextual variables and, possibly, on eliminators.</p>
<p>Example how <code>dup</code> would compute on a lambda:</p>
<pre><code>let f₀, f₁ = dup (x ↦ x) in (f₀ Z, f₁ Z)
=
let x ⊦ x₀, x₁ = dup x in let f₀ = x ↦ x₀(x/x) in let f₁ = x ↦ x₁(x/x) in (f₀ Z, f₁ Z)
=
let x ⊦ x₀ = x in let x ⊦ x₁ = x in let f₀ = x ↦ x₀(x/x) in let f₁ = x ↦ x₁(x/x) in (f₀ Z, f₁ Z)
=
let x ⊦ x₁ = x in let f₀ = x ↦ x(x/x) in let f₁ = x ↦ x₁(x/x) in (f₀ Z, f₁ Z)
=
let f₀ = x ↦ x(x/x) in let f₁ = x ↦ x(x/x) in (f₀ Z, f₁ Z)
=
let f₀ = x ↦ x in let f₁ = x ↦ x(x/x) in (f₀ Z, f₁ Z)
=
let f₀ = x ↦ x in let f₁ = x ↦ x in (f₀ Z, f₁ Z)
=
let f₁ = x ↦ x in ((x ↦ x) Z, f₁ Z)
=
((x ↦ x) Z, (x ↦ x) Z)
=
(Z, (x ↦ x) Z)
=
(Z, Z)
</code></pre>

CC BY-SA 4.0
2024-06-23T11:38:42.500Z
There are numerous typed $\lambda$-calculi with linear types. You could use one of those and remove types. Something like your `annih` construct could be found in the many papers on *"Region-Based Memory Management"* that was really trendy in the 1990s.
Martin Berger
CC BY-SA 4.0
2024-06-23T11:44:57.477Z
What's the semantics of `dup`? Are the `x` and `y` linear in `e` or unrestricted?
Martin Berger
CC BY-SA 4.0
2024-06-23T11:49:36.503Z
Another question is: what do you mean by *"restricts variable use to linear-only"*? There are two different forms of linear λ-calculus, that should not be confused. (1) A subsystem of the untyped λ-calculus that contains all terms where all free and bound variables occur exactly once. The linear λ-calculus has weak expressive power in that only $O(n)$ algorithms can be expressed; or (2) a proof calculus for linear logic. The latter is very much a typed λ-calculus.
Martin Berger
CC BY-SA 4.0
2024-06-23T12:33:42.467Z
Regarding semantics of `dup`: Every single variable in my hypothetical lambda calculus is linear (occurs exactly once).

Regarding which form of linear lambda calculus: the first one you named.

The proof calculus of linear logic has undesirable properties (for me). In particular, there is no way to duplicate a term of a linear type other than by the exponentiation operator. But elements of type `!A` have unrestricted use, hence are not suitable to model explicit memory management.
Russoul
CC BY-SA 4.0
2024-06-23T12:37:07.240Z
`dup` is a way to duplicate an arbitrary lambda-term. But the results must still be used exactly once each. `dup` could be modelled by explicit memory copying. `annih` is a way to discard an arbitrary linear term. `annih` could be modelled by explicit memory deallocation.
Russoul
CC BY-SA 4.0
2024-06-24T08:42:04.017Z
What does $\lambda x.\mathtt{let}\,y,z=\mathtt{dup}\,x\,\mathtt{in}\,yz$ reduce to in your operational semantics?
Damiano Mazza
CC BY-SA 4.0
2024-06-24T14:05:19.710Z
It doesn't reduce. It's in normal form.
Russoul
CC BY-SA 4.0
2024-06-25T19:24:54.503Z
Ok.  So when does a term of the form $\mathtt{let}\,x,y=\mathtt{dup}\,u\,\mathtt{in}\,t$ reduce?
Damiano Mazza
CC BY-SA 4.0
2024-06-25T19:57:22.453Z
Edited my question. In many cases: on every constructor, on contextual variables and possibly on most of the eliminators. We probably can't compute dup of dup.
But dup of dup is just creation of `4` copies instead of `1`. So we introduce a more general version of dup that creates N copies, it would be possible to compute dup of dup. So I think `dup` can compute on everything but a non-contextual variable.
Russoul
CC BY-SA 4.0
2024-06-25T20:03:54.387Z
To compute dup on a lambda we need contextual `let/annih/dup`. Basically as before but RHS can depend on a context (variables). To eliminate such binding one just provides an instance for every variable in the context.
Russoul
CC BY-SA 4.0
2024-06-25T20:28:07.427Z
annih can be pushed out of dup as well
Russoul
CC BY-SA 4.0
2024-06-25T20:52:40.990Z
What's the meaning of $\vdash$ in your derivation?
Martin Berger
CC BY-SA 4.0
2024-06-25T21:06:48.250Z
So originally I just had the following term for duplication:
`let x, y = dup t in e`. But it's not enough to duplicate a lambda expression.
So a more general solution is to have `let x̄ ⊦ x, y = dup t in e`, where:
`t` is a function of `x̄` and `e` has access to functions `x(x̄)` and `y(x̄)` that stand for duplicated `t(x̄)`.

`x̄` is just a set of variables.

By saying that `t` is a function of `x̄` I just mean that `FV(t) = x̄` (the set of free variables of `t` is exactly `x̄`)
Russoul
CC BY-SA 4.0
2024-06-25T21:12:31.627Z
And of course all those `x̄` must be used exactly once in `t`.
Russoul
CC BY-SA 4.0
2024-06-25T21:14:52.727Z
Those variables `x̄` I call "contextual". dup actually does reduce on them!
So I am positive that the only term `dup` can't reduce on is a "usual" variable.
Russoul
CC BY-SA 4.0
2024-06-25T21:49:24.160Z
Kesner and Lengrand's "Resource operators for λ-calculus" might be what you are looking for. Note, however, that having explicit annotations for weakening and contractions in proof terms nowadays is not really considered the way to go, because the calculus becomes too heavy to manage.
Beniamino Accattoli
CC BY-SA 4.0
2024-06-26T07:32:12.077Z
@BeniaminoAccattoli This is exactly what I've been looking for, thanks!
It looks like they are able to compute `dup` (`C` in their presentation) without contextual variables.
Russoul
CC BY-SA 4.0
2024-06-27T06:56:34.957Z
But Kesner and Lengrand's calculus is just a proof calculus for intuitionistic linear logic.  I thought you said that you are not seeking the behavior of linear logic...
Damiano Mazza
CC BY-SA 4.0
2024-06-27T07:16:37.610Z
It's not. The calculus of Kesner and Lengrand has weakening and contraction. 
Just like I do (annih and dup). We actually have exactly the same syntax up to some substitution business. They just supply different equality rules.
Russoul
<lambda-calculus><linear-logic>
An untyped lambda calculus for explicit memory management
Russoul
# An untyped lambda calculus for explicit memory management

(Asked by: username_0 on 2024-06-23)

I am trying to find resources on a lambda calculus one would use for explicit memory management, assuming there is such a calculus.
The concept is as follows: one takes untyped lambda calculus, restricts variable use to linear-only and adds two primitives: one for explicit term duplication:
let x, y = dup t in e
and one for explicit term annihilation:
let _ = annih t in e
dup duplicates the operand in memory.
annih cleans up the memory used by the operand.
Has someone come across a lambda calculus (or perhaps other model of computation) that tries to achieve the same goal?
EDIT:
dup computes on all constructors, including lambda, on contextual variables and, possibly, on eliminators.
Example how dup would compute on a lambda:
let f₀, f₁ = dup (x ↦ x) in (f₀ Z, f₁ Z)
=
let x ⊦ x₀, x₁ = dup x in let f₀ = x ↦ x₀(x/x) in let f₁ = x ↦ x₁(x/x) in (f₀ Z, f₁ Z)
=
let x ⊦ x₀ = x in let x ⊦ x₁ = x in let f₀ = x ↦ x₀(x/x) in let f₁ = x ↦ x₁(x/x) in (f₀ Z, f₁ Z)
=
let x ⊦ x₁ = x in let f₀ = x ↦ x(x/x) in let f₁ = x ↦ x₁(x/x) in (f₀ Z, f₁ Z)
=
let f₀ = x ↦ x(x/x) in let f₁ = x ↦ x(x/x) in (f₀ Z, f₁ Z)
=
let f₀ = x ↦ x in let f₁ = x ↦ x(x/x) in (f₀ Z, f₁ Z)
=
let f₀ = x ↦ x in let f₁ = x ↦ x in (f₀ Z, f₁ Z)
=
let f₁ = x ↦ x in ((x ↦ x) Z, f₁ Z)
=
((x ↦ x) Z, (x ↦ x) Z)
=
(Z, (x ↦ x) Z)
=
(Z, Z)

**Tags:** lambda-calculus, linear-logic
> **Comments:**
> **username_1**: There are numerous typed $\lambda$-calculi with linear types. You could use one of those and remove types. Something like your `annih` construct could be found in the many papers on *"Region-Based Memory Management"* that was really trendy in the 1990s.  
> **username_1**: What's the semantics of `dup`? Are the `x` and `y` linear in `e` or unrestricted?  
> **username_1**: Another question is: what do you mean by *"restricts variable use to linear-only"*? There are two different forms of linear λ-calculus, that should not be confused. (1) A subsystem of the untyped λ-calculus that contains all terms where all free and bound variables occur exactly once. The linear λ-calculus has weak expressive power in that only $O(n)$ algorithms can be expressed; or (2) a proof calculus for linear logic. The latter is very much a typed λ-calculus.  
> **username_0**: Regarding semantics of `dup`: Every single variable in my hypothetical lambda calculus is linear (occurs exactly once).  Regarding which form of linear lambda calculus: the first one you named.  The proof calculus of linear logic has undesirable properties (for me). In particular, there is no way to duplicate a term of a linear type other than by the exponentiation operator. But elements of type `!A` have unrestricted use, hence are not suitable to model explicit memory management.  
> **username_0**: `dup` is a way to duplicate an arbitrary lambda-term. But the results must still be used exactly once each. `dup` could be modelled by explicit memory copying. `annih` is a way to discard an arbitrary linear term. `annih` could be modelled by explicit memory deallocation.  
> **username_2**: What does $\lambda x.\mathtt{let}\,y,z=\mathtt{dup}\,x\,\mathtt{in}\,yz$ reduce to in your operational semantics?  
> **username_0**: It doesn't reduce. It's in normal form.  
> **username_2**: Ok.  So when does a term of the form $\mathtt{let}\,x,y=\mathtt{dup}\,u\,\mathtt{in}\,t$ reduce?  
> **username_0**: Edited my question. In many cases: on every constructor, on contextual variables and possibly on most of the eliminators. We probably can't compute dup of dup. But dup of dup is just creation of `4` copies instead of `1`. So we introduce a more general version of dup that creates N copies, it would be possible to compute dup of dup. So I think `dup` can compute on everything but a non-contextual variable.  
> **username_0**: To compute dup on a lambda we need contextual `let/annih/dup`. Basically as before but RHS can depend on a context (variables). To eliminate such binding one just provides an instance for every variable in the context.  
> **username_0**: annih can be pushed out of dup as well  
> **username_1**: What's the meaning of $\vdash$ in your derivation?  
> **username_0**: So originally I just had the following term for duplication: `let x, y = dup t in e`. But it's not enough to duplicate a lambda expression. So a more general solution is to have `let x̄ ⊦ x, y = dup t in e`, where: `t` is a function of `x̄` and `e` has access to functions `x(x̄)` and `y(x̄)` that stand for duplicated `t(x̄)`.  `x̄` is just a set of variables.  By saying that `t` is a function of `x̄` I just mean that `FV(t) = x̄` (the set of free variables of `t` is exactly `x̄`)  
> **username_0**: And of course all those `x̄` must be used exactly once in `t`.  
> **username_0**: Those variables `x̄` I call "contextual". dup actually does reduce on them! So I am positive that the only term `dup` can't reduce on is a "usual" variable.  
> **username_3**: Kesner and Lengrand's "Resource operators for λ-calculus" might be what you are looking for. Note, however, that having explicit annotations for weakening and contractions in proof terms nowadays is not really considered the way to go, because the calculus becomes too heavy to manage.  
> **username_0**: @BeniaminoAccattoli This is exactly what I've been looking for, thanks! It looks like they are able to compute `dup` (`C` in their presentation) without contextual variables.  
> **username_2**: But Kesner and Lengrand's calculus is just a proof calculus for intuitionistic linear logic.  I thought you said that you are not seeking the behavior of linear logic...  
> **username_0**: It's not. The calculus of Kesner and Lengrand has weakening and contraction.  Just like I do (annih and dup). We actually have exactly the same syntax up to some substitution business. They just supply different equality rules.  

---

## 2 answers

### Answer by username_2 on 2024-06-26. Score: 4 | Accepted answer

This is reminiscent of *sharing graphs*, introduced by Lamping ([POPL 1990](https://dl.acm.org/doi/10.1145/96709.96711)). More recently, Willem Heijltjes and coauthors introduced the *atomic $\lambda$-calculus* ([LICS 2013](https://researchportal.bath.ac.uk/en/publications/atomic-lambda-calculus-a-typed-lambda-calculus-with-explicit-shar), [FOSSACS 2020](https://link.springer.com/chapter/10.1007/978-3-030-45231-5_30#preview)), which provides a $\lambda$-calculus syntax for (something similar to) sharing graphs. It is based on *deep inference*, a proof system introduced by Alessio Guglielmi as an alternative to sequent calculus, natural deduction, etc. whose cut-elimination procedure suggests "atomic" duplication of terms.

The syntax is not as straightforward as the one you originally suggested (with just `dup` and `annih`), but you realized yourself pretty quickly that it can't work that simply. However, it is definitely linear and related to your naive calculus with `dup` and `annih`: in fact, pretty much that very same calculus is introduced in Definition 1 of the FOSSACS 2020 paper I linked above, under the name *sharing calculus*. It has a general sharing construct $t[x\_1,\ldots,x\_n\leftarrow s]$, of which the cases $n=2$ and $n=0$ are your `dup` and `annih`, respectively.


---

### Answer by username_3 on 2024-06-26. Score: 3

(This is a comment turned into an answer, given that apparently it is a very pertinent answer)

Kesner and Lengrand's "Resource operators for λ-calculus" might be what you are looking for.

The basic idea is to have explicit weakening and contraction in the calculus, plus explicit substitutions.

Note, however, that having explicit weakening and contractions in proof terms nowadays is not really considered the way to go, because the calculus becomes too heavy to manage.


---

