Abstract
We study the Church-Rosser property—which is also known as confluence—in term rewriting and λ-calculus. Given a system R and a peak t ←* s →* t′ in R, we are interested in the length of the reductions in the smallest corresponding valley t →* s′ ←* t′ as a function vs R (m, n) of the size m of s and the maximum length n of the reductions in the peak. For confluent term rewriting systems (TRSs), we prove the (expected) result that vs R (m, n) is a computable function. Conversely, for every total computable function ϕ(n) there is a TRS with a single term s such that vs R ( ∣ s ∣ , n) ≥ ϕ(n) for all n. In contrast, for orthogonal term rewriting systems R we prove that there is a constant k such that vs R (m, n) is bounded from above by a function exponential in k and independent of the size of s. For λ-calculus, we show that vs R (m,n) is bounded from above by a function contained in the fourth level of the Grzegorczyk hierarchy.
Original language | English |
---|---|
Title of host publication | Functional and Logic Programming |
Subtitle of host publication | 10th International Symposium, FLOPS 2010, Sendai, Japan, April 19-21, 2010. Proceedings |
Editors | Matthias Blume, Naoki Kobayashi, Germán Vidal |
Place of Publication | Berlin, Heidelberg |
Publisher | Springer |
Pages | 272-287 |
Number of pages | 16 |
ISBN (Electronic) | 978-3-642-12251-4 |
ISBN (Print) | 978-3-642-12250-7 |
DOIs | |
Publication status | Published - 11 Apr 2010 |
Event | 10th International Symposium on Functional and Logic Programming, FLOPS 2010 - Sendai, Japan Duration: 19 Apr 2010 → 21 Apr 2010 Conference number: 10 |
Publication series
Name | Lecture Notes in Computer Science |
---|---|
Publisher | Springer |
Volume | 6009 |
ISSN (Print) | 0302-9743 |
ISSN (Electronic) | 1611-3349 |
Conference
Conference | 10th International Symposium on Functional and Logic Programming, FLOPS 2010 |
---|---|
Abbreviated title | FLOPS |
Country/Territory | Japan |
City | Sendai |
Period | 19/04/10 → 21/04/10 |