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

Export file:

Format

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

Content

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

Received: , Accepted: , Published:

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

Abstract Full Text(HTML) Figure/Table

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.

Figure/Table

Supplementary

Article Metrics

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.

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.

Download full text in PDF

Export Citation

Article outline

Show full outline