We lift the theory of optimal reduction to a decomposition of the lambda calculus known as the Linear Substitution Calculus (LSC). LSC decomposes beta-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.
@InProceedings{barenbaum_et_al:LIPIcs.FSCD.2017.9, author = {Barenbaum, Pablo and Bonelli, Eduardo}, title = {{Optimality and the Linear Substitution Calculus}}, booktitle = {2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)}, pages = {9:1--9:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-047-7}, ISSN = {1868-8969}, year = {2017}, volume = {84}, editor = {Miller, Dale}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.9}, URN = {urn:nbn:de:0030-drops-77307}, doi = {10.4230/LIPIcs.FSCD.2017.9}, annote = {Keywords: Rewriting, Lambda Calculus, Explicit Substitutions, Optimal Reduction} }
Feedback for Dagstuhl Publishing