Strong Normalization of Typeable Rewrite Systems

Steffen van Bakel^{1}^{⋆} and Maribel Fernández^{2}

1 Afdeling Informatica, Universiteit Nijmegen, Toernooiveld 1, 6525 ED Nijmegen, Nederland. steffen@cs.kun.nl

2 LRI Bât. 490, CNRS / Université de Paris-Sud, 91405 Orsay Cedex, France. maribel@lri.fr

Abstract. This paper studies termination properties of rewrite systems that are typeable using intersection types. It introduces a notion of partial type assignment on Curryfied Term Rewrite Systems, that consists of assigning intersection types to function symbols, and specifying the way in which types can be assigned to nodes and edges between nodes in the tree representation of terms. Using a more liberal approach to recursion, a general scheme for recursive definitions is presented, that generalizes primitive recursion, but has full Turing-machine computational power. It will be proved that, for all systems that satisfy this scheme, every typeable term is strongly normalizable.

Introduction

Most functional programming languages, like Miranda [23] or ML [19] for instance, although implemented through an extended Lambda Calculus (LC) or a combinator system, allow programmers to specify an algorithm (function) as a set of equations using pattern-matching, i.e. the formal parameter of a function is allowed to have structure. Functional programs can then be seen as Term Rewriting Systems (TRS). Because of the underlying formalism, however, formal notions as type assignment (and other abstract interpretations) are studied in LC rather than on the level of the term rewriting language; the type assignment systems incorporated in most functional languages are in fact extensions of type assignment systems for LC.

It may seem straightforward to generalize formal systems defined on LC to the (significantly larger) world of TRS, but it is not evident that those ported systems have still all the properties they possessed in the world of LC. For example, type assignment in TRS in general does not satisfy the subject reduction property, i.e. types are not preserved under rewriting, as illustrated in [4]. Also, as argued in [2], not every notion of type assignment for LC can be used for TRS, and vice versa.

To study the problem of termination a notion of types can be of significant value. For LC, there exists a well understood and well defined notion of type assignment, known as the Curry Type Assignment System [11] which expresses abstraction and

⋆ Supported by the Netherlands Organisation for the advancement of pure research (N.W.O.).

application, and it can be shown that, for this notion of type assignment, all typeable terms are strongly normalizable. Curry’s system forms the basis for a number of notions of type assignment used in functional programming, like for example the ones used in ML, and Miranda. In [9] the Intersection Type Discipline (the BCDsystem) for LC is presented, which is a very powerful extension of Curry’s system: it is closed under β-equality. Moreover, the set of terms having a head-normal form, the set of terms having a normal form, and the set of strongly normalizable terms can all be characterized by the set of assignable types. Because of this power, type assignment in this system is undecidable. In [1] a system is studied that is a variant of the BCD-system: also in this system type assignment is undecidable. That paper also contains a proof, using a Computability Predicate [22], of the statement that all typeable terms are strongly normalizable; also the converse holds.

In this paper we study the problem of termination of functional programs. Instead of studying the problem of termination using types in the world of LC, the approach taken will be to study the desired property directly on the level of a programming language with patterns, i.e. in the world of TRS. For this purpose, we introduce a notion of type assignment on Curryfied TRS (CTRS) that uses intersection types. CTRS are defined as a slight extension of the first order TRS defined in [12], in that functional types are allowed. They are restrictions of the Applicative TRS (ATRS) as defined in [4], in that the role of Ap in the left-hand side is restricted further.

In the past the role of types in TRS has been studied within the framework of first-order sorted rewrite systems [12], as used in the underlying model for the language OBJ (see e.g. [14]). For notions of type assignment that use the sorted approach, an enumerable collection of sorts is defined, and it is assumed that every F with arity n has a type s_{1}×⋯×s_{n}→s_{n+1}, where s_{1}, …, s_{n+1} are sorts; functional types are not allowed. This implies that, by definition, there are sorts s_{1}, s_{2} and s_{3} such that (the binary operator) Ap has type s_{1}×s_{2}→s_{3}.

The disadvantage of this approach is, however, that the collection of typeable rewrite rules is very restricted. For example, the rewrite rules that correspond to Combinatory Logic,

Ap (Ap (Ap (S, x), y), z) → Ap (Ap (x, z), Ap (y, z))
Ap (Ap (K, x), y) → x
Ap (I, x) → x.

cannot be typed using the types associated to the lambda term that correspond to the combinators S, K, and I.

The notion of type assignment presented in this paper combines the approach taken in those many-sorted, first-order rewrite systems, with the one commonly used for type assignment in LC (normally defined by presenting derivation rules). First of all, by introducing Ap next to other function symbols, we are able to express partial applications of those symbols. Secondly, using for Ap the type implicitly used in the derivation rule (→E), as defined in type assignment systems for LC,

M:σ→τ  N:σ (→E):  MN:τ

i.e. (σ→τ)×σ→τ – or, in a Curryfied notation, (σ→τ)→σ→τ – invokes the possibility to assign arrow-types to all objects: we consider higher order types.

Our type assignment system is partial in the sense of [20]: we will assume that every function symbol already has a type (given in an environment), whose structure is usually motivated by a rewrite rule. In fact, the approach we take here is very much the same as the one taken by Hindley in [16], where he defines the principal Curry-type scheme of an object in Combinatory Logic. Even this notion of type assignment could be regarded as a partial one.

In [6] another partial type assignment system for higher-order rewrite systems that uses intersection types is defined. It differs from ours in that function symbols are strongly-typed with sorts only, whereas we allow for types to contain typevariables as well, and in this way we can model polymorphism (by allowing for the replacement of type-variables in types by other types).

In [4] and [2] two partial intersection type assignment systems for ATRS are presented. Apart from the difference in the syntactic definition, the system we present here is a restriction of the first one, mainly because we do not consider the typeconstant ω. The second system is a decidable restriction of the one presented here; the restriction lies in the structure of types.

Unlike typeable terms in LC, typeable terms in CTRS need not be strongly normalizable (consider a typeable term t and a rule t → t). In order to ensure strong normalization of typeable terms in CTRS we will impose some syntactical restrictions on the rewrite rules: we will present a general scheme for recursive definitions that generalizes primitive recursion. This kind of recursive definition was presented by Jouannaud and Okada in [17] for the incremental definition of higher order functionals based on first order definitions, so that the whole system is terminating. The general scheme of [17] was also used in [6] and [7] for defining higher order functions compatible with different lambda calculi.

We will prove (using the well-known method of Computability Predicates [15], [22]) that for all typeable CTRS satisfying this scheme, every typeable term is strongly normalizable.

In Sect. 1 we define CTRS. The type assignment system is presented in Sect. 2. In Sect. 3 we introduce the general scheme and we prove that typeable systems satisfying this scheme are strongly normalizing on typeable terms. Section 4 contains the conclusions.

1 Preliminaries

We assume the reader to be familiar with LC [8], and refer to the papers [9], [1], and [3] for an overview of intersection type assignment. For full definitions of rewrite systems we refer to [18] and [12]. Typeability of lambda terms in the system as presented in [4] is denoted in this paper by the symbol ⊢_{λ∩}, and by ⊢_{λ∩−ω} typeability in the system that is obtained from that one by removing the type-constant ω completely.

The intersection type assignment system for LC satisfies the following properties:

Theorem 1. 1. B ⊢_{λ∩} M:σ & M =_{β} N ⇒ B ⊢_{λ∩} N:σ.

2. ∃ B, σ [B ⊢_{λ∩} M:σ & B, σ ω-free] ⟺ M has a normal form.

