Derivational Complexity and Context-Sensitive Rewriting.
Saved in:
| 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 |
| FullText | Text: Availability: 0 |
|---|---|
| Header | DbId: egs DbLabel: Engineering Source An: 153186651 AccessLevel: 6 PubType: Academic Journal PubTypeId: academicJournal PreciseRelevancyScore: 0 |
| IllustrationInfo | |
| Items | – Name: Title Label: Title Group: Ti Data: Derivational Complexity and Context-Sensitive Rewriting. – Name: Author Label: Authors Group: Au Data: <searchLink fieldCode="AR" term="%22Lucas%2C+Salvador%22">Lucas, Salvador</searchLink><relatesTo>1</relatesTo><i> slucas@dsic.upv.es</i> – Name: TitleSource Label: Source Group: Src Data: <searchLink fieldCode="JN" term="%22Journal+of+Automated+Reasoning%22">Journal of Automated Reasoning</searchLink>. Dec2021, Vol. 65 Issue 8, p1191-1229. 39p. – Name: Subject Label: Subjects Group: Su Data: <searchLink fieldCode="DE" term="%22Rewriting+systems+%28Computer+science%29%22">Rewriting systems (Computer science)</searchLink><br /><searchLink fieldCode="DE" term="%22Programming+languages%22">Programming languages</searchLink><br /><searchLink fieldCode="DE" term="%22Polynomials%22">Polynomials</searchLink><br /><searchLink fieldCode="DE" term="%22Computational+complexity%22">Computational complexity</searchLink><br /><searchLink fieldCode="DE" term="%22Natural+numbers%22">Natural numbers</searchLink> – Name: Abstract Label: Abstract Group: Ab Data: 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] – Name: AbstractSuppliedCopyright Label: Group: Ab Data: <i>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.</i> (Copyright applies to all Abstracts.) |
| PLink | https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=egs&AN=153186651 |
| RecordInfo | BibRecord: BibEntity: Identifiers: – Type: doi Value: 10.1007/s10817-021-09603-1 Languages: – Code: eng Text: English PhysicalDescription: Pagination: PageCount: 39 StartPage: 1191 Subjects: – SubjectFull: Rewriting systems (Computer science) Type: general – SubjectFull: Programming languages Type: general – SubjectFull: Polynomials Type: general – SubjectFull: Computational complexity Type: general – SubjectFull: Natural numbers Type: general Titles: – TitleFull: Derivational Complexity and Context-Sensitive Rewriting. Type: main BibRelationships: HasContributorRelationships: – PersonEntity: Name: NameFull: Lucas, Salvador IsPartOfRelationships: – BibEntity: Dates: – D: 01 M: 12 Text: Dec2021 Type: published Y: 2021 Identifiers: – Type: issn-print Value: 01687433 Numbering: – Type: volume Value: 65 – Type: issue Value: 8 Titles: – TitleFull: Journal of Automated Reasoning Type: main |
| ResultId | 1 |
