zbMATH — the first resource for mathematics

Functions over free algebras definable in the simply typed lambda calculus. (English) Zbl 0792.03006
Summary: We show that a function over a free algebra is definable in the simply typed \(\lambda\)-calculus (modulo the Böhm-Berarducci embedding) iff it is generated by predicative monotonic recurrence. Monotonic recurrence here is the generalization of iteration-with-parameters from \(\mathbb{N}\) to arbitrary free algebras, and our predicativity condition uses the notion of tiers introduced by the author [Feasible mathematics, Proc. Math. Sci. Inst. Workshop, Ithaca/NY 1989, Prog. Comput. Sci. Appl. Log. 9, 281-291 (1990; Zbl 0772.03020)]. In fact, we show that the same functions are generated by tiered monotonic recurrence whether 2 tiers or all finite tiers are used.

03B40 Combinatory logic and lambda calculus
Full Text: DOI
[1] Abiteboul, S.; Vianu, V., Fixpoint extensions of first-order logic and Datalog-like languages, Proc. 4th IEEE symp. on logic in computer science, 71-79, (1989) · Zbl 0716.68020
[2] Abiteboul, S.; Vianu, V., Generic computation and its complexity, Proc. 23rd ACM symp. on theory of computing, 209-219, (1991)
[3] Bellantoni, S.; Cook, S., A new recursion-theoretic characterization of the poly-time functions, Computational complexity, 2, 97-110, (1992) · Zbl 0766.68037
[4] Bennett, C.H., Demons, engines and the second law, Sci. am., 108-116, (November 1986)
[5] Bloch, S., Functional characterizations of uniform log-depth and polylog-depth circuit families, Proc. 7th IEEE conf. on structure in complexity, 193-206, (1992)
[6] Böhm, C.; Berarducci, A., Automatic synthesis of typed λ-programs on term algebras, Theoret. comput. sci., 39, 135-154, (1985) · Zbl 0597.68017
[7] Kreisel, G., La prédicativité, Bull. soc. math. France, 88, 371-391, (1960) · Zbl 0131.00604
[8] Leivant, D., Monotonic use of space and computational complexity over abstract structures, ()
[9] Leivant, D., Subrecursion and lambda representation over free algebras, (), 281-292, Perspective in Computer Science · Zbl 0772.03020
[10] Leivant, D., Stratified functional programs and computational complexity, (), 325-333
[11] D. Leivant, Predicative Peano theories and the axiomatization of feasible mathematics, to appear.
[12] D. Leivant, Abstraction and computational complexity, to appear. · Zbl 0944.68070
[13] Leivant, D.; Marion, J.-Y., Lambda characterizations of poly-time, (), Special issue on Typed Lambda Calculi · Zbl 0788.68051
[14] Russell, Bertrand, Mathematical logic as based on the theory of types, (), 30, 150-182, (1908)
[15] Schwichtenberg, H., Definierbare funktionen im lambda-kalkul mit typen, Archiv logik grundlagenforsch., 17, 113-114, (1976) · Zbl 0329.02011
[16] Simmons, H., The realm of primitive recursion, Arch. math. logic, 27, 177-188, (1988) · Zbl 0659.03025
[17] Statman, R., The typed λ-calculus is not elementary recursive, Theoret. comput. sci., 9, 73-81, (1979) · Zbl 0411.03050
[18] Wang, Hao, A variant to Turing’s theory of computing machines, J. ACM, 4, 63-92, (1957)
[19] Zaionc, M., Λ-definability on free algebras, Ann. pure appl. logic, 51, 279-300, (1991) · Zbl 0727.03010
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.