3. ∃ B, σ [B ⊢_{λ∩} M:σ & σ ≠ ω] ⟺ M has a head normal form.

4. ∃ B, σ [B ⊢_{λ∩−ω} M:σ] ⟺ M is strongly normalizable.

1.1 Curryfied Term Rewriting Systems

In this subsection we will present Curryfied Term Rewriting Systems as an extension of first-order TRS ([18], [12]) that allow partial application of function symbols. It is easy to see that the systems presented here are equivalent to another popular way to write TRS, i.e. as the pure applicative systems, that contain only one function symbol (an implicit application that is normally omitted when writing terms and rules). In view of this equivalence, we have chosen to develop theory and results in the first-order setting. The language of our systems is first-order, and we add the binary operator Ap rather that restricting us to systems with only that function symbol.

CTRS are also an extension of the function constructor systems used in most functional programming languages. In function constructor systems the collection of function symbols is divided in two categories: constructor symbols that, given sufficient data of the right kind, create an object of a specific algebraic data-type, and function symbols that specify arbitrary operations; and in rewrite rules, function symbols are not allowed to occur in patterns, and constructor symbols can not occur at the left-most, outermost position of the left-hand side.

The systems proposed here do not discriminate in this way. The extension we made consists of allowing for not only constructor symbols in the operand space of the left-hand side of rewrite rules, but all function symbols.

Definition 2. An alphabet or signature Σ consists of:

1. A countable infinite set X of variables x_{1}, x_{2}, x_{3}, … (or x, y, z, x′, y′, …).

2. A non-empty set F of function symbols F, G, …, each with an ‘arity’.

3. A special binary operator, called application (Ap).

Definition 3. The set T (F, X) of terms (or expressions) is defined inductively:

1. X ⊆ T (F, X).

2. If F ∈ F ∪ {Ap} is an n-ary symbol (n ≥ 0), and t_{1}, …, t_{n} ∈ T (F, X), then F (t_{1}, …, t_{n}) ∈ T (F, X).

Definition 4. A replacement R is a map from T (F, X) to T (F, X) satisfying

R(F (t_{1}, …, t_{n})) = F (R(t_{1}), …, R(t_{n})) .

So, R is determined by its restriction to the set of variables, and sometimes we will use the notation {x_{1} ↦ t_{1}, …, x_{n} ↦ t_{n}} to denote a replacement. We also write t^{R} instead of R(t).

Definition 5. 1. A rewrite rule is a pair (l, r) of terms in T (F, X); we write r : l → r. Three conditions will be imposed:

(a) l is not a variable.

(b) The variables occurring in r are contained in l.

(c) If Ap occurs l, then r is of the shape:

Ap (F_{i} (x_{1}, …, x_{i}), x_{i+1}) → F_{i+1} (x_{1}, …, x_{i+1}).

2. For every rewrite rule with left-hand side F (t_{1}, …, t_{n}) there are n additional rewrite rules:

Ap (F_{n−1} (x_{1}, …, x_{n−1}), x_{n}) → F (x_{1}, …, x_{n}),

⋮

Ap (F_{0}, x_{1}) → F_{1} (x_{1}).

3. A rewrite rule r : l → r determines a set of rewrites l^{R} → r^{R} for all replacements R. The left hand side l^{R} is called a redex; it may be replaced by its ‘contractum’ r^{R} inside a context C[ ]; this gives rise to rewrite steps:

C[ l^{R} ] →_{r} C[ r^{R} ].

4. We call →_{r} the one-step rewrite relation generated by r. Concatenating rewrite steps we have (possibly infinite) rewrite sequences t_{0} → t_{1} → t_{2} → ⋯ (or derivations for short). If t_{0} → ⋯ → t_{n}, we write t_{0} →^{∗} t_{n}.

5. We write t →_{R} t′, if there is a r ∈ R such that t →_{r} t′.

The added rules in part 2 with F_{n−1}, …, F_{1}, F_{0}, etc. give the ‘Curried’-versions of F, and the rewrite systems are called Curry-closed. When presenting a rewrite system, however, we will only show the rules that are essential; we will not show the rules that define the Curried versions.

Definition 6. A Curryfied Term Rewriting System (CTRS) is a pair (Σ, R) of an alphabet Σ and a set R of rewrite rules.

We take the view that in a rewrite rule a certain symbol is defined; it is this symbol to which the structure of the rewrite rule gives a type.

Definition 7. In a rewrite rule r, the leftmost, outermost symbol in the left hand side that is not an Ap, is called the defined symbol of r. Then r defines F, and F is a defined symbol. Q ∈ F is called a constant symbol, if there is no rewrite rule that defines Q.

We can draw the dependency-graph of the defined function-symbols, i.e. we can construct a graph whose nodes are labeled by the defined symbols of the rewrite rules, and draw an edge going from F to G if G occurs in the right hand side of one of the rules that define F. Then in that graph cycles can occur, like for the rewrite rules

F (x) → G (x) G (x) → F (x).

We will call a defined symbol F a recursive symbol if F occurs on a cycle in the dependency-graph, and call every rewrite rule that defines F recursive. All functionsymbols that occur on one cycle in the dependency-graph depend on each other and are, therefore, defined simultaneously, so we are in fact forced to give a different notion of defined symbol; the two rewrite rules above are called mutually recursive, and both define the symbols F and G.

It is always possible to introduce tupels into the language, and solve the problem of mutual recursion using them, so without loss of generality, we will assume that rules are not mutually recursive.

Definition 8. A TRS whose dependency-graph is acyclic is called a hierarchical TRS. The rewrite rules of a hierarchical TRS can be regrouped in such a way that they are incremental definitions of the defined symbols F^{1}, …, F^{k}, so that the rules defining F^{i} only depend on F^{1}, …, F^{i−1}.

Example 1. Our definition of recursive symbols, using the notion of defined symbols, is different from the one normally considered. Since Ap is never a defined symbol, the following rewrite system

D (x) → Ap (x, x) Ap (D_{0}, x) → D (x)

– or, equivalently, Ap (D, x) → Ap (x, x) – is not considered a recursive system. Notice that, for example, the term D (D_{0}) (or Ap (D, D)) has no normal form (these terms play the role of (λx.xx)(λx.xx) in LC). This means that, in the formalism of this paper, there exist non-recursive first-order rewrite systems that are not normalizable.

Definition 9. Applicative Combinatory Logic (ACL) is the CTRS (Σ, R), where F = {S, S_{2}, S_{1}, S_{0}, K, K_{1}, K_{0}, I, I_{0}}, and R contains the rewrite rules

S (x, y, z) → Ap (Ap (x, z), Ap (y, z))

K (x, y) → x I (x) → x

Because ACL is Curry-closed, it is in fact combinatory complete: every lambda term can be translated into a term in ACL; for details of such a translation, see [8, 13].

2 Type assignment in CTRS

The set of types that will be used in the remainder of this paper is a subset of the one used in [4]: since we are going to use types to study strong normalization, we will not consider the type constant ω. This means that the system we present here is a subsystem of that of [4], and, in particular, no properties proved there are automatically ‘inherited’.

Definition 10. 1. T_{−ω}, the set of strict types, is inductively defined by: (a) All type-variables φ_{0}, φ_{1}, … ∈ T_{−ω}.

(b) If τ, σ_{1}, …, σ_{n} ∈ T_{−ω} (n ≥ 1), then σ_{1}∩⋯∩σ_{n}→τ ∈ T_{−ω}.

2. T_{∩}, the set of strict intersection types, is defined by: If σ_{1}, …, σ_{n} ∈ T_{−ω} (n ≥ 1), then σ_{1}∩⋯∩σ_{n} ∈ T_{∩}.

