Modularity of strong normalization and confluence in the algebraic-λ-cube

Author

Barbanera, Franco ; Fernández, Maribel ; Geuvers, Herman

Author_Institution

Dipartimento di Inf., Torino Univ., Italy

fYear

1994

fDate

4-7 Jul 1994

Firstpage

406

Lastpage

415

Abstract

Presents the algebraic-λ-cube, an extension of Barendregt´s (1991) λ-cube with first- and higher-order algebraic rewriting. We show that strong normalization is a modular property of all systems in the algebraic-λ-cube, provided that the first-order rewrite rules are non-duplicating and the higher-order rules satisfy the general schema of Jouannaud and Okada (1991). This result is proven for the algebraic extension of the calculus of constructions, which contains all the systems of the algebraic-λ-cube. We also prove that local confluence is a modular property of all the systems in the algebraic-λ-cube, provided that the higher-order rules do not introduce critical pairs. This property and the strong normalization result imply the modularity of confluence

Keywords

algebra; lambda calculus; rewriting systems; algebraic rewriting; algebraic-λ-cube; calculus of constructions; critical pairs; higher-order rules; local confluence; modularity; nonduplicating first-order rewrite rules; strong normalization; Calculus; Computational modeling; Computer languages; Equations; Informatics; Mathematics;

fLanguage

English

Publisher

ieee

Conference_Titel

Logic in Computer Science, 1994. LICS '94. Proceedings., Symposium on

Conference_Location

Paris

Print_ISBN

0-8186-6310-3

Type

conf

DOI

10.1109/LICS.1994.316049

Filename

316049