A semantic method to prove strong normalization from weak normalization - Inria - Institut national de recherche en sciences et technologies du numérique Access content directly
Preprints, Working Papers, ... Year : 2009

A semantic method to prove strong normalization from weak normalization

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.
Fichier principal
Vignette du fichier
RiceSaladLambdaModulo.pdf (183.14 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

inria-00385520 , version 1 (19-05-2009)

Identifiers

  • HAL Id : inria-00385520 , version 1

Cite

Denis Cousineau. A semantic method to prove strong normalization from weak normalization. 2009. ⟨inria-00385520⟩
139 View
69 Download

Share

Gmail Facebook X LinkedIn More