On Higher Order Recursive Program Schemes

Zurab Khasidashvili

School of Information Systems, UEA Norwich NR4 7TJ England zurab@sys.uea.ac.uk

Abstract. We define Higher Order Recursive Program Schemes (HRPSs) by allowing metasubstitutions (as in the λ-calculus) in righthand sides of function and quantifier definitions. A study of several kinds of similarity of redexes makes it possible to lift properties of (first order) Recursive Program Schemes to the higher order case. The main result is the decidability of weak normalization in HRPSs, which immediately implies that HRPSs do not have full computational power. We analyze the structural properties of HRPSs and introduce several kinds of persistent expression reduction systems (PERSs) that enjoy similar properties. Finally, we design an optimal evaluation procedure for PERSs.

1 Introduction

Higher Order Recursive Program Schemes (HRPSs) are recursive definitions of functions, predicates, and quantifiers, considered as rewriting systems. Similar definitions are used when one extends a theory by introducing new symbols [16]. ∃aA ⇔ (τa(A)/a)A and ∃!aA ⇔ ∃aA ∧ ∀a∀b(A ∧ (b/a)A ⇒ a = b) are examples of such definitions. Definitions of new symbols are added to the theory as axioms, and weak normalization of the system of definitions considered as a rewriting system ensures that the enriched theory is a conservative extension of the original one.

The main result of the paper — decidability of weak normalization (that is, existence of a normal form) in HRPSs — implies that HRPSs do not have full computational power: the existence of an interpreter for, say λ-calculus, in an HRPS would imply decidability of weak normalization for λ-terms, which is not valid [2]. Note that rewrite rules for the conditional cannot be used for evaluating expressions on the syntactic level, since they do not fall into the scope of our HRPSs. Indeed, it is well-known that addition of if − then − else yields full computational power [3]. The deep reason for Turing incompleteness of HRPSs is the restricted possibility for redex creation compared to languages with full computational power, the λ-calculus and Combinatory Logic, for example. This paper is a part of a general study of how various kinds of redex creation are reflected in syntactic properties of rewriting systems such as normalization, perpetuality, expressive power, etc. Some results in this direction are obtained in [7, 8, 10].

In [6], we introduced a formalism for higher order rewriting (i.e., term rewriting systems (TRSs) with bound variables and substitution mechanism) which is close to the Combinatory Reduction Systems (CRSs) of Klop [11]. The syntax of our Expression Reduction Systems (ERSs, called CRSs in [6]) is closer to the syntax of λ-calculus and First Order Logic. For example, the β-rule is written as β : Ap(λaA, B) → (B/a)A, where a is to be instantiated by a variable and A and B are to be instantiated by terms; an instance (t/x)s of (B/a)A denotes the result of substitution of the term t for x in the term s. To express “pure” substitutions syntactically we introduced S-reduction rules S^{n+1}a_{1} … a_{n}A_{1} … A_{n}A_{0} → (A_{1}/a_{1}, …, A_{n}/a_{n})A_{0}, n = 1, 2, . . ..

HRPSs are OERSs where left-hand sides of rewrite rules contain exactly one function or quantifier symbol. In order to construct an interpretation of HRPSs in (first order) Recursive Program Schemes (RPSs), we split an HRPS R into a “first order part” R_{f}, which delays substitutions, and a “substitution part” \underline{S}. (The method was originally used in [11] to prove the Church-Rosser property.) For example, a β-reduction step (λx t)s → (s/x)t expands to a β_{f}- reduction step (λx t)s → \underline{S}x s t and an \underline{S}-step \underline{S}x s t → (s/x)t (underlining of S-symbols is used to distinguish S-redexes created during R_{f}-reduction steps). Then the interpretation of HRPSs in RPSs, in which \underline{S}-reductions play the role of projection functions, can (roughly) be expressed by the following Representation Lemma: for any R-reduction P : t → → s, where R is an HRPS, there is an R_{f}-reduction P_{f} : t → → o such that s is obtained from o by any normalizing \underline{S}-reduction P\underline{S}; and conversely.

As in the case of orthogonal TRSs (OTRSs), we say that a subterm s of a term t in an orthogonal ERS (OERS) is inessential if there is a reduction P starting from t such that s does not have descendants under P; we call s essential otherwise [7]. The notion of descendant is a generalization of the usual notion of residual of a redex to all subterms in a way that makes it possible to trace contracted redexes: the descendant of a contracted redex is its contractum, while it does not have residuals. The descendant notion allows us to introduce the key concepts of this paper: several kinds of similarity of redexes. We explain the notion informally in terms of β-redexes. Let us consider the redexes u = (λx.x)s, v = (λx.(λy.z)x)o, w = (λx.xx)e, and u′ = (λx.y)t. We call u and v similar (written u ∼ v) because the binding variable x occurs free both in the bodies of u and v. In contrast, we have u ≁ u′. We call u and w essentially similar (written u ≈ w) because the binding variable x has essential occurrences in bodies of both redexes. Similarly, v ≈ u′, because the occurrence of x in the body (λy.z)x of v is inessential — it does not have descendants in the contractum of (λy.z)x. Similarity and essential similarity of terms obtained one from another by replacing some proper subterms are defined analogously.

The crucial property of essentially similar terms is the following Essential Similarity Lemma: corresponding subterms of essentially similar terms are either both essential or both inessential. A consequence is that corresponding arguments of essentially similar redexes are either both essential or both inessential. Hence, for any redex u, its essential similarity class ⟨u⟩_{e}, consisting of all redexes essentially similar to u, has an essentiality indicator which indicates which arguments of any v ∈ ⟨u⟩_{e} are essential. Another consequence of the Essential Similarity Lemma is that essentially similar redexes create essentially similar redexes, i.e., one can define an essential chain to be a sequence ⟨u_{0}⟩_{e}, ⟨u_{1}⟩_{e}, … such that any v_{i} ∈ ⟨u_{i}⟩_{e} creates an essential redex v_{i+1} ∈ ⟨u_{i+1}⟩_{e}. Then a term t in an HRPS R is weakly normalizable iff any essential chain of the essential similarity class of any essential redex of t is finite. So, in order to prove decidability of weak normalization in HRPSs, we need an algorithm for finding all essential (and inessential) subterms in a given term, and an algorithm for finding essentiality indicators of all redexes. Complete descriptions of the algorithms are presented in the body of the paper; we only note that our algorithm can also find essentiality indicators of redexes that do not have normal forms.

