tel-00724233, version 2

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

Frédéric Blanqui () ^a, 1

Université Paris-Diderot - Paris VII (13/07/2012), Dale Miller (Pr.)

• a –  INRIA
• 1 :  FORMES (LIAMA)
• http://liama.ia.ac.cn/wiki/projects:formes:home
  INRIA – Tsinghua University / Beijing – LIAMA Tsinghua University FIT Building Haidian District 100084 Beijing China Chine

Versions disponibles :  v1 (20-08-2012) v2 (24-08-2012)

Références bibliographiques

• Type de publication : HDR
• titre : Terminaison des systèmes de réécriture d'ordre supérieur basée sur la notion de clôture de calculabilité
• titre en anglais : Termination of higher-order rewrite systems based on the notion of computability closure
• date de soutenance : 13/07/2012
• résumé : 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.
• résumé en anglais : In this paper, we show how the notion of computability introduced by W. W. Tait and extended to polymorphic types by J.-Y. Girard can be used and easily extended to prove the termination of various kind of rewriting relations on lambda-terms, including matching on defined symbols, higher-order matching or class-rewriting modulo some equational theories. We also show how the notion of computability closure can easily be turned into a well-founded relation including J.-P. Jouannaud and A. Rubio's higher-order extension of N. Dershowitz' recursive path ordering.
• domaine :

  Mathématiques/Logique

  Informatique/Langage de programmation

  Informatique/Logique en informatique

• organisme de délivrance : Université Paris-Diderot - Paris VII
• langue : Français
• président du jury : Dale Miller
• courriel du président : dale.miller@inria.fr
• composition du Jury : Gilles BARTHE (rapporteur)
  Bernhard GRAMLICH (rapporteur)
  Delia KESNER (rapporteur)
  Nachum DERSHOWITZ
  Gilles DOWEK
  Claude KIRCHNER
• mots-clés : lambda-calcul – réécriture – terminaison – réductibilité – Girard
• mots-clés en anglais : lambda-calcul; rewriting; termination; reductibility; Girard

Liste des fichiers attachés à ce document :

• tel-00724233, version 2
• http://tel.archives-ouvertes.fr/tel-00724233
• oai:tel.archives-ouvertes.fr:tel-00724233
• Contributeur : Frédéric Blanqui <>
• Soumis le : Mardi 21 Août 2012, 04:07:21
• Dernière modification le : Vendredi 24 Août 2012, 14:41:10