Optimality & the linear substitution calculus

Pablo Barenbaum, Eduardo Bonelli

Research output: Chapter in Book/Report/Conference proceedingConference contribution

2 Citations (Scopus)

Abstract

We lift the theory of optimal reduction to a decomposition of the lambda calculus known as the Linear Substitution Calculus (LSC). LSC decomposes β-reduction into finer steps that manipulate substitutions in two distinctive ways: it uses context rules that allow substitutions to act "at a distance" and rewrites modulo a set of equations that allow substitutions to "float" in a term. We propose a notion of redex family obtained by adapting Lévy labels to support these two distinctive features. This is followed by a proof of the finite family developments theorem (FFD). We then apply FFD to prove an optimal reduction theorem for LSC. We also apply FFD to deduce additional novel properties of LSC, namely an algorithm for standardisation by selection and normalisation of a linear call-by-need reduction strategy. All results are proved in the axiomatic setting of Glauert and Khashidashvili's Deterministic Residual Structures.

Original languageEnglish (US)
Title of host publication2nd International Conference on Formal Structures for Computation and Deduction, FSCD 2017
EditorsDale Miller
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
ISBN (Electronic)9783959770477
DOIs
StatePublished - Sep 1 2017
Event2nd International Conference on Formal Structures for Computation and Deduction, FSCD 2017 - Oxford, United Kingdom
Duration: Sep 3 2017Sep 9 2017

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
Volume84

Other

Other2nd International Conference on Formal Structures for Computation and Deduction, FSCD 2017
CountryUnited Kingdom
CityOxford
Period9/3/179/9/17

Fingerprint

Substitution
Optimality
Calculus
Theorem
Decompose
Lambda Calculus
Standardization
Normalization
Modulo
Deduce
Family
Term

All Science Journal Classification (ASJC) codes

  • Software

Cite this

Barenbaum, P., & Bonelli, E. (2017). Optimality & the linear substitution calculus. In D. Miller (Ed.), 2nd International Conference on Formal Structures for Computation and Deduction, FSCD 2017 [9] (Leibniz International Proceedings in Informatics, LIPIcs; Vol. 84). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.FSCD.2017.9
Barenbaum, Pablo ; Bonelli, Eduardo. / Optimality & the linear substitution calculus. 2nd International Conference on Formal Structures for Computation and Deduction, FSCD 2017. editor / Dale Miller. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2017. (Leibniz International Proceedings in Informatics, LIPIcs).
@inproceedings{e3027aabad0948bdb0e179a49b86e327,
title = "Optimality & the linear substitution calculus",
abstract = "We lift the theory of optimal reduction to a decomposition of the lambda calculus known as the Linear Substitution Calculus (LSC). LSC decomposes β-reduction into finer steps that manipulate substitutions in two distinctive ways: it uses context rules that allow substitutions to act {"}at a distance{"} and rewrites modulo a set of equations that allow substitutions to {"}float{"} in a term. We propose a notion of redex family obtained by adapting L{\'e}vy labels to support these two distinctive features. This is followed by a proof of the finite family developments theorem (FFD). We then apply FFD to prove an optimal reduction theorem for LSC. We also apply FFD to deduce additional novel properties of LSC, namely an algorithm for standardisation by selection and normalisation of a linear call-by-need reduction strategy. All results are proved in the axiomatic setting of Glauert and Khashidashvili's Deterministic Residual Structures.",
author = "Pablo Barenbaum and Eduardo Bonelli",
year = "2017",
month = "9",
day = "1",
doi = "https://doi.org/10.4230/LIPIcs.FSCD.2017.9",
language = "English (US)",
series = "Leibniz International Proceedings in Informatics, LIPIcs",
publisher = "Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing",
editor = "Dale Miller",
booktitle = "2nd International Conference on Formal Structures for Computation and Deduction, FSCD 2017",
address = "Germany",

}

Barenbaum, P & Bonelli, E 2017, Optimality & the linear substitution calculus. in D Miller (ed.), 2nd International Conference on Formal Structures for Computation and Deduction, FSCD 2017., 9, Leibniz International Proceedings in Informatics, LIPIcs, vol. 84, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2nd International Conference on Formal Structures for Computation and Deduction, FSCD 2017, Oxford, United Kingdom, 9/3/17. https://doi.org/10.4230/LIPIcs.FSCD.2017.9

Optimality & the linear substitution calculus. / Barenbaum, Pablo; Bonelli, Eduardo.

2nd International Conference on Formal Structures for Computation and Deduction, FSCD 2017. ed. / Dale Miller. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2017. 9 (Leibniz International Proceedings in Informatics, LIPIcs; Vol. 84).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

TY - GEN

T1 - Optimality & the linear substitution calculus

AU - Barenbaum, Pablo

AU - Bonelli, Eduardo

PY - 2017/9/1

Y1 - 2017/9/1

N2 - We lift the theory of optimal reduction to a decomposition of the lambda calculus known as the Linear Substitution Calculus (LSC). LSC decomposes β-reduction into finer steps that manipulate substitutions in two distinctive ways: it uses context rules that allow substitutions to act "at a distance" and rewrites modulo a set of equations that allow substitutions to "float" in a term. We propose a notion of redex family obtained by adapting Lévy labels to support these two distinctive features. This is followed by a proof of the finite family developments theorem (FFD). We then apply FFD to prove an optimal reduction theorem for LSC. We also apply FFD to deduce additional novel properties of LSC, namely an algorithm for standardisation by selection and normalisation of a linear call-by-need reduction strategy. All results are proved in the axiomatic setting of Glauert and Khashidashvili's Deterministic Residual Structures.

AB - We lift the theory of optimal reduction to a decomposition of the lambda calculus known as the Linear Substitution Calculus (LSC). LSC decomposes β-reduction into finer steps that manipulate substitutions in two distinctive ways: it uses context rules that allow substitutions to act "at a distance" and rewrites modulo a set of equations that allow substitutions to "float" in a term. We propose a notion of redex family obtained by adapting Lévy labels to support these two distinctive features. This is followed by a proof of the finite family developments theorem (FFD). We then apply FFD to prove an optimal reduction theorem for LSC. We also apply FFD to deduce additional novel properties of LSC, namely an algorithm for standardisation by selection and normalisation of a linear call-by-need reduction strategy. All results are proved in the axiomatic setting of Glauert and Khashidashvili's Deterministic Residual Structures.

UR - http://www.scopus.com/inward/record.url?scp=85030556864&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85030556864&partnerID=8YFLogxK

U2 - https://doi.org/10.4230/LIPIcs.FSCD.2017.9

DO - https://doi.org/10.4230/LIPIcs.FSCD.2017.9

M3 - Conference contribution

T3 - Leibniz International Proceedings in Informatics, LIPIcs

BT - 2nd International Conference on Formal Structures for Computation and Deduction, FSCD 2017

A2 - Miller, Dale

PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing

ER -

Barenbaum P, Bonelli E. Optimality & the linear substitution calculus. In Miller D, editor, 2nd International Conference on Formal Structures for Computation and Deduction, FSCD 2017. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. 2017. 9. (Leibniz International Proceedings in Informatics, LIPIcs). https://doi.org/10.4230/LIPIcs.FSCD.2017.9