Context-sensitive Conditional Expression Reduction Systems

Zurab Khasidashvili School of Information Systems University of East Anglia Norwich NR4 7TJ England zurab@sys.uea.ac.uk^{∗}

Vincent van Oostrom Department of Mathematics and Computer Science Free University De Boelelaan 1081a, 1081 HV Amsterdam, The Netherlands oostrom@cs.vu.nl

Abstract

We introduce Context-sensitive Conditional Expression Reduction Systems (CERSs) by generalizing the notion of conditional TRSs to the higher order case. We define orthogonality for CERSs and prove confluence for orthogonal CERSs. The existing confluence results for orthogonal conditional systems are covered by our confluence theorem. Further, it can be used to infer confluence from the subject reduction property in several typed λ-calculi, and to establish confluence for rewrite systems with pattern-matching definitions, since the latter are conditional rewrite systems.

To justify further our framework, we show how easily can one express several proof and transition systems as CERSs. In particular, we give encodings of Hilbert-style proof systems, Gentzenstyle sequent-calculi, rewrite systems with rule priorities, and the π-calculus into CERSs; the latter is an important example of real context-sensitive systems.

Correspondence Address

Zurab Khasidashvili School of Information Systems University of East Anglia Norwich NR4 7TJ England

Email: zurab@sys.uea.ac.uk Tel: +44 1603 592607 Fax: +44 1603 593344

∗Supported by the Engineering and Physical Sciences Research Council of Great Britain under grant GR/H 41300

1 Conditional Expression Reduction Systems

Combinatory Reduction Systems (CRSs) have been introduced in Klop [Klo80] to provide a uniform framework for reductions with substitutions (referred to also as higher order rewrite systems), as in the λ-calculus and its extensions. Several interesting formalisms have been introduced latter [Kha92, Nip93, Wol93, OR94]. Here we introduce context-sensitive conditional Expression Reduction Systems (CERSs), by generalizing the notion of conditional TRSs (CTRSs), introduced in Klop&Bergstra [BK86], to the higher-order case.

Definition 1.1 Let Σ be an alphabet, comprising variables, denoted by x, y, z; function symbols, also called simple operators; and operator signs or quantifier signs. Each function symbol has an arity k ∈ N, and each operator sign σ has an arity (m, n) with m, n ≠ 0 such that, for any sequence x_{1}, …, x_{m} of pairwise distinct variables, σx_{1} … x_{m} is a compound operator or a quantifier with arity n. Occurrences of x_{1}, …, x_{m} in σx_{1} … x_{m} are called binding variables. Each quantifier σx_{1} … x_{m}, as well as the corresponding quantifier sign σ and binding variables x_{1} … x_{m}, has a scope indicator (k_{1}, …, k_{l}) to specify the arguments in which σx_{1} … x_{m} binds all free occurrences of x_{1}, …, x_{m}. Terms are constructed from variables using functions and quantifiers in the usual way. Further, we assume that each n-ary operator symbol comes together with n sets of admissible terms that are allowed in corresponding arguments of the symbol when admissible terms are constructed. We use t, s, e, o to denote (admissible) terms.

Metaterms are constructed similarly from terms and metavariables A, B, …, which range over terms. In addition, metasubstitutions, expressions of the form (t_{1}/x_{1}, …, t_{n}/x_{n})t_{0}, with t_{j} arbitrary metaterms, are allowed, where the scope of each x_{i} is t_{0}. Metaterms without metasubstitutions are simple metaterms. An assignment maps each metavariable to a term over Σ. If t is a metaterm and θ is an assignment, then the θ-instance tθ of t is the term obtained from t by replacing metavariables with their values under θ, and by replacing metasubstitutions (t_{1}/x_{1}, …, t_{n}/x_{n})t_{0}, in right to left order, with the result of substitution of terms t_{1}, …, t_{n} for free occurrences of x_{1}, …, x_{n} in t_{0}.

For example, a β-redex in the λ-calculus appears as Ap(λx t, s), where Ap is a function symbol of arity 2, and λ is an operator sign of arity (1,1) and scope indicator (1). Integrals such as ∫_{s}^{t} f(x) dx can be represented as ∫x(s, t, f(x)) using an operator sign ∫ of arity (1,3) and scope indicator (3).

Sets of admissible terms allowed for arguments of an operator can be considered as terms of certain sorts or types, thereby allowing to express sort and type disciplines in term construction. Hence function symbols can play role of, e.g., predicate symbols, etc. When useful, we can assume that our alphabet contains function variables as well, but we disallow their binding.

