Theory of higher order interpretations and application to Basic Feasible Functions

• الحاوية / القاعدة: Logical Methods in Computer Science
• المؤلفون الرئيسيون: Emmanuel Hainry, Romain Péchoux
• التنسيق: مقال
• اللغة: الإنجليزية
• منشور في: Logical Methods in Computer Science e.V. 2020-12-01
• الموضوعات: computer science - logic in computer science; computer science - computational complexity; computer science - programming languages
• الوصول للمادة أونلاين: https://lmcs.episciences.org/4237/pdf
• تدمد: 1860-5974

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.