<p>The terms "stratification" and "boxes" come from proof nets.  Elementary linear logic ($\mathbf{ELL}$) was originally introduced by Girard as a variant of <a href="http://iml.univ-mrs.fr/~girard/LLL.pdf" rel="nofollow noreferrer">light linear logic</a> ($\mathbf{LLL}$) and its execution was formulated in terms of proof nets.  It is on proof nets that the elementary bound is satified, i.e., every $\mathbf{ELL}$ proof net $\pi$ may be reduced to its cut-free form in a number of steps bounded by
$$\left.2^{\vdots^{2^s}}\right\}d$$
where $s$ and $d$ are the <em>size</em> and the <em>depth</em> of $\pi$ (maybe the height of the tower is not exactly $d$, it is linear in $d$ I guess).</p>

<p>The <em>size</em> of a proof net is similar to the size of a $\lambda$-term.  The <em>depth</em>, on the other hand, is the maximum number of nested <em>boxes</em> in $\pi$. A <em>box</em> is basically a sub-proof net which may be duplicated or erased: remember that in linear logic there is no free contraction or weakening, which means that proofs in general may not be duplicated or erased; those that can must be marked with a special construct, called <em>box</em>.</p>

<p>Stratification refers precisely to the depth.  It is an informal word that people in the linear logic community use to describe the restricted cut-elimination dynamics that is typical of systems like $\mathbf{ELL}$.  In full linear logic proof nets, cut-elimination may completely alter the depth: if $\pi\to\pi'$ by means of a cut-elimination step and $a$ is a node of $\pi$ at depth $i$ which has a residue $a'$ in $\pi'$, the depth of $a'$ may be anything between $0$ ($a$ is "pulled out" of all boxes) and $2d$, where $d$ is the depth of $\pi$ ($a$ is at maximal depth and it "enters" inside a box which is also at maximal depth).  On the contrary, $\mathbf{ELL}$ proof nets, because of the structural constraints that define them, have the remarkable property that the depth is invariant under cut-elimination: in the above case, the depth of $a'$ is exactly $i$.  This stratification property is essential in proving the complexity bounds of light logics (elementary for $\mathbf{ELL}$ and polynomial for $\mathbf{LLL}$).</p>

<p>From the point of view of Lamping's algorithm, the depth corresponds to the integer label of fan nodes.  Stratification means that a sharing graph corresponding to an $\mathbf{ELL}$ proof net will need no brackets and croissants to be evaluated, because the labels of fan nodes do not change.</p>

<p>After Girard, people started applying the principles of light and elementary linear logic to define type systems for usual $\lambda$-terms (instead of proof nets) which would ensure interesting normalization properties.  The paper you mention falls in this line of work, which explains the terminology they use.  Informally, typing a simply-typed $\lambda$-term amounts to decorating it with "boxes", which is what their so-called <em>pseudo-terms</em> are for.</p>

<p>For the rest, $EAL^\star$ is just like any other non-trivial type system for $\lambda$-terms: there is no simple description of what a typable term looks like; the shortest description is its type derivation!</p>

CC BY-SA 3.0
2017-05-29T11:21:39.867Z
2017-05-29T11:21:39.867Z
Damiano Mazza
<p>The answer to my <a href="https://cstheory.stackexchange.com/questions/36767/can-elementary-affine-logic-be-used-as-the-core-type-system-of-a-practical-progr">last question</a> on the subject made several insightful points on how EAL could be used as the basis of a practical programming language, which, in turn, could be evaluated using the abstract part of Lamping's algorithm. I understand most of the practical remarks and they match my experimentation. I don't, though, understand, in a precise manner, the restrictions that I must follow in order to ensure my terms are EAL-typeable.</p>

<p>Those are the typing rules for EAL*, as presented <a href="https://arxiv.org/pdf/cs/0412028.pdf" rel="nofollow noreferrer">here</a>:</p>

<p><a href="https://i.sstatic.net/hBktu.png" rel="nofollow noreferrer"><img src="https://i.sstatic.net/hBktu.png" alt="enter image description here"></a></p>

<p>I have a vague understanding of what this is saying. I do understand functions can only be applied on terms without <code>!</code>s, and I understand there is a rule to introduce and remove those <code>!</code>s, but I don't fully grasp it. What, exactly, are the restrictions imposed by EAL? What means for a term to be "stratified"? What are those "boxes" about? I'd highly appreciate (non-PHD) resources to catch up with the understanding I'm missing here.</p>