Definition 1.2 A Conditional (Context-sensitive) Expression Reduction System is a pair (Σ, R), where Σ is an alphabet, described in Definition 1.1, and R is a (finite or infinite) set of rewrite rules r : t → s, where t and s are closed metaterms (i.e., no free variables) such that t is not a metavariable, and each metavariable that occurs in s occurs also in t.

Each rule r has a set of admissible assignments AA(r) such that tθ and sθ are admissible terms and which, in order to prevent undesirable confusion of variable bindings, must satisfy the condition that:

(a) for any assignment θ ∈ AA(r), any metavariable A occurring in t or s, and any variable x ∈ F V (Aθ), either every occurrence of A in r is in the scope of some binding occurrence of x in r, or no occurrence is.

For any rule r : t → s in R and θ ∈ AA(r), tθ is an r-redex or an R-redex, and sθ is the contractum of tθ. We call two R-redexes u and v weakly similar if they are instances of the same rule (i.e., with the same set of admissible assignments).

Further, each pair (r, θ) with r ∈ R and θ ∈ AA(r) has a set AC(r, θ) of admissible contexts such that, if a context C[ ] is admissible for (r, θ) and o is the contractum of u = rθ according to r, then C[u] → C[o] is an R-reduction step. In this case, u is admissible for r in the term C[u]. We require that the set of admissible terms be closed under reduction. We also require that admissibility of terms, assignments, and contexts be closed under renaming of bound variables.

We call a CERS context-free if every context is admissible. An (unconditional) Expression Reduction System (ERS) is a CERS where all terms are admissible; an assignment θ is admissible for a rule r : t → s iff the condition (a) is satisfied; and all contexts are admissible for all redexes.

Our syntax is very close to the syntax of the λ-calculus and of First Order Logic. For example, the β-rule is written as Ap(λxA, B) → (B/x)A, where A and B can be instantiated by any terms; the η-rule is written as λx(Ax) → A which requires that an assignment θ is admissible iff x ∉ (Aθ), otherwise an x occurring in Aθ and therefore bound in λx(Aθx) would become free. A rule like f(A) → ∃x(A) is also allowed, but an assignment θ with x ∈ Aθ is not. The recursor rule is written as μ(λxA) → (μ(λxA)/x)A.

To express substitution, we use the S-rules

S^{n+1}x_{1} … x_{n}A_{1} … A_{n}A_{0} → (A_{1}/x_{1}, …, A_{n}/x_{n})A_{0}, n = 1, 2, …, where S^{n+1} is an operator sign of substitution with arity (n, n + 1) and scope indicator (n + 1), and x_{1}, …, x_{n} and A_{1}, …, A_{n}, A_{0} are pairwise distinct variables and metavariables. Each assignment is admissible for any rule in S. Hence a CERS R can be split into R_{fS} =_{def} R_{f} ∪ S, where R_{f} is obtained from R by adding symbols S^{n+1} in the alphabet and by replacing in the right-hand sides of the rules all metasubstitutions of the form (t_{1}/x_{1}, …, t_{n}/x_{n})t_{0} by S^{n+1}x_{1} … x_{n}t_{1} … t_{n}t_{0}, respectively. After defining the induced admissibility relations for R_{fS}, we can associate to any R-reduction an R_{fS}-reduction. And similarly to the case off ERSs [Kha92], we can define the descendant relation on subterms allowing to trace all subterms, including contracted redexes, along reductions in any CERS R.

2 Confluence for Orthogonal Conditional ERSs

Now we define orthogonal CERSs (OCERSs) and prove confluence for them. Our confluence proof is based on Nederpelt-Klop’s method [Ned73, Klo80] of reducing strong normalization proofs to weak normalization proofs. The trick is to use the method for proving termination of developments (FD), and all what remains is to check for permutation of TRS-steps and substitution steps. Our proof is considerably simpler than Klop’s [Klo80] original confluence proof for orthogonal CRSs which also establishes first FD and deduces confluence from it, and not more difficult than recent confluence proofs [vR93, Nip93, OR94], which use Tait&Martin-Löf’s method.

Definition 2.1 We call a CERS orthogonal (OCERS) if: (a) in no admissible term admissible redex-patterns can overlap; (b) all the descendants of an admissible redex u in an admissible term t under the contraction of any other admissible redex v ∈ t are again admissible redexes in the obtained term and are weakly similar to u; these redexes are v-residuals of u; and (c) no new metavariables are introduced in right-hand sides of rules. (Note that it follows from (b) that the familiar left-linearity condition is not needed any longer.)

