### 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 | Japan |

City | Sendai |

Period | 19/04/10 → 21/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