
handle: 2066/104051
Presents the algebraic-/spl lambda/-cube, an extension of Barendregt's (1991) /spl lambda/-cube with first- and higher-order algebraic rewriting. We show that strong normalization is a modular property of all systems in the algebraic-/spl lambda/-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-/spl lambda/-cube. We also prove that local confluence is a modular property of all the systems in the algebraic-/spl lambda/-cube, provided that the higher-order rules do not introduce critical pairs. This property and the strong normalization result imply the modularity of confluence. >
Foundations
Foundations
| citations This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 29 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Top 10% | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Top 10% |
