{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T15:34:53Z","timestamp":1753889693058,"version":"3.41.2"},"reference-count":42,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2012,3,27]],"date-time":"2012-03-27T00:00:00Z","timestamp":1332806400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>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.<\/jats:p>","DOI":"10.2168\/lmcs-8(1:28)2012","type":"journal-article","created":{"date-parts":[[2012,9,6]],"date-time":"2012-09-06T10:03:11Z","timestamp":1346925791000},"source":"Crossref","is-referenced-by-count":12,"title":["Preservation of Strong Normalisation modulo permutations for the structural lambda-calculus"],"prefix":"10.46298","volume":"Volume 8, Issue 1","author":[{"given":"Beniamino","family":"Accattoli","sequence":"first","affiliation":[]},{"given":"Delia","family":"Kesner","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2012,3,27]]},"reference":[{"key":"10.2168\/LMCS-8(1:28)2012_AccattoliTh","unstructured":"B. Accattoli.Jumping around the box: graphical and operational studies on Lambda Calculus and Linear Logic.Ph.D. Thesis, Universit\u00e0 di Roma La Sapienza, 2011."},{"key":"10.2168\/LMCS-8(1:28)2012_AG09","doi-asserted-by":"crossref","unstructured":"B. Accattoli and S. Guerrini. Jumping Boxes. representing Lambda-Calculus Boxes by Jumps. In E. Gr\u00e4del and R. Kahle, editors,Proc. of 18th Computer Science Logic (CSL), volume 5771 ofLecture Notes in Computer Science, pages 55-70. Springer-Verlag, Sept. 2009.","DOI":"10.1007\/978-3-642-04027-6_7"},{"key":"10.2168\/LMCS-8(1:28)2012_AK10","doi-asserted-by":"crossref","unstructured":"B. Accattoli and D. Kesner. The structural lambda-calculus. In A. Dawar and H. Veith, editors,Proc. of 24thComputer Science Logic (CSL), volume 6247 ofLecture Notes in Computer Science, pages 381-395. Springer-Verlag, Aug. 2010.","DOI":"10.1007\/978-3-642-15205-4_30"},{"key":"10.2168\/LMCS-8(1:28)2012_AKLPAR","doi-asserted-by":"crossref","unstructured":"B. Accattoli and D. Kesner. The permutative\u00ce\u00bb-calculus, 2012. Accepted at LPAR 2012.","DOI":"10.1007\/978-3-642-28717-6_5"},{"key":"10.2168\/LMCS-8(1:28)2012_Nipkow-Baader","doi-asserted-by":"crossref","unstructured":"F. Baader and T. Nipkow.Term Rewriting and it All That. Cambridge University Press, 1998.","DOI":"10.1017\/CBO9781139172752"},{"key":"10.2168\/LMCS-8(1:28)2012_BlooRoselx","unstructured":"R. Bloo and K. Rose. Preservation of strong normalization in named lambda calculi with explicit substitution and garbage collection. InComputing Science in the Netherlands, pages 62-72. NCSRF, 1995."},{"key":"10.2168\/LMCS-8(1:28)2012_Danos99opt","doi-asserted-by":"crossref","unstructured":"V. Danos and L. Regnier. Reversible, irreversible and optimal lambda-machines.Theoretical Computer Science, 227 (1): 79-97, 1999.","DOI":"10.1016\/S0304-3975(99)00049-3"},{"key":"10.2168\/LMCS-8(1:28)2012_DBLP:journals\/tcs\/David11","doi-asserted-by":"crossref","unstructured":"R. David. A short proof that adding some permutation rules to preserves sn.Theor. Comput. Sci., 412 (11): 1022-1026, 2011.","DOI":"10.1016\/j.tcs.2010.10.048"},{"key":"10.2168\/LMCS-8(1:28)2012_DBLP:journals\/mscs\/DavidG01","doi-asserted-by":"crossref","unstructured":"R. David and B. Guillaume. A lambda-calculus with explicit weakening and explicit substitution.Mathematical Structures in Computer Science, 11 (1): 169-206, 2001.","DOI":"10.1017\/S0960129500003224"},{"key":"10.2168\/LMCS-8(1:28)2012_deBruijn87","unstructured":"N. G. de Bruijn. Generalizing Automath by Means of a Lambda-Typed Lambda Calculus. InMathematical Logic and Theoretical Computer Science, number 106 in Lecture Notes in Pure and Applied Mathematics, pages 71\u00e2\u0080\u0093-92. Marcel Dekker, 1987."},{"key":"10.2168\/LMCS-8(1:28)2012_DCKP03","doi-asserted-by":"crossref","unstructured":"R. Di Cosmo, D. Kesner, and E. Polonovski. Proof nets and explicit substitutions.Mathematical Structures in Computer Science, 13 (3): 409-450, 2003.","DOI":"10.1017\/S0960129502003791"},{"key":"10.2168\/LMCS-8(1:28)2012_espiritoSanto2011","unstructured":"J. Esp\u00edrito Santo. A note on preservation of strong normalisation in the\u00ce\u00bb-calculus.Theoretical Computer Science, 412 (12-14): 169-183, 2011."},{"key":"10.2168\/LMCS-8(1:28)2012_LL","doi-asserted-by":"crossref","unstructured":"J.-Y. Girard. Linear logic.Theoretical Computer Science, 50, 1987.","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"10.2168\/LMCS-8(1:28)2012_GOI","unstructured":"J.-Y. Girard. Geometry of interaction I: an interpretation of system F.Proc. of the Logic Colloquium, 88: 221-260, 1989."},{"key":"10.2168\/LMCS-8(1:28)2012_Hasegawa","doi-asserted-by":"crossref","unstructured":"M. Hasegawa.Models of Sharing Graphs: A Categorical Semantics of let and letrec, volume Distinguished Dissertation Series. Springer-Verlag, 1999.","DOI":"10.1007\/978-1-4471-0865-8"},{"key":"10.2168\/LMCS-8(1:28)2012_HZ09","doi-asserted-by":"crossref","unstructured":"H. Herbelin and S. Zimmermann. An operational account of call-by-value minimal and classical lambda-calculus in \"natural deduction\" form. In P.-L. Curien, editor,Proc. of 9th Typed Lambda Calculus and Applications (TLCA), volume 5608 ofLecture Notes in Computer Science, pages 142-156. Springer-Verlag, July 2009.","DOI":"10.1007\/978-3-642-02273-9_12"},{"key":"10.2168\/LMCS-8(1:28)2012_Hindley78","doi-asserted-by":"crossref","unstructured":"J. R. Hindley. Reductions of residuals are finite.Transactions of the American Mathematical Society, 240: 345-361, 1978.","DOI":"10.2307\/1998825"},{"key":"10.2168\/LMCS-8(1:28)2012_HuetThEtat","unstructured":"G. Huet.R\u00e9solution d'\u00e9quations dans les langages d'ordre 1, 2, . . . , ?Th\u00e8se de doctorat d'\u00e9tat, Universit\u00e9 Paris VII, 1976."},{"key":"10.2168\/LMCS-8(1:28)2012_Kamareddine00","doi-asserted-by":"crossref","unstructured":"F. Kamareddine. Postponement, conservation and preservation of strong normalization for generalized reduction.Journal of Logic and Computation, 10 (5): 721-738, 2000.","DOI":"10.1093\/logcom\/10.5.721"},{"key":"10.2168\/LMCS-8(1:28)2012_Kes07","doi-asserted-by":"crossref","unstructured":"D. Kesner. The theory of calculi with explicit substitutions revisited. In J. Duparc and T. A. Henzinger, editors,Proc. of 16th Computer Science Logic (CSL), volume 4646 ofLecture Notes in Computer Science, pages 238-252. Springer-Verlag, Sept. 2007.","DOI":"10.1007\/978-3-540-74915-8_20"},{"key":"10.2168\/LMCS-8(1:28)2012_Kes09","doi-asserted-by":"crossref","unstructured":"D. Kesner. A theory of explicit substitutions with safe and full composition.Logical Methods in Computer Science, 5 (3:1): 1-29, 2009.","DOI":"10.2168\/LMCS-5(3:1)2009"},{"key":"10.2168\/LMCS-8(1:28)2012_OConchuirKesner","doi-asserted-by":"crossref","unstructured":"D. Kesner and S. O. Conch\u00fair. Milner's lambda calculus with partial substitutions, 2008. D. Kesner and S. Lengrand. Extending the explicit substitution paradigm. In J. Giesl, editor,16th International Conference on Rewriting Techniques and Applications (RTA), volume 3467 ofLecture Notes in Computer Science, pages 407-422. Springer-Verlag, Apr. 2005.","DOI":"10.1007\/978-3-540-32033-3_30"},{"key":"10.2168\/LMCS-8(1:28)2012_KL07","doi-asserted-by":"crossref","unstructured":"D. Kesner and S. Lengrand. Resource operators for lambda-calculus.Information and Computation, 205 (4):0 419-473, 2007.","DOI":"10.1016\/j.ic.2006.08.008"},{"key":"10.2168\/LMCS-8(1:28)2012_KR09","doi-asserted-by":"crossref","unstructured":"D. Kesner and F. Renaud. The prismoid of resources. In R. Kr\u00e1lovic and D. Niwinski, editors,Proc. of the 34th Mathematical Foundations in Computer Science, volume 5734 ofLecture Notes in Computer Science, pages 464-476. Springer-Verlag, Aug. 2009.","DOI":"10.1007\/978-3-642-03816-7_40"},{"key":"10.2168\/LMCS-8(1:28)2012_KfouryW95","doi-asserted-by":"crossref","unstructured":"A. J. Kfoury and J. B. Wells. New notions of reduction and non-semantic proofs of beta-strong normalization in typed lambda-calculi. In D. Kozen, editor,10th Annual IEEESymposium on Logic in Computer Science (LICS), pages 311-321. IEEE Computer Society Press, June 1995.","DOI":"10.1109\/LICS.1995.523266"},{"key":"10.2168\/LMCS-8(1:28)2012_Klo","unstructured":"J.-W. Klop.Combinatory Reduction Systems, volume 127 ofMathematical Centre Tracts. Mathematisch Centrum, Amsterdam, 1980. PhD Thesis."},{"key":"10.2168\/LMCS-8(1:28)2012_KvOvR93","unstructured":"J.-W. Klop, V. van Oostrom, and F. van Raamsdonk. Combinatory reduction systems: introduction and survey.Theoretical Computer Science, 121 (1\/2): 279-308, 1993."},{"key":"10.2168\/LMCS-8(1:28)2012_Krivinemachine","unstructured":"J.-L. Krivine. Un interpr\u00e9teur du lambda-calcul. Available on http:\/\/www.pps.jussieu.fr\/ krivine\/articles\/."},{"key":"10.2168\/LMCS-8(1:28)2012_DBLP:journals\/corr\/abs-0806-4859","unstructured":"S. Lengrand. Termination of lambda-calculus with the extra call-by-value rule known as assoc.CoRR, abs\/0806.4859, 2008."},{"key":"10.2168\/LMCS-8(1:28)2012_MaraistOTW99","doi-asserted-by":"crossref","unstructured":"J. Maraist, M. Odersky, D. N. Turner, and P. Wadler. Call-by-name, call-by-value, call-by-need and the linear lambda calculus.Theoretical Computer Science, 228 (1-2): 175-210, 1999.","DOI":"10.1016\/S0304-3975(98)00358-2"},{"key":"10.2168\/LMCS-8(1:28)2012_Mellies1995a","doi-asserted-by":"crossref","unstructured":"P.-A. Melli\u00e8s. Typed lambda-calculi with explicit substitutions may not terminate. InProc. of 2nd Typed Lambda Calculus and Applications (TLCA), volume 902 ofLecture Notes in Computer Science, pages 328-334. Springer-Verlag, Apr. 1995.","DOI":"10.1007\/BFb0014062"},{"key":"10.2168\/LMCS-8(1:28)2012_Milner07","unstructured":"R. Milner. Local Bigraphs and Confluence: Two Conjectures (extended abstract).Electronic Notes in Theoretical in Computer Science, 175 (3): 65-73, 2007."},{"key":"10.2168\/LMCS-8(1:28)2012_Moggi89","doi-asserted-by":"crossref","unstructured":"E. Moggi. Computational lambda-calculus and monads. In R. Parikh, editor,4th Annual IEEESymposium on Logic in Computer Science (LICS), pages 14-23. IEEE Computer Society Press, June 1989.","DOI":"10.1109\/LICS.1989.39155"},{"key":"10.2168\/LMCS-8(1:28)2012_Ned92","unstructured":"R. P. Nederpelt. The fine-structure of lambda calculus. Technical Report CSN 92\/07, Eindhoven Univ. of Technology, 1992."},{"key":"10.2168\/LMCS-8(1:28)2012_OH06","doi-asserted-by":"crossref","unstructured":"Y. Ohta and M. Hasegawa. A terminating and confluent linear lambda calculus. In F. Pfenning, editor,Rewriting Techniques and Applications (RTA), volume 4098 ofLecture Notes in Computer Science, pages 166-180. Springer-Verlag, 2006.","DOI":"10.1007\/11805618_13"},{"key":"10.2168\/LMCS-8(1:28)2012_regnier94","doi-asserted-by":"crossref","unstructured":"L. Regnier. Une \u00e9quivalence sur les lambda-termes.Theoretical Computer Science, 2 (126): 281-292, 1994.","DOI":"10.1016\/0304-3975(94)90012-4"},{"key":"10.2168\/LMCS-8(1:28)2012_Renaudth","unstructured":"F. Renaud.Les ressources explicites vues par la th\u00e9orie de la r\u00e9\u00e9criture. Ph.D. Thesis, Universit\u00e9 Paris-Diderot, 2011."},{"key":"10.2168\/LMCS-8(1:28)2012_DBLP:journals\/tcs\/Santo11","doi-asserted-by":"crossref","unstructured":"J. E. Santo. A note on preservation of strong normalisation in the -calculus.Theor. Comput. Sci., 412 (11): 1027-1032, 2011.","DOI":"10.1016\/j.tcs.2010.10.049"},{"key":"10.2168\/LMCS-8(1:28)2012_Schw99","doi-asserted-by":"crossref","unstructured":"H. Schwichtenberg. Termination of permutative conversions in intuitionistic Gentzen calculi.Theoretical Computer Science, 212 (1-2): 247-260, 99.","DOI":"10.1016\/S0304-3975(98)00143-1"},{"key":"10.2168\/LMCS-8(1:28)2012_SinotFM03","doi-asserted-by":"crossref","unstructured":"F.-R. Sinot, M. Fern\u00e1ndez, and I. Mackie. Efficient reductions with director strings. In R. Nieuwenhuis, editor,14th International Conference on Rewriting Techniques and Applications (RTA), volume 2706 ofLecture Notes in Computer Science, pages 46-60. Springer-Verlag, June 2003.","DOI":"10.1007\/3-540-44881-0_5"},{"key":"10.2168\/LMCS-8(1:28)2012_Terese03","unstructured":"Terese.Term Rewriting Systems, volume 55 ofCambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2003."},{"key":"10.2168\/LMCS-8(1:28)2012_Yoshida93","doi-asserted-by":"publisher","DOI":"10.1145\/165180.165217"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/847\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/847\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,7]],"date-time":"2025-04-07T23:10:26Z","timestamp":1744067426000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/847"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,3,27]]},"references-count":42,"URL":"https:\/\/doi.org\/10.2168\/lmcs-8(1:28)2012","relation":{"is-same-as":[{"id-type":"arxiv","id":"1203.0670","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1203.0670","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2012,3,27]]},"article-number":"847"}}