Séminaire du LIF
Jeudi 6 mars à 14h - CMI, Amphi C101
Roberto Amadio
LIF, équipe MoVe
Quasi-interprétations max-plus
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.
Home page : http://www.cmi.univ-mrs.fr/~amadio/
Roberto M. Amadio. Max-plus quasi-interpretations. LIF Research report 10-2002, Dec 2002. http://www.lim.univ-mrs.fr/Rapports/10-2002-Amadio.html