The method of our proof is as follows. Developments in an OERS R can be represented as reductions in the OERS \underline{R} the rules of which are obtained from R-rules by underlining their head-symbols. To prove termination of \underline{R}-reductions, we split \underline{R} into \underline{R}_{fS}=\underline{R}_{f} ∪ S and define a non-erasing version \underline{R}_{fS}^{μ} of \underline{R}_{fS}. We prove that each term in \underline{R}_{fS}^{μ} has exactly one normal form (the proof consists of checking that TRS-steps and substitution steps commute). This implies that \underline{R}_{fS}^{μ} is strongly normalizing. Since to each \underline{R}_{fS}-reduction we can associate an \underline{R}_{fS}^{μ}-reduction of the same length, \underline{R}_{fS} is also strongly normalizing. As a corollary, we have FD for OERSs. But developments in OCERSs can be simulated by developments in OERSs since residuals of admissible redexes in OCERSs are admissible redexes weakly similar to their ancestors, by orthogonality. Hence FD is valid for OCERSs too, and confluence follows. (In fact, FD implies the strong confluence.)

Theorem 2.1 Orthogonal conditional context-sensitive ERSs are confluent.

3 Expressive power of CERSs

In [Mes92], Meseguer gives encodings of labeled transition systems, several functional programming languages, Cholmsky grammars, and some concurrent languages (e.g. Chemical Abstract Machine and CCS), into CTRSs. In this section, we give encodings of some other proof and computation systems, to show that CERSs are even more expressive programming languages. (We do not pursue any issues of efficient implementation of the systems.)

3.1 Conditional TRSs

In Bergstra-Klop [BK86] a notion of conditional TRSs, let us call it CTRS*s, is introduced. Rules in CTRS*s have the form: t → s ⇐ P_{1}(\overline{t_{1}}), …, P_{n}(\overline{t_{n}}), where P_{i} are arbitrary predicates and \overline{t_{i}} are lists of terms of corresponding lengths. An instance tθ of t is a redex iff θ(\overline{t_{i}}) satisfy P_{i}; and tθ can be rewritten into sθ in any context, i.e., CTRS*s are context-free.

In Dershowitz&Okada&Sivakumar [DJS88] a classification of CTRS*s is introduced, which is a generalization of the one introduced in [BK86]. In particular, semi-equational, join, normal, and generalized CTRS*s are defined. Our CERSs cover all these systems. Further, closed orthogonal CTRS*s as defined in [BK86, Klo80] are orthogonal; therefore our confluence result covers some confluence results from [BK86] for orthogonal CTRS*s. Several confluence results are obtained in the above papers for non-orthogonal CTRS*s as well, which perhaps can also be generalized to the higher-order case.

3.2 Encoding of strategies

In the literature a strategy is a map F: T er(Σ) → T er(Σ) such that t → F (t) if t is not a normal form, and t = F (t) otherwise. For our purposes this definition is not satisfactory. A strategy in our sense is a set F of quadruples of the form (t, r, θ, C[ ]), where r is a rule, θ is an admissible substitution for r, C[ ] is an admissible context for (r, θ), such that t = C[LHS(r)θ].

Given an ERS R and a strategy F for it, we can construct a CERS R_{F} where exactly the Rreductions performed according to the strategy F are possible. We take the signature of R for the signature of R_{F}; we take the rules of R for R_{F} -rules without changing the sets of admissible assignments for them; finally, for each rule r and admissible assignment θ, if and only if (t, r, θ, C[ ]) ∈ F, we declare C[ ] to be admissible for (r, θ) in R_{F}. Of course, this encoding is neither the only nor always the best way of encoding a strategy.

3.3 Encoding of rewrite systems with priorities

A TRSs with priorities [BBKW89], PRSs for short, is a TRS with a well-founded ordering > on rules. An r-redex u ∈ t is admissible iff there is no r′-redex in t with r′ > r, and u cannot be rewritten to an r′-redex without contracting a redex involving the top symbol of u. So clearly PRSs are context-sensitive CERSs. Not every ordering can define a sound rewrite relation on ground terms; therefore some sufficient criteria for the relation to be well defined are studied in [BBKW89]. A criterion for ground confluence for PRSs with well defined operational semantics is also found. In particular, it is shown that left-linear and essentially non-ambiguous RPSs are ground confluent (in fact, essential non-ambiguity is enough). Such PRSs are orthogonal in our sense, and the confluence criterion is covered by our CR theorem for OCERSs.

3.4 Encoding of Hilbert style proof systems

