Cours INF889K – Systèmes de réécriture de termes

Les systèmes de réécriture offrent un formalisme pour modéliser très généralement la notion de transformation d’objets. Il est possible d’en définir par exemple sur les mots mais aussi de manière plus englobante sur les termes. Ceci constitue alors un formalisme pour exprimer la notion de calcul, où les termes sont les expressions, et les règles de réécriture expliquent comment calculer. Les systèmes de réécriture de termes sont au cœur de l’informatique théorique, de la théorie de la programmation, de l’algèbre et de la combinatoire. L’objectif de ce cours est de brosser un tableau général de cette théorie et de certaines de ses ramifications en adoptant un point de vue très concret et expérimental.

Relations binaires et systèmes de réécriture abstraits. Combinatoire des termes. Systèmes de réécriture de termes. Graphes de réécriture. Terminaison. Confluence. Systèmes applicatifs. Logique combinatoire. Algèbre universelle et variétés. Transformations de Tietze. Paradigme de programmation basé sur les systèmes de réécriture.