4
$\begingroup$

The answer to my last question 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:

enter image description here

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.

$\endgroup$
4
$\begingroup$

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 ($\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!

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.