Return to search

Terminaison des systèmes de réécriture d'ordre supérieur basée sur la notion de clôture de calculabilité

Dans ce document, nous montrons comment la notion de calculabilité introduite par W. W. Tait et étendue par Girard aux types polymorphes peut être utilisée et facilement étendue pour montrer la terminaison de différents types de relations de réécriture, y compris avec filtrage sur des symboles définis, filtrage d'ordre supérieur ou réécriture de classe modulo certaines théories équationnelles. Nous montrons également que la notion de clôture de calculabilité donne lieu a une relation bien fondée incluant l'extension à l'ordre supérieur par J.-P. Jouannaud et A. Rubio de l'ordre récursif sur les chemins de N. Dershowitz.

Identiferoai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00724233
Date13 July 2012
CreatorsBlanqui, Frédéric
PublisherUniversité Paris-Diderot - Paris VII
Source SetsCCSD theses-EN-ligne, France
LanguageFrench
Detected LanguageFrench
Typehabilitation ࠤiriger des recherches

Page generated in 0.002 seconds