Theory of higher order interpretations and application to Basic Feasible
FunctionsArticle
Authors: Emmanuel Hainry ; Romain Péchoux
NULL##NULL
Emmanuel Hainry;Romain Péchoux
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.
Volume: Volume 16, Issue 4
Secondary volumes: Selected Papers of the Conference "Continuity, Computability, Constructivity: From Logic to Algorithms" (CCC 2017)
Published on: December 14, 2020
Accepted on: October 22, 2020
Submitted on: January 26, 2018
Keywords: Computer Science - Logic in Computer Science, Computer Science - Computational Complexity, Computer Science - Programming Languages
Funding:
Source : OpenAIRE Graph- Expanding Logical Ideas for Complexity Analysis; Funder: French National Research Agency (ANR); Code: ANR-14-CE25-0005