Research article Special Issues

Normalization proofs for the un-typed μμ-calculus

  • 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

    Related Papers:

  • 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.


    加载中


    [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
  • © 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)
通讯作者: 陈斌, bchen63@163.com
  • 1. 

    沈阳化工大学材料科学与工程学院 沈阳 110142

  1. 本站搜索
  2. 百度学术搜索
  3. 万方数据库搜索
  4. CNKI搜索

Metrics

Article views(2492) PDF downloads(205) Cited by(0)

Article outline

Other Articles By Authors

/

DownLoad:  Full-Size Img  PowerPoint
Return
Return

Catalog