On Constructor Rewrite Systems and the Lambda Calculus

Ugo Dal Lago 1, 2 Simone Martini 1, 2
2 FOCUS - Foundations of Component-based Ubiquitous Systems
CRISAM - Inria Sophia Antipolis - Méditerranée , DISI - Dipartimento di Informatica - Scienza e Ingegneria [Bologna]
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.
Type de document :
Article dans une revue
Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2012, 8 (3)
Liste complète des métadonnées

https://hal.inria.fr/hal-00909372
Contributeur : Davide Sangiogi <>
Soumis le : mardi 26 novembre 2013 - 11:08:16
Dernière modification le : vendredi 12 janvier 2018 - 11:01:50

Identifiants

  • HAL Id : hal-00909372, version 1

Collections

Citation

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

Partager

Métriques

Consultations de la notice

100