AIMS Mathematics, 2020, 5(4): 3702-3713. doi: 10.3934/math.2020239.

Research article Special Issues

Export file:


  • RIS(for EndNote,Reference Manager,ProCite)
  • BibTex
  • Text


  • Citation Only
  • Citation and Abstract

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

Special Issues: LICMA ’19 Lebanese International Conference on Mathematics and Applications

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.
  Article Metrics

Keywords λμ-calculus; μμ'-calculus; strong normalization; weak normalization; normalization algorithm

Citation: Péter Battyányi, Karim Nour. Normalization proofs for the un-typed μμ-calculus. AIMS Mathematics, 2020, 5(4): 3702-3713. doi: 10.3934/math.2020239


  • 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.    
  • 4. P. de Groote, An environment machine for the λμ-calculus, Math. Struct. Comput. Sci., 8 (1998), 637-669.    
  • 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.    
  • 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: *   your email: *  

© 2020 the Author(s), licensee AIMS Press. This is an open access article distributed under the terms of the Creative Commons Attribution Licese (

Download full text in PDF

Export Citation

Copyright © AIMS Press All Rights Reserved