The above properties of HRPSs are due to the fact that each subterm s of a term t is free: if s is inside a redex u, then it is either inside an argument of u or coincides with u. We introduce persistent ERSs (PERSs), where not all subterms are free but all free subterms remain free under any reduction. This persistency property of free subterms is due to the fact that PERSs are the systems where only a special kind of redex creation — generation — is possible: all new redexes are actually present in right-hand sides of rewrite rules. For example, in the step σx(x) → f((σx(x)/x)x) = f(σx(x)), which corresponds to a rule σa(A) → f((σa(A)/a)A) and an assignment θ(a) = θ(A) = x, the created redex σx(x) is an instance of the metaterm σa(A) present in the right-hand side of the rewrite rule. We have generation here because θ(a) has an occurrence in θ(A). Therefore, the generation is not uniform — uniformly generated redexes are present in righthand sides of rules outside “mobile” arguments of metasubstitutions. During the reduction step σx(x) → f((d/x)x) = f(d) in the system {r_{1} : σa(A) → f((d/a)A), r_{2} : f(d) → c}, where d and c are constants, we have quasi-generation in the sense that all symbols needed to create the new redex f(d) are present in the right-hand side of r_{1}. The Essential Similarity Lemma remains valid in PERSs if the replaced subterms are free. Therefore, all the results obtained for HRPSs, the decidability of weak normalization in particular, remain valid for PERSs in general. Similar reasoning shows that strong normalization (that is, termination of all reductions) also is decidable in PERSs.

For uniformly persistent systems, we show that the strategy that in each step contracts an innermost essential redex is optimal. For PERSs in general, sharing of redexes of the same origin [14] is necessary. Alternatively, one can define an irreducible version of the PERS and use the innermost essential strategy without sharing in the irreducible system. As a corollary, we have an algorithm for optimal S-reductions and, in general, algorithms for optimal developments in OERSs, since developments are (up to isomorphism) reductions in non-creating HRPSs (where no redex-creation is possible). The above results cannot be generalized to quasi-persistent ERSs, where quasi-generation of redexes is possible.

The paper is organized as follows. In section 2, the review ERSs; in section 3, we study similarity of redexes; the main results are obtained in section 4 and are generalized to PERSs in section 5; we study optimal reductions in PERSs in section 6. Complete proofs of the results are reported in [9].

2 Orthogonal Expression Reduction Systems

Combinatory Reduction Systems have been introduced in Klop [11] to provide a uniform framework for reductions with substitutions (referred to also as higher order rewriting) as in the λ-calculus [2]. Several other formalisms have been introduced later. We refer to Klop et al. [13] for further information. Here we describe a system for higher order rewriting, called Expression Reduction Systems, as defined in [6] (under the name of CRSs).

Definition 2.1 (1) Let Σ be an alphabet, comprising variables v_{0}, v_{1}, …; 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.

(2) Metaterms are constructed from terms, term metavariables, which range over terms, and object metavariables, which range over variables. Apart from the usual rules for term-formation, one is allowed to have metasubstitutions — expressions of the form (A_{1}/a_{1}, …, A_{n}/a_{n})A_{0}, where a_{i} are object metavariables and A_{j} are metaterms. Metaterms that do not contain metasubstitutions are called simple metaterms. An assignment maps each object metavariable to a variable and each term 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 replacement of subterms of the form (t_{1}/x_{1}, …, t_{n}/x_{n})t by the result of substitution of terms t_{1}, …, t_{n} for free occurrences of x_{1}, …, x_{n} in t.

Definition 2.2 (1) An Expression Reduction System (ERS) is a pair (Σ, R), where Σ is an alphabet, described in Definition 2.1, and R is a set of rewrite rules r : t → s, where t and s are metaterms such that t is a simple metaterm and is not a metavariable, and each term metavariable which occurs in s occurs also in t. Further,

(a) The metaterms t and s do not contain variables, and each occurrence of an object metavariable in t and s is bound.

(b) An occurrence of a term-metavariable A in s is in the scope of an occurrence of an object metavariable a in s iff any occurrence of A in t is in the scope of an occurrence of a in t.

(2) An assignment θ is admissible for a rule r : t → s if occurrences of binding variables in sθ corresponding to object metavariables of s not occurring in t do not bind variables in subterms corresponding to term metavariables of s. For any admissible assignment θ′, tθ′ is an r-redex, and sθ is the contractum of tθ. Redexes that are instances of the left-hand side of the same rule are called weakly similar.

(3) R is simple if right-hand sides of R-rules are simple.

Below we ignore questions relating to renaming of bound variables.

Notation We use a, b for object metavariables, A, B for term metavariables, c, d for constants, t, s, e, o for terms and metaterms, u, v, w for redexes, σ, δ, ε for operators and operator signs, and P, Q for reductions. We write s ⊆ t if s is a subterm of t. A one-step reduction in which a redex u in a term t is contracted is written as t →^{u} s or t → s. We write P : t → → s if P denotes a reduction of t to s. |P | denotes the length of P. P + Q denotes the concatenation of P and Q.

The ERS S consists of the rules of the form S^{n+1}a_{1} … a_{n}A_{1} … A_{n}A → (A_{1}/a_{1}, …, A_{n}/a_{n})A, n = 1, 2 …, where S^{n+1} is the operator sign of substitution with arity (n, n + 1) and scope indicator (n + 1), and a_{1}, …, a_{n} and A_{1}, …, A_{n}, A are pairwise distinct object and term metavariables, respectively. For any ERS R, R_{f} is the ERS obtained from R by adding symbols \underline{S}^{n+1} in the alphabet and by replacing in right-hand sides of the rules all metasubstitutions of the form (t_{1}/a_{1}, …, t_{n}/a_{n})t with \underline{S}^{n+1}a_{1} … a_{n}t_{1} … t_{n}, t, respectively. If R is simple, then R_{fS} =_{def} R_{f} =_{def} R. Otherwise R_{fS} =_{def} R_{f} ∪ \underline{S}, where \underline{S}-rules are obtained from S-rules by underlining the S-symbols. For each step e = C[t_{i}θ] →^{u} C[s_{i}θ] = o in R there is a reduction P : e = C[t_{i}θ] → C[s′_{i}θ] → → C[sθ] = o in R_{fS}, where C[s′θ] → → C[sθ] is the rightmost innermost normalizing \underline{S}-reduction. We call P the expansion of u. The notion of expansion generalizes naturally to R-reductions with 0 or more steps.

