Strong normalizability for the combined system of the typed lmbda calculus and an arbitrary convergent term rewrite system

ABSTRACT

We give a proof of strong normalizability of the typed &lgr;-calculus extended by an arbitrary convergent term rewriting system, which provides the affirmative answer to the open problem proposed in Breazu-Tannen [1]. Klop [6] showed that a combined system of the untyped &lgr;-calculus and convergent term rewriting system is not Church-Rosser in general, though both are Church-Rosser. It is well-known that the typed &lgr;-calculus is convergent (Church-Rosser and terminating). Breazu-Tannen [1] showed that a combined system of the typed &lgr;-calculus and an arbitrary Church-Rosser term rewriting system is again Church-Rosser. Our strong normalization result in this paper shows that the combined system of the typed &lgr;-calculus and an arbitrary convergent term rewriting system is again convergent. Our strong normalizability proof is easily extended to the case of the second order (polymorphically) typed lambda calculus and the case in which &mgr;-reduction rule is added.

REFERENCES

• 1: V. Breazu-Tannen, "Combining Algebra and Higher-Order Types', Proceedings of 3rd IEEE Syrup. on Logic in Computer Science, Edinburgh, 1988.
• 2: N. Dershowitz-NI. Okada, "Proof-theoretic Techniques for Theory of Rewriting", Proceedings of 3rd IEEE Syrup. on Logic in Computer Science, Edinburgh, 1988.
• 3: N. Dershowitz-M. Okada, "Conditional Equational Programming and Conditional Rewriting", Proc. of International Conference on Fifth Generation Computer Systems, ICOT, Tokyo, 1988.
• 4: J. Y. Girard, "Une extension de rinterpretatin de Godel a r analyse, et son application a l'elimination des coupures dans l'analyse et la theorie des types", in Proceedings of the Second Scandinavian Logic Symposium, ed. Fenstad, 1971, pp. 63-92.
• 5: G. Huet, D. C. Oppen, Equations and Rewrite Rules, in Formal Language Theory; A Survey, ed. Book, 1980.
• 6: J. W. Klop, Combinatory Reduction Systems, Tract 129, Math Center, Amsterdam, 1980.
• 7: P. Martin-Lof, "Hauptsatz for the Theory of Species", in Proceedings of the Second Scandinavian Logic Symposium, ed. Fenstad, 1971, pp. 217-233.
• 8: M. Okada, Introduction to Proof Theory for Computer Science, Lecture Notes, Laboratoire de Recherche en Informatique, Universi~e de Paris XI, Orsay, France, 1988.
• 9: D. Prawitz, "Ideas and Results in Proof Theory", in Proceedings of the Second Scandinavian Logic Symposium, ed. Fenstad, 1971, pp. 235-307.
• 10: Yoshihito Toyama, On the Church-Rosser property for the direct sum of term rewriting systems, Journal of the ACM (JACM), v.34 n.1, p.128-143, Jan. 1987 [doi>10.1145/7531.7534]

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Lambda calculus and related systems

Additional Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Computational logic

General Terms:
Algorithms, Design, Theory