Skip to main content
SpringerLink
Log in

An Arithmetical Proof of the Strong Normalization for the λ-Calculus with Recursive Equations on Types

  • Conference paper
Typed Lambda Calculi and Applications (TLCA 2007)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 4583))

Included in the following conference series:

  • 499 Accesses

Abstract

We give an arithmetical proof of the strong normalization of the λ-calculus (and also of the λμ-calculus) where the type system is the one of simple types with recursive equations on types.

The proof using candidates of reducibility is an easy extension of the one without equations but this proof cannot be formalized in Peano arithmetic. The strength of the system needed for such a proof was not known. Our proof shows that it is not more than Peano arithmetic.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  • Barendregt, H.P.: The Lambda Calculus, Its Syntax and Semantics. North-Holland, Amsterdam (1985)

    MATH  Google Scholar 

  • Barendregt, H.P.: Lambda Calculi with types. In: Abramsky & al. pp. 117–309 (1992)

    Google Scholar 

  • Barendregt, H.P., Dekkers, W., Statman, R.: Typed lambda calculus (to appear)

    Google Scholar 

  • Berger, U., Schwichtenberg, H.: An Inverse of the Evaluation Functional for Typed lambda-calculus. LICS, pp. 203–211 (1991)

    Google Scholar 

  • Church, A.: A Formulation of the Simple Theory of Types. JSL 5 (1940)

    Google Scholar 

  • Coppo, M., Dezani, M.: A new type assignment for lambda terms. Archiv. Math. Logik (19), 139–156 (1978)

    Article  MATH  Google Scholar 

  • Coquand, T., Huet, G.: A calculus of constructions. Information and Computation (76), 95–120 (1988)

    Article  Google Scholar 

  • David, R.: Normalization without reducibility. Annals of Pure. and Applied Logic (107), 121–130 (2001)

    Article  MATH  Google Scholar 

  • David, R.: A short proof of the strong normalization of the simply typed lambda calculus www.lama.univ-savoie.fr/d̃avid

  • David, R., Nour, K.: A short proof of the strong normalization of the simply typed λμ-calculus. Schedae Informaticae 12, 27–34 (2003)

    Google Scholar 

  • David, R., Nour, K.: Arithmetical proofs of strong normalization results for the symmetric lambda-mu-calculus. In: Urzyczyn, P. (ed.) TLCA 2005. LNCS, vol. 3461, pp. 162–178. Springer, Heidelberg (2005)

    Google Scholar 

  • David, R., Nour, K.: Arithmetical proofs of strong normalization results for symmetric λ-calculi. Fundamenta Informaticae (to appear)

    Google Scholar 

  • de Groote, P.: On the Relation between the Lambda-Mu-Calculus and the Syntactic Theory of Sequential Control. LPAR, pp. 31–43 (1994)

    Google Scholar 

  • de Groote, P.: A CPS-Translation of the λμ-Calculus. In: Tison, S. (ed.) CAAP 1994. LNCS, vol. 787, pp. 85–99. Springer, Heidelberg (1994)

    Chapter  Google Scholar 

  • Doyen, J.: Quelques propriétés du typage des fonctions des entiers dans les entiers. C.R. Acad. Sci. Paris, t.321, Série 1, 663–665 (1995)

    Google Scholar 

  • Fortune, S., Leivant, D., O’Donnell, M.: Simple and Second order Types Structures. JACM 30-1, 151–185 (1983)

    Article  Google Scholar 

  • Friedman, H.: Equality between functionals. Logic Coll’73, LNM 453, pp. 22–37 (1975)

    Google Scholar 

  • Girard, J.-Y., Lafont, Y., Taylor, P.: Proofs and Types. Cambridge University Press, Cambridge (1989)

    MATH  Google Scholar 

  • Gödel, K.: Über eine bisher noch nicht benütztz Erweiterung des finiten Standpunkts. Dialectica 12, 280–287 (1958)

    Article  MATH  Google Scholar 

  • Goldfarb, W.D.: The undecidability of the 2nd order unification problem. TCS (13), 225–230 (1981)

    Article  MATH  Google Scholar 

  • Huet, G.P.: The Undecidability of Unification in Third Order Logic. Information and Control 22(3), 257–267 (1973)

    Article  Google Scholar 

  • Joachimski, F., Matthes, R.: Short proofs of normalization for the simply-typed lambda-calculus, permutative conversions and Gödel’s T. Archive for Mathematical Logic 42(1), 59–87 (2003)

    Article  MATH  Google Scholar 

  • Jung, A., Tiuryn, J.A.: A New Characterization of Lambda Definability. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol. 664, pp. 245–257. Springer, Heidelberg (1993)

    Chapter  Google Scholar 

  • Krivine, J.-L.: Un algorithme non typable dans le système F. C. R. Acad. Sci. Paris 304(5), (1987)

    Google Scholar 

  • Krivine, J.-L.: Lambda Calcul: types et modèles. Masson, Paris (1990)

    Google Scholar 

  • Krivine, J.-L.: Classical Logic, Storage Operators and Second-Order lambda-Calculus. Ann. Pure Appl. Logic 68(1), 53–78 (1994)

    Article  MATH  Google Scholar 

  • Lambek, J.: Cartesian Closed Categories and Typed Lambda-calculi. Combinators and Functional Programming Languages, pp. 136-175 (1985)

    Google Scholar 

  • Loader, R.: The Undecidability of ł-definability. In: Essays in memory of A. Church, pp. 331–342 (2001)

    Google Scholar 

  • Mendler, N.P.: Recursive Types and Type Constraints in Second-Order Lambda Calculus. LICS, pp. 30–36 (1987)

    Google Scholar 

  • Mendler, N.P.: Inductive Types and Type Constraints in the Second-Order Lambda Calculus. Ann. Pure Appl. Logic 51(1-2), 159–172 (1991)

    Article  Google Scholar 

  • Parigot, M.: Programming with proofs: a second order type theory. In: Ganzinger, H. (ed.) ESOP 1988. LNCS, vol. 300, pp. 145–159. Springer, Heidelberg (1988)

    Google Scholar 

  • Parigot, M.: On representation of data in lambda calculus. CSL, pp. 309–321 (1989)

    Google Scholar 

  • Parigot, M.: Recursive programming with proofs. Theoritical Computer Science 94, 335–356 (1992)

    Article  MATH  Google Scholar 

  • Parigot, M.: Strong Normalization for Second Order Classical Natural Deduction. LICS, pp. 39–46 (1993)

    Google Scholar 

  • Parigot, M.: λμ-calculus: An algorithmic interpretation of classical natural deduction. Journal of symbolic logic 62(4), 1461–1479 (1997)

    Article  MATH  Google Scholar 

  • Parigot, M.: Proofs of Strong Normalisation for Second Order Classical Natural Deduction. J. Symb. Log. 62(4), 1461–1479 (1997)

    Article  MATH  Google Scholar 

  • Plotkin, G.D.: Lambda-definability and logical relations. Technical report (1973)

    Google Scholar 

  • Schwichtenberg, H.: Functions definable in the simply-typed lambda calculus. Arch. Math Logik 17, 113–114 (1976)

    Article  MATH  Google Scholar 

  • Statman, R.: The Typed lambda-Calculus is not Elementary Recursive. FOCS, pp. 90–94 (1977)

    Google Scholar 

  • Statman, R.: λ-definable functionals and βη-conversion. Arch. Math. Logik 23, 21–26 (1983)

    Article  MATH  Google Scholar 

  • Statman, R.: Recursive types and the subject reduction theorem. Technical report, Carnegie Mellon University, pp. 94–164 (March 1994)

    Google Scholar 

  • Tait, W.W.: Intensional Interpretations of Functionals of Finite Type I. JSL, vol. 32(2) (1967)

    Google Scholar 

  • Weiermann, A.: A proof of strongly uniform termination for Gödel’s T by methods from local predicativity. Archive fot Mathematical Logic 36, 445–460 (1997)

    Article  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Université de Savoie, Campus Scientifique, 73376 Le Bourget du Lac, France

    René David & Karim Nour

Authors
  1. René David
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Karim Nour
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Simona Ronchi Della Rocca

Rights and permissions

Reprints and permissions

Copyright information

© 2007 Springer Berlin Heidelberg

About this paper

Cite this paper

David, R., Nour, K. (2007). An Arithmetical Proof of the Strong Normalization for the λ-Calculus with Recursive Equations on Types. In: Della Rocca, S.R. (eds) Typed Lambda Calculi and Applications. TLCA 2007. Lecture Notes in Computer Science, vol 4583. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-73228-0_8

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-73228-0_8

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-73227-3

  • Online ISBN: 978-3-540-73228-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation