research-article

A nonstandard standardization theorem

Authors:

Beniamino Accattoli,

Eduardo Bonelli,

Carlos LombardiAuthors Info & Claims

ACM SIGPLAN Notices, Volume 49, Issue 1

Pages 659 - 670

https://doi.org/10.1145/2578855.2535886

Published: 08 January 2014 Publication History

Abstract

Standardization is a fundamental notion for connecting programming languages and rewriting calculi. Since both programming languages and calculi rely on substitution for defining their dynamics, explicit substitutions (ES) help further close the gap between theory and practice.

This paper focuses on standardization for the linear substitution calculus, a calculus with ES capable of mimicking reduction in lambda-calculus and linear logic proof-nets. For the latter, proof-nets can be formalized by means of a simple equational theory over the linear substitution calculus.

Contrary to other extant calculi with ES, our system can be equipped with a residual theory in the sense of Lévy, which is used to prove a left-to-right standardization theorem for the calculus with ES but without the equational theory. Such a theorem, however, does not lift from the calculus with ES to proof-nets, because the notion of left-to-right derivation is not preserved by the equational theory. We then relax the notion of left-to-right standard derivation, based on a total order on redexes, to a more liberal notion of standard derivation based on partial orders.

Our proofs rely on Gonthier, Lévy, and Melliès' axiomatic theory for standardization. However, we go beyond merely applying their framework, revisiting some of its key concepts: we obtain uniqueness (modulo) of standard derivations in an abstract way and we provide a coinductive characterization of their key abstract notion of external redex. This last point is then used to give a simple proof that linear head reduction --a nondeterministic strategy having a central role in the theory of linear logic-- is standard.

Supplementary Material

JPG File (d3_left_t9.jpg)

Download
7.41 KB

MP4 File (d3_left_t9.mp4)

Download
352.30 MB

References

[1]

M. Abadi, L. Cardelli, P. L. Curien, and J.-J. Lévy. Explicit substitutions. Journal of Functional Programming, 4(1):375--416, 1991.

[2]

B. Accattoli. An abstract factorization theorem for explicit substitutions. In RTA, pages 6--21, 2012.

[3]

B. Accattoli. Evaluating functions as processes. In TERMGRAPH, pages 41--55, 2013.

[4]

B. Accattoli. Jumping around the box: graphical and operational studies on λ-calculus and Linear Logic. PhD thesis, La Sapienza University of Rome, february 2011.

[5]

B. Accattoli and U. Dal Lago. On the invariance of the unitary cost model for head reduction. In RTA, pages 22--37, 2012.

[6]

B. Accattoli and D. Kesner. The structural λ-calculus. In CSL, pages 381--395, 2010.

Digital Library

[7]

B. Accattoli, P. Barenbaum, and D. Mazza. Distilling abstract machines. Submitted, 2013. https://sites.google.com/site/beniaminoaccattoli/machines.pdf?attredirects=0.

[8]

H. P. Barendregt, R. Kennaway, J. W. Klop, and M. R. Sleep. Needed reduction and spine strategies for the lambda calculus. Information and Computation, 75(3):191--231, 1987.

Digital Library

[9]

R. Bloo and K. Rose. Preservation of strong normalization in named lambda calculi with explicit substitution and garbage collection. In Computing Science in the Netherlands, pages 62--72. Netherlands Computer Science Research Foundation, 1995.

[10]

G. Boudol. Computational semantics of term rewriting systems. In Algebraic methods in semantics, pages 169--236. Cambridge University Press, 1986.

Digital Library

[11]

H. S. Bruggink. Equivalence of reductions in higher-order rewriting. PhD thesis, Utrecht University, 2008.

[12]

D. Clark and R. Kennaway. Some properties of non-orthogonal term graph rewriting systems. In SEGRAGRA, volume 2 of ENTCS, pages 36--45, 1995.

[13]

H. Curry and R. Feys. Combinatory Logic. Number Vol. 1 in Studies in logic and the foundations of mathematics. North-Holland, 1958.

[14]

V. Danos and L. Regnier. Head linear reduction, 2003. http://iml.univ-mrs.fr/~regnier/articles/pam.ps.gz.

[15]

V. Danos, H. Herbelin, and L. Regnier. Game semantics & abstract machines. In LICS, pages 394--405, 1996.

Digital Library

[16]

D. de Carvalho, M. Pagani, and L. Tortora de Falco. A semantic measure of the execution time in linear logic. Theor. Comput. Sci., 412(20):1884--1902, 2011.

Digital Library

[17]

