A semantic method to prove strong normalization from weak normalization

Denis Cousineau 1, 2
2 TYPICAL - Types, Logic and computing
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, Polytechnique - X, CNRS - Centre National de la Recherche Scientifique : UMR
Abstract : Deduction modulo is an extension of first-order predicate logic where axioms are replaced by rewrite rules and where many theories, such as arithmetic, simple type theory and some variants of set theory, can be expressed. An important question in deduction modulo is to find a condition of the theories that have the strong normalization property. In a previous paper we proposed a refinement of the notion of model for theories expressed in deduction modulo, in a way allowing not only to prove soundness, but also completeness: a theory has the strong normalization property if and only if it has a model of this form. In this paper, we present how we can use these techniques to prove that all weakly normalizing theories expressed in minimal deduction modulo, are strongly normalizing.
Type de document :
Pré-publication, Document de travail
2009
Liste complète des métadonnées

Littérature citée [17 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00385520
Contributeur : Denis Cousineau <>
Soumis le : mardi 19 mai 2009 - 14:53:24
Dernière modification le : jeudi 11 janvier 2018 - 06:22:10
Document(s) archivé(s) le : lundi 15 octobre 2012 - 10:45:32

Fichier

RiceSaladLambdaModulo.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00385520, version 1

Collections

Citation

Denis Cousineau. A semantic method to prove strong normalization from weak normalization. 2009. 〈inria-00385520〉

Partager

Métriques

Consultations de la notice

214

Téléchargements de fichiers

74