Least Upper Bounds on the Size of Church-Rosser Diagrams in Term Rewriting and λ-Calculus

Jeroen Ketema; Jakob Grue Simonsen

doi:10.1007/978-3-642-12251-4_20

Least Upper Bounds on the Size of Church-Rosser Diagrams in Term Rewriting and λ-Calculus

Jeroen Ketema, Jakob Grue Simonsen

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

1 Citation (Scopus)

114 Downloads (Pure)

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	https://doi.org/10.1007/978-3-642-12251-4_20
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

Access to Document

10.1007/978-3-642-12251-4_20

Ketema2010leastAccepted author version, 275 KB

Cite this

Ketema, J., & Simonsen, J. G. (2010). Least Upper Bounds on the Size of Church-Rosser Diagrams in Term Rewriting and λ-Calculus. In M. Blume, N. Kobayashi, & G. Vidal (Eds.), Functional and Logic Programming: 10th International Symposium, FLOPS 2010, Sendai, Japan, April 19-21, 2010. Proceedings (pp. 272-287). (Lecture Notes in Computer Science; Vol. 6009). Springer. https://doi.org/10.1007/978-3-642-12251-4_20

Ketema, Jeroen ; Simonsen, Jakob Grue. / Least Upper Bounds on the Size of Church-Rosser Diagrams in Term Rewriting and λ-Calculus. Functional and Logic Programming: 10th International Symposium, FLOPS 2010, Sendai, Japan, April 19-21, 2010. Proceedings. editor / Matthias Blume ; Naoki Kobayashi ; Germán Vidal. Berlin, Heidelberg : Springer, 2010. pp. 272-287 (Lecture Notes in Computer Science).

@inproceedings{a759bbbb9d8849ebba4bb79d55ee5e35,

title = "Least Upper Bounds on the Size of Church-Rosser Diagrams in Term Rewriting and λ-Calculus",

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.",

author = "Jeroen Ketema and Simonsen, {Jakob Grue}",

year = "2010",

month = apr,

day = "11",

doi = "10.1007/978-3-642-12251-4_20",

language = "English",

isbn = "978-3-642-12250-7",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "272--287",

editor = "Matthias Blume and Naoki Kobayashi and Germ{\'a}n Vidal",

booktitle = "Functional and Logic Programming",

address = "Germany",

note = "10th International Symposium on Functional and Logic Programming, FLOPS 2010, FLOPS ; Conference date: 19-04-2010 Through 21-04-2010",

}

Ketema, J & Simonsen, JG 2010, Least Upper Bounds on the Size of Church-Rosser Diagrams in Term Rewriting and λ-Calculus. in M Blume, N Kobayashi & G Vidal (eds), Functional and Logic Programming: 10th International Symposium, FLOPS 2010, Sendai, Japan, April 19-21, 2010. Proceedings. Lecture Notes in Computer Science, vol. 6009, Springer, Berlin, Heidelberg, pp. 272-287, 10th International Symposium on Functional and Logic Programming, FLOPS 2010, Sendai, Japan, 19/04/10. https://doi.org/10.1007/978-3-642-12251-4_20

Least Upper Bounds on the Size of Church-Rosser Diagrams in Term Rewriting and λ-Calculus. / Ketema, Jeroen; Simonsen, Jakob Grue.
Functional and Logic Programming: 10th International Symposium, FLOPS 2010, Sendai, Japan, April 19-21, 2010. Proceedings. ed. / Matthias Blume; Naoki Kobayashi; Germán Vidal. Berlin, Heidelberg: Springer, 2010. p. 272-287 (Lecture Notes in Computer Science; Vol. 6009).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Least Upper Bounds on the Size of Church-Rosser Diagrams in Term Rewriting and λ-Calculus

AU - Ketema, Jeroen

AU - Simonsen, Jakob Grue

N1 - Conference code: 10

PY - 2010/4/11

Y1 - 2010/4/11

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-642-12251-4_20

DO - 10.1007/978-3-642-12251-4_20

M3 - Conference contribution

SN - 978-3-642-12250-7

T3 - Lecture Notes in Computer Science

SP - 272

EP - 287

BT - Functional and Logic Programming

A2 - Blume, Matthias

A2 - Kobayashi, Naoki

A2 - Vidal, Germán

PB - Springer

CY - Berlin, Heidelberg

T2 - 10th International Symposium on Functional and Logic Programming, FLOPS 2010

Y2 - 19 April 2010 through 21 April 2010

ER -

Ketema J, Simonsen JG. Least Upper Bounds on the Size of Church-Rosser Diagrams in Term Rewriting and λ-Calculus. In Blume M, Kobayashi N, Vidal G, editors, Functional and Logic Programming: 10th International Symposium, FLOPS 2010, Sendai, Japan, April 19-21, 2010. Proceedings. Berlin, Heidelberg: Springer. 2010. p. 272-287. (Lecture Notes in Computer Science). doi: 10.1007/978-3-642-12251-4_20

Least Upper Bounds on the Size of Church-Rosser Diagrams in Term Rewriting and λ-Calculus

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this