The Church-Rosser theorem and quantitative analysis of witnesses. (English) Zbl 1436.03104

Summary: We show that an upper bound function for the Church-Rosser theorem of type-free \(\lambda\)-calculus with \(\beta\)-reduction must be in the fourth level of the Grzegorczyk hierarchy, i.e., the smallest Grzegorczyk class properly extending the class of elementary functions. At this level we also find common reducts for the confluence property. The proof method here can be applied not only to type-free \(\lambda\)-calculus with \(\beta\eta\)-reduction but also to typed \(\lambda\)-calculi such as Pure Type Systems.


03B40 Combinatory logic and lambda calculus


Full Text: DOI


[1] Barendregt, H. P., The Lambda Calculus. Its Syntax and Semantics, (1984), North-Holland · Zbl 0551.03007
[2] Barendregt, H. P., Lambda calculi with types, (Abramsky, S.; Gabbay, D. M.; Maibaum, T. S.E., Handbook of Logic in Computer Science, Vol. II, (1992), Oxford University Press)
[3] Baader, F.; Nipkow, T., Term Rewriting and All That, (1998), Cambridge University Press
[4] Beckmann, A., Exact bound for lengths of reductions in typed λ-calculus, J. Symb. Log., 66, 1277-1285, (2001) · Zbl 1159.03305
[5] Church, A.; Rosser, J. B., Some properties of conversion, Trans. Am. Math. Soc., 39, 3, 472-482, (1936) · JFM 62.0037.03
[6] Curry, H. B.; Feys, R.; Craig, W., Combinatory Logic, Vol. 1, (1974), North-Holland
[7] Dehornoy, P.; van Oostrom, V., Z: proving confluence by monotonic single-step upper bound functions, (Logical Models of Reasoning and Computation, (May 2008), Steklov Mathematical Institute: Steklov Mathematical Institute Moscow, Russia), 5-8
[8] Fujita, K., On upper bounds on the Church-Rosser theorem, (Third International Workshop on Rewriting Techniques for Program Transformation and Evaluation, Porto, Portugal, (23rd June 2016)), 235, 16-31, (2017)
[9] Girard, J.-Y.; Lafont, Y.; Taylor, P., Proofs and Types, Cambridge Tracts in Theoretical Computer Science (Book 7), (1989), Cambridge University Press
[10] Grzegorczyk, A., Some classes of recursive functions, Rozprawy Mathematyczne, IV, 1-48, (1953)
[11] Hindley, J. R., Reductions of residuals are finite, Trans. Am. Math. Soc., 240, 345-361, (1978) · Zbl 0387.03007
[12] Hindley, J. R.; Seldin, J. P., Introduction to Combinators and λ-Calculus, London Mathematical Society Student Texts, vol. 1, (1986), Cambridge University Press · Zbl 0614.03014
[13] Hindley, J. R.; Seldin, J. P., Lambda-Calculus and Combinators, an Introduction, (2008), Cambridge University Press · Zbl 1149.03016
[14] Ketema, J.; Simonsen, J. G., Least upper bounds on the size of confluence and Church-Rosser diagrams in term rewriting and λ-calculus, ACM Trans. Comput. Log., 14, 4, (2013), 1-28 · Zbl 1354.68143
[15] Khasidashvili, Z., β-reductions and β-developments with the least number of steps, (Martin-Löf, P.; Mints, G., International Conference on Computer Logic, COLOG-88, Tallinn, USSR, 12-16 December 1988, Lecture Notes in Computer Science, vol. 417, (1990)), 105-111
[16] Loader, R., Notes on Simply Typed Lambda Calculus, (1998), School of Informatics at the University of Edinburgh, Laboratory for Foundations of Computer Science, Technical Reports ECS-LFCS-98-381
[17] Nakazawa, K.; Fujita, K., Compositional Z: confluence proofs for permutative conversion, Stud. Log., 104, 1205-1224, (2016) · Zbl 1368.03020
[18] Terese, Term Rewriting Systems, Cambridge Tracts in Theoretical Computer Science (Book 55), (2003), Cambridge University Press
[19] Sørensen, M. H., A note on shortest developments, Log. Methods Comput. Sci., 3, 4:2, 1-8, (2007) · Zbl 1131.68039
[20] Sørensen, M. H.; Urzyczyn, P., Lectures on the Curry-Howard Isomorphism, (2006), Elsevier · Zbl 1183.03004
[21] Takahashi, M., Parallel reductions in λ-calculus, J. Symb. Comput., 7, 113-123, (1989) · Zbl 0661.03008
[22] Takahashi, M., Parallel reductions in λ-calculus, Inf. Comput., 118, 120-127, (1995) · Zbl 0827.68060
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.