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

    Consultation statistics

    This page has been seen 1036 times.
    This article's PDF has been downloaded 182 times.