Research article
Special Issues
Normalization proofs for the un-typed μμ-calculus
-
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.
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
-
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.
|
-
-
-
-