×

zbMATH — the first resource for mathematics

The typed lambda-calculus is not elementary recursive. (English) Zbl 0411.03050

MSC:
03F20 Complexity of proofs
03B40 Combinatory logic and lambda calculus
03D99 Computability and recursion theory
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Aho, A.V.; Hopcroft, J.E.; Ullman, J.D., The design and analysis of computer algorithms, (1974), Addison-Wesley Reading, MA · Zbl 0207.01701
[2] Church, A., The calculi of lambda-conversion, Annals of math. studies no. 6, (1941), Princeton · JFM 67.0041.01
[3] Friedman, H., Equality between functionals, () · Zbl 0311.02040
[4] Gödel, K., On an extension of finitary mathematics which has not yet been used, Dialectica, 12, (1958)
[5] Grzegorczyk, A., Some classes of recursive functions, Rozprawy mat., 4, 46, (1953)
[6] Henkin, L., A theory of propositional types, Fund. math., 52, 323-344, (1963) · Zbl 0127.00609
[7] Hindley, J.R.; Lercher, B.; Seldin, J.P., Introduction to combinatory logic, (), Lecture Note No. 7 · Zbl 0269.02005
[8] Huet, G., A unification algorithm for typed λ-calculus, Theoret. comput. sci., 1, 27-57, (1975) · Zbl 0337.68027
[9] Kleene, S.L., Introduction to mathematics, (1952), Van Nostrand New York
[10] Lauchli, H., An abstract notion of realizability for which the intuitionistic predicate calculus is complete, () · Zbl 0216.00501
[11] Mann, C., The connection between equivalence of proofs and Cartesian closed categories, Proc. London math. soc. (3), 31, 3, (1975) · Zbl 0317.02036
[12] Milner, R., Fully abstract models of typed λ-calculi, Theoret. comput. sci., 4, 1-22, (1977) · Zbl 0386.03006
[13] Meyer, A.R., The inherent computational complexity of theories of ordered sets, () · Zbl 0361.02061
[14] Montague, R., The proper treatment of quantification in ordinary English, ()
[15] Prawitz, D., Natural deduction, (1965), Almqvist and Wiksell · Zbl 0173.00205
[16] Schwichtenberg, H., Definierbare functionem im λ-kalkul mit typen, Arch. math. logic, 17, 3-4, (1975-1976) · Zbl 0329.02011
[17] Statman, R., Intuitionistic propositional logic is polynomial-space complete, Theoret. comput. sci., 9, 67-72, (1979) · Zbl 0411.03049
[18] R. Statman, Completeness, invariance and λ-definability, J. Symbolic Logic, to appear. · Zbl 0487.03006
[19] Stockmeyer, L.V., The polynomial-time hierarchy, Theoret. comput. sci., 3, 1-22, (1976) · Zbl 0353.02024
[20] Tait, W.W., A realizability interpretation of the theory of species, () · Zbl 1111.03004
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.