En logique mathématique , un calcul formel , ou opération formelle , est un calcul systématique mais sans justification rigoureuse . Il consiste à manipuler des symboles dans une expression en utilisant une substitution générique sans prouver que les conditions nécessaires sont réunies. Essentiellement, il s'agit de la forme d'une expression sans tenir compte de sa signification sous-jacente. Ce raisonnement peut soit servir de preuve positive qu'une affirmation est vraie lorsqu'il est difficile ou inutile d'en fournir la preuve, soit servir d'inspiration pour la création de nouvelles définitions (complètement rigoureuses).
Cependant, cette interprétation du terme formel n’est pas universellement acceptée, et certains considèrent qu’il signifie tout le contraire : un argument complètement rigoureux, comme dans la logique mathématique formelle .
Exemples
Les calculs formels peuvent conduire à des résultats erronés dans un contexte, mais corrects dans un autre. L'équation
est valable si q a une valeur absolue inférieure à 1. En ignorant cette restriction et en remplaçant q = 2, on obtient
En substituant q = 2 dans la preuve de la première équation, on obtient un calcul formel qui produit la dernière équation. Mais il est faux sur les nombres réels, car la série ne converge pas. Cependant, dans d'autres contextes (par exemple, en travaillant avec des nombres 2-adiques , ou avec des entiers modulo une puissance de 2 ), la série converge. Le calcul formel implique que la dernière équation doit être valide dans ces contextes.
Un autre exemple est obtenu en substituant q =-1. La série résultante 1-1+1-1+... est divergente (sur les nombres réels et p-adiques ) mais une valeur peut lui être assignée avec une méthode de sommation alternative, telle que la sommation de Cesàro . La valeur résultante, 1/2, est la même que celle obtenue par le calcul formel.
Séries formelles entières
Une série formelle est un concept qui adopte la forme d' une série formelle issue de l'analyse réelle . Le mot « formelle » indique que la série n'a pas besoin de converger. En mathématiques, et en particulier en algèbre, une série formelle est une somme infinie qui est considérée indépendamment de toute notion de convergence et qui peut être manipulée à l'aide d'opérations algébriques sur les séries (addition, soustraction, multiplication, division, sommes partielles, etc.).
Une série formelle est un type particulier de série formelle, qui peut être considérée comme une généralisation d'un polynôme, où le nombre de termes peut être infini, sans exigence de convergence. Ainsi, la série ne peut plus représenter une fonction de sa variable, mais simplement une séquence formelle de coefficients, contrairement à une série formelle, qui définit une fonction en prenant des valeurs numériques pour la variable dans un rayon de convergence. Dans une série formelle, les puissances de la variable ne sont utilisées que comme détenteurs de position pour les coefficients, de sorte que le coefficient de est le cinquième terme de la séquence. En combinatoire, la méthode de génération de fonctions utilise des séries formelles pour représenter des séquences numériques et des multi-ensembles, permettant par exemple des expressions concises pour des séquences définies de manière récursive, que la récursivité puisse être résolue explicitement ou non. Plus généralement, les séries formelles peuvent inclure des séries avec n'importe quel nombre fini (ou dénombrable) de variables, et avec des coefficients dans un anneau arbitraire.
Les anneaux de séries formelles sont des anneaux locaux complets, qui supportent des méthodes de type calcul dans le cadre purement algébrique de la géométrie algébrique et de l'algèbre commutative . Ils sont analogues aux entiers p-adiques, qui peuvent être définis comme des séries formelles des puissances de p.
Manipulation des symboles
Équations différentielles
Pour résoudre l' équation différentielle
ces symboles peuvent être traités comme des symboles algébriques ordinaires, et sans donner aucune justification concernant la validité de cette étape, nous prenons les réciproques des deux côtés :
Une primitive simple :
Puisqu'il s'agit d'un calcul formel , il est acceptable de laisser et d'obtenir une autre solution :
Les solutions finales peuvent être vérifiées pour confirmer qu’elles résolvent l’équation.
Produit vectoriel
Le produit vectoriel peut être exprimé comme le déterminant suivant :
où est une base orthonormée orientée positivement d'un espace vectoriel euclidien orienté tridimensionnel , tandis que sont des scalaires tels que , et similaire pour .