License
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2017.9
URN: urn:nbn:de:0030-drops-77307
URL: http://drops.dagstuhl.de/opus/volltexte/2017/7730/
Go to the corresponding LIPIcs Volume Portal


Barenbaum, Pablo ; Bonelli, Eduardo

Optimality and the Linear Substitution Calculus

pdf-format:
LIPIcs-FSCD-2017-9.pdf (0.6 MB)


Abstract

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.

BibTeX - Entry

@InProceedings{barenbaum_et_al:LIPIcs:2017:7730,
  author =	{Pablo Barenbaum and Eduardo Bonelli},
  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 =	{Dale Miller},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2017/7730},
  URN =		{urn:nbn:de:0030-drops-77307},
  doi =		{10.4230/LIPIcs.FSCD.2017.9},
  annote =	{Keywords: Rewriting, Lambda Calculus, Explicit Substitutions, Optimal Reduction}
}

Keywords: Rewriting, Lambda Calculus, Explicit Substitutions, Optimal Reduction
Seminar: 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)
Issue Date: 2017
Date of publication: 21.08.2017


DROPS-Home | Fulltext Search | Imprint Published by LZI