Theory of higher order interpretations and application to Basic Feasible Functions
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 i...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2020-12-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/4237/pdf |
| _version_ | 1797268537583075328 |
|---|---|
| author | Emmanuel Hainry Romain Péchoux |
| author_facet | Emmanuel Hainry Romain Péchoux |
| author_sort | Emmanuel Hainry |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-04-25T01:34:03Z |
| format | Article |
| id | doaj.art-02875a8e58dc40e4a4d4ebaa9e30ce4e |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:34:03Z |
| publishDate | 2020-12-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-02875a8e58dc40e4a4d4ebaa9e30ce4e2024-03-08T10:32:05ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742020-12-01Volume 16, Issue 410.23638/LMCS-16(4:14)20204237Theory of higher order interpretations and application to Basic Feasible FunctionsEmmanuel HainryRomain PéchouxInterpretation 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.https://lmcs.episciences.org/4237/pdfcomputer science - logic in computer sciencecomputer science - computational complexitycomputer science - programming languages |
| spellingShingle | Emmanuel Hainry Romain Péchoux Theory of higher order interpretations and application to Basic Feasible Functions Logical Methods in Computer Science computer science - logic in computer science computer science - computational complexity computer science - programming languages |
| title | Theory of higher order interpretations and application to Basic Feasible Functions |
| title_full | Theory of higher order interpretations and application to Basic Feasible Functions |
| title_fullStr | Theory of higher order interpretations and application to Basic Feasible Functions |
| title_full_unstemmed | Theory of higher order interpretations and application to Basic Feasible Functions |
| title_short | Theory of higher order interpretations and application to Basic Feasible Functions |
| title_sort | theory of higher order interpretations and application to basic feasible functions |
| topic | computer science - logic in computer science computer science - computational complexity computer science - programming languages |
| url | https://lmcs.episciences.org/4237/pdf |
| work_keys_str_mv | AT emmanuelhainry theoryofhigherorderinterpretationsandapplicationtobasicfeasiblefunctions AT romainpechoux theoryofhigherorderinterpretationsandapplicationtobasicfeasiblefunctions |