The #lambda#_(arrow up)-calculus is a confluent first-order term rewriting system which contains the #lambda#-calculus written in de Bruijn's notation. The substitution is defined explicitly in #lambda#_(arrow up) by a subsystem, called the #sigma#_(arrow up)-calculus. In this paper, we use the #sigma#_(arrow up)-calculus as the substitution mechanism of general higher-order systems which we will name Explicit Reduction Systems. We give general conditions to define a confluent XRS. Particularly, we restrict the general condition of orthogonality of the classical higher-order rewriting systems to the orthogonality of the rules initiating substitutions.
展开▼