Let t →^{u} s be an R_{f}-reduction step and let e be the contractum of u in s. For each argument o of u there are 0 or more arguments of e. We call them (u- )descendants of o. Correspondingly, subterms of o have 0 or more descendants. The descendant of each pattern-subterm (i.e., a subterm headed at the pattern) of u is e. It is clear what is to be meant by descendants of a subterm that is not

in u. In an S-reduction step C[S^{n+1}x_{1} … x_{n} t_{1} … t_{n}t_{0}]→^{u}C[(t_{1}/x_{1}, …, t_{n}/x_{n})t_{0}],

the argument t_{i} and subterms in t_{i} have the same number of descendants as the number of free occurrences of x_{i} in t_{0}. All subterms of t_{0}, including free occurrences of x_{1}, …, x_{n}, have exactly one descendant. The descendant of the contracted redex u itself is its contractum. The notion of descendant extends by transitivity to arbitrary R_{fS}-reductions. If P is an R-reduction, then P - descendants are defined to be the descendants under the expansion of P. The ancestor relation is converse to that of descendant. If t →^{u} s in R, then a redex in s is called a new redex or a created redex if it is not a residual of a redex of t (descendants of all redexes except the contracted redex are residuals).

We call the co-initial reductions P : t → → s and Q : t → → e strictly equivalent (written P ≈_{st} Q) if s = e and P -descendants and Q-descendants of any subterm of t are the same in s and e.

The definition of orthogonality in ERSs is similar to the case of TRSs: all the rules are left-linear and in no term redex-patterns can overlap (redex-pattern in ERSs and contractum-pattern in simple ERSs are defined similarly to the case of TRSs, see [11, 6]). As in the case of the λ-calculus [2], for any co-initial reductions P and Q, one can define in OERSs the notion of residual of P under Q, written P/Q, due to Lévy [14]. Below, we use the following properties of /:

Theorem 2.1 [6] Let P, P′, Q and Q′ be co-initial reductions in an OERS. (1) (Strict Church-Rosser) P + Q/P ≈_{st} Q + P/Q.

(2) (P + P′)/Q ≈_{st} P/Q + P′/(Q/P), P/(Q + Q′) ≈_{st} (P/Q)/Q′.

3 Similarity of redexes

In this section, we study some properties of substitutions and similarity of terms in HRPSs. In particular we prove the Replacement Lemma, the Essential Similarity Lemma, and the Uniform Generation Lemma.

We call a subterm s in t essential (written ES(s, t)) if s has at least one descendant under any reduction starting from t and call it inessential (written IE(s, t)) otherwise [7]. We say that P : t → → s erases a subterm s ⊆ t if s does not have descendants under P. The notion of essentiality is a generalization of the notion of neededness [5, 15] in a way that it works for all subterms, bound variables in particular.

The following lemma is valid for all OERSs; the proof is the same as in the case of OTRSs [7] and follows easily from the strict CR theorem.

Lemma 3.1 (1) Let s_{0}, …, s_{k} ⊆ t be inessential in t. Then there is a reduction starting from t that erases them.

(2) Let P : t → → t′ and s ⊆ t. Then IE(s, t) iff any P -descendant of s is inessential in t′.

Definition 3.1 We call an ERS R′ a subsystem of an ERS R if the alphabet and the set of rules of R′ are subsets of those of R.

