Résumé de rapport du LIF


Rapport 18-2004
Roberto M. Amadio
Synthesis of max-plus quasi-interpretations


Téléchargement / Download : pdf 280k , 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. We prove that the synthesis problem is NP-hard under various conditions and in NP for the particular case of multi-linear quasi-interpretations when programs are specified by rules of bounded size. We provide a polynomial time algorithm to synthesize homogeneous quasi-interpretations of bounded degree and show how to extend the algorithm to synthesize (general) quasi-interpretations. The resulting algorithm generalizes certain syntactic and type theoretic conditions proposed in the literature to control time and space complexity.

Keywords

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. Nous démontrons que dans ce cas le problème de la synthèse est NP-difficile sous différentes conditions et dans NP pour le cas particulier des quasi-interprétations multi-linéaires quand les programmes sont spécifiés par des règles de taille bornée. Nous définissons un algorithme polynomial en temps pour synthétiser des quasi-interprétations homogènes de degré borné et nous montrons comment adapter l'algorithme pour synthétiser des quasi-interprétations générales. L'algorithme dérivé généralise certaines conditions syntaxiques et de typage proposées dans la littérature pour contrôler la complexité en temps et en espace.

Mots clés

Bibtex

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

[css]   [GenRap] [xhtml] Direction : François Denis - Secrétariat de direction : Martine Quessada
Tel. 04 91 11 36 00 - Fax : 04 91 11 36 02 - Mel. Martine.Quessada@cmi.univ-mrs.fr

webmaster - La dernière mise à jour de cette page date du 04 septembre 2008