Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

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
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.
Document type :
Preprints, Working Papers, ...
Complete list of metadata

Cited literature [17 references]  Display  Hide  Download

https://hal.inria.fr/inria-00385520
Contributor : Denis Cousineau <>
Submitted on : Tuesday, May 19, 2009 - 2:53:24 PM
Last modification on : Thursday, March 5, 2020 - 6:26:40 PM
Long-term archiving on: : Monday, October 15, 2012 - 10:45:32 AM

File

RiceSaladLambdaModulo.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00385520, version 1

Collections

Citation

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

Share

Metrics

Record views

338

Files downloads

116