Abstract
This paper gives new confluence proofs for several lambda calculi with permutation-like reduction, including lambda calculi corresponding to intuitionistic and classical natural deduction with disjunction and permutative conversions, and a lambda calculus with explicit substitutions. For lambda calculi with permutative conversion, naïve parallel reduction technique does not work, and (if we consider untyped terms, and hence we do not use strong normalization) traditional notion of residuals is required as Ando pointed out. This paper shows that the difficulties can be avoided by extending the technique proposed by Dehornoy and van Oostrom, called the Z theorem: existence of a mapping on terms with the Z property concludes the confluence. Since it is still hard to directly define a mapping with the Z property for the lambda calculi with permutative conversions, this paper extends the Z theorem to compositional functions, called compositional Z, and shows that we can adopt it to the calculi.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
Accattoli, B., and D. Kesner, The permutative \({\lambda}\)-calculus, in Proceedings of the International Conference on Logic Programming and Automated Reasoning (LPAR 2012), vol. 7180 of Lecture Notes in Computer Science, 2012, pp. 15–22.
Ando Y.: Church-rosser property of a simple reduction for full first-order classical natural deduction. Annals of Pure and Applied Logic 119, 225–237 (2003)
Baba K., Hirokawa S., Fujita K.: Parallel reduction in type free \({\lambda\mu}\)-calculus. Electronic Notes in Theoretical Computer Science 42, 52–66 (2001)
Church A., Rosser J.B.: Some properties of conversion. Transactions of ASM 39(3), 472–482 (1936)
Dehornoy, P., and V. van Oostrom, Z., Proving confluence by monotonic single-step upperbound functions, in Logical Models of Reasoning and Computation (LMRC-08), 2008.
Hardin, T., Résultats de confluence pour les règles fortes de la logique combinatoire et liens avec les lambda-calculus, Ph.D. Thesis, Université de Paris VII, 1987.
Kesner D.: Confluence of extensional and non-extensional \({\lambda}\)-calculi with explicit substitutions. Theoretical Computer Science 238, 183–220 (2000)
Kikuchi K.: Call-by-name reduction and cut-elimination in classical logic. Annals of Pure and Applied Logic 153(1–3), 38–65 (2008)
Komori Y., Matsuda N., Yamakawa F.: A simplified proof of the Church–Rosser theorem. Studia Logica 102(1), 175–183 (2013)
Nakazawa, K., and T. Nagai, Reduction system for extensional lambda-mu calculus, in 25th International Conference on Rewriting Techniques and Applications joint with the 12th International Conference on Typed Lambda Calculi and Applications (RTA-TLCA 2014), vol. 8560 of Lecture Notes in Computer Science, 2014, pp. 349–363.
Parigot, M., \({\lambda\mu}\)-calculus: an algorithmic interpretation of classical natural deduction, in Proceedings of the International Conference on Logic Programming and Automated Reasoning (LPAR ’92), vol. 624 of Lecture Notes in Computer Science, Springer, Berlin, 1992, pp. 190–201.
Prawitz D.: Natural Deduction: A Proof Theoretical Study. Dover, Mineola (2006)
Takahashi M.: Parallel reduction in \({\lambda}\)-calculus. Information and Computation 118, 120–127 (1995)
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Nakazawa, K., Fujita, Ke. Compositional Z: Confluence Proofs for Permutative Conversion. Stud Logica 104, 1205–1224 (2016). https://doi.org/10.1007/s11225-016-9673-0
Received:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s11225-016-9673-0