An Abstract Strong Normalization Theorem

  • Ulrich Berger
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3634)


We prove a strong normalization theorem for abstract term rewriting systems based on domain-theoretic models. The theorem applies to extensions of Gödel’s system T by various forms of recursion related to bar recursion for which strong normalization was hitherto unknown.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Plotkin, G.: LCF considered as a programming language. Theoretical Computer Science 5, 223–255 (1977)CrossRefMathSciNetGoogle Scholar
  2. 2.
    Berger, U.: Continuous semantics for strong normalization. In: Cooper, S.B., Löwe, B., Torenvliet, L. (eds.) CiE 2005. LNCS, vol. 3526, pp. 23–34. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  3. 3.
    Berger, U.: Strong normalization for applied lambda calculi. Submitted to: Logical Methods in Computer Science, January 2005 (2005)Google Scholar
  4. 4.
    Spector, C.: Provably recursive functionals of analysis: a consistency proof of analysis by an extension of principles in current intuitionistic mathematics. In: Dekker, F.D.E. (ed.) Recursive Function Theory: Proc. Symposia in Pure Mathematics, vol. 5, pp. 1–27. American Mathematical Society, Providence (1962)Google Scholar
  5. 5.
    Howard, W.A.: Functional interpretation of bar induction by bar recursion. Composito Mathematicae 20, 107–124 (1968)zbMATHGoogle Scholar
  6. 6.
    Berardi, S., Bezem, M., Coquand, T.: On the computational content of the axiom of choice. Journal of Symbolic Logic 63, 600–622 (1998)zbMATHCrossRefMathSciNetGoogle Scholar
  7. 7.
    Berger, U., Oliva, P.: Modified bar recursion and classical dependent choice. In: Logic Colloquium 2001, Springer, Heidelberg (2005)Google Scholar
  8. 8.
    Berger, U.: A computational interpretation of open induction. In: Titsworth, F. (ed.) Proceedings of the Ninetenth Annual IEEE Symposium on Logic in Computer Science, pp. 326–334. IEEE Computer Society, Los Alamitos (2004)CrossRefGoogle Scholar
  9. 9.
    Scott, D.S.: Outline of a mathematical theory of computation. In: 4th Annual Princeton Conference on Information Sciences and Systems, pp. 169–176 (1970)Google Scholar
  10. 10.
    Griffor, E., Lindström, I., Stoltenberg-Hansen, V.: Mathematical theory of domains. Cambridge University Press, Cambridge (1993)Google Scholar
  11. 11.
    Abramsky, S., Jung, A.: Domain theory. In: Abramsky, S., Gabbay, D.M., Maibaum, T.S.E. (eds.) Handbook of Logic in Computer Science, vol. 3, pp. 1–168. Clarendon Press, Oxford (1994)Google Scholar
  12. 12.
    Raoult, J.C.: Proving open properties by induction. Information processing letters 29, 19–23 (1988)zbMATHCrossRefMathSciNetGoogle Scholar
  13. 13.
    Coquand, T.: A note on the open induction principle (1997)Google Scholar
  14. 14.
    Mahboubi, A.: An induction principle over real numbers. Submitted to Archive for Mathematical Logic (2004)Google Scholar
  15. 15.
    Nash-Williams, C.: On well-quasi-ordering finite trees. Proc. Cambridge Phil. Soc. 59, 833–835 (1963)zbMATHCrossRefMathSciNetGoogle Scholar
  16. 16.
    Tait, W.: Normal form theorem for barrecursive functions of finite type. In: Fenstad, J. (ed.) Proceedings of the Second Scandinavian Logic Symposium, pp. 353–367. North–Holland, Amsterdam (1971)CrossRefGoogle Scholar
  17. 17.
    Girard, J.Y.: Interprétation functionelle et élimination des coupures de l’arithmétique d’ordre supérieur. PhD thesis, Université Paris VII (1972)Google Scholar
  18. 18.
    Bezem, M.: Strong normalization of barrecursive terms without using infinite terms. Archive for Mathematical Logic 25, 175–181 (1985)zbMATHCrossRefMathSciNetGoogle Scholar
  19. 19.
    Ong, L., Ritter, E.: A generic normalisation argument: Application to the calculus of constructions. In: Meinke, K., Börger, E., Gurevich, Y. (eds.) CSL 1993. LNCS, vol. 832, pp. 261–279. Springer, Heidelberg (1994)CrossRefGoogle Scholar
  20. 20.
    Hyland, J., Ong, C.H.: Modified realizability semantics and strong normalization proofs. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol. 664, pp. 179–194. Springer, Heidelberg (1993)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Ulrich Berger
    • 1
  1. 1.University of Wales Swansea 

Personalised recommendations