Skip to Main content Skip to Navigation
Journal articles

Theory of Higher Order Interpretations and Application to Basic Feasible Functions

Emmanuel Hainry 1 Romain Péchoux 1
1 MOCQUA - Designing the Future of Computational Models
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : 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.
Complete list of metadata

https://hal.inria.fr/hal-02499206
Contributor : Romain Péchoux Connect in order to contact the contributor
Submitted on : Wednesday, January 6, 2021 - 11:36:55 AM
Last modification on : Saturday, October 16, 2021 - 11:26:10 AM

File

1801.08350v4.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Emmanuel Hainry, Romain Péchoux. Theory of Higher Order Interpretations and Application to Basic Feasible Functions. Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2020, 16 (4), pp.25. ⟨10.23638/LMCS-16(4:14)2020⟩. ⟨hal-02499206v2⟩

Share

Metrics

Record views

78

Files downloads

131