Normalization proofs for the un-typed <em>μμ</em>-calculus

Péter Battyányi; Karim Nour; Péter Battyányi; Karim Nour

doi:10.3934/math.2020239

AIMS Mathematics

2020, Volume 5, Issue 4: 3702-3713. doi: 10.3934/math.2020239

Previous Article Next Article

Research article Special Issues

Normalization proofs for the un-typed μμ-calculus

Péter Battyányi ¹,
Karim Nour ^{2
,
,}

1.
Department of Computer Science, Faculty of Informatics, University of Debrecen, Kassai út 26, 4028 Debrecen, Hungary
2.
Université Grenoble Alpes, Université Savoie Mont Blanc, CNRS, LAMA, LIMD, 73000 Chambéry, France

Received: 04 October 2019 Accepted: 09 April 2020 Published: 20 April 2020
MSC : 03B40, 03B70, 03F05, 68Q42

A long-standing open problem of Parigot has been solved by David and Nour, namely, they gave a syntactical and arithmetical proof of the strong normalization of the untyped μμ'-reduction. In connection with this, we present in this paper a proof of the weak normalization of the μ and μ'-rules. The algorithm works by induction on the complexity of the term. Our algorithm does not necessarily give a unique normal form: sometimes we may get different normal forms depending on our choice. We also give a simpler proof of the strong normalization of the same reduction. Our proof is based on a notion of a norm defined on the terms.
- λμ-calculus,
- μμ'-calculus,
- strong normalization,
- weak normalization,
- normalization algorithm
Citation: Péter Battyányi, Karim Nour. Normalization proofs for the un-typed μμ-calculus[J]. AIMS Mathematics, 2020, 5(4): 3702-3713. doi: 10.3934/math.2020239

Related Papers:

Abstract

A long-standing open problem of Parigot has been solved by David and Nour, namely, they gave a syntactical and arithmetical proof of the strong normalization of the untyped μμ'-reduction. In connection with this, we present in this paper a proof of the weak normalization of the μ and μ'-rules. The algorithm works by induction on the complexity of the term. Our algorithm does not necessarily give a unique normal form: sometimes we may get different normal forms depending on our choice. We also give a simpler proof of the strong normalization of the same reduction. Our proof is based on a notion of a norm defined on the terms.

References

[1]	M. Parigot, Free Deduction: An Analysis of "Computations" in Classical Logic, In: A. Voronkov, editors. Logic Programming Lecture Notes in Artificial Intelligence 592, Berlin, Heidelberg: Springer-Verlag, 1992, 361-380.
[2]	M. Parigot, λμ-calculus: An algorithmic interpretation of classical natural deduction, In: A. Voronkov, editors. Logic Programming and Automated Reasoning, LPAR 1992, Lecture Notes in Artificial Intelligence 624, Berlin, Heidelberg: Springer-Verlag, 1992, 190-201.
[3]	K. Nour, La valeur d'un entier classique en λμ-calcul, Archive Math. Logic, 36 (1997), 461-473. doi: 10.1007/s001530050076
[4]	P. de Groote, An environment machine for the λμ-calculus, Math. Struct. Comput. Sci., 8 (1998), 637-669. doi: 10.1017/S0960129598002667
[5]	W. Py, Confluence en λμ-calcul [dissertation], University of Chambéry, 1998, 117.
[6]	A. Saurin, Böhm theorem and Böhm trees for the Λμ-calculus, Theor. Comput. Sci., 435 (2012), 106-138. doi: 10.1016/j.tcs.2012.02.027
[7]	E. Polonovsky, Substitutions explicites, logique et normalisation [dissertation], Paris 7, 2004, 257.
[8]	R. David, K. Nour, Arithmetical proofs of strong normalization results for symmetric lambda calculi, Fundamenta Informaticae, 77 (2007), 489-510.
[9]	P. Battyányi, Normalization properties of symmetric logical calculi [dissertation], University of Chambéry, 2007, 118.

Reader Comments

Your name:*

Email:*
© 2020 the Author(s), licensee AIMS Press. This is an open access article distributed under the terms of the Creative Commons Attribution License (http://creativecommons.org/licenses/by/4.0)