An equational characterization of the poly-time functions on any constructor data structure

Abstract

We give a purely syntactical, equational characterization of the poly-time functions on any constructor data structure (free algebra). The equations defining a function f have the shape of simple patterns: (f (c y1 : : :ym)x2 : : :xn) = r, where c is a constructor, y1,. . . ,ym, x2,. . . , xn are different variables. There are restrictions on the right-hand sides (rhs) r. The first restrictions concern the general shape of calls to mutually recursive functions, and they imply that we recur on first argument. To express the two main restrictions on rhs we use a concept of \critical position" which is closely related to the notion \safe" of Bellantoni and Cook, and to the \tiers" of Leivant. A function f's i'th argument position is critical i in this position f may have access to the result of a recursive call. Then the two main restrictions are (there will be some exceptions for if-then-else, projections and unary addition):

1. The first position of every recursive function is noncritical. 2. Every rhs is linear in all variables from critical positions in the lhs.

Say that a function g on input X1; : : :;Xk \doubles" Xi if the length of (gX) is at least twice the length of Xi. The purpose of (1) and (2) is to forbid doubling of arguments in critical positions. (1) forbids doubling by recursion (which otherwise would have been possible for i = 1). (2) forbids explicit doubling of a variable from position i.