Notation Below F V (t) (resp. EF V_{R}(t)) denotes the set of variables having (R-essential) free occurrences in t. For any subsystems R_{1} and R_{2} of R and any s ⊆ t, EBV_{R_{1},R_{2}}(s) is the set of variables having such free occurrences in s that are R_{2}-essential in s and are bound by quantifiers belonging to patterns of R_{1}- redexes that are outside s. We write BV_{R}(s) for EBV_{R,∅}(s) and EBV_{R}(s) for EBV_{R,R}(s). We write t = (t_{1}//e_{1}, …, t_{n}//e_{n})e if t is obtained from e by replacing non-overlapping proper subterms e_{1}, …, e_{n} in e with t_{1}, …, t_{n}, respectively.

Definition 3.2 We call an OERS R a Higher Order Recursive Program Scheme (HRPS) if, for any rule t → s, pattern of t consists of one operator, i.e., t has the form σa_{1} … a_{m}(A_{1}, …, A_{n}), where σ is an operator sign with arity (m, n).

Definition 3.3 (1) Let σa_{1} … a_{n}A_{1} … A_{m} be the left-hand side of a rewrite rule r in an HRPS R and let u = σx_{1} … x_{n}t_{1} … t_{m} be an r-redex. The characteristic system of u (written CS(u)) is the set of pairs (a_{j}, A_{i}) such that t_{i} is in the scope of σ and x_{j} ∈ F V (t_{i}) (i = 1, …, m, j = 1, …, n). We call u an ⟨r⟩-redex, where ⟨r⟩ = (r, CS(u)) is a characterized rule (C-rule for short). For any subsystem R′ of R, an R′-essential characteristic system of u (written ECS_{R′}(u)) is the set of pairs (a_{j}, A_{i}) such that t_{i} is in the scope of σ and x_{j} ∈ EF V_{R′}(t_{i}). We call u an ⟨r⟩_{e}-redex, where ⟨r⟩_{e} = (r, ECS_{R′}(u)) is an R′-essentially characterized rule (EC_{R′}-rule for short). (We omit the subscript R′ if R = R′.)

(2) Let t = (t_{1}//e_{1}, …, t_{k}//e_{k})e. We write e ≺_{R_{1},R_{2}} t if EBV_{R_{1},R_{2}}(e_{i}) ⊆ EBV_{R_{1},R_{2}}(t_{i}) for all i = 1, …, k, and write e ∼_{R_{1},R_{2}} t if e ≺_{R_{1},R_{2}} t and t ≺_{R_{1},R_{2}} e. We abbreviate ≺_{R,∅} to ≺_{R} and ≺_{R,R} to ≺≺_{R}. We call t and e R-similar (resp. R-essentially similar), written e ∼_{R} t (resp. e ≈_{R} t), if s ≺_{R} t and t ≺_{R} s (resp. s ≺≺_{R} t and t ≺≺_{R} s).

Of course, (essential) similarity of terms depends on the specification of the replaced subterms. Note that, for any weakly similar R-redexes v and u, if one specifies replaced subterms to be the arguments of the redexes, then v ≺ u (resp. v ≺≺ u) iff CS(v) ⊆ CS(u) (resp. ECS_{R}(v) ⊆ ECS_{R}(u)). Below, when we speak of (essential) similarity of redexes without specifying replaced subterms, we mean that the replaced subterms are the arguments of the redexes; we write v≺^{r}u, v≺≺^{r}u, v∼^{r}u, and v≈^{r}u for v ≺ u, v ≺≺ u, v ∼ u, and v ≈ u, respectively, to stress the fact that the replaced subterms are specified to be arguments of the redexes. ⟨r⟩, as well as ⟨u⟩, will also denote the equivalence class of all ⟨r⟩-redexes (which are similar to u). ⟨r⟩_{e}, as well as ⟨u⟩_{e}, will also denote the equivalence class of all ⟨r⟩_{e}-redexes.

3.1 The Replacement Lemma

Definition 3.4 Let u = Sx_{1} … x_{n}t_{1} … t_{n}t_{0} and t′_{0} be an S-normal form of t_{0}. A subterm e in u is called u-inessential (written IE_{S}(u; e)) if e is in t_{i} for some 1 ≤ i ≤ n and x_{i} ∉ F V (t′_{0}).

Lemma 3.2 (1) Let u = Sx_{1} … x_{n}t_{1} … t_{n}t_{0} ⊆ t. Then IE_{S}(u; t_{i}) iff x_{i} ∉ EF V_{S}(t_{0}).

(2) Let s ⊆ t. Then IE_{S}(s, t) iff IE_{S}(u; s) for some S-redex u in t.

(3) Let e ⊆ s ⊆ t. Then ES_{S}(e, t) iff ES_{S}(e, s) and ES_{S}(s, t).

Proof. (1) From Lemma 3.1.(2). (2) One can take for u the redex whose residual erases all descendants of s in the rightmost innermost normalizing S-reduction.

(3) (⇒) From the definition of essentiality. (⇐) By (2), the redex that would make e inessential can neither occur in s nor contain s in its argument.

Lemma 3.3 (Replacement Lemma) Let s be obtained from t by replacing non-overlapping proper subterms t_{1}, …, t_{n} with s_{1}, …, s_{n}, respectively, where s_{i} and t_{i} do not contain S-redexes, and let ES_{S}(s_{i}, s) ⇒ BV_{S}(t_{i}) ⊆ BV_{S}(s_{i}) (i = 1, …, n). Further, let s′ and t′ be any corresponding subterms in s and t that are not in replaced subterms. Then IE_{S}(s′, s) ⇒ IE_{S}(t′, t).

Proof sketch. By induction on the length of s. It is enough to consider the case when t and s are S-redexes. Let t = Sx_{1} … x_{k}e_{1} … e_{k}e, s = Sx_{1} … x_{k}o_{1} … o_{k}o, s′ ⊆ o_{l}, and IE_{S}(s′, s). If IE_{S}(s′, o_{l}), then by the induction assumption IE_{S}(t′, e_{l}) and hence IE_{S}(t′, t). Otherwise, by Lemma 3.2.(3), IE_{S}(o_{l}, s); by Lemma 3.2.(2), IE_{S}(s; o_{l}); and by Lemma 3.2.(1), x_{l} ∉ EF V_{S}(o). Therefore, it follows from the induction assumption (which is valid by Lemma 3.2.(2)) that x_{l} does not have an essential occurrence in e_{0} either outside or inside the replaced subterms. Hence, by Lemma 3.2.(1), IE_{S}(t; e_{l}) and by Lemma 3.2.(2), IE_{S}(t; t′) and IE_{S}(t′, t).

3.2 The Essential Similarity Lemma

In the rest of this section we only consider HRPSs.

Notation Recall that, if F is a set of R-redexes in a term t, then a complete F -development of t is a reduction that contracts residuals of redexes from F as long as possible. Below F_{R} denotes a complete F -development in R, F_{f} denotes a complete F -development in R_{f}, and F\underline{S} denotes a complete development of the set of \underline{S}-redexes created during F_{f}. If F consists of one redex u only, then we write u_{R}, u_{f}, and u\underline{S} for F_{R}, F_{f}, and F\underline{S}, respectively.

Lemma 3.4 Let F be a set of R-redexes in a term t. Then F_{R} ≈_{st} F_{f} + F\underline{S}.

Proof. By induction on number n of redexes in F. The case n = 0 is trivial. So let F = F′∪{u}, where u is an outermost among redexes in F. Then F_{R} ≈_{st} F′_{R}+u′_{R} (where u′ = u/F_{R}) ≈_{st}(by the induction assumption)≈_{st} F′_{f} +F ′ ; \underline{S} +u′_{R} ≈_{st} F′_{f} +

u′′_{R}+F ′ ; \underline{S}/u′′_{R} (where u′′ is the unique ancestor of u′) ≈_{st} F′_{f} +u′′_{f}+u′′ ; \underline{S} +F ′ ; \underline{S}/u′′_{R} ≈_{st}

F_{f} + u′′ ; \underline{S} + F ′ ; \underline{S}/u′′_{R} ≈_{st} F_{f} + F\underline{S}.

[figure: F′_{f}; F ′ ; \underline{S}; u′_{R}; F_{f}; u′′_{f}; u′′ ; \underline{S}; ∅; F ′ ; \underline{S}/u′′_{R}]

Lemma 3.5 (Representation Lemma) Let R be an HRPS.

(1) For any P : t → →_{R} s there are Q : s → →_{R} e and P′ : t → →_{R_{f}} o such that P + Q ≈_{st} P′ + P′′, where P′′ is a normalizing \underline{S}-reduction starting from o.

(2) If P_{f} : t → →_{R_{f}} s and P\underline{S} is a normalizing \underline{S}-reduction starting from s, then there is an R-reduction P_{R} such that P_{f} + P\underline{S} ≈_{st} P_{R}.

Proof. (1) By induction on |P |. Let P = P^{∗} + u. By the induction assumption, there are R-reduction Q^{∗}, R_{f}-reduction P_{1}, and a normalizing \underline{S}-reduction Q_{1} such that P^{∗} + Q^{∗} ≈_{st} P_{1} + Q_{1}. Let F be the set of all Q^{∗}-residuals of u and let F′ be the set of their Q_{1}-ancestors for which redexes from F are residuals (\underline{S}-reduction steps do not create new redexes). Then, F′_{R} + Q_{1}/F′_{R} ≈_{st} Q_{1} + F_{R}.

By Lemma 3.4, F′_{R} = F′_{f} +F ′ ; \underline{S}. Thus P_{1} +F′_{f} +F ′ ; \underline{S} +Q_{1}/F′_{R} ≈_{st} P_{1} +Q_{1} +F_{R} ≈_{st}

P^{∗} + Q^{∗} + F_{R} ≈_{st} P^{∗} + u + Q^{∗}/u = P + Q^{∗}/u and we can take Q = Q^{∗}/u, P′ = P_{1} + F′_{f}, and P′′ = F ′ ; \underline{S} + Q_{1}/F′_{R}. (Note that Q contracts the redexes that belong to the families [14, 1] of redexes contracted by P.)

[figure: .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; P^{∗}; P_{1}; Q_{1}; Q^{∗}/u; Q^{∗}; F′_{R}; F_{R}; u; Q_{1}/F′_{R}; P′_{f}; P′_{R}; u_{f}; F_{f}; F_{R}; P ′ ; \underline{S}; P\underline{S}; F\underline{S}]

(2) By induction on |P_{f}|. The case |P_{f}| = 1 is immediate. So let P_{f} : t → → e→^{u}s and let P′_{f} : t → → e be the initial part of P_{f}. By the induction assumption, there is

an R-reduction P′_{R} such that P′_{R} ≈_{st} P′_{f} +P ′ ; \underline{S}. Hence P_{f} +P\underline{S} ≈_{st} P′_{f} +u_{f} +P\underline{S} ≈_{st}

P′_{f} + P ′ ; \underline{S} + F_{f} + F\underline{S} (where F is the set of residuals of u under P ′ ; \underline{S}) ≈_{st} (by the induction assumption) ≈_{st} P′_{R} + F_{f} + F\underline{S} ≈_{st} (by Lemma 3.4)≈_{st} P′_{R} + F_{R}, and we can take P_{R} = P′_{R} + F_{R}.

Corollary 3.1 Let R be an HRPS. Then IE_{R}(s, t) iff there is an R_{f}-reduction P : t → → e such that all P -descendants of s in t′ are \underline{S}-inessential.

Lemma 3.6 (Essential Similarity Lemma) Let s = (s_{1}//t_{1}, …, s_{n}//t_{n})t, in an HRPS R, let t ≺≺_{R} s, and let s′ and t′ be any corresponding subterms of s and t that are outside the replaced subterms. Then IE_{R}(s′, s) ⇒ IE_{R}(t′, t).

Proof. Let IE_{R}(s′, s). By Lemma 3.1.(1), there are R-reductions s_{i} → → s_{i}^{∗} and t_{i} → → t_{i}^{∗} such that none of R-inessential free variables of s_{i} and t_{i} that are bound in s and t have descendants in s_{i}^{∗j} and t_{i}^{∗j}. Hence, by Lemma 3.1.(2), it is enough to consider the case then EBV_{R}(s_{i}) = BV (s_{i}) and EBV_{R}(t_{i}) = BV (t_{i}). By Corollary 3.1, there is an R_{f}-reduction P : s → → e such that all P -descendants of s′ are \underline{S}-inessential. Let Q : t → → o be an R_{f}-reduction that contracts redexes corresponding to the contracted redexes of P that are not inside (the descendants of) s_{1}, … s_{n} and omits the steps made inside s_{1}, … s_{n}. Thus, if s_{i}^{1}, … s_{i}^{k_{i}} is the enumeration of all P -descendants of s_{i} from left to right and t_{i}^{1}, … t_{i}^{k_{i}} is the enumeration of all Q-descendants of t_{i} from left to right (i = 1, …, n), then o is obtained from e by replacing s_{i}^{j} with t_{i}^{j} (subterms s_{i}^{j} and t_{i}^{j} are disjoint, t_{i}^{j} = t_{i}, and s_{i} → → s_{i}^{j}). Since t ≺≺_{R} s, it follows from the conditions (a)-(b) in the Definition 2.2 that o ≺_{R∪\underline{S},R} e; and since EBV_{R}(s_{i}) = BV (s_{i}) and EBV_{R}(t_{i}) = BV (t_{i}), we have that o ≺_{R∪\underline{S},∅} e, in particular, o ≺\underline{S} e. Thus, by Lemma 3.1.(2) and the Replacement Lemma, all descendants of t′ in o′ are \underline{S}-inessential. Hence, by Corollary 3.1, IE_{R}(t′, t).

3.3 The Uniform Generation Lemma

In this subsection, we prove the Uniform Generation Lemma; it establishes a relation between similarity of redexes and generation of redexes in HRPSs.

Lemma 3.7 Let e_{0} ⊆ s_{0} ⊆ t_{0}, P : t_{0}→^{u_{0}}t_{1}→^{u_{1}} … → t_{n}, and let s_{i+1} ⊆ t_{i+1}

be a u_{i}-descendant of s_{i} ⊆ t_{i} (i = 0, …, n − 1). Then there is a reduction Q : o_{0} = s_{0}→^{v_{0}}o_{1}→^{v_{1}} … → o_{n} such that s_{i} = o_{i}θ_{i} for some substitution θ_{i} and the descendants of e_{0} in s_{i} and o_{i} are corresponding occurrences.

Proof sketch. By induction on |P |, considering relative positions of u_{i} and s_{i}.

Lemma 3.8 (1) Each outermost redex in a term t is essential.

(2) ES(e, t) iff ES(s, t) and ES(e, s).

(3) IE(e, t) iff e is in an inessential argument of an essential redex u of t.

Proof sketch. Similarly to the case of OTRSs [7], using Lemma 3.7.

Lemma 3.9 Let t→^{w}s and let v ⊆ s be a residual of a redex u ⊆ t. Then u≈^{r}_{R}v.

Proof. If u ⊆ w, then by Lemma 3.7, v = uθ for some substitution θ and u≈^{r}_{R}v follows from the Essential Similarity Lemma. If u and w do not overlap, then u = v. Otherwise, if w ⊆ u, then u≈^{r}_{R}v follows from Lemma 3.1.(2).

Lemma 3.10 (Uniform Generation Lemma) Let R be an HRPS, R′ be a subsystem of R, u and v be R-redexes, u≺≺^{r}_{R′}v, u→^{u}o, and v→^{v}e. If there is an R′-essential R-redex w in o created by u, then e contains an R′-essential R-redex w′, created by v, such that w≺≺^{r}_{R′}w′.

Proof. Let o′ and e′ be contracta of u and v in R_{f}. Then e′ is obtained from o′ by replacing the descendants of arguments of u with corresponding descendants of arguments of v. Since the replaced subterms do not contain \underline{S}-redexes (and R′-essentiality coincides with R′ ∪ \underline{S}-essentiality), it follows from conditions (a)- (b) of Definition 2.2 that o′ ≺≺_{\underline{S}∪R′} e′. Let w_{1} be the ancestor of w in o′ and w_{2} be the corresponding redex of w_{1} in e′. Then ES_{\underline{S}∪R′}(w_{1}, o′) and, by Lemma 3.6, ES_{\underline{S}∪R′}(w_{2}, e′). Therefore, w_{2} has an R′-essential residual w′ in e′.

Let w_{1} = σx_{1} … x_{k}(o_{1}, …, o_{m}) and w_{2} = σy_{1} … y_{k}(e_{1}, …, e_{m}). Let o_{j} be in the scope of σ and x′_{i} be an occurrence of x_{i} in o_{j} that is R′ ∪ \underline{S}-essential in o_{j}. If x′_{i} is outside the replaced subterms, then its corresponding occurrence of y_{i} in e_{j} is R′ ∪ \underline{S}-essential in e_{j} by Lemma 3.6. If x′_{i} is in a replaced subterm t^{∗}, then, by Lemma 3.8.(2), t^{∗} is R′ ∪ \underline{S}-essential in o_{j}, its corresponding replaced subterm s^{∗} is R′ ∪\underline{S}-essential in e_{j} by Lemma 3.6, and, again by Lemma 3.8.(2), each occurrence of y_{i} in s^{∗} that is R′ ∪\underline{S}-essential in s^{∗} (there exists one because o′ ≺≺_{\underline{S}∪R′} e′) is R′ ∪ \underline{S}-essential in e_{j} as well. Thus w_{1}≺≺^{r}_{\underline{S}∪R′}w_{2}. Hence, by

Lemma 3.9, w≺≺^{r}_{R′}w′.

Remark 3.1 It follows easily from Lemmas 3.8 and 3.6 that the latter remains valid if the condition t ≺≺_{R} s is replaced by a (strictly) weaker condition that, for any corresponding redexes w and w′ in t and s, w≺≺^{r}_{R}w′.

4 Decidability of weak normalization in HRPSs

In this section, we prove decidability of weak and strong normalization in HRPSs. The following definition is crucial; its correctness follows from the Essential similarity Lemma and the Uniform Generation Lemma.

Definition 4.1 (1) We call a sequence ⟨r_{0}⟩_{e}, ⟨r_{1}⟩_{e}, … an essential ⟨r_{0}⟩_{e}-chain or an essential u_{0}-chain, where u_{0} ∈ ⟨r_{0}⟩_{e}, if an essential ⟨r_{i+1}⟩_{e}-redex is created by contraction of any ⟨r_{i}⟩_{e}-redex.

(2) We call the sequence of numbers of essential arguments of u the essentiality indicator of ⟨u⟩_{e} and of u.

(3) We call a sequence ⟨r_{0}⟩, ⟨r_{1}⟩, … an ⟨r_{0}⟩-chain or a u_{0}-chain, where u_{0} ∈ ⟨r_{0}⟩, if an ⟨r_{i+1}⟩-redex is generated by contraction of any ⟨r_{i}⟩-redex .

Lemma 4.1 (1) A term t in an HRPS is weakly normalizable iff all essential chains of essential redexes in t are finite.

(2) A term t in an HRPS R is strongly normalizable iff all chains of redexes in t are finite.

Proof sketch. (1) Similarly to the case of OTRSs [7]. (2) (⇒) Immediate. (⇐) Existence of an infinite reduction would imply existence of an infinite sequence u_{0}, v_{0}, u_{1}, v_{1}, …, such that v_{i} is a contracted residual of u_{i} and v_{i} generates u_{i+1}, i = 0, 1, …; therefore, by Lemma 3.10, there would exist an infinite chain ⟨u_{0}⟩ = ⟨w_{0}⟩, ⟨w_{1}⟩, … (such that u_{i}≺^{r}w_{i}), a contradiction.

Lemma 4.2 Let essentiality indicators of all EC-rules in an HRPS R be known. Then one can find all inessential subterms of a term t in R as follows:

Algorithm 4.1 Choose in t an innermost redex; find its essential characteristic system (which coincides with its characteristic system); underline its inessential arguments; and mark the redex itself. Now choose in t an unmarked redex that only contains marked redexes; find its essential characteristic system (only occurrences that are in the underlined subterms are inessential); underline its inessential arguments; mark the redex itself; and so on, as long as possible. Then exactly occurrences that are in underlined subterms are inessential in t.

Proof. From Lemma 3.8.

Definition 4.2 Let r : t = σa_{1} … a_{n}A_{1} … A_{m} → B, and let θ be an admissible assignment such that A_{i}θ are in R-normal form and tθ ∈ ⟨r⟩_{e}. Then we call rθ : tθ → sθ a trivial ⟨r⟩_{e}-instance of r.

Lemma 4.3 Let ⟨r_{1}⟩_{e}, …, ⟨r_{l}⟩_{e} be all EC-rules in an HRPS R and r_{i}θ_{i} : t_{i}θ → s_{i}θ be a trivial ⟨r_{i}⟩_{e}-instance of r_{i} : t_{i} → s_{i} (i = 1, …, l). Then the essentiality indicators of the EC-rules in R can be found using the following Algorithm 4.2 Find, for each i, all arguments of t_{i}θ_{i} that do not have descendants in s_{i}θ_{i}. Let the corresponding arguments of any ⟨r_{i}⟩_{e}-redex be 0inessential. Let the 0-essentiality indicator of ⟨r_{i}⟩_{e} be the list of numbers of arguments of any ⟨r_{i}⟩_{e}-redex that are not 0-inessential. Apply Algorithm 4.1 to the right-hand sides of all EC-rules of R using 0-essentiality indicators of EC-rules instead of essentiality indicators. Let the 1-inessential arguments of t_{i}θ_{i} be all arguments whose descendants in s_{i}θ_{i} are in underlined subterms. Let the corresponding arguments of any ⟨r_{i}⟩_{e}-redex be 1-inessential, and let the 1-essentiality indicator of ⟨r_{i}⟩_{e} be the list of numbers of arguments of any ⟨r_{i}⟩_{e}-redex that are not 1-inessential. Apply again Algorithm 4.1 to the right-hand sides of all EC-rules of R using 1-essentiality indicators of EC-rules instead of essentiality indicators; and so on. The algorithm stops after n_{0} steps if n_{0}-essentiality indicator of each EC-rule in R coincides with its (n_{0} − 1)-essentiality indicator. Let the n_{0}-inessential arguments of R-redexes be inessential*. Then the essentiality indicator of ⟨r_{i}⟩_{e} coincides with the list of non-inessential* arguments of t_{i}θ_{i}.

Proof. An easy induction on n shows that n-inessential arguments of each redex are inessential; the case n = 0 follows from Lemma 3.6, and the induction step follows from Lemmas 4.2 and 3.1.(2). Now let us prove by induction on k that if, for an EC-rule ⟨r_{i}⟩_{e}, there is an ⟨r_{i}⟩_{e}-redex u whose j-th argument s_{j} (is inessential and) is erased by some reduction P with a length |P | ≤ k, then the j-th argument e_{j} of t_{i}θ_{i} is inessential*. The case k = 1 is obvious. So suppose P : u→^{u}o → → e. Let s′_{j} be a descendant of s_{j} in o, and let v be the minimal redex that contains s′_{j} and has a descendant in e. Suppose that v ∈ ⟨r_{m}⟩_{e} and s′_{j} is in its p-th argument. By Lemma 3.7, there is a reduction Q starting from v with a length less than k, such that the p-th argument of v does not have Q-descendants. Hence, by the induction assumption, the p-th argument of tθ_{m} is inessential*. Similarly, any descendant of s_{j} in o is in an inessential* argument of some redex. Since CS(t_{i}θ_{i}) = ECS(t_{i}θ_{i}) = ECS(u) ⊆ CS(u), for any descendant e′_{j} of e_{j} there is a descendant s_{j}^{∗} of s_{j} in o that is not in an inessential argument of a non-created redex and such that, for any q = 1, …, l, e′_{j} is in an argument of an ⟨r_{q}⟩_{e}-redex iff s_{j}^{∗} is in the corresponding argument of a created ⟨r_{q}⟩_{e}-redex. Hence, any descendant of e_{j} in s_{i}θ_{i} is in an inessential* argument of some redex, and e_{j} itself is inessential*.

Example 4.1 In order to illustrate Algorithm 4.2, let us consider the following HRPS R = {σa(A, B) → (εa(A)/a)B, δa(A) → σa(A, f(A)), f(A) → g(A, A), g(A, B) → const}, where a is an object metavariable, A, B are term metavariables, f, g are function symbols, σ, ε, and δ are quantifier signs with arities (1, 2), (1, 1), and (1, 1), and scope indicators (1, 2), (1), and (1), respectively. The rule for σ has four trivial instances r_{1} : σx(x, x) → (εx(x)/x)x = εx(x), r_{2} : σx(x, y) → (εx(x)/x)y = y, r_{3} : σx(y, x) → (εx(y)/x)x = εx(y), and r_{4} : σx(y, y) → (εx(y)/x)y = y with ECSs {(a, A), (a, B)}, {(a, A)}, {(a, B)}, and { }, respectively. Similarly, we can choose trivial instances of the rules for δ, f, and g: r_{5} : δx(x) → σx(x, f(x)), r_{6} : δx(y) → σx(y, f(y)), r_{7} : f(x) → g(x, x), and r_{8} : g(x, y) → const. The result of Algorithm 4.2 is then as follows:

r_{1} : σx(x, x) → (εx(x)/x)x = εx(x) r_{5} : δx(\overbrace{x}^{2}) → σx(\underline{x}_{2,3}, f(\underline{x}_{2,3}))

r_{2} : σx(\overbrace{x}^{0}, y) → (εx(x)/x)y = y r_{6} : δx(\overbrace{y}^{2}) → σx(\underline{y}_{1,2,3}, f(\underline{y}_{2,3}))

r_{3} : σx(y, x) → (εx(y)/x)x = εx(y) r_{7} : f(\overbrace{x}^{1}) → g(\underline{x}_{1,2,3}), \underline{x}_{1,2,3}))

r_{4} : σx(\overbrace{y}^{0}, y) → (εx(y)/x)y = y r_{8} : g(\overbrace{x}^{0}, \overbrace{y}^{0}) → const

where ^{i} indicates that the subterm is i-inessential and _{−j} indicates that the underlining was made in j-th running of Algorithm 4.1 (we have j ≤ 3). Note that, for example, the ECS of the right-hand side σx(x, f(x)) of r_{5} used in the second running is a proper subset of ECS of σx(x, f(x)) used in the first running, and this makes it possible to determine that the argument x of the left-hand side δx(x) of r_{5} is 2-inessential, and hence inessential.

Theorem 4.1 (1) Weak normalization is decidable in HRPSs.

(2) HRPSs do not have full computational power.

(3) Strong normalization is decidable in HRPSs.

Proof. (1) From Lemmas 4.1-4.3. (2) From (1). (3) From Lemmas 4.1.

5 Persistent systems

Without restricting the class of OERSs we can assume that in right-hand sides of rewrite rules the last argument of each metasubstitution is a term-metavariable or a metasubstitution.

Definition 5.1 Let R be an orthogonal ERS.

(1) Let t→^{u}s, let t → t′ → → s be its expansion, let o ⊆ t′ be the contractum of u in R_{f}, and let v be a new redex in s. We call v generated if v is a residual of a redex w of t′ whose pattern is in the pattern of o. We call v uniformly generated if the pattern of w is in the pattern of o and is not inside an \underline{S}-redex. We call v quasi-generated if any of its pattern-subterms is a descendant of a pattern-subterm of o that is not an \underline{S}-redex.

(2) We call R respectively persistent (PERS), uniformly persistent, or quasipersistent if, for any R-reduction step, each created redex is generated, uniformly generated, or quasi-generated.

A quasi-persistent ERS that is not persistent was considered in the introduction. It is easy to see that a non-simple OERS R is an HRPS iff R_{fS} is persistent. Obviously, a PERS need not be an HRPS.

We call a subterm s in t free if s is not a proper pattern-subterm of a redex in t. It is easy to see that all free subterms remain free under any reduction in PERSs. This fails already for quasi-persistent systems. All properties of similar and essentially similar terms in HRPSs are valid because all subterms are free in HRPSs. Therefore, it is not difficult to check that this properties remain valid for all PERSs if in the definition of similarity and essential similarity one requires the replaced subterms to be free; Theorem 4.1 generalizes to PERSs as well.

Obviously, a PERS R is weakly (resp. strongly) normalizing iff all essential chains (resp. all chains) in R are finite. For any subsystem R′ of R, we call an R-redex u ECS_{R′}-complete if each binding variable of a pattern quantifier of u has an R′-essential free occurrence in each argument that belongs to its binding scope. It can be shown that any R-essential chain (resp. any chain) of a redex w is a subsequence of an R-essential chain (resp. chain) of an ECS_{R}-complete (resp. ECS_{∅}-complete) redex that is weakly similar to w. Thus, in order to establish weak (strong) normalization of a PERS, it is enough to check essential chains (chains) of ECS_{R}-complete (ECS_{∅}-complete) redexes only.

6 Optimal normalization in persistent ERSs

Theorem 6.1 Let t be a term in a uniformly persistent ERS. Contraction of innermost essential redexes gives a reduction of t to normal form with the least number of steps, whenever the normal form exists.

Proof sketch. Let P : t = t_{0} →^{u_{0}} … → t_{n} be a normalizing reduction starting from t and Q : t = s_{0} →^{v_{0}} s_{1} →^{v_{1}} … be an innermost essential reduction. It can be shown by induction on i that, for each i < |Q|, there is a number n_{i} < n such that ES(u_{n_{i}}, t_{n_{i}}), u_{n_{i}} ≈ v_{i}, and i ≠ j implies n_{i} ≠ n_{j}. Therefore |Q| ≤ |P |.

Thus, one can construct optimal sequential normalizing reductions in uniformly persistent ERSs. For PERSs in general, sharing of redexes of the same family [14, 1] is necessary. For example, one can check that all normalizing reductions starting from a term σx(f(x)) in the following PERS R = {σa(A) → (εa(A)/a)A, εa(A) → (τa(A)/a)A, f(A) → g(A, A)} must contract two copies of at least one generated redex. Alternatively, for each PERS one can construct its irreducible version, by eliminating all defined symbols in the right-hand sides of rules. To avoid (sometimes vain) substitutions during reduction steps, one can instead use trivial instances of the rules in the following way (we consider only the case of HRPSs). Let r : t = σa_{1} … a_{n}A_{1} … A_{m} → s and let θ be an admissible assignment such that tθ ∈ ⟨r⟩_{e} and A_{i}θ = f_{l}(x_{i_{1}}, …, x_{i_{k}}), where x_{i_{j}} = θ(a_{i_{j}}) and f_{l} is a fresh function symbol, chosen different for each EC-rule ⟨r⟩_{e} and each i. By Theorem 4.1, one can decide wheither tθ has a normal form t′ and find it. Let us call tθ → t′ the irreducible ⟨r⟩_{e}-rule (it is not an ERS rule, but represents the irreducible rule whose admissible assignments are all assignments θ′ such that tθ′ ∈ ⟨r⟩_{e}). Then, for any ⟨r⟩_{e}-redex u = σx_{1}, …, x_{n}s_{1} … s_{m}, one defines its contractum according to tθ → t′ to be the normal form of t′ with respect to the rules f_{l}(x_{i_{1}}, …, x_{i_{k}}) → s_{i}. Now an optimal normalizing reduction of a normalizable term o in an HRPS R consists of execution of essential redexes in an inside out order according to the irreducible EC-rules; and the length of the reduction coincides with the number of essential redexes in o.

Acknowledgments I thank G. Gonthier and L. Maranget for many suggestions, R. Kennaway, B. Pierce, and F. J. de Vries for careful reading, and J.W. Klop and J.-J. Lévy for their support during my stay at CWI and INRIA.

References

1. Asperti A, Laneve C. Interaction Systems 1. The theory of optimal reductions. INRIA Report 1748, 1992.

2. Barendregt H. P. The Lambda Calculus, its Syntax and Semantics. North-Holland, 1984.

3. Courcelle B. Recursive Applicative Program Schemes. In: J. van Leeuwen ed. Handbook of Theoretical Computer Science, Chapter 9, vol.B, 1990, p. 459-492.

4. Dershowitz N., Jouannaud J.-P. Rewrite Systems. In: J.van Leeuwen ed. Handbook of Theoretical Computer Science, Chapter 6, vol. B, 1990, p. 243-320.

5. Huet G., Lévy J.-J. Computations in Orthogonal Rewriting Systems. In Computational Logic, Essays in Honour of Alan Robinson, ed. by J.-L. Lassez and G. Plotkin, MIT Press, 1991.

6. Khasidashvili Z. The Church-Rosser theorem in Orthogonal Combinatory Reduction Systems. INRIA Report 1825, 1992.

7. Khasidashvili Z. Optimal normalization in orthogonal term rewriting systems. In: Proc. of the fifth International Conference on Rewriting Techniques and Applications, Springer LNCS, vol. 690, C. Kirchner, ed. Montreal, 1993, p. 243-258.

8. Khasidashvili Z. Perpetuality and strong normalization in orthogonal term rewriting systems. CWI report CS-R9345, 1993. To appear in: Proc. of 11-th Symposium on Theoretical Aspects of Computer Science, Springer LNCS, Caen, 1994.

9. Khasidashvili Z. Higher order recursive program schemes are Turing incomplete. CWI report CS-R9348, 1993.

10. Khasidashvili Z. Perpetual reductions in orthogonal combinatory reduction systems. CWI report CS-R9349, 1993.

11. Klop J. W. Combinatory Reduction Systems. Mathematical Centre Tracts n.127, CWI, Amsterdam, 1980.

12. Klop J. W. Term Rewriting Systems. In: S. Abramsky, D. Gabbay, and T. Maibaum eds. Handbook of Logic in Computer Science, vol. II, Oxford University Press, 1992, p. 1-116.

13. 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.

14. Lévy J.-J. Optimal Reduction in the Lambda-Calculus. In: To H. B. Curry Essays on Combinatory Logic, Lambda Calculus and Formalism, J. P. Seldin and J. R. Hindley eds, Academic Press, 1980.

15. Maranget L. “La stratégie paresseuse”, These de l’Université’ de Paris VII, 1992.

16. Pkhakadze Sh. Some problems of the Notation Theory (in Russian). Proceedings of I. Vekua Institute of Applied Mathematics of Tbilisi State University, 1977.

This article was processed using the LaTEX macro package with LLNCS style