Context-sensitive Conditional Expression Reduction Systems
Zurab Khasidashvili, Vincent van Oostrom · Electronic Notes in Theoretical Computer Science · 1995
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.