3. On T_{∩}, the relation ≤_{∩} is defined by:

(a) ∀ 1 ≤ i ≤ n (n ≥ 1) [σ_{1}∩⋯∩σ_{n} ≤_{∩} σ_{i}].

(b) ∀ 1 ≤ i ≤ n (n ≥ 1) [σ ≤_{∩} σ_{i}] ⇒ σ ≤_{∩} σ_{1}∩⋯∩σ_{n}.

(c) σ ≤_{∩} τ ≤_{∩} ρ ⇒ σ ≤_{∩} ρ.

4. On T_{∩}, the relation ∼_{∩} is defined by:

(a) σ ≤_{∩} τ ≤_{∩} σ ⇒ σ ∼_{∩} τ.

(b) ρ ∼_{∩} σ & τ ∼_{∩} μ ⇒ σ→τ ∼_{∩} ρ→μ. T_{∩} may be considered modulo ∼_{∩} . Then ≤_{∩} becomes a partial order, and in this paper we consider types modulo ∼_{∩} .

Unless stated otherwise, if σ_{1}∩⋯∩σ_{n} is used to denote a type, then by convention all σ_{1}, …, σ_{n} are assumed to be strict. Notice that T_{−ω} is a proper subset of T_{∩}. The notion of type assignment as presented in [2] is a (decidable) restriction of the one presented in this paper (and of the one presented in [4]). Decidability is, in that paper, achieved by limiting the structure of types, by requiring that in σ_{1}∩⋯∩σ_{n}→τ, the types σ_{1}, …, σ_{n} do not contain intersections.

Definition 11. 1. A statement is an expression t:σ, with t ∈ T (F, X) and σ ∈ T_{∩}. t

is the subject and σ the predicate of t:σ.

2. If B is a basis and σ ∈ T_{S}, then T_{⟨B,σ⟩} is the set of all strict subtypes occurring in the pair ⟨B, σ⟩.

3. If B_{1}, …, B_{n} are bases, then Π{B_{1}, …, B_{n}} is the basis defined as follows: x:σ_{1}∩⋯∩σ_{m} ∈ Π{B_{1}, …, B_{n}} if and only if {x:σ_{1}, …, x:σ_{m}} is the set of all statements whose subject is x that occur in B_{1} ∪ … ∪ B_{n}.

Notice that if n = 0, then Π{B_{1}, …, B_{n}} = ∅.

2.1 Operations on pairs

In this subsection we present two different operations on pairs of ⟨basis, type⟩, namely substitution and expansion, that are variants of similar definitions given in [4, 5, 3]. The operation of substitution deals with the replacement of type-variables by types and is the one normally used. The operation of expansion replaces types by the intersection of a number of copies of that type and coincides with the one given in [10, 21].

Definition 12. 1. The substitution (φ ↦ α) : T_{∩} → T_{∩}, where φ is a type-variable and α ∈ T_{−ω}, is defined by:

(a) (φ ↦ α) (φ) = α.

(b) (φ ↦ α) (φ′) = φ′, if φ ≢ φ′.

(c) (φ ↦ α) (σ→τ) = (φ ↦ α) (σ) → (φ ↦ α) (τ).

(d) (φ ↦ α) (σ_{1}∩⋯∩σ_{n}) = (φ ↦ α) (σ_{1}) ∩⋯∩ (φ ↦ α) (σ_{n}).

2. If S_{1}, S_{2} are substitutions, then so is S_{1}∘S_{2}, where S_{1}∘S_{2} (σ) = S_{1} (S_{2} (σ)).

The operation of expansion is an operation on types that deals with the replacement of (sub)types by an intersection of a number of copies of that type. In this process, it can be that also other types need to be copied. An expansion indicates not only the type to be expanded, but also the number of copies that has to be generated.

Definition 13. The last type-variable of a strict type is defined by:

1. The last type-variable of φ is φ.

2. The last type-variable of σ_{1}∩⋯∩σ_{n}→τ is the last type-variable of τ.

Definition 14. For every μ ∈ T_{−ω}, n ≥ 2, basis B and σ ∈ T_{∩}, the quadruple ⟨μ, n, B, σ⟩ determines an expansion E_{⟨μ,n,B,σ⟩} : T_{∩} → T_{∩}, that is constructed as follows.

1. The set of type-variables V_{μ}(⟨B, σ⟩) is constructed by:

(a) If φ occurs in μ, then φ ∈ V_{μ}(⟨B, σ⟩).

(b) If the last type-variable of τ ∈ T_{⟨B,σ⟩} is in V_{μ}(⟨B, σ⟩), then all type-variables

that occur in τ are in V_{μ}(⟨B, σ⟩).

2. Suppose V_{μ}(⟨B, σ⟩) = {φ_{1}, …, φ_{m}}. Choose m × n different type-variables φ_{1}^{1}, …, φ_{1}^{n}, …, φ_{m}^{1}, …, φ_{m}^{n}, such that each φ_{i}^{j} (1 ≤ i ≤ m,1 ≤ j ≤ n) does not occur in ⟨B, σ⟩. Let S_{i} = (φ_{1} ↦ φ_{1}^{i})∘⋯∘(φ_{m} ↦ φ_{m}^{i}).

3. Let α ∈ T_{∩}. E_{⟨μ,n,B,σ⟩} (α) is obtained by traversing α top-down and replacing, in α, a subtype β which last type-variable is an element of V_{μ}(⟨B, σ⟩), by S_{1} (β) ∩⋯∩S_{n} (β).

Both operations are, in a natural way, extended into operations that are also defined on bases and pairs of basis and type.

For these operations, the following properties hold:

Lemma 15. Let S be a substitution, and E = E_{⟨μ,n,B,σ⟩} an expansion.

1. If τ ≤_{∩} ρ, then S (τ) ≤_{∩} S (ρ), and E (τ) ≤_{∩} E (ρ).

2. If B ≤_{∩} B′, then S (B) ≤_{∩} S (B′), and E (B′) ≤_{∩} E (B′′).

3. If τ ∈ T_{⟨B,σ⟩}, then either: E (τ) = τ_{1}∩⋯∩τ_{n} where for every 1 ≤ i ≤ n, τ_{i} is a trivial variant of τ, or E (τ) ∈ T_{−ω}.

4. E (Π{B_{1}, …, B_{n}}) = Π{E (B_{1}), …, E (B_{n})}.

Definition 16. A chain is an object <O_{1}, …, O_{n}>, with each O_{i} an operation of substitution or expansion, such that:

<O_{1}, …, O_{n}> (⟨B, σ⟩) = O_{n} (⋯(O_{1} (⟨B, σ⟩))⋯).

2.2 Type assignment

The notion of type assignment on CTRS will in fact be defined on the treerepresentation of terms and rewrite rules of these systems.

Definition 17. 1. The tree-representation of terms and rewrite rules is obtained in a straightforward way by representing a term F (t_{1}, …, t_{n}) by:

[figure: F; t_{1}; t_{n}; ⋯]

The spine of a term-tree is defined as usual, i.e. the root node of the term-tree is on the spine, and if a node is on the spine, then its left most descendent is on the spine. The first node on the spine of the left hand side (starting from the root node) that does not contain an Ap is called the defining node of that rule. The edge pointing to the the root of a term is called the root edge, and a node containing a term-variable (a function symbol F ∈ F, the symbol Ap) will be called a variable node (function node, application node). Notice that if F is the defined symbol of the rule, then it occurs in the defining node.