A Hilbert style system H has a number of axioms F_{1}, F_{2}, … and two rules: Modus Ponens, allowing to infer B when A and A ⇒ B are theorems, and the ∃-rule, allowing to infer ∃x.A[x] if A[t] is a theorem. A proof in the axiomatic theory H is a finite sequence of formulas G_{1}, G_{2}, G_{3}, …, G_{m} such that G_{i} is either an axiom (i.e., coincides with one of the F_{j}) or is obtained from G_{1}, …, G_{i−1} by one of the above two rules. In order to model proofs in the system H, to each proof in H we associate a reduction sequence, in an appropriate CERS R_{H}, starting from the term P^{0} and leading to the term P^{m}(G_{1}, …, G_{m}), where P^{n} is an n-ary operator symbol of type Bool × … × Bool → Nat. P^{n} encodes a list of m formulae. The alphabet of R_{H} consists of the alphabet of R augmented by the predicate symbols P^{n} of arity n. The rules, more precisely the rule-schemata, of R_{H} are:

• P^{n}(A_{1}, …, A_{n}) → P^{n+1}(A_{1}, …, A_{n}, F), for each n and axiom F. In particular P^{0} → P^{1}(F). Admissible assignments assign arbitrary formulae to the metavariables A_{1}, …, A_{n}, and an axiom to the metavariable F.

• P^{n}(A_{1}, …, A_{k}, …, A_{k} ⇒ A, …, A_{n}) → P^{n+1}(A_{1}, …, A_{k}, …, A_{k} ⇒ A, …, A_{n}, A) for each n ≥ 2. The A_{k} may also appear after A_{k} ⇒ A in the sequence. Admissible substitutions are the same as in the previous case.

• P^{n}(A_{1}, …, (A/x)A_{k}, …, A_{n}) → P^{n+1}(A_{1}, …, (A/x)A_{k}, …, A_{n}, ∃aA_{k}) for each n ≥ 1. An admissible assignment θ assigns arbitrary formulae to A_{1}, …, A_{n} and a term to A.

3.5 Encoding of Gentzen style proof systems

A sequent calculus G has rules of one of the two following forms, where Γ and Δ are lists of formulas (we ignore structural rules, which do not cause problems for our encoding):

r : \frac{Γ′ ⊢ Δ′}{Γ ⊢ Δ} , r : \frac{Γ′ ⊢ Δ′, Γ′′ ⊢ Δ′′}{Γ ⊢ Δ}

We present a sequent F_{1}, …, F_{n} ⊢ G_{1}, …, G_{m} from G as a term P_{n,m}(F_{1}, …, F_{n}, G_{1}, …, G_{m}), where P_{n,m} is an n+m-ary function symbol. A proof is presented as r(sequ, pr_{1}) or r(sequ, pr_{1}, pr_{2}), depending on the number of premises in the G-rule, where r is the name of the last applied rule, considered as a binary or ternary function symbol, sequ is the root of the proof tree in G, and pr_{i} are representations of the proofs whose roots have been used as the premises in the last step of the G-inference. In a stage of a G-inference several subproofs SP R_{1}, …, SP R_{k} are constructed. We represent that stage as P S^{k}(pr_{1}, …, pr_{k}), where pr_{i} is the representation of SP R_{i}.

The CERS R_{G} that encodes G has three kinds of rewrite rule-schemata, which correspond to introduction of axioms, and to applications of one and two premise rules, respectively:

1. P S^{k}(pr_{1}, …, pr_{k}) → P S^{k+1}(pr_{1}, …, pr_{k}, ax(axiom, ∅));

2. P S^{k}(pr_{1}, …, r′(sequ′, pr′), …, pr_{k}) → P S^{k}(pr_{1}, …, r(sequ, r′(sequ′, pr′)), …, pr_{k});

3. \begin{matrix}P S^{k}(pr_{1}, …, r′(sequ′, pr′), r′′(sequ′′, pr′′), …, pr_{k}) → \\ P S^{k}(pr_{1}, …, r(sequ, r′(sequ′, pr′), r′′(sequ′′, pr′′)), …, pr_{k}); \end{matrix}

Here axiom is the representation of an axiom of G – a sequent of the form Γ ⊢ Γ, sequ represents the sequent Γ ⊢ Δ, and similarly for sequ′ and sequ′′. Now a G-inference is encoded as an R_{G}-reduction starting from the constant P S^{0}.

3.6 Encoding of the π-calculus

Recall that the π-calculus [Mil92] terms P are defined as follows:

P = \overline{x}y.P | x(y).P | 0 | P |Q | !P | (x)P

