Abstract FR:

Dans ce travail nous nous interessons a la beta-reduction du point de vue des longueurs des reductions et essayerons de trouver une structure de donnees permettant de partager, et donc reduire en meme temps, les radicaux dupliques. Nous developperons un systeme d'etiquettes pour les termes du lambda-k-calcul. Ce systeme rend compte des sous-termes partages. La notion de beta-reduction est etendue vers les termes etiquetes. Nous pourrons alors identifier des termes issus d'un meme terme initial et dupliques par reduction. En particulier, les radicaux de meme etiquette seront tous residus d'un unique radical initial. Nous introduisons ensuite une notion de beta-reduction parallele qui contracte en une seule operation elementaire, c'est-a-dire equivalente a la reduction d'une occurrence de radical, tous les radicaux de meme etiquette. Cette notion correspond, en termes de beta-reduction non parallele, au developpement complet d'un ensemble de radicaux. Certaines strategies paralleles que nous definirons seront plus efficaces que les exemples de reductions partagees connues dans la litterature. Cependant, elles ne seront pas optimales. En effet, le partage ne saura pas toujours caracteriser l'ensemble des radicaux issus d'un seul radical initial, encore appele famille de radicaux. Nous montrerons qu'il n'y a aucune structure de donnees fondee sur le partage qui attribue, pour tout terme et toute reduction, une seule et meme etiquette a tous les radicaux d'une famille. Ceci est du au fait que deux radicaux distincts pris dans une meme famille ne sont pas forcement des termes disjoints. Le phenomene se produit egalement dans le lambda-i-calcul pour des termes normalisables et typables