Tag Info

6

I am not aware of any implementation of Lamping's algorithm directly in the interaction combinators. I do know that the presence of integer labels is a necessary feature of Lamping's algorithm, even for EAL-typable terms, because the labels reflect the nesting of so-called exponential boxes in proof nets, and Lamping's algorithm is essentially the execution ...

5

Efficiency of optlam I have not studied the details of BADTERM nor of the implementation of optlam evaluator, but I find quite strange that optlam performs a number of ß-interactions drastically different than another optimal evaluator like BOHM. Such a number must be, by definition, basically the same on a given term. Are you sure of the correctness of ...

4

Like Martin said, nothing like an equivalent for the $\lambda$-cube has ever been developed for interaction nets or interaction combinators. The only work that considers types for interaction nets is Lafont's original paper [1]. (My own CONCUR 2005 paper also considers types but adds nothing new to what Lafont did). It is an extremely simple system: only ...

4

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

4

For question 1, if by "deadlock" you mean "non-trivial vicious circle", then the answer is obviously yes, simply because a non-trivial vicious circle cannot be typed: you will have a cut between a formula $A$ and a formula $F$ containing $A^\bot$ as strict subformula, so it is impossible that $F=A^\bot$. But this is kind of trivial: by refusing a priori to ...

3

This has been a subject of investigation for the Implicit Computational Complexity (ICC) community recently. It is known that in certain cases, when the graph you want to evaluate is of a specific type (be it from typing or a global shape restriction, see references) there is a path-based evaluation strategy that is more efficient than the naive one, ...

3

So, yes, turns out it is possible, as can be seen on the decode function of my abstract algorithm implementation here. Basically, Lambda and Apply nodes are given the same tag (here, I use 0), and you can infer which is the case based on their positions. Each Duplication node, though, requires an unique tag. Note some terms such as (2 2) will reduce to a net ...

3

Your observation about cut-elimination being faithfully represented in the unlabelled interaction nets is correct. However, the answer to your question is no. Let us call $\delta$ the unique agent of the system. Such an agent is binary; we distinguish its two auxiliary ports by referring to as left and right. We call cell an occurrence of the agent in a ...

1

The term that you gave does have one duplication, i.e.: ones is used in the body and returned in form of a free variable. The following example illustrates the same effect but is smaller: loop = λ_. loop To make the graph structure clear, let's make sure that each identifier is used exactly twice (_ represents connected erasing node): C[loop, loop_rec] = ...

1

The Structure of Interaction paper seems to be what you are asking for.

Only top voted, non community-wiki answers of a minimum length are eligible