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

Untyped Confluence In Dependent Type Theories: Full version

Abstract : We investigate techniques based on van Oostrom's decreasing diagrams that reduce confluence proofs to the checking of critical pairs in the absence of termination properties, which are useful in dependent type calculi to prove confluence on untyped terms. These techniques are applied to a complex example taken from practice: a faithful encoding in an extension of LF with rewrite rules on objects and types, of the calculus of constructions with a cumulative hierarchy of predicative universes above Prop. The rules may be first-order or higher-order, plain or modulo, non-linear on the right or on the left. Variables which occur non-linearly in lefthand sides of rules or in equations must take their values in confined types: in our example, the natural numbers. The first-order rules are assumed to be terminating and confluent modulo some theory: in our example, associativity, commutativity and identity. Critical pairs involving higher-order rules must satisfy van Oostrom's decreasing diagram condition with respect to their indexes taken as labels. Our use of decreasing diagrams yields a modular proof of confluence on open terms. Our encoding of the hierarchy of universes was obtained by using the MAUDE completion tool twisted to fit our needs. The obtained set of rules exploits all the sophistication of our confluence theorem.
Document type :
Preprints, Working Papers, ...
Complete list of metadata

Cited literature [28 references]  Display  Hide  Download

https://hal.inria.fr/hal-01515505
Contributor : Jean-Pierre Jouannaud <>
Submitted on : Thursday, April 27, 2017 - 3:41:59 PM
Last modification on : Tuesday, June 1, 2021 - 2:34:10 PM
Long-term archiving on: : Friday, July 28, 2017 - 1:11:46 PM

File

conf.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01515505, version 1

Citation

Ali Assaf, Gilles Dowek, Jean-Pierre Jouannaud, Jiaxiang Liu. Untyped Confluence In Dependent Type Theories: Full version. 2017. ⟨hal-01515505⟩

Share

Metrics

Record views

574

Files downloads

174