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 proceedingConference contributionAcademicpeer-review

    1 Citation (Scopus)
    42 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 languageEnglish
    Title of host publicationFunctional and Logic Programming
    Subtitle of host publication10th International Symposium, FLOPS 2010, Sendai, Japan, April 19-21, 2010. Proceedings
    EditorsMatthias Blume, Naoki Kobayashi, Germán Vidal
    Place of Publication Berlin, Heidelberg
    PublisherSpringer
    Pages272-287
    Number of pages16
    ISBN (Electronic)978-3-642-12251-4
    ISBN (Print)978-3-642-12250-7
    DOIs
    Publication statusPublished - 11 Apr 2010
    Event10th International Symposium on Functional and Logic Programming, FLOPS 2010 - Sendai, Japan
    Duration: 19 Apr 201021 Apr 2010
    Conference number: 10

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer
    Volume6009
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349

    Conference

    Conference10th International Symposium on Functional and Logic Programming, FLOPS 2010
    Abbreviated titleFLOPS
    CountryJapan
    CitySendai
    Period19/04/1021/04/10

    Fingerprint Dive into the research topics of 'Least Upper Bounds on the Size of Church-Rosser Diagrams in Term Rewriting and λ-Calculus'. Together they form a unique fingerprint.

  • 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). Berlin, Heidelberg: Springer. https://doi.org/10.1007/978-3-642-12251-4_20