Emmanuel Hainry ; Romain Péchoux - Theory of higher order interpretations and application to Basic Feasible Functions

lmcs:4237 - Logical Methods in Computer Science, December 14, 2020, Volume 16, Issue 4 - https://doi.org/10.23638/LMCS-16(4:14)2020
Theory of higher order interpretations and application to Basic Feasible FunctionsArticle

Authors: 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

1 Document citing this article

Consultation statistics

This page has been seen 2033 times.
This article's PDF has been downloaded 385 times.