On Constructor Rewrite Systems and the Lambda Calculus - Archive ouverte HAL Access content directly
Journal Articles Logical Methods in Computer Science Year : 2012

On Constructor Rewrite Systems and the Lambda Calculus

(1, 2) , (1, 2)
1
2

Abstract

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.
Not file

Dates and versions

hal-00909372 , version 1 (26-11-2013)

Identifiers

  • HAL Id : hal-00909372 , version 1

Cite

Ugo Dal Lago, Simone Martini. On Constructor Rewrite Systems and the Lambda Calculus. Logical Methods in Computer Science, 2012, 8 (3). ⟨hal-00909372⟩

Collections

INRIA INRIA2
74 View
0 Download

Share

Gmail Facebook Twitter LinkedIn More