Skip to Main content Skip to Navigation
Journal articles

Synthesis of sup-interpretations: a survey

Romain Péchoux 1
1 CARTE - Theoretical adverse computations, and safety
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
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.
Document type :
Journal articles
Complete list of metadata

Cited literature [39 references]  Display  Hide  Download
Contributor : Romain Péchoux Connect in order to contact the contributor
Submitted on : Friday, October 26, 2012 - 10:49:42 AM
Last modification on : Saturday, October 16, 2021 - 11:26:05 AM
Long-term archiving on: : Sunday, January 27, 2013 - 3:38:19 AM


Files produced by the author(s)




Romain Péchoux. Synthesis of sup-interpretations: a survey. Theoretical Computer Science, Elsevier, 2012, pp.24. ⟨10.1016/j.tcs.2012.11.003⟩. ⟨hal-00744915⟩



Les métriques sont temporairement indisponibles