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


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.

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

Download full text in PDF

Export Citation

Article outline

Show full outline
Copyright © AIMS Press All Rights Reserved