2. Subterms can be numbered by positions, which are sequences of natural numbers denoting the path from the root of the term to the root of the subterms. The letters p and q stand for positions. The empty sequence (root position) is denoted by Λ. The subterm of t at position p is denoted by t|_{p} and t[u]_{p} is the result of replacing the subterm of t at position p by u.

Partial intersection type assignment on a CTRS (Σ, R) is defined as the labelling of nodes and edges in the tree-representation of terms and rewrite rules with types in T_{∩}. In this labelling, we use a mapping that provides a type in T_{−ω} for every F ∈ F ∪ {Ap}. Such a mapping is called an environment.

Definition 18. Let (Σ, R) be a CTRS.

1. An environment E : F ∪ {Ap} → T_{−ω} is such that for every F ∈ F with arity n, E (F) = E (F_{n−1}) = ⋯ = E(F_{0}), and E(Ap) = (φ_{1}→φ_{2})→φ_{1}→φ_{2}.

2. For F ∈ F with arity n ≥ 0, σ ∈ T_{−ω}, and E an environment, the environment

E[F := σ] is defined by:

E[F := σ] (G) = σ, if G ∈ {F, F_{n−1}, …, F_{0}},

E[F := σ] (G) = E (G), otherwise.

Type assignment on CTRS is defined in two stages. In the next definition we define type assignment on terms, in Def.22 we define type assignment on term rewrite rules.

Definition 19. Let (Σ, R) be a CTRS, and E an environment.

1. We say that t ∈ T (F, X) is typeable by σ ∈ T_{∩} with respect to E, if there exists an assignment of types to edges and nodes that satisfies the following constraints:

(a) The root edge of t is typed with σ.

(b) The type assigned to a function node containing F ∈ F ∪ {Ap} (where F has arity n ≥ 0) is τ_{1}∩⋯∩τ_{m}, if and only if, for every 1 ≤ i ≤ m, there are σ_{1}^{i}, …, σ_{n}^{i} ∈ T_{∩}, and σ_{i} ∈ T_{−ω}, such that τ_{i} = σ_{1}^{i}→⋯→σ_{n}^{i}→σ_{i}, the type assigned to the j-th (1 ≤ j ≤ n) out-going edge is σ_{j}^{1}∩⋯∩σ_{j}^{m}, and the type assigned to the incoming edge is σ_{1}∩⋯∩σ_{m}.

[figure: σ_{1}∩⋯∩σ_{m}; F:(σ_{1}^{1}→⋯→σ_{n}^{1}→σ_{1}) ∩⋯∩ (σ_{1}^{m}→⋯→σ_{n}^{m}→σ_{m}); σ_{1}^{1}∩⋯∩σ_{1}^{m}; σ_{2}^{1}∩⋯∩σ_{2}^{m}; σ_{n−1}^{1}∩⋯∩σ_{n−1}^{m}; σ_{n}^{1}∩⋯∩σ_{n}^{m}; …]

(c) If the type assigned to a function node containing F ∈ F ∪ {Ap} is τ, then

there is a chain C, such that C (E (F)) = τ.

2. Let t ∈ T (F, X) be typeable by σ with respect to E. If B is a basis such that for every statement x:τ occurring in the typed term-tree there is a x:τ′ ∈ B such that τ′ ≤_{∩} τ, we write B ⊢_{E} t:σ.

Notice that if B ⊢_{E} t:σ, then B can contain more statements than needed to obtain t:σ.

The use of an environment and part 1c of Def.19 introduce a notion of polymorphism into our type assignment system. The environment returns the ‘principal type’ for a function symbol; this symbol can be used with types that are ‘instances’ of its principal type.

A typical example for part 1b of Def.19 is the symbol Ap; for every occurrence of Ap in a term-tree, there are σ_{1}, …, σ_{n} and τ_{1}, …, τ_{n} such that the following is part of the term-tree.

[figure: τ_{1}∩⋯∩τ_{n}; Ap: ((σ_{1}→τ_{1})→σ_{1}→τ_{1})∩⋯∩((σ_{n}→τ_{n})→σ_{n}→τ_{n}); (σ_{1}→τ_{1})∩⋯∩(σ_{n}→τ_{n}); σ_{1}∩⋯∩σ_{n}]

Example 2. The term S (K_{0}, S_{0}, I_{0}) can be typed with the type σ→σ, under the assumption that: E (S) = (1→2→3)→(4→2)→1∩4→3, E (K) = 5→6→5, and E (I) = 7→7.

[figure: σ→σ; S:((σ→σ)→((τ→ρ)→(ρ→μ)∩τ→μ)→σ→σ) →; (((ρ→μ)→ρ→μ)→(τ→ρ)→(ρ→μ)∩τ→μ) →; (σ→σ)∩((ρ→μ)→ρ→μ) → σ→σ; K_{0}:(σ→σ)→((τ→ρ)→(ρ→μ)∩τ→μ)→σ→σ; S_{0}:((ρ→μ)→ρ→μ)→(τ→ρ)→(ρ→μ)∩τ→μ; I_{0}:(σ→σ)∩((ρ→μ)→ρ→μ)]

Notice that to obtain the type for S in the root-node, we have used the chain <(1 ↦ σ→σ), (2 ↦ (τ→ρ)→(ρ→μ)∩τ→μ), (3 ↦ σ→σ), (4 ↦ (ρ→μ)→ρ→μ)>. Notice, moreover, that to obtain the type for I_{0}, an expansion is needed.

If we define D (x) → Ap (x, x), then we can even check that for example D (S (K_{0}, S_{0}, I_{0})) and D (I_{0}) are both typeable by σ→σ.

The here defined notion of type assignment satisfies the following properties:

Lemma 20. 1. B ⊢_{E} t:σ_{1}∩⋯∩σ_{n} ⟺ ∀ 1 ≤ i ≤ n [B ⊢_{E} t:σ_{i}].

2. B ⊢_{E} t:σ & σ ≤_{∩} τ ⇒ B ⊢_{E} t:τ.

3. B ⊢_{E} F_{n} (t_{1}, …, t_{n}):σ & σ ∈ T_{−ω} ⇒ ∃ α ∈ T_{∩}, β ∈ T_{−ω} [σ = α→β].

4. Π{B,{x:α}} ⊢_{E} Ap (t, x):β & x does not occur in B ⇒ B ⊢_{E} t:α→β.

By Def.5, if a term t is rewritten to the term t′ using the rewrite rule l → r, there is a subterm t_{0} of t, and a replacement R, such that l^{R} = t_{0}, and t′ is obtained by replacing t_{0} by r^{R}. The subject reduction property for this notion of reduction is: If B ⊢_{E} t:σ, and t can be rewritten to t′, then B ⊢_{E} t′:σ.

To ensure the subject reduction property, as in [4], type assignment on rewrite rules will be defined using the notion of principal pair for a typeable term.

Definition 21. Let t ∈ T (F, X). A pair ⟨P, π⟩ is called a principal pair for t with respect to E, if P ⊢_{E} t:π and for every B, σ such that B ⊢_{E} t:σ there is a chain C such that C (⟨P, π⟩) = ⟨B, σ⟩.

Notice that we do not show that every typeable term has a principal pair with respect to E; at the moment we cannot give a construction of such a pair for every term. But even with this non-constructive approach we can show that the condition is sufficient with respect to the subject reduction property.

Definition 22. Let (Σ, R) be a CTRS, and E an environment.

1. We say that l → r ∈ R with defined symbol F is typeable with respect to E, if there are basis P, type π ∈ T_{∩}, and an assignment of types to nodes and edges such that:

(a) ⟨P, π⟩ is a principal pair for l with respect to E, and P ⊢_{E} r:π.

