Bibliographic Details
| Title: |
Derivational Complexity and Context-Sensitive Rewriting. |
| Authors: |
Lucas, Salvador1 slucas@dsic.upv.es |
| Source: |
Journal of Automated Reasoning. Dec2021, Vol. 65 Issue 8, p1191-1229. 39p. |
| Subjects: |
Rewriting systems (Computer science), Programming languages, Polynomials, Computational complexity, Natural numbers |
| Abstract: |
Context-sensitive rewriting is a restriction of rewriting where reduction steps are allowed on specific arguments μ (f) ⊆ { 1 , ... , k } of k-ary function symbols f only. Terms which cannot be further rewritten in this way are called μ -normal forms. For left-linear term rewriting systems (TRSs), the so-called normalization via μ -normalization procedure provides a systematic way to obtain normal forms by the stepwise computation and combination of intermediate μ -normal forms. In this paper, we show how to obtain bounds on the derivational complexity of computations using this procedure by using bounds on the derivational complexity of context-sensitive rewriting. Two main applications are envisaged: Normalization via μ -normalization can be used with non-terminating TRSs where the procedure still terminates; on the other hand, it can be used to improve on bounds of derivational complexity of terminating TRSs as it discards many rewritings. [ABSTRACT FROM AUTHOR] |
|
Copyright of Journal of Automated Reasoning is the property of Springer Nature and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.) |
| Database: |
Engineering Source |
