Unification et Intégration Formelle

Benjamin Werner
Benjamin.Werner@inria.fr






NOUVEAU
Une page avec des indications complémentaires et des réponses aux questions se trouve ici.

Par ailleurs, je n'ai toujours par les mails de tout le monde. Ecrivez-moi !

 

 

1   Objet

Les logiciels de calcul formel qui manipulent des expressions symboliques de l'analyse réelle se sont popularisées dans l'enseignement depuis une douzaine d'années. Dans l'enseignement supérieur d'abord avec des programmes comme maple, puis au lycée avec des calculettes de plus en plus perfectionnées (la TI-92 devenant même un objet culte chez certains bacheliers).

Il s'agit donc de réaliser un programme capable de faire quelques-unes de ces opérations. C'est-à-dire de dériver (toujours) et d'intégrer (parfois) des expressions correspondant à des fonctions réelles.

2   Principe

Les logiciels mentionnés ci-dessus utilisent des techniques extrèmement complexes aussi bien du point de vue informatique que par leur justification mathématiquement. Il n'est donc pas question de les utiliser ici.

2.1   Les termes

Les objets que l'on va manipuler sont des termes. Ils sont naturellement représentés sous forme d'arbres dont les noeuds seront sin, cos, +, 0....

Comme on se restreint à des fonctions unaires, qu'on ne veut dériver et intégrer que par rapport à une variable, il est pratique d'omettre cette dernière. Les termes sont ainsi plus compacts et plus faciles à manipuler. Par contre, on a alors besoin d'un opérateur de composition; ainsi, sin(x*cos(x)) est alors représenté par l'arbre:




C'est-à-dire que x désigne en fait la fonction identité. Dans la suite, on notera cela sin°(cos * x).

2.2   Règles, unification

Le monde des termes est régit par des règles. Par exemple sin'=cos, 0*t=t ou t*u=u*t. Ces règles sont des équations ou, plus précisément, des familles d'équations: la seconde règle peut, en effet, être instanciée en 0*1=0, 0*sin=0, 0*(a+3*sin)=0, etc. En d'autres termes, dans cette règle, t a un statut particulier: c'est une variable alors que 0, sin, la dérivation ou la multiplication sont ce qu'on appelle des constantes.

De plus, quand c'est possible, les règles sont orientées. Le membre droit étant une simplification du membre gauche.

L'opération qui permet de vérifier si une règle peut être appliquée à un terme s'appelle l'unification. Elle consiste à exhiber la substitution des variables, sous laquelle les deux termes deviennent identiques. Par exemple, 0*t et 0*1 sont unifiables par la substitution [t¬ 1]; les termes f*(sin+g) et exp*(sin+0) le sont par [f¬ exp; g¬ 0]. Les termes 1*f et sin*0 ne sont pas unifiables.

Pour appliquer une règle à un terme, on doit donc unifier celui-ci au membre gauche de la règle, puis appliquer la substitution obtenue au membre droit. Le résultat est le terme réduit. Etant donné un ensemble de règles, l'opération qui consiste à réduire un terme jusqu'a ce qu'aucune règle ne s'applique plus, est appelée la normalisation de ce terme. Le terme resultant est dit normal.

2.3   Ensembles de règles

Pour pouvoir normaliser un terme, il est nécessaire que l'ensemble des règles considéré termine. Par exemple, l'équation f+0=f doit être orienté de gauche à droite; dans le cas contraire on aurait la séquence de réductions infinie x|® x+0|® x+0+0|®....

Une autre propriété intéressante est la confluence: c'est-à-dire que quel que soit l'ordre dans lequel on applique des règles pour normaliser un terme donné, on tombe toujours sur le même terme normal. Lorsque c'est le cas, il est facile de vérifier sont égaux modulo les règles: il suffit de comparer leur formes normales.

Ici on a la difficulté liée aux règles de commutativité t+u=u+t que l'on ne peut pas orienter à priori. On ignorera en première approximation ce problème; il faudra ensuite se débrouiller pour orienter à la main ces règles.

Voici par exemple un ensemble de règles (orientées) confluent et terminant pour les anneaux abeliens:
t+0 ® t      
(-t)+t ® 0      x+(-y)+y ® x
1*t ® t t*(u+v) ® (t*u)+(t*v)
-0 ® 0 -(t+u) ® (-t)+(-u)
-(-t) ® t t*(-u) ® -(t*u)
x*0 ® 0      
Auxquelles il faut ajouter les variantes par commutativité comme 0*x® 0. Clairement on va utiliser ici toutes ces règles, auxquelles on ajoutera également celles liées à la dérivée.