(b) In P ⊢_{E} l:π and P ⊢_{E} r:π, all nodes containing F are typed with E (F).

2. We say that (Σ, R) is typeable with respect to E, if every r ∈ R is typeable with respect to E.

From now on, we will only consider CTRS that are typeable with respect to a certain environment.

Condition 1b of Def.22 is in fact added to make sure that the type provided by the environment for a function symbol F is not in conflict with the rewrite rules that define F. By restricting the type that can be assigned to the defined symbol to the type provided by the environment, we are sure that the rewrite rule is typed using that type, and not using some other type. Since by part 1b of Def.22 all occurrences of the defined symbol in a rewrite rule are typed with the same type, type assignment of rewrite rules is actually defined using Milner’s way of dealing with recursion [19].

Using the same technique as in [4], it is possible to show that subject reduction holds.

Theorem 23 Subject Reduction Theorem. If B ⊢_{E} t:σ, and t →_{R} t′, then B ⊢_{E} t′:σ.

It is possible to show that the two operations on pairs (substitution and expansion) are sound on typed term-trees, and that part 1c of Def.19 is sound in the following sense: if there is an operation O such that O (E (F)) = σ, then for every type τ ∈ T_{−ω} such that σ ≤_{∩} τ, the rewrite rules that define F are typeable with respect to the changed environment E[F := τ].

Theorem 24 Soundness of substitution. Let S be a substitution.

1. If B ⊢_{E} t:σ, then S (B) ⊢_{E} t:S (σ).

2. Let r: l → r with defined symbol F be typeable with respect to E. Then r is typeable with respect to E[F :=S (E (F))].

Theorem 25 Soundness of expansion. Let E be an expansion.

1. If B ⊢_{E} t:σ, then E (B) ⊢_{E} t:E (σ).

2. Let r: l → r with defined symbol F be typeable with respect to E. If E (E (F)) = τ ∈ T_{∩}, then for every μ ∈ T_{−ω} such that τ ≤_{∩} μ, r is typeable with respect to E[F := μ].

3 Strong Normalization and Typeability

Unlike typeable terms in ⊢_{λ∩}, typeable terms in ⊢_{E} need not be normalizable. This means that the characterization of strongly normalizable terms and strongly normalizing CTRS can not be based on type conditions only, as it is possible for LC (see [1]).

In this section we analyze the relations between typeability and strong normalization in CTRS. First we show the relation between strong normalization in CTRS and normalization in ⊢_{λ∩}; however, since the property we are characterizing is non-decidable, the condition we obtain is non-decidable as well. From a practical point of view, a decidable, sufficient (but not necessary) condition is clearly better. For this reason, in the second subsection we introduce a general scheme, inspired by [17], which imposes some syntactical restrictions on CTRS’s rules so as to guarantee the strong normalization of all typeable terms.

From now on, we will abbreviate ‘t is strongly normalizable’ by SN(t).

3.1 Strong Normalization of CTRS and Typeability in ⊢_{λ∩}

Let us consider an interpreter of CTRS, i.e. a program such that, given a term t and a CTRS (Σ, R), returns the set {t’ | t →_{R} t’} (the empty set if t is a normal form for (Σ, R)). In fact, we will consider a generalized interpreter P, which takes a set I of terms and a CTRS (Σ, R) as input and returns the set ⋃_{t∈I} {t’ | t →_{r} t’} (the empty set if I is a set of normal forms for (Σ, R)). We assume that the inputs and the output of P are sets of strings representing terms and rewrite rules. Besides, we assume that pure LC is used to write P, that is, P is a λ-term that will be applied to sets of strings (also coded in LC). We will use the symbol t for both the term in CTRS and its interpretation in LC. Then the λ-term P R t has a β-normal form which represents the set of one-step reducts of t (with respect to (Σ, R)).

The following property will be used to characterize strongly normalizable terms and CTRS:

Property 26. Let (Σ, R) be a CTRS, and let us denote by P^{n}R t the term (P R (P R⋯(P R t)⋯)), with n times P.

1. SN_{R} (t) ⟺ ∃ n ≥ 0 [P^{n}R t =_{β} ∅],

2. SN ((Σ, R)) ⟺ ∀ t ∈ T (F, X) [SN_{R} (t)].

Given t and (Σ, R), we can obtain any t′ such that t →_{R}^{∗} t’ using a program P^{∗} (also in pure LC) that applies P a number of times. By definition, the result of applying P^{∗} to (Σ, R) and t is the set of strings {t’ | t →_{R}^{∗} t’}.

Since β-reduction is confluent, property 26 can be reformulated in this way: For any strongly normalizable term t in a CTRS (Σ, R), the λ-term P^{∗}Rt has a βnormal form. A CTRS (Σ, R) is strongly normalizing if for all t the term P^{∗}Rt has a β-normal form. Therefore, using Thm.1 we can characterize strongly normalizable terms and strongly normalizing systems using ⊢_{λ∩}:

Property 27. Let (Σ, R) be a CTRS.

1. SN_{R} (t) ⟺ P^{∗}Rt is typeable in ⊢_{λ∩} with a type different from ω, 2. SN ((Σ, R)) ⟺ for all t, P^{∗}Rt is typeable in ⊢_{λ∩} with a type different from ω.

Note that the above results show no relation between the types assignable to a term in a CTRS, and those assignable to its interpretation in LC. In fact, Prop.27 shows only the relation between β-reduction and →_{R} , since we are implementing →_{R} by means of →_{β} .

3.2 Strong Normalization versus Typeability in CTRS

In this section we give decidable conditions for strong normalization of typeable CTRS. Since typeability alone is not sufficient, we will impose syntactic restrictions on the rules in order to get strongly normalizing systems.

We will prove that the class of typeable non-recursive CTRS is strongly normalizing. To appreciate the non-triviality of this condition, remember Ex.1: a non-recursive CTRS can be non-terminating. In fact, the main result of this section (every typeable term is strongly normalizable) shows that the term D (D_{0}) (or Ap (D, D)) is not typeable.

Theorem 28. If R contains no recursive rule and is typeable in ⊢_{E} , then any typeable term is strongly normalizable with respect to R.

The converse of this theorem does not hold. However, the restriction to nonrecursive systems is too strong indeed. In the following we will show that there is class of recursive functions that are safe: generalized primitive recursive functions satisfying the general scheme below. This scheme for definitions is inspired by [17] where generalized primitive recursive definitions were shown strongly normalizing when combined with typed LC. The same results were shown in [6] in the context of type assignment systems for LC and in [7] for typed LC of order ω.

Definition 29. Let F_{n} = C ∪ {Ap} ∪ {F^{1}, …, F^{n}}, where F^{1}, …, F^{n} are the defined symbols of the signature, that are not Curried-versions, and assume that F^{1}, …, F^{n} are defined in an incremental way. Suppose, moreover, that the rules defining F^{1}, …, F^{n} satisfy the general scheme:

F^{i} (C^{→}[x^{→}], y^{→}) → C′[F^{i} (C_{1}^{→}[x^{→}], y^{→}), …, F^{i} (C_{m}^{→}[x^{→}], y^{→}), x^{→}, y^{→}],

where x^{→}, y^{→} are sequences of variables, and x^{→} ⊆ y^{→}. Also, C^{→}[ ], C’[ ], C_{1}^{→}[ ], and C_{m}^{→}[ ] are sequences of contexts in T (F_{i−1}, X), and, for 1 ≤ j ≤ m, C^{→}[x^{→}] >_{mul} C_{j}^{→}[x^{→}] (where < is the strict subterm ordering and mul denotes multiset extension).

