Size-based termination : semantics and generalizations

Ce manuscrit présente une réflexion sur la terminaison des systèmes de réécriture d'ordres supérieurs. Nous nous concentrons sur une méthode particulière, la terminaison à base de tailles. La terminaison à base de tailles utilise le typage pourdonner une approximation syntaxique à la taille d'un élément du langage. Notre contribution est double: premièrement, nous permettons d'aborder de manière structurée le problème de la correction des approches à base de taille. Pour ce faire, nous montrons qu'elle peut être traitée par une version de la méthode des annotations sémantiques. Cette dernière utilise des annotations sur les termescalculés à partir de la sémantique des sous-termes dans un certain prémodèle équationnel. Nous montrons la correction de notre approche par annotations sémantiques, ainsi que du critère qui permet de traiter le système annoté, et nous construisons un prémodèle pour le système qui correspond intuitivement à lasémantique du système de réécriture. Nous montrons alors que le système annoté passe le critère de terminaison. D'un autre côté nous modifions l'approche classique de la terminaison à base de tailles et montrons que le système modifiépermet une analyse fine du flot de contrôle dans un langage d'ordre supérieur. Ceci nous permet de construire un graphe, dit graphe de dépendance approxime, et nous pouvons montrer qu'un critère syntaxique sur ce graphe suffit à montrer la terminaison de tout terme bien typéThe present manuscript is a reflection on termination of higher-order rewrite systems. We concentrate our efforts on a particular approach, size-based termination. This method uses typing to give a syntactic approximation to the size of an element of the language. Our contribution is twofold: first we give a structured approach to proving the correctness of size-based termination. To do this, we show that it is possible to apply a certain version of semantic labelling. This technique uses annotations on terms computed using the semantics of subterms in a certain equational premodel. We show correctness of our labelling framework and of the criterion that allows us to prove termination of the labelled system, and we build a premodel of the rewrite system that intuitively corresponds to the rewrite system. We show that the system labelled using these semantics passes the termination criterion. Furthermore we show that a modification of the classical size-types approach allows us to perform a fine control-flow analysis in a higher-order language. This allows us to build an approximated dependency graph, and show that if a certain syntactic criterion issatisfied by the graph, then all well-typed terms are terminatin