Synopsis
As a contribution to ongoing research on computing over general algebraic structures, we consider subrecurrence over free algebras. Since the natural sub-recursive classification of functions by recurrence-nesting depth fails to separate polynomial from exponential numeric functions, we define a subrecursive hierarchy {T n}n which does, based on nesting depth of a newly defined tiered recurrence.
We show that, for algebras with at least one non-unary function, no non-trivial level of (at least one variant of) the hierarchy is finitely generated. This contrasts with the result of [Par68] about numeric subrecursion, and therefore testifies to a fundamental dissimilarity between numeric computing and general algebraic computing.
One variant of tiered recurrence yields T 2 = the functions over free algebras A-representable in the simply typed ⋋calculus 1⋋. This characterization is akin to the main result of [Zaiα]. We conclude that the class of functions over trees that are representable in 1⋋ is not finitely generated, corroborating a conjecture in [Zai90].
Research partially supported by onr grant N00014-84-K-0415 and by darpa grant F33615-81-K-1539.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
P. Axt, Iteration of primitive recursion, Zeit, für mathematische Logik u. Grundlagen d. Math 11 (1965) 253–255.
Corrado Böhm and Allessandro Berarducci, Automatic synthesis of typed X-programs on term algebras, Theoretical Computer Science 39 (1985) 135–154.
Michael Garey and David Johnson, Computers and Intractability, Freeman, San Francisco, 1979.
A. Grzegorczyk, Some classes of recursive functions, Rozprawy Mate. IV, Warsaw, 1953.
W. Heinermann, Untersuchungen über die Rekursionszahlen rekursiver Funktionen, Dissertation, Universität Munster, 1961.
Daniel Leivant, Reasoning about functional programs and complexity classes associated with type disciplines, Twenty-fourth Annual Symposium on Foundations of Computer Science (1983) 460–469.
Daniel Leivant, Stratified polymorphism, Proceedings of the Fourth Annual Symposium of logic in Computer Science, IEEE Computer Society, Washington DC, 1989, 39–47.
Daniel Leivant, Strictly predicative arithmetic, manuscript, 1990, submitted for publication.
Daniel Leivant, Monotonie use of space and computational complexity over finite structures, manuscript, 1990, submitted for publication.
H. Müller, Characterization of the elmentary functions in terms of deapth of nesting of primitive recursions, Recursive Function Theory Newsletters 5 (1973) 14–15. Initially reported in Dissertation, Universität Münster, 1973(7).
Edward Nelson, Predicative Arithmetic, Princeton University Press, Princeton, 1986.
Charles Parsons, Hierarchies of primitive recursive functions, Zeitschr. für Logik und Grundlagen der Mathematik 14 (1968) 357–376.
H.E. Rose, Subrecursion, Clarendon Press (Oxford University Press), Oxford, 1984.
Helmut Schwichtenberg, Rekursionszahlen und die Grzegorczyk-Hierarchie, Archiv für mathematische Logik 12 (1969) 85–97.
Helmut Schwichtenberg, Definierbare Funktionen im Lambda-Kal- kul mit Typen, Archiv Logik Grundlagenforsch. 17 (1976) 113–114.
Richard Statman, The typed ⋋-calculus is not elementary recursive, Theoretical Computer Science 9 (1979) 73–81.
Marek Zaionc, Word operations definable in typed ⋋-calculus, Theoretical Computer Science 52 (1987).
Marek Zaionc, How to define Junctionals on free structures in typed ⋋ calculus, in H. Ganzinger (ed.), European Symposium on Porgramming (ESOP’88), Springer-Verlag (LNCS # 379), Berlin, 1988.
Zai90 Marek Zaionc, A characterization of ⋋-definable tree operations, to appear in Information and Computation.
Zaia Marek Zaionc, ⋋-definability on free algebras, manuscript submitted for publication.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1990 Birkhäuser Boston
About this chapter
Cite this chapter
Leivant, D. (1990). Subrecursion and lambda representation over free algebras. In: Buss, S.R., Scott, P.J. (eds) Feasible Mathematics. Progress in Computer Science and Applied Logic, vol 9. Birkhäuser Boston. https://doi.org/10.1007/978-1-4612-3466-1_16
Download citation
DOI: https://doi.org/10.1007/978-1-4612-3466-1_16
Publisher Name: Birkhäuser Boston
Print ISBN: 978-0-8176-3483-4
Online ISBN: 978-1-4612-3466-1
eBook Packages: Springer Book Archive