Synthesis of sup-interpretations: a survey

DOI10.1016/J.TCS.2012.11.003MaRDI QIDQ1935778zbMATH OpenOpenAlexFDO

Authors Romain Péchoux

Publication date 19 February 2013

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1210.7136

zbMATH Keywords

complexity analysisinterpretationquasi-interpretationresource upper boundsstatic analysissup-interpretation

Mathematics Subject Classification ID

Research exposition (monographs, survey articles) pertaining to computer science (68-02) Functional programming and lambda calculus (68N18) Analysis of algorithms and problem complexity (68Q25) Grammars and rewriting systems (68Q42)

Abstract: In this paper, we survey the complexity of distinct methods that allow the programmer to synthesize a sup-interpretation, a function providing an upper- bound on the size of the output values computed by a program. It consists in a static space analysis tool without consideration of the time consumption. Although clearly related, sup-interpretation is independent from termination since it only provides an upper bound on the terminating computations. First, we study some undecidable properties of sup-interpretations from a theoretical point of view. Next, we fix term rewriting systems as our computational model and we show that a sup-interpretation can be obtained through the use of a well-known termination technique, the polynomial interpretations. The drawback is that such a method only applies to total functions (strongly normalizing programs). To overcome this problem we also study sup-interpretations through the notion of quasi-interpretation. Quasi-interpretations also suffer from a drawback that lies in the subterm property. This property drastically restricts the shape of the considered functions. Again we overcome this problem by introducing a new notion of interpretations mainly based on the dependency pairs method. We study the decidability and complexity of the sup-interpretation synthesis problem for all these three tools over sets of polynomials. Finally, we take benefit of some previous works on termination and runtime complexity to infer sup-interpretations.

Recommendations

• scientific article; zbMATH DE number 4001450
• Sup-interpretations, a semantic method for static analysis of program resources
• scientific article; zbMATH DE number 2182486
• Syntax and semantics of superintuitionistic logics
• Supervaluations and the strict-tolerant hierarchy
• scientific article; zbMATH DE number 4021104
• Comparison of the topological and relational semantics of superintuitionistic logics
• On supremal languages of classes of sublanguages that arise in supervisor synthesis problems with partial observation
• UNIFICATION IN SUPERINTUITIONISTIC PREDICATE LOGICS AND ITS APPLICATIONS

Cited in

(9)

• Automatic synthesis of logical models for order-sorted first-order theories
• Applications and extensions of context-sensitive rewriting
• Derivational complexity and context-sensitive Rewriting
• Characterizing polynomial time complexity of stream programs using interpretations
• Sup-interpretations, a semantic method for static analysis of program resources
• Analyzing the implicit computational complexity of object-oriented programs
• Resource Analysis by Sup-interpretation
• scientific article; zbMATH DE number 2061700 (Why is no real title available?)
• scientific article; zbMATH DE number 2182486 (Why is no real title available?)

This page was built for publication: Synthesis of sup-interpretations: a survey

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1935778)