Context-sensitive Conditional Expression Reduction Systems

We introduce Context-sensitive Conditional Expression Reduction Systems (CERS) by extending and generalizing the notion of conditional TRS to the higher order case. We justify our framework in two ways. First, we define orthogonality for CERSs and show that the usual results for orthogonal systems (finiteness of developments, confluence, permutation equivalence) carry over immediately. This can be used e.g. to infer confluence from the subject reduction property in several typed -calculi possibly enriched with pattern-matching definitions. Second, we express several proof and transition systems as CERSs. In particular, we give encodings of Hilbert-style proof systems, Gentzen-style sequent-calculi, rewrite systems with rule priorities, and the ß-calculus into CERSs. This last encoding is an (important) example of real context-sensitive rewriting. 1 Introduction A term rewriting system is a pair consisting of an alphabet and a set of rewrite rules. The alphabet is used freely to gene..