On Constructor Rewrite Systems and the Lambda Calculus

We prove that orthogonal constructor term rewrite systems and lambda-calculuswith weak (i.e., no reduction is allowed under the scope of alambda-abstraction) call-by-value reduction can simulate each other with alinear overhead. In particular, weak call-by- value beta-reduction can besimulated by an orthogonal constructor term rewrite system in the same numberof reduction steps. Conversely, each reduction in a term rewrite system can besimulated by a constant number of beta-reduction steps. This is relevant toimplicit computational complexity, because the number of beta steps to normalform is polynomially related to the actual cost (that is, as performed on aTuring machine) of normalization, under weak call-by-value reduction.Orthogonal constructor term rewrite systems and lambda-calculus are thus bothpolynomially related to Turing machines, taking as notion of cost their naturalparameters.Comment: 27 pages. arXiv admin note: substantial text overlap with arXiv:0904.412