Termination of canonical context-sensitive rewriting and productivity of rewrite systems
Termination of programs, i.e., the absence of infinite computations, ensures the existence of normal forms for all initial expressions, thus providing an essential ingredient for the definition of a normalization semantics for functional programs. In lazy functional languages, though, infinite data...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2015-12-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1512.06942v1 |
| _version_ | 1811331003071856640 |
|---|---|
| author | Salvador Lucas |
| author_facet | Salvador Lucas |
| author_sort | Salvador Lucas |
| collection | DOAJ |
| description | Termination of programs, i.e., the absence of infinite computations, ensures the existence of normal forms for all initial expressions, thus providing an essential ingredient for the definition of a normalization semantics for functional programs. In lazy functional languages, though, infinite data structures are often delivered as the outcome of computations. For instance, the list of all prime numbers can be returned as a neverending stream of numerical expressions or data structures. If such streams are allowed, requiring termination is hopeless. In this setting, the notion of productivity can be used to provide an account of computations with infinite data structures, as it "captures the idea of computability, of progress of infinite-list programs" (B.A. Sijtsma, On the Productivity of Recursive List Definitions, ACM Transactions on Programming Languages and Systems 11(4):633-649, 1989). However, in the realm of Term Rewriting Systems, which can be seen as (first-order, untyped, unconditional) functional programs, termination of Context-Sensitive Rewriting (CSR) has been showed equivalent to productivity of rewrite systems through appropriate transformations. In this way, tools for proving termination of CSR can be used to prove productivity. In term rewriting, CSR is the restriction of rewriting that arises when reductions are allowed on selected arguments of function symbols only. In this paper we show that well-known results about the computational power of CSR are useful to better understand the existing connections between productivity of rewrite systems and termination of CSR, and also to obtain more powerful techniques to prove productivity of rewrite systems. |
| first_indexed | 2024-04-13T16:12:17Z |
| format | Article |
| id | doaj.art-e07e3a3f329341d08fbec0ffd78b8e6f |
| institution | Directory Open Access Journal |
| issn | 2075-2180 |
| language | English |
| last_indexed | 2024-04-13T16:12:17Z |
| publishDate | 2015-12-01 |
| publisher | Open Publishing Association |
| record_format | Article |
| series | Electronic Proceedings in Theoretical Computer Science |
| spelling | doaj.art-e07e3a3f329341d08fbec0ffd78b8e6f2022-12-22T02:40:11ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802015-12-01200Proc. PROLE 2015183110.4204/EPTCS.200.2:10Termination of canonical context-sensitive rewriting and productivity of rewrite systemsSalvador Lucas0 DSIC, Universitat Politècnica de València, Spain Termination of programs, i.e., the absence of infinite computations, ensures the existence of normal forms for all initial expressions, thus providing an essential ingredient for the definition of a normalization semantics for functional programs. In lazy functional languages, though, infinite data structures are often delivered as the outcome of computations. For instance, the list of all prime numbers can be returned as a neverending stream of numerical expressions or data structures. If such streams are allowed, requiring termination is hopeless. In this setting, the notion of productivity can be used to provide an account of computations with infinite data structures, as it "captures the idea of computability, of progress of infinite-list programs" (B.A. Sijtsma, On the Productivity of Recursive List Definitions, ACM Transactions on Programming Languages and Systems 11(4):633-649, 1989). However, in the realm of Term Rewriting Systems, which can be seen as (first-order, untyped, unconditional) functional programs, termination of Context-Sensitive Rewriting (CSR) has been showed equivalent to productivity of rewrite systems through appropriate transformations. In this way, tools for proving termination of CSR can be used to prove productivity. In term rewriting, CSR is the restriction of rewriting that arises when reductions are allowed on selected arguments of function symbols only. In this paper we show that well-known results about the computational power of CSR are useful to better understand the existing connections between productivity of rewrite systems and termination of CSR, and also to obtain more powerful techniques to prove productivity of rewrite systems.http://arxiv.org/pdf/1512.06942v1 |
| spellingShingle | Salvador Lucas Termination of canonical context-sensitive rewriting and productivity of rewrite systems Electronic Proceedings in Theoretical Computer Science |
| title | Termination of canonical context-sensitive rewriting and productivity of rewrite systems |
| title_full | Termination of canonical context-sensitive rewriting and productivity of rewrite systems |
| title_fullStr | Termination of canonical context-sensitive rewriting and productivity of rewrite systems |
| title_full_unstemmed | Termination of canonical context-sensitive rewriting and productivity of rewrite systems |
| title_short | Termination of canonical context-sensitive rewriting and productivity of rewrite systems |
| title_sort | termination of canonical context sensitive rewriting and productivity of rewrite systems |
| url | http://arxiv.org/pdf/1512.06942v1 |
| work_keys_str_mv | AT salvadorlucas terminationofcanonicalcontextsensitiverewritingandproductivityofrewritesystems |