Interpretation methods and their restrictions to polynomials have been deeply used to control the termination and complexity of first-order term rewrite systems. This paper extends interpretation methods to a pure higher order functional language. We develop a theory of higher order functions that is well-suited for the complexity analysis of this programming language. The interpretation domain is a complete lattice and, consequently, we express program interpretation in terms of a least fixpoint. As an application, by bounding interpretations by higher order polynomials, we characterize Basic Feasible Functions at any order.
@cite_0: We design an interpretation-based theory of higher-order functions that is well-suited for the complexity analysis of a standard higher-order functional language a la ml. We manage to express the interpretation of a given program in terms of a least fixpoint and we show that when restricted to functions bounded by higher-order polynomials, they characterize exactly classes of tractable functions known as Basic Feasible Functions at any order.
@cite_15: This paper deals with termination proofs for Higher-Order Rewrite Systems (HRSs), introduced in [12]. This formalism combines the computational aspects of term rewriting and simply typed lambda calculus. The result is a proof technique for the termination of a HRS, similar to the proof technique “Termination by interpretation in a well-founded monotone algebra”, described in [8, 19]. The resulting technique is as follows: Choose a higher-order algebra with operations for each function symbol in the HRS, equipped with some well-founded partial ordering. The operations must be strictly monotonic in this ordering. This choice generates a model for the HRS. If the choice can be made in such a way that for each rule the interpretation of the left hand side is greater than the interpretation of the right hand side, then the HRS is terminating. At the end of the paper some applications of this technique are given, which show that this technique is natural and can easily be applied.
@cite_18: 
@cite_20: Polynomial interpretations and their generalizations like quasi-interpretations have been used in the setting of first-order functional languages to design criteria ensuring statically some complexity bounds on programs 10. This fits in the area of implicit computational complexity, which aims at giving machine-free characterizations of complexity classes. In this paper, we extend this approach to the higher-order setting. For that we consider simply-typed term rewriting systems 35, we define higher-order polynomial interpretations for them, and we give a criterion ensuring that a program can be executed in polynomial time. In order to obtain a criterion flexible enough to validate interesting programs using higher-order primitives, we introduce a notion of polynomial quasi-interpretations, coupled with a simple termination criterion based on linear types and path-like orders.
The present paper is an extended version of the results in @cite_0 : more proofs and examples have been provided. An erratum has been provided: the interpretation of the case construct has been slightly modified so that we can consider non decreasing functions (and not only strictly increasing functions). There are two lines of work that are related to our approach. @cite_15 , Van De Pol introduced higher order interpretation for showing the termination of higher order term rewrite systems. @cite_18 @cite_20 , Baillot and Dal Lago introduce a higher order interpretations for complexity analysis of term rewrite systems. While the first work only deals with termination properties, the second work is restricted to a family of higher order term rewrite systems called simply typed term rewrite systems.