zbMATH — the first resource for mathematics

Strong normalization of classical natural deduction with disjunctions. (English) Zbl 1141.03027
In $$\lambda\mu$$-calculus, a vacuous $$\mu$$-term, namely $$\mu aM$$ with no occurrence of $$a$$ in $$M$$, causes trouble, which the authors call erasing-continuation, in connexion with CPS-translation. (‘CPS’ is for ‘continuation passing style’.) This difficulty was overlooked by P. de Groote in his article [“Strong normalization of classical natural deduction with disjunction”, Lect. Notes Comput. Sci. 2044, 182–196 (2001; Zbl 0981.03027)], and so his proof of strong normalization is incomplete. To overcome the difficulty, the authors use the device of augmentations which they introduced in a previous paper [J. Symb. Log. 68, No. 3, 851–859 (2003); Corrigendum ibid. 68, No. 4, 1415–1416 (2003; Zbl 1058.03060)]. To a term $$M$$, a set, $$\text{Aug}(M)$$, of non-vacuous terms are associated in such a way that any reduction of $$M$$ is simulated by terms in $$\text{Aug}(M)$$ while avoiding erasure of continuation. Thus, in this paper, the authors complete a proof of strong normalization of the $$\lambda\mu$$-calculus with $$\rightarrow$$, $$\wedge$$, $$\vee$$, and $$\perp$$. They extend the strong normalization proof to the calculus that incorporates general elimination rules of J. von Plato [Arch. Math. Logic 40, No. 7, 541–567 (2001; Zbl 1021.03050)]. {The authors’ citation ‘Annals of\hbox…’ is in error.} This calculus allows permutative conversions and thus provides the sub-formula property.

MSC:
 03F05 Cut-elimination and normal-form theorems 03B05 Classical propositional logic 03B40 Combinatory logic and lambda calculus
Full Text:
References:
 [1] Andou, Y., Church – rosser property of a simple reduction for full first-order classical natural deduction, Annals of pure and applied logic, 119, 225-237, (2003) · Zbl 1016.03006 [2] P.-L. Curien, H. Herbelin, The duality of computation, in: Proc. 5th International Conference on Functional Programming, ICFP ’00, 2000, pp. 233-243 · Zbl 1321.68146 [3] David, R.; Nour, K., A short proof of the strong normalization of classical natural deduction with disjunction, Journal of symbolic logic, 68, 4, 1277-1288, (2003) · Zbl 1066.03056 [4] de Groote, P., A simple calculus of exception handling, (), 201-215 · Zbl 1063.68565 [5] de Groote, P., Strong normalization of classical natural deduction with disjunction, (), 182-196 · Zbl 0981.03027 [6] de Groote, P., On the strong normalisation of intuitionistic natural deduction with permutation-conversions, Information and computation, 178, 441-464, (2002) · Zbl 1031.03071 [7] Fujita, K., Domain-free $$\lambda \mu$$-calculus, Theoretical informatics and applications, 34, 6, 433-466, (2000) · Zbl 0974.68032 [8] T. Griffin, A formulae-as-types notion of control, in: 17th Ann. ACM Symp. on Principles of Programming Languages, POPL ’90, 1990, pp. 47-58 [9] Joachimski, F.; Matthes, R., Standardization and confluence for a lambda calculus with generalized applications, (), 141-155 · Zbl 0964.03014 [10] Joachimski, F.; Matthes, R., Short proofs of normalization for the simply-typed $$\lambda$$-calculus, permutative conversions and Gödels’s T, Archive for mathematical logic, 42, 59-87, (2003) · Zbl 1025.03010 [11] Matthes, R., Stabilization — an alternative to double-negation translation for classical natural deduction, (), 167-199 · Zbl 1102.03008 [12] Matthes, R., Non-strictly positive fixed-points for classical natural deduction, Annals of pure and applied logic, 133, 205-230, (2005) · Zbl 1066.03057 [13] Nakazawa, K.; Tatsuta, M., Strong normalization proof with CPS-translation for second order classical natural deduction, Journal of symbolic logic, Journal of symbolic logic, 68, 4, 1415-1416, (2003), Corrigendum is available in · Zbl 1058.03060 [14] Nakazawa, K., An isomorphism between cut-elimination procedure and proof reduction, (), 336-350 · Zbl 1215.03067 [15] Nour, K.; Saber, K., (), 31-39 [16] Ohori, A., The logical abstract machine: A curry – howard isomorphism for machine code, (), 300-318 · Zbl 0988.68042 [17] Parigot, M., $$\lambda \mu$$-calculus: an algorithmic interpretation of classical natural deduction, (), 190-201 · Zbl 0925.03092 [18] Parigot, M., Strong normalization for second order classical natural deduction, Journal of symbolic logic, 62, 4, 1461-1479, (1997) · Zbl 0941.03063 [19] Takahashi, M., Parallel reduction in $$\lambda$$-calculus, Information and computation, 118, 1, 120-127, (1995) · Zbl 0827.68060 [20] Tatsuta, M.; Mints, G., A simple proof of second-order strong normalization with permutative conversions, Annals of pure and applied logic, 136, 134-155, (2005) · Zbl 1095.03057 [21] von Plato, J., Natural deduction with general elimination rules, Annals of mathematical logic, 40, 7, 541-567, (2001) · Zbl 1021.03050 [22] P. Wadler, Call-by-value is dual to call-by-name, in: C. Runciman, O. Shivers (Eds.), in: Proc. International Conference on Functional Programming, ICFP ’03, 2003, pp. 189-201 · Zbl 1315.68060 [23] Yamagata, Y., Strong normalization of second order symmetric lambda-mu calculus, Information and computation, 193, 1, 1-20, (2004) · Zbl 1051.03016
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.