A certain congruence relation is imposed on the π-terms, and the τ-rule then has the form:

x(y).P | \overline{x}z.Q → [z/y]P | Q.

Below [ ] is our translation function of π-terms, I and R are quantifier symbols, where I binds only in the second argument; and O, A, ! and 0 are function symbols of the encoding CERS R_{π}. (We do not impose the analogous congruence relation on terms in R_{π}.)

[x(y).P] = Iy(X, [P]); [\overline{x}z.Q] = O(X, Z, [Q]); [(x)P] = Rx([P]); [P |Q] = A([P], [Q]); [!P] =![P]; [0] = 0

The rules of R_{π} have the form: C[Iy(X, P), O(X, Z, Q)] → C[(Z/y)P, Q], where

(a) P, Q, X, Z are metavariables, and admissible assignments for X, Z are variables.

(b) C[ ] is a context such that among symbols above Iy(X, P) and O(X, Z, Q) in the LHS only the operators A, !, and Rx′ with x′ ≠ X can occur.

(c) The top-symbol of the LHS is A.

(d) No proper subterm of C[ ] contain both Iy(X, P) and O(X, Z, Q).

(e) A context C′[ ] is admissible for an R_{π}-redex iff above the hole in C′[ ] only the operators A, !, and R can occur. (Note that it is not possible to bind, in an admissible redex, the occurrences of variables corresponding to X with different occurrences of R.)

References

[BBKW89] Baeten J.C.M., Bergstra J.A., Klop J.W., Weijland W.P. Term Rewriting Systems with rule priorities. Journal of TCS 67, 1989, p. 283-301.

[BK86] Bergstra J. A., Klop J. W. Conditional Rewrite Rules: confluence and termination. JCSS vol. 32, n. 3, 1986, p. 323-362.

[DJS87] Dershowitz N., Okada M., Sivakumar G. Confluence of Conditional Rewrite Systems. In: Proc. of the 1^{st} International Workshop on Conditional Term Rewrite Systems, CTRS’87, Springer LNCS, vol. 308, p. 31-44.

[DJS88] Dershowitz N., Okada M., Sivakumar G. Canonical conditional rewrite systems. In: Proc. of the 9^{th} International Conference on Automated Deduction, Springer LNCS, vol. 310, p. 538-549.

[Kha92] Khasidashvili Z. The Church-Rosser theorem in Orthogonal Combinatory Reduction Systems. Report 1825, INRIA Rocquencourt, 1992.

[Klo80] Klop J.W. Combinatory Reduction Systems. Mathematical Centre Tracts 127. Centre for Mathematics and Computer Science, Amsterdam, 1980.

[KOR93] Klop J. W., van Oostrom V., van Raamsdonk F. Combinatory reduction systems: introduction and survey. In: To Corrado Böhm, J. of Theoretical Computer Science 121, 1993, p. 279-308.

[Mes92] Meseguer J. Conditional Rewriting Logic as a unified model of concurrency. Journal of TCS 96, 1992, p. 73-155.

[Mil92] Milner R. Functions as processes. In: Journal of Mathematical structures in Computer Science. 2(2): 1992, p. 119-141.

[Ned73] Nederpelt R.P. Strong normalization for a typed lambda-calculus with lambda structured types. Ph.D. Thesis, Eindhoven, 1973.

[Nip93] Nipkow T. Orthogonal higher-order rewrite systems are confluent. In: Proc. of the 1^{st} International conference on Typed Lambda Calculus and Applications, TLCA’93, Springer LNCS, vol. 664, Bazem M., Groote J.F., eds. Utrecht, 1993, p. 306-317.

[Oos94] Van Oostrom V. Confluence for Abstract and Higher-Order Rewriting. Ph. D. Thesis, Free University of Amsterdam, 1994.

[OR94] Van Oostrom V., van Raamsdonk F. Weak orthogonality implies confluence: the higherorder case. In: Proc. of the 3^{rd} International Symposium on Logical Foundations of Computer Science, LFCS’94, Springer LNCS, vol. 813, Nerode A., Matiyasevich Yu. V., eds. St. Petersburg, 1994, p. 379-392.

[vR93] Van Raamsdonk F. Confluence and superdevelopments. In: Proc. of the 5^{th} International Conference on Rewriting Techniques and Applications, RTA’93, Springer LNCS, vol. 690, C. Kirchner, ed. Montreal, 1993, p. 168-182.

[Wol93] Wolfram D. The clausal theory of types. Cambridge Tracts in Theoretical Computer Science, vol. 21, Cambridge University Press, 1993.