<cc.complexity-theory><lambda-calculus><interaction-nets>
What, in simple terms, are the restrictions imposed by Elementary Affine Logic?
MaiaVictor
# What, in simple terms, are the restrictions imposed by Elementary Affine Logic?

(Asked by: username_0 on 2017-05-27)

The answer to my [last question](https://cstheory.stackexchange.com/questions/36767/can-elementary-affine-logic-be-used-as-the-core-type-system-of-a-practical-progr) on the subject made several insightful points on how EAL could be used as the basis of a practical programming language, which, in turn, could be evaluated using the abstract part of Lamping's algorithm. I understand most of the practical remarks and they match my experimentation. I don't, though, understand, in a precise manner, the restrictions that I must follow in order to ensure my terms are EAL-typeable.

Those are the typing rules for EAL\*, as presented [here](https://arxiv.org/pdf/cs/0412028.pdf):

[![enter image description here](https://i.sstatic.net/hBktu.png)](https://i.sstatic.net/hBktu.png)

I have a vague understanding of what this is saying. I do understand functions can only be applied on terms without `!`s, and I understand there is a rule to introduce and remove those `!`s, but I don't fully grasp it. What, exactly, are the restrictions imposed by EAL? What means for a term to be "stratified"? What are those "boxes" about? I'd highly appreciate (non-PHD) resources to catch up with the understanding I'm missing here.

**Tags:** cc.complexity-theory, lambda-calculus, interaction-nets


---

## 1 answers

### Answer by username_1 on 2017-05-29. Score: 4 | Accepted answer

The terms "stratification" and "boxes" come from proof nets. Elementary linear logic ($\mathbf{ELL}$) was originally introduced by Girard as a variant of [light linear logic](http://iml.univ-mrs.fr/~girard/LLL.pdf) ($\mathbf{LLL}$) and its execution was formulated in terms of proof nets. It is on proof nets that the elementary bound is satified, i.e., every $\mathbf{ELL}$ proof net $\pi$ may be reduced to its cut-free form in a number of steps bounded by
$$\left.2^{\vdots^{2^s}}\right\}d$$
where $s$ and $d$ are the *size* and the *depth* of $\pi$ (maybe the height of the tower is not exactly $d$, it is linear in $d$ I guess).

The *size* of a proof net is similar to the size of a $\lambda$-term. The *depth*, on the other hand, is the maximum number of nested *boxes* in $\pi$. A *box* is basically a sub-proof net which may be duplicated or erased: remember that in linear logic there is no free contraction or weakening, which means that proofs in general may not be duplicated or erased; those that can must be marked with a special construct, called *box*.

Stratification refers precisely to the depth. It is an informal word that people in the linear logic community use to describe the restricted cut-elimination dynamics that is typical of systems like $\mathbf{ELL}$. In full linear logic proof nets, cut-elimination may completely alter the depth: if $\pi\to\pi'$ by means of a cut-elimination step and $a$ is a node of $\pi$ at depth $i$ which has a residue $a'$ in $\pi'$, the depth of $a'$ may be anything between $0$ ($a$ is "pulled out" of all boxes) and $2d$, where $d$ is the depth of $\pi$ ($a$ is at maximal depth and it "enters" inside a box which is also at maximal depth). On the contrary, $\mathbf{ELL}$ proof nets, because of the structural constraints that define them, have the remarkable property that the depth is invariant under cut-elimination: in the above case, the depth of $a'$ is exactly $i$. This stratification property is essential in proving the complexity bounds of light logics (elementary for $\mathbf{ELL}$ and polynomial for $\mathbf{LLL}$).

From the point of view of Lamping's algorithm, the depth corresponds to the integer label of fan nodes. Stratification means that a sharing graph corresponding to an $\mathbf{ELL}$ proof net will need no brackets and croissants to be evaluated, because the labels of fan nodes do not change.

After Girard, people started applying the principles of light and elementary linear logic to define type systems for usual $\lambda$-terms (instead of proof nets) which would ensure interesting normalization properties. The paper you mention falls in this line of work, which explains the terminology they use. Informally, typing a simply-typed $\lambda$-term amounts to decorating it with "boxes", which is what their so-called *pseudo-terms* are for.

For the rest, $EAL^\star$ is just like any other non-trivial type system for $\lambda$-terms: there is no simple description of what a typable term looks like; the shortest description is its type derivation!


---

