TY - GEN
T1 - A nonstandard standardization theorem
AU - Accattoli, Beniamino
AU - Bonelli, Eduardo
AU - Kesner, Delia
AU - Lombardi, Carlos
PY - 2014
Y1 - 2014
N2 - 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.
AB - 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.
KW - explicit substitutions
KW - lambda-calculus
KW - proof-nets
KW - residuals
KW - standardization
UR - http://www.scopus.com/inward/record.url?scp=84893452673&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84893452673&partnerID=8YFLogxK
U2 - 10.1145/2535838.2535886
DO - 10.1145/2535838.2535886
M3 - Conference contribution
AN - SCOPUS:84893452673
SN - 9781450325448
T3 - Conference Record of the Annual ACM Symposium on Principles of Programming Languages
SP - 659
EP - 670
BT - POPL 2014 - Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
T2 - 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2014
Y2 - 22 January 2014 through 24 January 2014
ER -