Preservation of strong normalisation modulo permutations for the structural -calculus

DOI10.2168/LMCS-8(1:28)2012MaRDI QIDQ2881096zbMATH OpenFDO

Authors Beniamino Accattoli, Delia Kesner

Publication date 3 April 2012

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1203.0670

zbMATH Keywords

explicit substitutionslambda-calculuspreservation of strong normalisation

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Proof-theoretic aspects of linear logic and other substructural logics (03F52)

Abstract: Inspired by a recent graphical formalism for lambda-calculus based on linear logic technology, we introduce an untyped structural lambda-calculus, called lambda 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 lambda j such as confluence and preservation of beta-strong normalisation. Second, we add a strong bisimulation to lambda j by means of an equational theory which captures in particular Regnier's sigma-equivalence. We then complete this bisimulation with two more equations for (de)composition of substitutions and we prove that the resulting calculus still preserves beta-strong normalization. Finally, we discuss some consequences of our results.

Recommendations

• The structural \(\lambda \)-calculus
• The permutative -calculus
• \(\lambda\)-calculi with explicit substitutions preserving strong normalization
• Foundations of Software Science and Computation Structures
• -calculi with explicit substitutions and composition which preserve -strong normalization

Cited in

(14)

• Spinal atomic \(\lambda\)-calculus
• The permutative -calculus
• Unification for -calculi without propagation rules
• The structural \(\lambda \)-calculus
• The full-reducing Krivine abstract machine KN simulates pure normal-order reduction in lockstep: a proof via corresponding calculus
• scientific article; zbMATH DE number 6744143 (Why is no real title available?)
• Non-linearity as the metric completion of linearity
• scientific article; zbMATH DE number 7756108 (Why is no real title available?)
• A strong bisimulation for a classical term calculus
• A faithful and quantitative notion of distant reduction for the lambda-calculus with generalized applications
• A deep quantitative type system
• Meaningfulness and genericity in a subsuming framework (invited talk)
• Genericity through stratification
• The benefits of diligence

Describes a project that uses

Uses Software

• Automath

This page was built for publication: Preservation of strong normalisation modulo permutations for the structural \(\lambda\)-calculus

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2881096)