The rules defining F^{1}, …, F^{n} and their Curry-closure together form a safe recursive system.

This general scheme imposes some restrictions on the definition of functions: the terms in every C_{j}^{→}[x^{→}] are subterms of terms in C^{→}[x^{→}] (this is the ‘primitive recursive’ aspect of the scheme), and the variables x^{→} must also appear as arguments in the left-hand side of the rule.

It is worthwhile noting that the rewrite rules of Def. 9 are not recursive, so, in particular, satisfy the scheme. Therefore, although the severe restriction imposed on rewrite rules, the systems satisfying the scheme still have full Turing-machine computational power, a property that systems without Ap would not possess.

Example 3. The following rewrite system satisfies the general scheme:

Add (Zero, y) → y

Add (Succ (x), y) → Succ (Add (x, y))

Mul (Zero, y) → Zero

Mul (Succ (x), y) → Add (Mul (x, y), y)

Fac (Zero) → Succ (Zero)

Fac (Succ (x)) → Mul (Succ (x),Fac (x))

Note that if we extend the definition of Add with the rule that expresses the associativity of Add,

Add (Add (x, y), z) → Add (x,Add (y, z))

the rewrite system is no longer safe.

Theorem 28 is actually a corollary of the Strong Normalization Theorem (Thm.35). To prove this theorem, we will use the well-known method of Computability Predicates ([15], [22]). The proof will have two parts; in the first one we give the definition of a predicate Comp on bases, terms, and types, and prove some properties of Comp. The most important one states that if for a term t there are a basis B and type σ such that Comp (B, t, σ) holds, then t is strongly normalizable. In the second part Comp is shown to hold for each typeable term.

Definition 30. 1. Let B be a basis, t a term, and σ a type, such that B ⊢_{E} t:σ. We define the Computability Predicate Comp (B, t, σ) by induction on σ:

(a) Comp (B, t, φ) ⟺ SN(t).

(b) Comp (B, t, σ→τ) ⟺ ∀ u ∈ T (F, X) [Comp (B’, u, σ) ⇒ Comp (Π{B,B’}, Ap (t, u), τ)].

(c) Comp (B, t, σ_{1}∩⋯∩σ_{n}) ⟺ ∀ 1 ≤ i ≤ n [Comp (B, t, σ_{i})].

2. We say that t is computable if there exist B, σ such that Comp (B, t, σ).

3. R is computable in B ⟺ ∃ B’ [∀ x:σ ∈ B [Comp (B’, x^{R}, σ)]].

Notice that because we use intersection types, and because of Def.11:3, in part 3 we need not consider the existence of different bases for each x:σ ∈ B.

Definition 31. A term is neutral if it is not of the form F_{n}(t_{1}, …, t_{n}) where F_{n} is a ‘Curried’-version of some defined symbol F.

Property 32. Comp satisfies the standard properties of computability predicates:

1. C1. Comp (B, t, σ) ⇒ SN(t).

2. C2. If Comp (B, t, σ), and t →^{∗} t′, then Comp (B, t′, σ).

3. C3. If t is neutral, B ⊢_{E} t:σ for some B, σ, and for all v such that t →_{R} v, Comp (B, v, σ) holds, then also Comp (B, t, σ) holds.

Proof: By induction on the structure of types.

1. σ = φ.

C1. By Def.30:1a.

C2. By Def.30:1a, using Thm. 23 and Lem. 20.

C3. By Def.30:1a, SN(v). Then SN(t) and again by 30:1a Comp (B, t, σ).

2. σ = α→β. C1. Let u ≡ x (a new variable). x is a neutral term in normal form,

and {x:α} ⊢_{E} x:α. Then, by induction hypothesis (C3), Comp ({x:α}, x, α), and by Def.30:1b, Comp (Π{B,{x:α}}, Ap (t, x), β). By induction hypothesis, SN(Ap (t, x)), which implies SN(t).

C2. Again, let u ≡ x, then, as in the previous proof, Comp ({x:α}, x, α), and by Def.30:1b, Comp (Π{B,B’}, Ap (t, x), β). Since Ap (t, x) →^{∗} Ap (t′, x), by induction we get Comp (B, Ap (t′, x), β). Then, by Def.30:1b, Comp (B, t′, σ).

C3. Since σ = α→β, we have to prove:

∀ u ∈ T (F, X) [Comp (B’, u, α) ⇒ Comp (Π{B,B’}, Ap (t, u), β)]. Since Ap (t, u) is neutral of type β, by induction hypothesis, it is sufficient to prove that for all v′ such that Ap (t, u) →_{R} v′, Comp (Π{B,B’}, v′, β) holds. For this we apply induction on the length of the maximal derivation from u to its normal form (by Property (C1) we know that SN(u)). Base. If u is a normal form, because t is neutral Ap (t, u) reduces only inside

t, so Ap (t, u) →_{R} Ap (v, u) and Comp (B, v, σ) holds by assumption. Then,

by Def.30, Comp (Π{B,B’}, Ap (v, u), β) holds.

Induction step. Consider all possible one step reductions from Ap (t, u): In case Ap (t, u) →_{R} Ap (v, u) we proceed as before. In case Ap (t, u) →_{R} Ap (t, u′), Comp (Π{B,B’}, Ap (t, u′), β) follows by induction hypothesis. And these are all possible cases, because Ap (t, u) can not be a redex itself since t is neutral and the rewrite system is safe.

3. σ = σ_{1}∩⋯∩σ_{n}. C1. By Def.30:1c, Comp (B, t, σ) implies Comp (B, t, σ_{i}) for 1 ≤ i ≤ n, and then

by induction SN(t). C2. As in the previous proof, Comp (B, t, σ_{i}) holds for 1 ≤ i ≤ n. By induction,

for 1 ≤ i ≤ n, Comp (B, t′, σ_{i}), then, by Def.30:1c, also Comp (B, t′, σ). C3. Using Lem.20:1, we obtain B ⊢_{E} t:σ_{i}, and by theorem 23, B ⊢_{E} v:σ_{i}.

Moreover, Comp (B, v, σ) implies Comp (B, v, σ_{i}) for 1 ≤ i ≤ n. Then, by induction, Comp (B, t, σ_{i}) for 1 ≤ i ≤ n, and by Def.30:1c, Comp (B, t, σ).

In order to prove the Strong Normalization Theorem we shall prove a stronger property, for which we will need the following ordering.

Definition 33. Let (Σ, R) be a CTRS. Let >I I N denote the standard ordering on natural numbers, ·^{>} stand for the well-founded encompassment ordering, (i.e. u ·^{>} v if u ≠ v and u|_{p} = v^{R} for some position p ∈ u and replacement R), and lex, mul denote respectively the lexicographic and multiset extension of an ordering. Note that encompassment contains strict subterm.

We define the ordering ≫ on triples – consisting of a pair of natural numbers, a term, and a multiset of terms – as the object (>I I N, ·^{>}, (→_{R} ∪ >)_{mul} )_{lex} .

We will interpret the term u^{R} by the triple I(u^{R}) = <(i, j), u, {R}>, where i is the maximal super-index of the function symbols belonging to u, j is the minimum of the differences arity(F^{i}) − arity(F_{j}^{i}) such that F_{j}^{i} occurs in u, and {R} is the multiset {x^{R} | x ∈ Var (u)}. These triples are compared in the ordering ≫.

When R is computable, then by Prop. C1 every t in the image of R is strongly normalizable, so →_{R} is well-founded on the image of R. Also, because the union of the strict subterm relationship with a terminating rewrite relation is well-founded [12], the relation (→_{R} ∪ >)_{mul} is well-founded on {R}. Hence, when restricted to computable replacements, ≫ is a well-founded ordering.

