Résumé de rapport du LIF

Téléchargement / Download : pdf 284k , ps.gz 252k , bibtex

Abstract

Quasi-interpretations are a tool to bound the size of the values computed by a first-order functional program (or a term rewriting system) and thus a mean to extract bounds on its computational complexity. We study the synthesis of quasi-interpretations selected in the space of polynomials over the max-plus algebra determined by the non-negative rationals extended with -infinite and equipped with binary operations for the maximum and the addition. We prove that in this case the synthesis problem is NP-hard, and in NP for the particular case of multi-linear quasi-interpretations when programs are specified by rules of bounded size. The relevance of multi-linear quasi-interpretations is discussed by comparison to certain syntactic and type theoretic conditions proposed in the literature to control time and space complexity.

Keywords

Functional languages and term rewriting. Function algebras and implicit computational complexity. Static analysis. Polynomial interpretations and max-plus algebras.

Résumé

Les quasi-interprétations sont un outil pour borner la taille des valeurs calculées par un programme fonctionnel du premier ordre (ou un système de réécriture de termes) et ainsi un moyen pour extraire des bornes sur sa complexité. Nous étudions la synthèse des polynômes sur l'algèbre max-plus déterminée par les rationnels non-négatifs étendus avec -infini. Nous démontrons que dans ce cas le problème de la synthèse est NP-difficile et dans NP pour le cas particulier des quasi-interpretations multi-linéaires quand les programmes sont specifiés par des règles de taille bornée. L'intérêt des quasi-interprétations multi-linéaires est discuté par comparaison à certaines restrictions syntaxiques et de typage proposées dans la littérature pour contrôler la complexité en temps et en espace.

Mots clés

Langages fonctionnels et réécriture de termes. Algèbres de fonctions et complexité implicite. Analyse statique. Interprétations polynômiales et algèbre max-plus.

Bibtex

@TECHREPORT{10-2002,
    AUTHOR	= {Roberto M. Amadio},
    TITLE	= {{Max-plus quasi-interpretations}},
    INSTITUTION	= {{LIF}},
    ADDRESS	= {Marseille, France},
    TYPE	= {Research report},
    NUMBER	= {10-2002},
    MONTH	= {Dec},
    YEAR	= {2002},
    NOTE	= {http://pageperso.lif.univ-mrs.fr/~edouard.thiel/RESP/Rapports/10-2002.html},
}