Arithmetical Proofs of Strong Normalization Results for Symmetric [lambda]-calculi

• Autorzy: David R. , Nour K.
• Języki publikacji: EN

Abstrakty

EN

We give arithmetical proofs of the strong normalization of two symmetric l-calculi corresponding to classical logic. The first one is the [`(l)]m[(m~)]-calculus introduced by Curien & Herbelin. It is derived via the Curry-Howard correspondence from Gentzen's classical sequent calculus LK in order to have a symmetry on one side between "program" and "context" and on other side between "call-by-name" and "call-by-value". The second one is the symmetric lm-calculus. It is the lm-calculus introduced by Parigot in which the reduction rule m?, which is the symmetric of m, is added. These results were already known but the previous proofs use candidates of reducibility where the interpretation of a type is defined as the fix point of some increasing operator and thus, are highly non arithmetical.

Słowa kluczowe

EN

lambda calculus; symmetric calculi; classical logic; strong normalisation

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2007
• Tom: Vol. 77, nr 4
• Strony: 489--510
• Opis fizyczny: bibliogr. 32 poz.

Twórcy

autor

David R.

autor

Nour K.

• Laboratoire de Mathematiques. Campus Scientifique, F-73376 Le Bourget du Lac., France,

Bibliografia

• [1] F. Barbanera and S. Berardi. A symmetric lambda-calculus for classical program extraction. In M. Hagiya and J.C. Mitchell, editors, Proceedings of theoretical aspects of computer software, TACS'94. LNCS (789), pp. 495-515. Springer Verlag, 1994.
• [2] P. Battyanyi. Normalization results for the symmetric _μ- calculus. Private communication. To appear in his PhD thesis.
• [3] R. Constable and C. Murthy. Finding computational content in classical proofs. In G. Huet and G. Plotkin, editors, Logical Frameworks, pp. 341-362, Cambridge University Press, 1991.
• [4] P.L. Curien and H. Herbelin. The Duality of Computation. Proc. International Conference on Functional Programming, September 2000,Montral, IEEE, 2000.
• [5] P. de Groote. A CPS-translation of the lambda-mu-calculus. In S. Tison, editor, 19th International Colloquium on Trees in Algebra and Programming, CAAP'94, volume 787 of Lecture Notes in Computer Science, pp 85-99. Springer, 1994.
• [6] P. de Groote. A simple calculus of exception handling. In M. Dezani and G. Plotkin, editors, Second International Conference on Typed Lambda Calculi and Applications, TLCA'95, volume 902 of Lecture Notes in Computer Science, pp. 201-215. Springer, 1995.
• [7] R. David. Normalization without reducibility. Annals of Pure and Applied Logic (107), pp. 121-130, 2001.
• [8] R. David and K. Nour. A short proof of the strong normalization of the simply typed _μ-calculus. Schedae Informaticae n12, pp. 27-34, 2003.
• [9] R. David and K. Nour. A short proof of the strong normalization of classical natural deduction with disjunction. The Journal of Symbolic Logic n 68.4, pp. 1277 - 1288, 2003.
• [10] R. David and K. Nour. Why the usual candidates of reducibility do not work for the symetric _μ-calculus. Electronic Notes in Computer Science vol 140, pp 101-111, 2005.
• [11] R. David and K. Nour. Arithmetical proofs of some strong normalization results for the symmetric _μ-calculus. TLCA'05, LNCS 3461, pp. 162-178, 2005.
• [12] D. Dougherty, S.Ghilezan, P.Lescanne, S. Likavec. Strong normalization of the classical dual sequent calculus. LPAR'05 LNCS 3835 p 169-183.
• [13] M. Felleisen, D.P. Friedman, E.E. Kohlbecker and B.F. Duba. A Syntactic Theory of Sequential Control. Theoretical Computer Science 52, pp. 205-237, 1987.
• [14] J.-Y. Girard. A new constructive logic: classical logic. MSCS (1), pp. 255-296, 1991.
• [15] T.G. Griffin. A formulae-as-types notion of control. POPL'90 pp 47-58.
• [16] F. Joachimski and R. Matthes. Short proofs of normalization for the simply-types _-calculus, permutative conversions and Godel's T. Archive for Mathematical Logic 42, pp. 59-87, 2003.
• [17] J.-L. Krivine. Classical logic, storage operators and 2nd order lambda-calculus. Annals of Pure and Applied Logic (68), pp. 53-78, 1994.
• [18] C.R. Murthy. An evaluation semantics for classical proofs. In Proceedings of the sixth annual IEEE symposium on logic in computer science, pp. 96-107, 1991.
• [19] K. Nour. La valeur d'un entier classique en _μ-calcul. Archive for Mathematical Logic (36), pp. 461-471, 1997.
• [20] K. Nour. A non-deterministic classical logic (the _μ++-calculus). Mathematical Logic Quarterly (48), pp. 357 - 366, 2002.
• [21] K. Nour and K. Saber. A semantical proof of the strong normalization theorem of full propositionnal classical natural deduction. Archive for Mathematical Logic vol 45, pp 357-364, 2006.
• [22] M. Parigot. Free Deduction: An Analysis of "Computations" in Classical Logic. Proceedings. Lecture Notes in Computer Science, Vol. 592, Springer, pp. 361-380, 1992.
• [23] M. Parigot. _μ-calculus: An algorithm interpretation of classical natural deduction. Lecture Notes in Artificial Intelligence (624), pp. 190-201. Springer Verlag, 1992.
• [24] M. Parigot. Strong normalization for second order classical natural deduction. In Proceedings, Eighth Annual IEEE Symposium on Logic in Computer Science, pp. 39-46,Montreal, Canada, 19-23 June 1993. IEEE Computer Society Press.
• [25] M. Parigot. Classical proofs as programs. In G. Gottlob, A. Leitsch, and D. Mundici, eds., Proc. of 3rd Kurt Godel Colloquium, KGC'93, vol. 713 of Lecture Notes in Computer Science, pp. 263-276. Springer-Verlag, 1993.
• [26] M. Parigot. Proofs of strong normalization for second order classical natural deduction. Journal of Symbolic Logic, 62 (4), pp. 1461-1479, 1997.
• [27] E. Polonovsky. Substitutions explicites, logique et normalisation. PhD thesis. Paris 7, 2004.
• [28] W. Py. Confluence en _μ-calcul. PhD thesis. University of Chambéry, 1998.
• [29] N.J. Rehof and M.H. Sorensen. The _-calculus. In M. Hagiya and J.C. Mitchell, editors, Proceedings of the international symposium on theoretical aspects of computer software, TACS'94, LNCS (789), pp. 516-542. Springer Verlag, 1994.
• [30] P. Wadler. Call-by-value is dual to Call-by-name. International Conference on Functional Programming. Uppsala, August 2003.
• [31] P. Wadler. Call-by-value is dual to Call-by-name. Re-loaded. RTA'05, LNCS 3467, pp. 185-203, 2005
• [32] Y. Yamagata. Strong Normalization of Second Order Symmetric Lambda-mu Calculus. TACS 2001, Lecture Notes in Computer Science 2215, pp. 459-467, 2001.