Mostrar el registro sencillo del ítem
dc.contributor.author
Barenbaum, Pablo
dc.contributor.author
Bonelli, Eduardo Augusto
dc.date.available
2018-04-06T15:31:32Z
dc.date.issued
2017-09
dc.identifier.citation
Barenbaum, Pablo; Bonelli, Eduardo Augusto; Optimality & the linear substitution calculus; Schloss Dagstuhl. Leibniz-Zentrum für Informatik; Leibniz International Proceedings in Informatics, LIPIcs; 84; 9-2017; 1-16
dc.identifier.issn
1868-8969
dc.identifier.uri
http://hdl.handle.net/11336/41112
dc.description.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.
dc.format
application/pdf
dc.language.iso
eng
dc.publisher
Schloss Dagstuhl. Leibniz-Zentrum für Informatik
dc.rights
info:eu-repo/semantics/openAccess
dc.rights.uri
https://creativecommons.org/licenses/by/2.5/ar/
dc.subject
Explicit Substitutions
dc.subject
Lambda Calculus
dc.subject
Optimal Reduction
dc.subject
Rewriting
dc.subject.classification
Ciencias de la Computación
dc.subject.classification
Ciencias de la Computación e Información
dc.subject.classification
CIENCIAS NATURALES Y EXACTAS
dc.title
Optimality & the linear substitution calculus
dc.type
info:eu-repo/semantics/article
dc.type
info:ar-repo/semantics/artículo
dc.type
info:eu-repo/semantics/publishedVersion
dc.date.updated
2018-04-06T13:45:50Z
dc.journal.volume
84
dc.journal.pagination
1-16
dc.journal.pais
Alemania
dc.journal.ciudad
Leibniz
dc.description.fil
Fil: Barenbaum, Pablo. Universidad de Buenos Aires; Argentina. Université Paris Diderot - Paris 7; Francia. Stevens Institute of Technology; Estados Unidos. Consejo Nacional de Investigaciones Científicas y Técnicas; Argentina
dc.description.fil
Fil: Bonelli, Eduardo Augusto. Consejo Nacional de Investigaciones Científicas y Técnicas; Argentina. Stevens Institute of Technology; Estados Unidos. Universidad Nacional de Quilmes; Argentina
dc.journal.title
Leibniz International Proceedings in Informatics, LIPIcs
dc.relation.alternativeid
info:eu-repo/semantics/altIdentifier/doi/http://dx.doi.org/10.4230/LIPIcs.FSCD.2017.9
dc.relation.alternativeid
info:eu-repo/semantics/altIdentifier/url/http://drops.dagstuhl.de/opus/volltexte/2017/7730/
Archivos asociados