Unification et Intégration Formelle
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:
-
Si, lors de la simplification, on trouve une équation du style
cos=sin, on a aucune chance de résoudre le système. Il faut donc
revenir en arrière, et explorer une autre branche.
- Rien ne garantit que la première règle essayée sera la bonne et
on ne veut donc pas explorer indéfiniment la même branche de
recherche. Une solution est de se donner une borne sur le nombre
d'itérations de la recherche. Si le système n'est pas résolu lorsque
le nombre d'itérations est epuisée, on considère que l'on a échoué et
on explore, récursivement, une autre branche.
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:
-
Assigner un ``cout'' aux règles, pour les différencier. Par
exemple une règle complexe consommera plus de d'itérations de
recherche qu'une règle plus simple.
- Ajouter des règles nouvelles (mais pas dans la partie de
normalisation) qui court-circuitent plusieurs règles
élémentaires.
- Eviter de considérer certaines règles; par exemple s'il n'y a
pas de fonctions trigonomètriques au départ, il n'y en aura pas non
plus dans la primitive, etc.
Il est plus que conseillé de me contacter si vous choisissez ce
projet.
This document was translated from LATEX by HEVEA.
