Paper Info
Title
Modularity of strong normalization and confluence in the algebraic-λ-cube
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
Year
DOI
Venue
1994
10.1109/LICS.1994.316049
Paris
Keywords
Field
DocType
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,satisfiability,informatics,mathematics,computational modeling,computer languages,first order,higher order
Discrete mathematics,Lambda calculus,Combinatorics,Typed lambda calculus,Binary lambda calculus,Lambda cube,Calculus of constructions,Algebraic extension,Confluence,Pure type system,Mathematics
Conference
ISSN
Citations 
PageRank 
1043-6871
13
0.70
References 
Authors
8
3
Name
Order
Citations
PageRank
Franco Barbanera135735.14
Maribel Fernández231523.44
Herman Geuvers345753.92