Ugo Dal Lago ; Simone Martini - On Constructor Rewrite Systems and the Lambda Calculus

lmcs:1213 - Logical Methods in Computer Science, August 14, 2012, Volume 8, Issue 3 -
On Constructor Rewrite Systems and the Lambda Calculus

Authors: Ugo Dal Lago ORCID-iD; Simone Martini ORCID-iD

    We prove that orthogonal constructor term rewrite systems and lambda-calculus with weak (i.e., no reduction is allowed under the scope of a lambda-abstraction) call-by-value reduction can simulate each other with a linear overhead. In particular, weak call-by- value beta-reduction can be simulated by an orthogonal constructor term rewrite system in the same number of reduction steps. Conversely, each reduction in a term rewrite system can be simulated by a constant number of beta-reduction steps. This is relevant to implicit computational complexity, because the number of beta steps to normal form is polynomially related to the actual cost (that is, as performed on a Turing machine) of normalization, under weak call-by-value reduction. Orthogonal constructor term rewrite systems and lambda-calculus are thus both polynomially related to Turing machines, taking as notion of cost their natural parameters.

    Volume: Volume 8, Issue 3
    Published on: August 14, 2012
    Accepted on: June 25, 2015
    Submitted on: November 6, 2009
    Keywords: Computer Science - Programming Languages,F.4.1

    Linked data

    Source : ScholeXplorer IsCitedBy ARXIV 2107.06591
    Source : ScholeXplorer IsCitedBy DOI 10.4230/lipics.csl.2022.4
    Source : ScholeXplorer IsCitedBy DOI 10.48550/arxiv.2107.06591
    • 10.48550/arxiv.2107.06591
    • 10.4230/lipics.csl.2022.4
    • 2107.06591
    Useful Open Call-by-Need
    Accattoli, Beniamino ; Leberle, Maico ;

    8 Documents citing this article


    Consultation statistics

    This page has been seen 387 times.
    This article's PDF has been downloaded 191 times.