2.4   Trouver une primitive

Calculer la dérivée d'un terme t est relativement facile: il suffit de normaliser t'. L'opération inverse est plus ardue. La méthode proposée consiste essentiellement à essayer d'appliquer les règles de réduction à l'envers. Une possibilité est de considérer un ensemble d'équations que l'on cherche à résoudre.

Prenons un exemple: le calcul de la primitive de sin+x*cos. Cela revient à résoudre l'équation F'=sin+x*cos. On ne peut pas unifier les deux membres de cette équation. Qui plus est, chercher à unifier sin+x*cos avec les membres droits des règles de réduction ne nous avancera pas. En revanche, une variante plus ``laxiste'' de l'unification peut repérer que sin+x*cos=f'*g+f*g' à condition que f'*g=sin et f*g'=x*cos. En utilisant la règle (f*g)'=f'*g+f*g', on peut donc remplacer l'équation de départ par:
[F'=(f*g)'; f'*g=sin ; f*g'=x*cos]
L'étape suivante consiste à simplifier le système obtenu. On remarque alors que la première équation présente une solution par unification: la substitution F¬ f*g. On retire donc cette équation du système, en gardant la substitution correspondante à part. On a donc:
[F¬ f*g]  et  [f'*g=sin ; f*g'=x*cos]
En continuant à chercher à simplifier le système de droite, une possibilité est de remplacer f*g'=x*cos par f=x et g'=cos ce qui donne:
[F¬ f*g]  et  [f'*g=sin ; f=x; g'=cos]
La fonction de simplification doit alors remarquer que l'une des équations définit la variable f et permet de retirer celle-ci. On passe à:
[f¬ x; F¬ f*g]  et  [x'*g=sin; g'=cos]
Remarquez que l'on en a profité pour remplacer les autres occurences de f par sa nouvelle définition. En normalisant x'*g=sin on trouve g=sin, qui peut donc être également retirée du système:
[g¬ sin;f¬ x; F¬ f*g]  et  [sin'=cos]
Il ne reste alors qu'une équation sin'=cos, qui possède la particularité de ne pas contenir de variables, et dont on peut vérifier la validité en normalisant. Lorsqu'il ne reste plus d'équations, on a résolu le système. Le résultat est donc la substitution [g¬ sin;f¬ x; F¬ f*g] qui appliquée à F donne bien le résultat x*sin escompté.

2.5   De quoi se sert-on ?

Pour écrire le programme capable de trouver ce cheminement, on a d'abord besoin d'une fonction de semi-unification qui, par exemple, appliquée aux termes sin+x*cos et f'*g+f*g', retourne les deux équations f'*g=sin et f*g'=x*cos. Cette fonction sert d'abord à essayer d'appliquer les règles de réductions à l'envers, comme dans la première étape du cheminement ci-dessus.

Elle peut être également utile dans la fonction de simplification, qui correspond aux étapes suivantes. Essentiellement, cette fonction doit examiner les différentes équations du système et éliminer celle qui sont triviales. Elle doit également construire au fur-et-à-mesure la substitution qui sera le résultat final.

L'algorithme consiste donc à appliquer à l'envers une règle de réduction, puis à simplifier le système ainsi obtenu. Si l'on a alors pas tout résolu, on peut ré-itérer le processus. Remarquons que: Il faut donc faire attention à ne pas boucler d'une part, et surtout à ne pas oublier d'explorer toutes les possibilités. Bien sûr, dès que l'on trouve une solution, on peut stopper la recherche.

3   Travail demandé

Dans un premier temps, il faudra définir la structure des termes et les fonctions d'unification, ainsi qu'un afficheur et un parseur pour lire les termes au clavier. Quitte à enrichir la structure des termes ensuite, il est conseillé de se restreindre à une algèbre de termes pas trop riche, au moins dans un premier temps. Un minimum est de prendre les noeuds suivants: sin, cos, exp, la composition, la fonction identité, l'addition, la multiplication, 0, 1 et l'opposé. Plus tard, on pourra éventuellement ajouter, par exemple, l'exponantiation par des entiers et, pour que cela apporte quelque chose, les fonctions constantes entières.

Une fonction de normalisation par rapport à un ensemble de règles permet alors d'obtenir un petit dérivateur formel.

Lorsque ce dernier semble raisonnablement au point, on peut passer à la programmation de la réduction d'un ensemble d'équations pour calculer quelques primitives. Lorsque ça tourne, il est possible de tenter quelques optimisations; voici quelques idées: Il est plus que conseillé de me contacter si vous choisissez ce projet.


This document was translated from LATEX by HEVEA.