We use ≫_{n} when we want to indicate that the nth element of the triple has decreased but not the n-1 first ones.

We would like to stress that we do not just interpret terms, but terms that are obtained by performing a replacement. This implies that when t^{R} = t^{′R′}, their interpretations are not necessarily equal.

We now come to the main theorem of this section, in which we show that for any typeable term and computable replacement R also the term t^{R} is computable. The strong normalization result then follows, using property C1, for any typeable term t, taking for R the identity.

In the proof, the main idea is to write a term t^{R} like t^{′R′} (so they are equal as terms), where t ·^{>} t′, and R′ is a computable extension of R. This is accomplished by taking a computable subterm v of t, to put a new variable z in its place and to define R′ = R ∪ {z ↦ v}.

Property 34. Let t be such that B ⊢_{E} t:σ, and R be computable in B. Then there is a B’ such that Comp (B’, t^{R}, σ).

Proof: By noetherian induction on ≫. Let B = {x_{1}:σ_{1}, …, x_{n}:σ_{n}}, and R = {x_{1} ↦ u_{1}, …, x_{n} ↦ u_{n}}. Because of part 1c of Def.30, we can restrict the proof to the case σ ∈ T_{−ω}.

We distinguish the cases:

1. t is a neutral term. If t is a term-variable then the thesis follows trivially since R is computable. Let t be a non-variable term, so also t^{R} is neutral. If t^{R} is irreducible, then Comp (B’, t^{R}, σ) holds by Prop.C3. Otherwise, let t^{R} →_{R} w at position p. We will prove either Comp (B’, t^{R}, σ) itself, or prove Comp (B’, w, σ) and apply Prop.C3.

(a) p = qp′, t|_{q} = x_{i} ∈ X, so the rewriting takes place in a subterm of t^{R} that is introduced by the replacement. Let z be a new term-variable. Take R′ = R ∪ {z ↦ w|_{q}}, and note that t^{R}|_{q} →_{R} w|_{q} at position p′. Since t^{R}|_{q} ∈ {R}, and R is assumed to be computable, also Comp (B, t^{R}|_{q}, σ_{i}) holds. So Comp (B, w|_{q}, σ_{i}) holds by Prop.C2, hence R′ is computable in B ∪ {z_{i}:σ_{i}}. Now, if the variable x_{i} has exactly one occurrence in t, then t = t[z]_{q} modulo renaming of term-variables, and otherwise t ·^{>} t[z]_{q}. In the first case (since R contains a term that is rewritten to get R′) we have I(t^{R}) ≫_{3} I(t[z]_{q}^{R′}), and I(t^{R}) ≫_{2} I(t[z]_{q}^{R′}) in the second case. Both cases yield, by induction, Comp (B’, t[z]_{q}^{R′}, σ) and note that t[z]_{q}^{R′} ≡ w.

(b) Now assume that p is a non-variable position in t. We analyze separatedly the cases: i. p ≠ Λ (p is not the root position). Then t ·^{>} t|_{p}, hence I(t^{R}) ≫_{2} I(t|_{p}^{R}), and t|_{p}^{R} = t^{R}|_{p}. Let τ be the type assigned to t|_{p} in the derivation of B ⊢_{E} t:σ, then Comp (B, t^{R}|_{p}, τ) holds by induction.

Let z be a new variable, and R′ = R ∪ {z ↦ t^{R}|_{p}}, then R′ is computable in

B ∪ {z:τ}, and B ∪ {z:τ} ⊢_{E} t[z]_{p}:σ. Now t ·^{>} t[z]_{p}, hence I(t^{R}) ≫_{2} I(t[z]_{p}^{R′}),

hence Comp (B, t^{R}, σ). ii. p = Λ. Then the possible cases for t are:

A. t ≡ F (t_{1}, …, t_{n}), where F is a defined symbol of arity n or F ≡ Ap and n = 2, and at least one of the t_{i} is not a variable. Take R′ = {z_{1} ↦ t_{1}^{R}, …, z_{n} ↦ t_{n}^{R}}. Since t ·^{>} t_{i}, I(t^{R}) ≫_{2} I(t_{i}^{R}). If B ⊢_{E} t_{i}:σ_{i}, then by induction Comp (B, t_{i}^{R}, σ_{i}). Hence, R′ is computable in B ∪ {z_{1}:σ_{1}, …, z_{n}:σ_{n}}. But I(t^{R}) ≫_{2} I(F (z_{1}, …, z_{n})^{R′}), and F (z_{1}, …, z_{n})^{R′} = t^{R} and B ∪ {z_{1}:σ_{1}, …, z_{n}:σ_{n}} ⊢_{E} F (z_{1}, …, z_{n}):σ. Hence Comp (B, t^{R}, σ). B. t ≡ F^{k} (z_{1}, …, z_{n}) where z_{1}, …, z_{n} are different term-variables. (If z_{i} = z_{j} for some i ≠ j, we can reason as in part (i.a).) Then t^{R} must be an instance of the left hand side of a rule defining F^{k}: t^{R} = F^{k} (z_{1}, …, z_{n})^{R} = F^{k} (C^{→}[M^{→}], N^{→}) →_{R} C’[F^{k} (C_{1}^{→}[M^{→}], N^{→}), …, F^{k} (C_{m}^{→}[M^{→}], N^{→}), M^{→}, N^{→}] = w, where C^{→}[M^{→}], N^{→} are all terms in {R}, so are computable by hypothesis. Now, we will deduce Comp (B, w, σ) in three steps: Step I. Let R′ be the replacement that maps the left-hand side of the rewrite

rule into t^{R}, so x^{R′}^{→} = M^{→}. Since M^{→} ⊆ N^{→}, and all N^{→} are computable, also R′ is computable. For every 1 ≤ j ≤ m, F^{k} does not occur in C_{j}^{→} (by definition of the general scheme), hence I(F^{k} (z_{1}, …, z_{n})^{R}) ≫_{1} I(C_{j}^{R′}), hence C_{j}^{R′} is computable.

Step II. Let, for 1 ≤ j ≤ m, R_{j} be the computable replacement such that t^{R_{j}} = F^{k} (C_{j}^{→}[x^{→}], y^{→})^{R′}. Since C^{→} >_{mul} C_{j}^{→}, and > is closed under replacement,

also C^{→}^{R′} >_{mul} C_{j}^{→}^{R′}, hence I(F^{k} (z_{1}, …, z_{n})^{R}) ≫_{3} I(F^{k} (z_{1}, …, z_{n})^{R_{j}}), hence F^{k} (z_{1}, …, z_{n})^{R_{j}} is computable.

Step III. Let v be the term obtained by replacing, in the right hand side of the rule, the terms F^{k} (C_{1}^{→}[M^{→}], N^{→}), …, F^{k} (C_{m}^{→}[M^{→}], N^{→}), M^{→}, and N^{→} by fresh variables. Let R′′ be the replacement such that C’[F^{k} (C_{1}^{→}[M^{→}], N^{→}), …, F^{k} (C_{m}^{→}[M^{→}], N^{→}), M^{→},N^{→}] = v^{R′′}, then t^{R} →_{R} v^{R′′}. Notice that above we have shown that R′′ is computable. When F^{j} occurs in v, then by definition of the general scheme j < k, and therefore I(t^{R}) ≫_{1} I(v^{R′′}), hence v^{R′′} is computable, and since w = v^{R′′}, we get Comp (B, w, σ). C. t = Ap (z_{1}, z_{2}) where z_{1}, z_{2} ∈ X. By assumption, z_{1}^{R} and z_{2}^{R} are computable, and since t is well-typed, z_{1} must have an arrow type. Then, by Def.30, Ap (z_{1}^{R}, z_{2}^{R}) is computable. But Ap (z_{1}^{R}, z_{2}^{R}) is the same as Ap (z_{1}, z_{2})^{R}.

