# zbMATH — the first resource for mathematics

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.

##### MSC:
 03B40 Combinatory logic and lambda calculus
Automath
Full Text:
##### References:
  Barendregt, H. P., The Lambda Calculus. Its Syntax and Semantics, (1984), North-Holland · Zbl 0551.03007  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)  Baader, F.; Nipkow, T., Term Rewriting and All That, (1998), Cambridge University Press  Beckmann, A., Exact bound for lengths of reductions in typed λ-calculus, J. Symb. Log., 66, 1277-1285, (2001) · Zbl 1159.03305  Church, A.; Rosser, J. B., Some properties of conversion, Trans. Am. Math. Soc., 39, 3, 472-482, (1936) · JFM 62.0037.03  Curry, H. B.; Feys, R.; Craig, W., Combinatory Logic, Vol. 1, (1974), North-Holland  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  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)  Girard, J.-Y.; Lafont, Y.; Taylor, P., Proofs and Types, Cambridge Tracts in Theoretical Computer Science (Book 7), (1989), Cambridge University Press  Grzegorczyk, A., Some classes of recursive functions, Rozprawy Mathematyczne, IV, 1-48, (1953)  Hindley, J. R., Reductions of residuals are finite, Trans. Am. Math. Soc., 240, 345-361, (1978) · Zbl 0387.03007  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  Hindley, J. R.; Seldin, J. P., Lambda-Calculus and Combinators, an Introduction, (2008), Cambridge University Press · Zbl 1149.03016  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  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  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  Nakazawa, K.; Fujita, K., Compositional Z: confluence proofs for permutative conversion, Stud. Log., 104, 1205-1224, (2016) · Zbl 1368.03020  Terese, Term Rewriting Systems, Cambridge Tracts in Theoretical Computer Science (Book 55), (2003), Cambridge University Press  Sørensen, M. H., A note on shortest developments, Log. Methods Comput. Sci., 3, 4:2, 1-8, (2007) · Zbl 1131.68039  Sørensen, M. H.; Urzyczyn, P., Lectures on the Curry-Howard Isomorphism, (2006), Elsevier · Zbl 1183.03004  Takahashi, M., Parallel reductions in λ-calculus, J. Symb. Comput., 7, 113-123, (1989) · Zbl 0661.03008  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.