Pourquoi la réécriture des termes?

J'ai fait un peu de recherche sur Google et je suis venu un peu court.

Je me demande quelles sont les principales raisons pour lesquelles les informaticiens, les programmeurs, étudient la réécriture de termes et / ou la réécriture de graphes de termes.

Pour autant que je sache, cela aide simplement à un raisonnement de base sur les programmes fonctionnels et le contrôle (impératif) des programmes. Apparemment, c'est un sujet d'un grand intérêt pour les logiciens et ceux qui étudient les algèbres abstraites constructives.

Toute aide serait appréciée!

Je ne suis pas sûr que cela vous apportera plus que vous ne le savez déjà. Mais alors, je peux ne pas comprendre les raisons qui vous font vous interroger sur la réécriture des termes. Ça aide.

Comme vous le savez peut-être, les grammaires sont des systèmes de réécriture de chaînes. Au sommet de la hiérarchie Chomsky, vous avez des grammaires de type 0, qui définissent des angulations récursivement énumérables (RE), et ont la puissance de calcul des machines Turing.

Cela vous indique donc que les systèmes de réécriture en général ont beaucoup à voir avec l'expression d'algorithmes.

Le problème avec les chaînes en général est qu'il n'y a aucun moyen évident de leur attacher la sémantique. C'est une sorte de réécriture amorphe.

Ce qui intéresse généralement les gens, c'est d'exprimer des algorithmes dans des domaines spécifiques qui ont une structure et des propriétés. Ces domaines sont souvent définis à partir d'entités élémentaires (atomiques) et fermés par diverses opérations, éventuellement cotées par des relations d'équivalence, etc. Celles-ci sont souvent appelées algèbres.

Ces domaines sont souvent abstraits. Mais les calculs sur leurs éléments ne peuvent s'exprimer que sur des représentations concrètes. Les termes sont une représentation naturelle de ces éléments car ils expriment comment les éléments peuvent être obtenus pour d'autres éléments par l'application d'opérations, récursivement jusqu'aux éléments atomiques (bien que les propriétés générales n'aient pas toujours besoin de descendre jusqu'au bout). Les termes sont une sorte de syntaxe de structure arborescente qui peut être manipulée pour exprimer des algorithmes (comme pour une chaîne). Mais la structure d'opérande des termes permet également de leur associer une sémantique dans un domaine abstrait au moyen d'homomorphismes.

Plutôt que de prendre la vue très formelle de wikipedia et de nombreux textes sur ce sujet, il suffit de considérer les programmes. Il est généralement reconnu qu'une représentation syntaxique pratique des programmes est ce qu'on appelle l'arbre de syntaxe abstraite (AST). Mais un AST n'est qu'un terme pour représenter un objet programme. La sémantique dénotationnelle est un moyen de définir des domaines abstraits et d'associer des valeurs de ces domaines à AST (ou sous-arbres AST) au moyen d'homomorphismes. Les programmes sous forme AST peuvent être transformés ou optimisés en appliquant des règles de réécriture (je n'affirme pas que toutes les optimisations peuvent ou doivent être faites de cette façon).

La transformation d'expressions algébriques à diverses fins peut être exprimée par la réécriture des termes. Par exemple, la simplification de certaines expressions. Différents types de calculs peuvent également être naturellement exprimés sous forme de réécriture de termes, tels que le calcul de dérivés. La réécriture de termes est également parfois utilisée pour définir des formes canoniques dans des algèbres, quand la même entité sémantique peut avoir plusieurs représentations syntaxiques.

Je vous suggère de consulter l' article de wikipedia sur ce sujet .

Ma pensée est que c'est parce que la réécriture de termes est quelque chose d'extrêmement fondamental, et cela vous permet de décrire les choses de manière extrêmement basique, indépendamment de tout matériel.

La réécriture de termes peut décrire les grammaires, mais elle vous donne également la mécanique des systèmes logiques décrits, comme la logique du premier ordre, etc. Ensuite, la substitution de la réécriture de termes est vraiment la seule opération que vous ayez. La simplicité ici est précieuse car vous décrivez la logique, vous ne pouvez donc pas utiliser toute la complexité de la logique pour décrire votre système (puisque c'est le système que vous essayez de décrire).

Cela vous donne alors la mécanique dont vous avez besoin pour parler du calcul lambda en tant que système logique / axiomatique, ce qui vous donne une version extrêmement formelle et fondamentale du calcul.

Les machines de Turing sont utiles, mais leurs définitions sous-jacentes nécessitent que vous ayez un concept d'ensembles, de fonctions, etc. Il y a beaucoup plus de mathématiques supposées avoir été construites.

Le calcul lambda, d'autre part, est défini en termes de logique, vous pouvez donc l'utiliser sans trop de définitions de la théorie des ensembles, des fonctions, etc.

La réécriture des termes, modélisée par la logique, ne s'applique pas uniquement à la programmation fonctionnelle. Lorsque vous effectuez une vérification formelle du matériel ou du logiciel, vous allez toujours faire un raisonnement quelconque, et ce raisonnement peut être modélisé par la réécriture des termes.

Une raison très pratique est qu'elle conduit à la construction de systèmes de transformation de programmes , des outils qui permettent de manipuler le code des programmes sous forme de termes (arbres de syntaxe abstraits) en utilisant des réécritures de syntaxe de surface.

Un exemple de mon système, le DMS Software Reengineering Toolkit , qui a été utilisé pour une grande variété d'analyses de programmes et de tâches de transformation massives. Vous pouvez voir comment DMS exprime les réécritures . Ces réécritures sont appliquées par un système de réécriture de termes associatif-commutatif qui opère en arrière-plan.