research-article

A nonstandard standardization theorem

Authors:

Beniamino Accattoli,

Eduardo Bonelli,

Carlos LombardiAuthors Info & Claims

POPL '14: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

Pages 659 - 670

https://doi.org/10.1145/2535838.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

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

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

A nonstandard standardization theorem
POPL '14

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 ...
The lambda-context calculus (extended version)

We present the Lambda Context Calculus. This simple lambda-calculus features variables arranged in a hierarchy of strengths such that substitution of a strong variable does not avoid capture with respect to abstraction by a weaker variable. This allows ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

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

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

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

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

In-Cooperation

SIGACT: ACM Special Interest Group on Algorithms and Computation Theory

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 08 January 2014

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

POPL '14

Sponsor:

SIGPLAN

POPL '14: The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

January 22 - 24, 2014

California, San Diego, USA

Acceptance Rates

POPL '14 Paper Acceptance Rate 51 of 220 submissions, 23%;

Overall Acceptance Rate 824 of 4,130 submissions, 20%

Upcoming Conference

POPL '25

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

30
Total Citations
View Citations
286
Total Downloads

Downloads (Last 12 months)16
Downloads (Last 6 weeks)3

Reflects downloads up to 18 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

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
Ghica D(2021)Operational Semantics with Hierarchical Abstract Syntax GraphsElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.334.1334(1-10)Online publication date: 8-Feb-2021
https://doi.org/10.4204/EPTCS.334.1
ACCATTOLI BGRAHAM-LENGRAND SKESNER D(2020)Tight typings and split bounds, fully developedJournal of Functional Programming10.1017/S095679682000012X30Online publication date: 19-May-2020
https://doi.org/10.1017/S095679682000012X
Lombardi CRíos Ade Vrijer R(2019)Projections for infinitary rewriting (extended version)Theoretical Computer Science10.1016/j.tcs.2019.02.017Online publication date: Mar-2019
https://doi.org/10.1016/j.tcs.2019.02.017
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.

Media

Figures

Other

Tables

View Table of Contents