HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

Simulating expansions without expansions

Abstract : We add extensional equalities for the functional and product types to the typed l-calculus with not only products and terminal object, but also sums and bounded recursion (a version of recursion that does not allow recursive calls of infinite length). We provide a confluent and strongly normalizing (thus desidable) rewriting system for the calculus, that stays confluent when allowing unbounded recursion. For that, we turn the extensional equalities into expansion rules and not into contractions as is done traditionally. We first prove the calculus to be weakly confluent, which is a more complex and interesting task than for the usual l-calculus. Then we provide an effective mechanism to simulate expansions without expansion rules, so that the strong normalization of the calculus can be derived from that of the underlying, traditional, non extensional system. These results give us the confluence of the full calculus, but we also show how to deduce confluence directly form our simulation technique, without the weak confluence property.
Document type :
Complete list of metadata

Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Wednesday, May 24, 2006 - 4:15:18 PM
Last modification on : Friday, February 4, 2022 - 3:22:16 AM
Long-term archiving on: : Tuesday, April 12, 2011 - 7:10:09 PM


  • HAL Id : inria-00074762, version 1



R. Di Cosmo, D. Kesner. Simulating expansions without expansions. RR-1911, INRIA. 1993. ⟨inria-00074762⟩



Record views


Files downloads