Computer Science – Programming Languages
Scientific paper
2009-04-27
Computer Science
Programming Languages
20 pages. Extended version of a paper in the proceedings of ICALP 2009, Track B
Scientific paper
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.
Lago Ugo Dal
Martini Simone
No associations
LandOfFree
On Constructor Rewrite Systems and the Lambda-Calculus does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with On Constructor Rewrite Systems and the Lambda-Calculus, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and On Constructor Rewrite Systems and the Lambda-Calculus will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-322514