Subrecursion and lambda representation over free algebras
Daniel M. Leivant · Birkhäuser Boston eBooks · 1990
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].