2. Let t ≡ F_{n} (t_{1}, …, t_{n}). Again we distinguish two cases:

(a) Assume that at least one of the t_{i} is not a term-variable. Since t ·^{>} t_{i} (for 1 ≤ i ≤ n), by induction there exist B′, σ_{i} such that Comp (B’, t_{i}, σ_{i}), and also the replacement R′ = {z_{1} ↦ t_{1}, …, z_{n} ↦ t_{n}} is computable. Since t ·^{>} F_{n}(z_{1}, …, z_{n}), we have I(t^{R}) ≫ I(t^{R′}), and t^{R′} is computable by induction. Note that t^{R′} = t^{R}.

(b) All t_{i} are term-variables. Since B ⊢_{E} t:σ, by Lem.20:3 there exist α ∈ T_{∩}, β ∈ T_{−ω} such that σ = α→β. For all u such that Comp (B”, u, α), we have to prove Comp (Π{B’,B”}, Ap (t^{R}, u), β). Since Ap (t^{R}, u) is neutral, by Prop.C3, it is sufficient to prove Comp (Π{B’,B”}, t′, β) for all t′ such that Ap (t^{R}, u) →_{R} t′. This will be proved by induction on the sum of the maximal length of the derivations out of u and out of R. Note that since u and R are computable, by Prop.C1, SN(u) and SN(R). Base. If u and R are in normal form, the only reduction step out of Ap (t^{R}, u) could be: Ap (F_{n}(z_{1}, …, z_{n})^{R}, u) →_{R} t′ ≡ F_{n+1}(z_{1}^{R}, …, z_{n}^{R}, u). Then, since

I(t^{R}) ≫_{1} I(F_{n+1}(z_{1}^{R}, …, z_{n}^{R}, u)), t′ is computable.

Induction step. If the reduction step out of Ap (t^{R}, u) takes place inside u or inside t^{R} (in the last case it must be inside R since the rewrite system is safe) then t′ is computable by induction. If Ap (F_{n}(z_{1}, …, z_{n})^{R}, u) →_{R} t′ ≡ F_{n+1}(z_{1}^{R}, …, z_{n}^{R}, u), then, we proceed as in the base case.

Theorem 35 Strong Normalization Theorem. If (Σ, R) is typeable in ⊢_{E} and safe, then any typeable term is strongly normalizable with respect to R.

Proof: From Prop. 34 and C1, taking R such that x^{R} = x.

4 Final remarks

The type assignment system defined in this paper for CTRS is undecidable: it is feasible to show that for every lambda term typeable in ⊢_{λ∩−ω} there exists a term in ACL, obtained by bracket-abstraction, that is typeable as well, and vice versa. However, if we restrict the system as in [2], then typeability is decidable, and since the Strong Normalization Theorem we proved in Section 3.2 is still valid in this weaker system, any typeable CTRS satisfying the general scheme (as given in Def.29) is terminating on typeable terms.

References

1. S. van Bakel. Complete restrictions of the Intersection Type Discipline. Theoretical Computer Science, 102:135–163, 1992.

2. S. van Bakel. Partial Intersection Type Assignment of Rank 2 in Applicative Term Rewriting Systems. Technical Report 92-03, Department of Computer Science, University of Nijmegen, 1992.

3. S. van Bakel. Essential Intersection Type Assignment. In R.K. Shyamasunda, editor, Proceedings of FST&TCS ’93. 13^{th} Conference on Foundations of Software Technology and Theoretical Computer Science, LNCS 761, pages 13–23, Bombay, India, 1993.

4. S. van Bakel. Partial Intersection Type Assignment in Applicative Term Rewriting Systems. In M. Bezem and J.F. Groote, editors, Proceedings of TLCA ’93. International Conference on Typed Lambda Calculi and Applications, LNCS 664, pages 29–44, Utrecht, the Netherlands, 1993.

5. S. van Bakel. Principal type schemes for the Strict Type Assignment System. Logic and Computation, 3(6):643–670, 1993.

6. F. Barbanera and M. Fernández. Combining first and higher order rewrite systems with type assignment systems. In M. Bezem and J.F. Groote, editors, Proceedings of TLCA ’93. International Conference on Typed Lambda Calculi and Applications, LNCS 664, pages 60–74, Utrecht, the Netherlands, 1993.

7. F. Barbanera and M. Fernández. Modularity of Termination and Confluence in Combinations of Rewrite Systems with λ_{ω}. In A. Lingas, R. Karlsson, and S. Carlsson, editors, Proceedings of ICALP ’93. 20^{th} International Colloquium on Automata, Languages and Programming, LNCS 700, pages 657–668, Lund, Sweden, 1993.

8. H. Barendregt. The Lambda Calculus: its Syntax and Semantics. North-Holland, Amsterdam, revised edition, 1984.

9. H. Barendregt, M. Coppo, and M. Dezani-Ciancaglini. A filter lambda model and the completeness of type assignment. Journal of Symbolic Logic, 48(4):931–940, 1983.

10. M. Coppo, M. Dezani-Ciancaglini, and B. Venneri. Principal type schemes and λcalculus semantics. In J.R. Hindley and J.P. Seldin, editors, To H.B. Curry, Essays in combinatory logic, lambda-calculus and formalism, pages 535–560. Academic press, New York, 1980.

11. H.B. Curry and R. Feys. Combinatory Logic, volume 1. North-Holland, Amsterdam, 1958.

12. N. Dershowitz and J.P. Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, chapter 6, pages 245–320. North-Holland, 1990.

13. M. Dezani-Ciancaglini and J.R. Hindley. Intersection types for combinatory logic. Theoretical Computer Science, 100:303–324, 1992.

14. K. Futatsugi, J. Goguen, J.P. Jouannaud, and J. Meseguer. Principles of OBJ2. In Proceedings 12^{th} ACM Symposium on Principles of Programming Languages, pages 52–66, 1985.

15. J.Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1989.

16. J.R. Hindley. The principal type scheme of an object in combinatory logic. Transactions of the American Mathematical Society, 146:29–60, 1969.

17. J.P. Jouannaud and M. Okada. Executable higher-order algebraic specification languages. In Proceedings of the Sixth Annual Symposium on Logic in Computer Science, pages 350–361, 1991.

18. J.W. Klop. Term Rewriting Systems. In S. Abramsky, Dov.M. Gabbay, and T.S.E. Maibaum, editors, Handbook of Logic in Computer Science, volume 2, chapter 1, pages 1–116. Clarendon Press, 1992.

19. R. Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17:348–375, 1978.

20. F. Pfenning. Partial Polymorphic Type Inference and Higher-Order Unification. In Proceedings of the 1988 ACM conference on LISP and Functional Programming Languages, pages 153–163, 1988.

21. S. Ronchi della Rocca and B. Venneri. Principal type schemes for an extended type theory. Theoretical Computer Science, 28:151–169, 1984.

22. W.W. Tait. Intensional interpretation of functional of finite types. Journal of Symbolic Logic, 32, 1967.

23. D.A. Turner. Miranda: A non-strict functional language with polymorphic types. In Proceedings of the conference on Functional Programming Languages and Computer Architecture, LNCS 201, pages 1–16.

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