Analysis of Bounds for Lengths of Reductions in Typed λ-calculus
Abstract
We analyze bounds for the lengths of arbitrary reduction sequences of terms in typed ¸-calculus, consider some estimates obtained by the other authors and compare these estimates. The cut elimination and normalization algorithms are also investigated in this paper. Thereafter we re¯ne the estimates achieved in [3] (for pure implicational logic only) by supplement of ´-conversion and then we extend evaluations to ¯rst-order logic.
References
Baaz, M., Leitsch, A.: Cut-Elimination and Redundancy-Elimination by Resolution. Journal of Symbolic Computation, 29: 149-176, 2000.
Beckmann, A., Weiermann, A.: Analyzing Gödel's T via expanded head reduction trees. Mathematical Logics Quarterly, 46:517-536, 2000.
Beckmann, A.:Exactboundsforlengthsofreductionsintypedlambda-calculus.J.SymbolicLogic,66:1277-1285,2001.
Galoyan, T.: Strong normalization for first-order logic. Transactions of the Institute for Informatics and Automation Problems of the NAS of RA. Mathematical Problems of Computer Science 28, pp. 45-50, 2007.
Kleene, S.: Introduction to Metamathematics. D. van Nostrand, New York, 1952.
Schwichtenberg, H.: Normalization. In F.L. Bauer, editor, Logic, Algebra and Computation. Proceedings of the International Summer School Marktoberdorf, Germany, July 25 - August 6, 1989, Series F: Computer and Systems Sciences, Vol. 79, pages 201-237. NATO Advanced Study Institute, Springer Verlag, Berlin, Heidelberg, New York, 1991.
Schwichtenberg, H.: An upper bound for reduction sequences in the typed lambda-calculus. Archive for Mathematical Logic, 30:405-408, 1991.
Schwichtenberg, H.: Proof theory. Lecture notes, Mathematisches Institut der Universität München, Germany, 1994.
Downloads
Published
How to Cite
Issue
Section
License
This work is licensed under a Creative Commons Attribution-NonCommercial 4.0 International License.
