Compositional Z: confluence proofs for permutative conversion. (English) Zbl 1368.03020

Nakazawa, Koji; Fujita, Ken-etsu

Stud. Log. 104, No. 6, 1205-1224 (2016).

The Z-theorem of P. Dehorney and Z. van Oostrom [“Proving confluence by monotonic single-step upperbound functions”, in: Logical models of reasoning and computation (LMRC-08) (2008)] allows the proof of confluence for a number of variants of the \(\lambda\)-calculus. In the current paper, the authors generalise this to a compositional Z-theorem, which is easily proved from the Z-theorem. The new theorem allows, in addition, proofs of confluence for \(\lambda\)-calculi corresponding to intuitionistic and classical natural deduction with disjunction and permutative conversions as well as a \(\lambda\)-calculus with explicit substitution.

Reviewer: Martin W. Bunder (Wollongong)

MSC:

03B40

Combinatory logic and lambda calculus

Keywords:

lambda calculus; lambda-mu calculus; confluence; permutative conversion

References:

[1]	Accattoli, B., and D. Kesner, The permutative \({λ}\)-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. · Zbl 1352.03019
[2]	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) · Zbl 1016.03006
[3]	Baba, K.; Hirokawa, S.; Fujita, K., Parallel reduction in type free \({λμ}\)-calculus, Electronic Notes in Theoretical Computer Science, 42, 52-66, (2001) · Zbl 0971.68019
[4]	Church, A.; Rosser, J.B., Some properties of conversion, Transactions of ASM, 39, 472-482, (1936) · Zbl 0014.38504
[5]	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. · Zbl 1136.03036
[6]	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. · Zbl 0971.68019
[7]	Kesner, D., Confluence of extensional and non-extensional \({λ}\)-calculi with explicit substitutions, Theoretical Computer Science, 238, 183-220, (2000) · Zbl 0944.68033
[8]	Kikuchi, K., Call-by-name reduction and cut-elimination in classical logic, Annals of Pure and Applied Logic, 153, 38-65, (2008) · Zbl 1136.03036
[9]	Komori, Y.; Matsuda, N.; Yamakawa, F., A simplified proof of the church-rosser theorem, Studia Logica, 102, 175-183, (2013) · Zbl 1338.03017
[10]	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. · Zbl 1417.03133
[11]	Parigot, M., \({λμ}\)-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. · Zbl 0925.03092
[12]	Prawitz D.: Natural Deduction: A Proof Theoretical Study. Dover, Mineola (2006) · Zbl 0173.00205
[13]	Takahashi, M., Parallel reduction in \({λ}\)-calculus, Information and Computation, 118, 120-127, (1995) · Zbl 0827.68060