T. Ehrhard and L. Regnier. Böhm trees, krivine's machine and the taylor expansion of lambda-terms. In CiE, pages 186--197, 2006.

Digital Library

[18]

J.-Y. Girard. Linear logic. Theoretical Computer Science, 50(1):1--101, 1987.

Digital Library

[19]

G. Gonthier, J.-J. Lévy, and P.-A. Melli`es. An abstract standardisation theorem. In LICS, pages 72--81, 1992.

[20]

G. Huet. Residual theory in λ-calculus: A formal development. Journal of Functional Programming, 4(3):371--394, 1994.

[21]

G. Huet and J.-J. Lévy. Computations in orthogonal rewriting systems, I and II. In Computational Logic - Essays in Honor of Alan Robinson, pages 395--414, 1991.

[22]

G. Huet and J.-J. Lévy. Call by Need computations in non ambiguous linear term rewriting systems. Technical Report 359, INRIA, 1979.

[23]

D. Kesner and S. Lengrand. Resource operators for lambda-calculus. Information and Computation, 205(4):419--473, 2007.

Digital Library

[24]

D. Kesner and S. O'Conchúir. Milner's lambda calculus with partial substitutions, 2008. http://www.pps.univ-paris-diderot.fr/~kesner/papers/shortpartial.pdf.

[25]

Z. Khasidashvili and J. R. W. Glauert. Discrete normalization and standardization in deterministic residual structures. In ALP, pages 135--149, 1996.

Digital Library

[26]

J. W. Klop. Combinatory Reduction Systems. Phd thesis, Utrecht University, 1980.

[27]

J.-J. Lévy. Réductions correctes et optimales dans le lambda calcul. Thése d'Etat, Univ. Paris VII, France, 1978.

[28]

L. Maranget. Optimal derivations in weak lambda-calculi and in orthogonal terms rewriting systems. In POPL, pages 255--269, 1991.

Digital Library

[29]

G. Mascari and M. Pedicini. Head linear reduction and pure proof net extraction. Theoretical Computer Science, 135(1):111--137, 1994.

Digital Library

[30]

P.-A. Melliès. Axiomatic rewriting theory I: A diagrammatic standardization theorem. In Processes, Terms and Cycles: Steps on the Road to Infinity, volume 3838 of LNCS, pages 554--638. Springer, 2005.

Digital Library

[31]

P.-A. Melliès. Axiomatic rewriting theory VI: Residual theory revisited. In RTA, pages 24--50, 2002.

Digital Library

[32]

P.-A. Melliès. Description Abstraite de système de réécriture. PhD thesis, Paris 7 University, 1996.

[33]

R. Milner. Local bigraphs and confluence: Two conjectures. ENTCS, 175(3):65--73, 2007.

Digital Library

[34]

L. Paolini and S. Ronchi Della Rocca. Parametric parameter passing lambda-calculus. Information and Computation, 189(1):87--106, 2004.

Digital Library

[35]

G. D. Plotkin. Call-by-name, call-by-value and the lambda-calculus. Theoretical Computer Science, 1(2):125--159, 1975.

[36]

L. Regnier. Une équivalence sur les lambda-termes. Theoretical Computer Science, 2(126):281--292, 1994.

Digital Library

[37]

M. Takahashi. Parallel reductions in λ-calculus. Inf. Comput., 118(1): 120--127, 1995.

Digital Library

[38]

Terese. Term Rewriting Systems, volume 55 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2003.

[39]

V. van Oostrom. Normalisation in weakly orthogonal rewriting. In RTA, pages 60--74, 1999.

Digital Library

[40]

V. van Oostrom and R. C. de Vrijer. Four equivalent equivalences of reductions. ENTCS, 70(6):21--61, 2002.

[41]

H. Xi. Upper bounds for standardizations and an application. Journal of Symbolic Logic, 64(1):291--303, 1999.

Cited By

Torrens POrchard DVasconcellos C(2024)On the Operational Theory of the CPS-Calculus: Towards a Theoretical Foundation for IRsProceedings of the ACM on Programming Languages10.1145/36746308:ICFP(147-176)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674630
Kesner DPeyrot LVentura D(2021)The Spirit of Node ReplicationFoundations of Software Science and Computation Structures10.1007/978-3-030-71995-1_18(344-364)Online publication date: 27-Mar-2021
https://dl.acm.org/doi/10.1007/978-3-030-71995-1_18
Barenbaum PCiruelos G(2018)Factoring Derivation Spaces via Intersection TypesProgramming Languages and Systems10.1007/978-3-030-02768-1_2(24-44)Online publication date: 22-Oct-2018
https://doi.org/10.1007/978-3-030-02768-1_2
Show More Cited By

Index Terms

A nonstandard standardization theorem
1. Mathematics of computing
  1. Continuous mathematics
    1. Calculus
      1. Lambda calculus
  2. Mathematical analysis
    1. Calculus
      1. Lambda calculus
2. Theory of computation
  1. Semantics and reasoning
    1. Program semantics
      1. Operational semantics

Recommendations

Distilling abstract machines
ICFP '14

It is well-known that many environment-based abstract machines can be seen as strategies in lambda calculi with explicit substitutions (ES). Recently, graphical syntaxes and linear logic led to the linear substitution calculus (LSC), a new approach to ...
A nonstandard standardization theorem
POPL '14: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

Standardization is a fundamental notion for connecting programming languages and rewriting calculi. Since both programming languages and calculi rely on substitution for defining their dynamics, explicit substitutions (ES) help further close the gap ...
A fine-grained computational interpretation of Girard’s intuitionistic proof-nets

This paper introduces a functional term calculus, called pn, that captures the essence of the operational semantics of Intuitionistic Linear Logic Proof-Nets with a faithful degree of granularity, both statically and dynamically. On the static side, we ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 49, Issue 1

POPL '14

January 2014

661 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/2578855

Editor:
Mark W. Bailey
Hamilton College, Clinton, NY

Issue’s Table of Contents

POPL '14: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
January 2014
702 pages
ISBN:9781450325448
DOI:10.1145/2535838
General Chair:
Suresh Jagannathan
Purdue University, USA
,
Program Chair:
Peter Sewell
University of Cambridge, UK

Copyright © 2014 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 08 January 2014

Published in SIGPLAN Volume 49, Issue 1

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

32
Total Citations
View Citations
287
Total Downloads

Downloads (Last 12 months)13
Downloads (Last 6 weeks)1

Reflects downloads up to 03 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Torrens POrchard DVasconcellos C(2024)On the Operational Theory of the CPS-Calculus: Towards a Theoretical Foundation for IRsProceedings of the ACM on Programming Languages10.1145/36746308:ICFP(147-176)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674630
Kesner DPeyrot LVentura D(2021)The Spirit of Node ReplicationFoundations of Software Science and Computation Structures10.1007/978-3-030-71995-1_18(344-364)Online publication date: 27-Mar-2021
https://dl.acm.org/doi/10.1007/978-3-030-71995-1_18
Barenbaum PCiruelos G(2018)Factoring Derivation Spaces via Intersection TypesProgramming Languages and Systems10.1007/978-3-030-02768-1_2(24-44)Online publication date: 22-Oct-2018
https://doi.org/10.1007/978-3-030-02768-1_2
Arrial VGuerrieri GKesner D(2024)The Benefits of DiligenceAutomated Reasoning10.1007/978-3-031-63501-4_18(338-359)Online publication date: 2-Jul-2024
https://doi.org/10.1007/978-3-031-63501-4_18
Accattoli BStorm THirschfeld R(2023)Sharing a Perspective on the 𝜆-CalculusProceedings of the 2023 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software10.1145/3622758.3622884(179-190)Online publication date: 18-Oct-2023
https://dl.acm.org/doi/10.1145/3622758.3622884
Wu J(2023)Proofs as Terms, Terms as GraphsProgramming Languages and Systems10.1007/978-981-99-8311-7_5(91-111)Online publication date: 21-Nov-2023
https://doi.org/10.1007/978-981-99-8311-7_5
Accattoli BBarenbaum P(2023)A Diamond Machine for Strong EvaluationProgramming Languages and Systems10.1007/978-981-99-8311-7_4(69-90)Online publication date: 26-Nov-2023
https://dl.acm.org/doi/10.1007/978-981-99-8311-7_4
Acclavio MCatta DOlimpieri F(2023)Canonicity of Proofs in Constructive Modal LogicAutomated Reasoning with Analytic Tableaux and Related Methods10.1007/978-3-031-43513-3_19(342-363)Online publication date: 14-Sep-2023
https://doi.org/10.1007/978-3-031-43513-3_19
Accattoli B(2022)Exponentials as Substitutions and the Cost of Cut Elimination in Linear LogicProceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3531130.3532445(1-15)Online publication date: 2-Aug-2022
https://dl.acm.org/doi/10.1145/3531130.3532445
Kesner D(2022)A fine-grained computational interpretation of Girard’s intuitionistic proof-netsProceedings of the ACM on Programming Languages10.1145/34986696:POPL(1-28)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3498669
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Issue’s Table of Contents