Preservation of strong normalisation modulo permutations for the structural λ-calculus

Inspired by a recent graphical formalism for λ-calculus based on linear logic technology, we introduce an untyped structural λ-calculus, called λj, which combines actions at a distance with exponential rules decomposing the substitution by means of weakening, contraction and derelicition. First, we prove some fundamental properties of λj such as confluence and preservation of β-strong normalisation. Second, we add a strong bisimulation to λj by means of an equational theory which captures in particular Regnier's σ-equivalence. We then complete this bisimulation with two more equations for (de)composition of substitutions and we prove that the resulting calculus still preserves β--strong normalization. Finally, we discuss some consequences of our results.