JAIST Repository
https://dspace.jaist.ac.jp/

Title

Unique normal form property of Higher‑Order
RewritingAuthor(s)Mano, Ken; Ogawa, Mizuhito

Citation

Lecture Notes in Computer Science, 1139: 269‑283

Issue Date

1996

Type

Journal Article

Text version

author

URL

http://hdl.handle.net/10119/7888

RightsThis is the author‑created version of Springer,
Ken Mano and Mizuhito Ogawa, Lecture Notes in
Computer Science, 1139, 1996, 269‑283. The
original publication is available atwww.springerlink.com,
http://dx.doi.org/10.1007/3‑540‑61735‑3̲18

Description

Japan Advanced Institute of Science and Technology

Unique Normal Form Property of Higher-Order
Rewriting Systems
Ken Mano1 and Mizuhito Ogawa2
1

NTT Communication Science Laboratories, Japan2

mano@cslab.kecl.ntt.jp

NTT Basic Research Laboratories, Japanmizuhito@theory.brl.ntt.jp

Abstract. Within the framework of Higher-Order Rewriting Systems pro-

posed by van Oostrom, a sucient condition for the unique normal form
property is presented. This requires neither left-linearity nor termination of
the system.
1 Introduction

Several frameworks of rewriting systems for higher-order expressions have been proposed [Klo80, Nip91, MN94, LS93, KvO95]. Van Oostrom and van Raamdonk proposed a framework of Higher-Order Rewriting Systems (HORSs) [vO94, vOvR94,
vR96], capable of unifying the existing theory of rewriting, e.g., Combinatory Reduction Systems (CRSs) [Klo80], (another variation of) Higher-order Rewriting Systems (HRSs) by Nipkow [Nip91], and Term Rewriting Systems (TRSs). They alsopresented a sucient condition for the Church-Rosser property of HORSs by introducing a notion corresponding to orthogonality (i.e., non-overlap and left-linearity)of TRSs.
The framework of HORSs is characterised by the clear separation of replacementwith rewrite rules and matching/substitution for application of the rules. The latter isdone by another rewriting system called substitution calculus, which is a parameterthat determines an HORS together with a set of rewrite rules. In [vO94], someabstract conditions are rst presented on rewrite rules and substitution calculi, andthen properties such as the Church-Rosser property are derived for HORSs satisfying
the conditions. In particular, a non-overlapping left-linear pattern HORS is shownto satisfy the conditions (see also [vOvR94], [vR96]).
It is well-known that a non-overlapping left-linear TRS has the Church-Rosser
property. Without left-linearity and with a slight modi cation of the non-overlap
requirement, some results [Che81, dV90, TO94, MO95] have concluded the uniquenormal form property of TRSs. The unique normal form property is a sucientcondition for consistency of the system [KdV89] and weaker than the Church-Rosser
property.
Let us brie y introduce the methodology in [dV90] (see also [KdV90]). The following theorem concerning (abstract) rewriting systems is the key observation.
Theorem 1 [dV90]. Suppose that rewriting systems !0 and !1 satisfy the following:1.

! ! ,
01

!

2.
1 has the Church-Rosser property, and3. the set of normal forms of
1 contains those of
Then,

!

! has the unique normal form property.

!.
0

0

In order to apply this to TRSs, the notion of (conditional) linearisation is introduced. Linearisation is a transformation from a TRS R to a left-linear semiequational conditional TRS RL and non-left-linearity of R is expressed in the condition part of RL . Then, 1 of Theorem 1 apparently holds, and 3 is derived byassuming 2. Consequently, the unique normal form property of R is reduced to the
Church-Rosser property of RL. Using the result that a non-overlapping left-linear
semi-equational conditional TRS has the Church-Rosser property [BK84], we obtaina sucient condition for the unique normal form property of TRSs.
In this paper we extend this result to HORSs. The main theorem states that \astrongly non-overlapping pattern HORS has the unique normal form property".
The structure of this paper is as follows. Section 2 provides basic de nitions
and Section 3 explains HORSs. In Section 4, we introduce the notion of ContextConditional HORS (CCHORS, for short), and give a sucient condition for the
Church-Rosser property of CCHORSs. Based on this result, we present the main
result using Context-Conditional Linearisation in Section 5.
2 De nitions

The de nitions in this subsection are based on [vO94].

2.1 Rewriting Systems
A rewriting system hD; !i is a pair of the underlying domain D and the binary
relation ! called the rewrite relation. The domain D is often omitted when it isclear from the context. Suppose a1 ; a2; : : : 2 D. Each element a1 ! a2 of the rewrite
relation is called a rewrite step. A sequence of rewrite steps a1 ! 111 ! an is calleda rewrite. The symmetric closure, the re exive transitive closure and the re exive
transitive symmetric closure of ! are written as $, !3 and $3 , respectively. If
there is no a2 such that a1 ! a2, then a1 is a normal form of the reduction system.
The set of normal forms of ! is denoted by NF!. If a1 !3 a2 and a2 2 NF! , thena2 is called a normal form of a1, with notation a1 !3! a2 .
A rewriting system ! is terminating if there is no in nite sequence such as
a1 ! a2 ; ! 111. A rewriting system ! has the unique normal form property if for
any normal forms a1 and a2 , a1 $3 a2 implies a1  a2 . A rewriting system ! has
the Church-Rosser property if for any a1 $3 a2 there exists a3 such that a1 !3 a3and a2 !3 a3 . A rewriting system is said to be complete if it is terminating and has
the Church-Rosser property.
2.2 Simply-typed preterms
In this subsection, we introduce higher-order expressions with so-called simple types.
Note that the following de nition distinguishes between the syntactic category ofbound variables and that of free variables. Note also that the phrase \(x; y 2) X "introduces a set X with variables x, y ranging over X .

De nition 2. The set (; 2) T of Simple types is inductively de ned as follows:
1. the base type o is a simple type,2. if  and  are simple types, then  !  is a simple type.
A function arity : T ! N is de ned by (1) arity(o) def= 0, and (2) arity( !  ) def=
arity( ) + 1.
De nition 3. An alphabet (a; b; c 2) A is a countable set consisting of the following
symbols:
1. application -(-),
2. abstraction -:-,
3. for each simple type  ,(a) operator (or constant) symbols F ; G ; H ; 111,(b) bound variables  ;  ;   ; 111,(c) free variables x ; y ; z  ; 111. Among these symbols, we have distinguishedsymbols 21 ; 22 ; 111 called holes. The hole 21 is also written as 2 .
The operators together with the free variables form the rewrite alphabet AR .
The type information of the symbols are omitted if they are clear from the context.
Therefore,   , F , x and 2i are often written as  , F, x and 2i, respectively.
From the symbols in the alphabet, (simply-typed) raw preterms are built in thefollowing way. Let Z be a set of bound variables. The set (s; t; r 2) RPT(A) of raw
preterms is inductively de ned as follows:
1. operator F , bound variable   and free variable x are raw preterms of type  .
2. if s is a raw preterm of type  !  and t is a raw preterm of type , then s(t)is a raw preterm of type  ,3. if s is a raw preterm of type  , then  :s is a raw preterm of type  !  .
Since every raw preterm has a unique simple type, we can de ne arity(s) as thearity of the type of s.
De nition 4. Let A be an alphabet. The set (; ;  2) Pos def= f0; 1g3 is called theset of positions (or occurrences). The concatenation of  and is denoted by ; .
We say  is a pre x of when there exists 0 such that = ; 0 . We write  when  is a pre x of , and   when   and  6= . Two positions are
disjoint if they are not pre xes of each other.
Positions in a raw preterm t are represented in Pos in the usual way (see also
[MN94] and [LS93]3 ). The set of all positions in t is denoted by Pos(t). The subtermat position  in s is denoted by s=. Furthermore, the symbol at position  in s isdenoted by s(). For a symbol a, we de ne aPos(s) def= f 2 Pos(s) j s() = ag. If
aPos(s) is a singleton set, the element is also denoted by aPos(s). We also de ne
RPos(s) def= f 2 Pos(s) j s() 2 Ag. The function Fvar (Bvar) maps a raw pretermto the set of free (bound) variables occurring in it.
For a term s and a position  2 Pos(s), we say  is in the scope of  in s if there
exists satisfying s= = :s0 and  . If s() =  and  is not in the scope of in s, then  is called an unbound occurrence of  , and  is said to occur unboundly
in s. The set of bound variables occurring unboundly in a raw preterm s is denoted
by UBvar(s).
3

In [MN94] and [LS93], f1 2g3 is used instead of f0 1g3 for Pos.
;;De nition 5. Let A be an alphabet. A preterm is a raw preterm without any unbound occurrences of bound variables. From now on, we restrict s, t and r to range
over the set PT(A) of preterms. If Fvar(s) = ;, then s is said to be closed .
An instantiation is a set  def= fxi := ti j i = 1; 111 ; ng of pairs consisting of a freevariable and a preterm. For a preterm t, t denotes the term obtained by replacing
all xi with ti (i = 1; : :: ; n).
A preterm is an m-ary precontext, if the holes occurring in it are among 21 ; : : : ;2m . We use C , D and E to range over precontexts. We denote m-ary precontexts by
C [m], D[m] and E [m]. We also write a unary precontext as C [ ], and a binary precontext as C [ ; ]. The term C [m]f2i := si j i = 1; 111 ; mg is denoted by C [s1 ; 111 ;sm].
An m-ary precontext is linear if every hole 21 ; 111 ; 2m occurs exactly once in it.
De nition 6. Let s be a preterm and x a free variable. Then :s0 is called an xclosure of s if x does not appear in the scope of  in s and s0 is obtained from s
by replacing every occurrence ofdefx with  . The set of all x-closures of s is denotedby closx (s). For a sequence  = x1 ; :: : xm of free variables, a -closure of s is an
x1 -closure of : : : of an xm -closure of s.
3 Higher-Order Rewriting Systems

As is mentioned at the beginning, the actual rewrite relation of an HORS is de ned by
two rewrite relations, that is, replacement with rewrite rules and another rewriting
system called substitution calculus which performs matching and substitution. In
other words, the rewrite relation of an HORS is de ned modulo the substitution
calculus. For example, let us consider an HORS which has the usual -calculus asits substitution calculus, and as rules 1 + 1 ! 2, 2 + 2 ! 4, := ! :1 and:2 2  ! : +  . Then we have the following computation. Subexpressions to which
rewrite rules are applied are indicated by [ ].
3 2 2 (:((1) + (3)))([:= ])2 2 (1=1 + 3=3)
! 2 2 (:((1) + (3)))(:1) !3 2 2 ([1 + 1])! 222([:2 2  ])(2)! (: + )(2)! [2 + 2]!4
In this paper, we are interested in a pattern HORS, not a general HORS. A pattern
HORS has a simply-typed -calculus !
 with restricted  -expansion as its substitution calculus, and the left-hand side of each of its rewrite rules is a special term
called a pattern. Various rewriting systems, e.g., CRSs [Klo80], HRSs [Nip91] andalso TRSs, can be embedded into pattern HORSs [vO94].
Basically, the de nitions in this section follow [vO94]. The theorems in this section without any notice appear in [vO94] and/or [vOvR94].

3.1 Simply-Typed -calculus as Substitution Calculus
De nition 7. The -, - and -rewrite relations on PT(A) are denoted by ! , !
and ! , respectively [Bar84]. In order to indicate that the rewrite contracts thesubterm at position , we also use !(;@) for @ = ; ; . We de ne !(;)def= (;)0 and ! is the union over all positions  of ! ; . The rewriting system
hPT(A); ! [ ! [ !i is denoted by ! .
A rewrite step s ! ;@ t is below if   . In order to indicate that a rewritefrom s to t is a sequence of @-rewrite steps below , we write s !3 ;@ t.


( )



(



)

(

)

The following property is a basic fact about typed -calculi, see e.g., Thm. 2.35
and Thm. 2.38 in [Wol93].
Theorem 8. !  is complete modulo $3 .
Theorem 9. Suppose s 2 NF!. Then s ! t implies t 2 NF!. Moreover, if
u 2 NF!, then sfx := ug 2 NF!.
De nition 10. A term (context, resp.) is a preterm (precontext) in ! -normal
form. The set of A-terms is denoted by T(A).
Remark. A term s0 of arity m can always be written as 1 ; 111 ; m :a(s01 ) 111 (s0k ),where k is the arity of the symbol a. Each s0i (i = 1; 111 ; k) is in this form again.
That is, s0 is the x1 ; 111 ; xm-closure of some term s def= a(s1 ) 111 (sk ). In this case, ais called the head of s0 and its position is denoted by head(s0 ).
The descendant relation de ned below traces the occurrences of AR -symbols
along a rewrite.
De nition 11. For a rewrite step u def= s !(;@) t (@ = ; ;  or ), the descendant
relation juj: Pos 2 Pos is de ned as follows. Let 2 RPos(s). If  6 , then juj .
Otherwise:
1. if @ = , then juj ,2. if @ = and s= def
= :s1(s2), then= ;00; 1 , and(a) juj ; 1 if def(b) juj ; 1 ; 2 if def= ; 1; 2 and s1 ( 1) =  ,3. if @ =  and = ;00; 0 , then juj  0 ,4. if @ = , then jujdef= jt !(;) sj01 .
The descendant relation jdj associated to a rewrite d : t1 !3  tn is the concatenation of descendant relations corresponding to each rewrite step in d. If  2 RPos(t1)and  jdj , then is called a descendant of , and  is called an origin of .

3.2 Pattern HORS
De nition 12. Let l0 of arity m be the x1 ; 111 ; xm-closure of a term l. Then l0 iscalled a pattern, if it satis es the following conditions:
1. the head of l is an operator symbol,
2. let x of arity k be among x1 ; 111 ; xm,(a) there is at least one occurrence of x in l,(b) for every occurrence ; 0k of x in l, we have that if l !3(! ;) g, then g= xi(1) 111 (k ), where 1 ; 111 ; k is a list of pairwise distinct bound variables.
Moreover, in (a) above, if there is precisely one occurrence of x in l, then l0 is calleda linear pattern.

Intuitively, 1 of the above conditions corresponds to \the left-hand side of each rule is
not a variable" on TRSs, and 2 to \every variable in the right-hand side of each ruleappears in the left-hand side". For the precise discussion about the correspondence
between a pattern HORS and a TRS, see Lemma 15.
De nition 13. A pattern Higher-Order Rewriting System (pattern HORS) is a triple
hA; ! ; Ri consisting of an alphabet A, a substitution calculus ! , and a set R ofpattern rewrite rules. A pattern rewrite rule is a pair of terms of the form l ! r
satisfying the following conditions: (1) both l and r are closed, (2) l and r are of thesame type and (3) l is a pattern.
We use @ and i to range over rewrite rules. The rst and second components
of a rule @ are denoted by lhs(@) and rhs(@) and are its left- and right-hand side,
respectively.
A pattern rewrite rule with a linear left-hand side is called a left-linear patternrewrite rule, and a pattern HORS with only left-linear pattern rewrite rules is calleda left-lineardef pattern HORS.
Let H = hA; ! ; Ri be a pattern HORS. We associate two rewriting systems toa pattern HORS. They are both de ned on the set of preterms.
1. For a rule @ def= l ! r 2 R and precontext C [ ], we de ne the replacement of@ in C [] by C [l] !C[@] C [r]. This is generalised
to the replacement of @ in an
def S
arbitrary precontext, by de ning !@ = C [ ] !C [@] , and to replacement of anarbitrary rule, by de ning !R def= S@2R !@ .
2. The rewrite relation of H is obtained by !Hdef= $3 ; !R ; $3 .
Next, we present some basic de nitions and properties related to pattern HORSs.
In the following, we regard terms (i.e., ! -normal forms) as representatives of the$3 -equivalence classes, and restrict, in principle, the rewrite relation !H to therelation on the terms. Then, the following property is useful for simplifying thearguments.
Theorem 14. When we restrict the domain of the rewrite relation !H to T(A), we
may assume the following without loss of generality:

C [ ] in the de nition of !R is a linear context,; !R; !3  instead of $3 ; !R; $3  in the de nition of !H.
In the second item, 3  and !3  are called the expansion and reduction of therewrite step, respectively.
The following property is called `head-de nedness' in [vO94].
Theorem 15. Let l ! r be any pattern rewrite rule.
1. Let C [ ] be a linear context with hole-position . Then ;  has a unique descendant  along any reduction from C [l] to its normal form C [l]# .
2. For a position  in a term s, there is at most one linear context C [ ] with holeposition , such that ; head(l) is an origin of  along the expansion from s to
C [l].
The head-de nedness of a pattern HORS guarantees that \a rewrite step is determined by the position and the rewrite rule" which trivially holds in the case of TRSs.
This makes it possible to give the following de nition.
1. the precontext
3
2. we may useDe nition 16. In the second item of the lemma above, if C [ ] exists, the pair (; @)is called a redex in s and any such expansion is called an extraction of (; @) from s(into C []). If the expansion of a rewrite step w : s !H t is an extraction of (; @),we say w rewrites the redex (; @), with notation s !(;@) t.
The descendant relation de ned for ! is extended to pattern HORSs in thefollowing way.
De nition 17. Let H be a pattern HORS and @ : l ! r a rewrite rule of H.
For a replacement u : C [l] !C [@] C [r], the descendant relation juj: RPos(C [l]) 2
RPos(C [r]) is de ned as follows: juj i  = 6 2Pos(C [ ]):For a rewrite step s !H t in H, the descendant relation js !H tj is the concatenation of the descendant relations corresponding to its expansion, replacement andreduction. The extension of the descendant relation to a rewrite t1 !3H tn parallels
the case of ! .
De nition 18. Let H be a pattern HORS and u : s !3 t a rewrite in H or ! .
Suppose that (; @) is a redex in s and that  juj 0. If (0 ; @) is a redex in t, it iscalled a residual of (; @).
In the following, we outline the proof that \a non-overlapping left-linear pattern
HORS has the Church-Rosser property" in [vO94] and [vOvR94]. The Church-Rosser
property is derived from the Finite Developments theorem, which is an extension of
the rst-order case. In the case of a pattern HORS, the technical notion `simultaneity'
is introduced, and it mediates between the sucient condition (i.e., non-overlap andleft-linearity) and the Finite Developments theorem.
De nition 19. Let H be a pattern HORS and U a set of redexes in s1. A rewrite
w : s1 !H 111 !H sn is called a development of U if for each wi : ti !H ti+1 , there
exists ui 2 U and wi rewrites a residual of ui . If there are no residuals of U in sn , w
is called complete.
De nition 20. Let H be a pattern HORS. LetdefU def= fu1; 111 ; um g be a set of (pairwise distinct) redexes in a term s, where ui = (i ; li ! ri ) (i = 1; 111 ; m). An
expansion e : s 3  C [l1; 111 ; lm ] is called an extraction of U from s (into C [m]), if
C [m] is a linear context and for every ui 2 U , we have that 2i Pos(C [m]); head(li )is an origin of i . If such an extraction exists for the set U , then U is called a simultaneous set of redexes. A pattern HORS is simultaneous (pairwise simultaneous) if
every set (pair) of redexes is simultaneous.
De nition 21. Let u def= (; 0m ; @) and v def= ( ; 0n; i) be distinct redexes in a terms, where m (n) is the arity of the head symbol of lhs(@) (lhs(i)).
1. The redexes are said to be disjoint if  and are disjoint.
2. Otherwise we may assume without loss of generality that  . Let lhs(@) be
the x1 ; 111 ; xk -closure of l. Two cases are distinguished:(a) the redex u is said to nest v, if ; ; ! = , where ; 0i is the position ofsome variable x of arity i in l, and x is among x1 ; 111 ; xk ,(b) otherwise u is said to overlap with v .

A rule @ overlaps with another rule i, if some @-redex overlaps with some i-redex.
A pattern HORS has overlap if some rule overlaps with another one, it is nonoverlapping otherwise.
It is decidable whether an HORS has overlap or not.
The following theorem 22, 23 and 24 correspond to Lemma 3.9, Lemma 3.8 andTheorem 3.10 in [vOvR94], respectively.
Theorem 22. Let H be a left-linear pattern HORS. Then H is non-overlapping i

H is pairwise simultaneous i H is simultaneous.

Theorem 23 (Finite Developments).

For any left-linear pattern HORS, every
complete development of a set of simultaneous redexes ends in the same term.

From these theorems, the following theorem is derived immediately.
Theorem 24. A non-overlapping left-linear pattern HORS has the Church-Rosser
property.

4 Context-Conditional HORS

In this section, we introduce Context-Conditional HORSs (CCHORSs). We thengive a sucient condition for the Church-Rosser property of CCHORSs.

4.1 Context Condition
De nition 25. A Context-Conditional pattern rewrite rule (CC rule, for short) is@^ def= l^ ! r^ ( Q satisfying the following:
1. ^l ! r^ is a pattern rewrite rule, and
2. Q isSa sequence N1 ; : : : ; Nm of sets of natural numbers satisfying:(a) 1im Ni = f1; : : : ; arity(l^)g, and(b) Ni \ Nj = ; for i; j = 1; : :: ; m and i 6= j .
We call Q the condition part of @^ , and l^ ! r^ the unconditional part of @^ . A CC
rule is left-linear if its unconditional part is left-linear. A Context-Conditional HORS
^ consisting of an alphabet A, a substitution calculus(CCHORS) is a triple hA; !
 ; Ri!
^ , and a set R of CC rules.
^ denotes a CCHORS. The rewriting
In the rest of this section, H^ def= hA; !
 ; Ri^system associated to H is de ned as follows.
De nition 26. Let @^ : ^l ! r^ ( N1 ; 111 ;Nm 2 R^ . The replacement !@^ with @^ ofrank i (i = 0; 1; 111) is inductively de ned as follows:!@^0 = ;;!@^ +1 = f(C [^l]; C [^r]) j the precontext C [ ] satis es the $3H^ -context condition of @^ g;where !R^ def= Si^2 R^ !i^ , !H^ def= $3 ; !R^ ; $3 , and we say C [ ] satis es the $3H^ context condition of @^ if the following holds:
i

i

i

i

i

i

i

i

for any 2 2Pos(C [ ]),1. there exists 0 such that = 0 ; 0m^ and C [^l]= 0 = ^l(s1) 111 (sm^ ),where m^ is the arity of ^l,
2. for any j = 1; 111 ; m, s~k $3H^ s~k if k; k0 2 Nj , where ^l(~s1 ) 111 (~sm^ )is the preterm obtained by replacing all bound variables 1 ; 111 ;koccurring unboundly in the raw preterm ^l(s1 ) 111 (sm^ ) with fresh freevariables x1; 111 ; xk .
i0

We de ne theS replacement in R^ by !R^ def= Si !R^ and then the rewrite relation ofH^ by !H^ def= i !H^
It is apparent from the de nition that !H^ 0 !H^ 1  111 !H^ . Thus C [ ] satis es
the $3H^ -context condition of @^ for some i i C [] satis es the $3H^ -context conditionof @^ . Hereafter, we call the $3H^ -context condition simply the context condition.
Let R be the set of unconditional parts of R^ , and H the pattern HORS with theset R of rewrite rules. Then, !R^ and !H^ are the subsets of !R and !H restrictedto satisfying the context condition, respectively. In particular, the substitution cal!
culus !
 does not change at all. Therefore, the above de nitions related only to  
can be extended to CCHORSs with no modi cation.
In order to extend other de nitions and statements about a pattern HORS we
must show that some `operations' (division, substitution and rewrite of the context)
preserve the context condition.
The following lemma directly follows from the de nition of the context condition.
Lemma 27 (division). Let C [ ] be a context with m occurrences of 2. Let D[m] be
the linear context such that D[2; 111 ; 2] = C [2]. Then C [ ] satis es the context con^ : ^l ! r^ ( Q 2 H^ i D[l^; 111 ; ^l; 2; ^l; 111 ; l^] satis es the context condition
dition of @
i

i

i

of

| {z }
i01@^ for i = 1; 111 ; m.

Lemma 28 (substitution). For any preterms s, t, u, and a free variable x, s !H^ t
implies sfx := ug !H^ tfx := ug. Moreover, if a precontext C [ ] satis es the context
condition of @, C [ ]fx := ug also satis es it.
Proof
Using Theorem 9, it is proved by induction on the rank.
Lemma 29 (rewrite of the context). Suppose that C [ ] satis es the context con^ 2 R^ .
dition of @00^.
1. If C [ ] !R
^ C [ ], then C [ ] satis es the context condition of @00^.
2. If C [ ] !  C [ ], then C [ ] satis es the context condition of @Then, we can prove the following lemma, which corresponds to Theorem 14.
Lemma 30. When we restrict the domain of the rewrite relation !H^ to T(A), we
may assume the following without loss of generality:

C []

!

1. the precontext
in the de nition of^ i is a linear context,R
3
3 instead of
2. in the de nition of H
^ i , we may use R^ i


!

;! ;!

$3  ; !R ; $3  .


^i



The proof is done similarly to that of Propositions 3.1.17 and 3.1.22 in[vO94] using Lemma 27 and Lemma 29.
De nition 31. The de nition of the redex of a CCHORS is obtained by replacing
if C [ ] exists
in De nition 16 with
if C [ ] exists and it satis es the context condition of @^.
The descendant relation and the residual of a CCHORS can be de ned completely
in the same way as a pattern HORS.
De nition 32. The de nition of the simultaneity of redexes of a CCHORS is obtained by modifying De nition 20 as follows:
1. replace H and @i : li ! ri with H^ and @^ i : ^li ! r^i ( Qi , respectively,
2. add the following:
3. each occurrence of holes in C [m] satis es the context condition, that
is, C [^l1; 111 ; ^li01; 2; ^li+1 ; 111 ; ^lm ] satis es the context condition of @^ i for
i = 1; 111 ; m.
to the condition for simultaneity of redexes.
De nition 33.
Let @^ and i^defbe CC rules with unconditional parts @ and i, respecdef
tively. Let u^ = (; @^ ) and v^ = ( ; i^) be distinct redexes in a term s. We say u and v
are disjoint (u nests v, u overlaps v, resp.) if u def= (; @ ) and v def= ( ; i) are disjoint(u nests v, u overlaps v).
A CC rule @^ overlaps with another CC rule i^, if some @^ -redex overlaps withsome i^-redex. A CCHORS has overlap if some rule overlaps with another one; it isnon-overlapping otherwise.
Proof

4.2 Church-Rosser Property of CCHORS
A sucient condition for the Church-Rosser property of CCHORSs is derived in asimilar way to pattern HORSs.
The following two statements concerning pattern HORSs are used to derive properties of non-overlapping left-linear CCHORSs.
Theorem 34. Let U def= f(i ; @i ) j i = 1; 111 ; ng be a simultaneous redex in a term s
3 C [l ; 111 ;l ] andof a left-linear pattern HORS H. For any extractions w1 : sn 1 13
w2 : s  C2[l1 ; 111 ; ln ], we have C1[n]  C2 [n].
ProofThe result is immediate from Lemma 3.1.40 in [vO94].
Lemma 35.defLet @ : l0 ! r0 be a pattern rewrite rule. Suppose that l0 is an x1 ; 111 ; xm3 C [l0 ] is an extraction of aclosure of l = F(u1 ) 111 (uk ). Suppose also that u : skredex (; 0 ; @) in a term s. Then, for any xi of arity mi and  s.t. ; 0m 2 xi Pos(l)(i = 1; 111 ; m), the following holds:
30
1. s(; ) C [l ],2. s=;  and C [ ]=; 0m0i ;1; 0m are the same modulo renaming of bound variables,ii; ; ! 2 RPos(s), then ; ; ! juj ; 0m0i; 1; 0m ; ! ,2 (C [ ]) = ; 0m.

3. if
4. Posi

Lemma 36. A non-overlapping left-linear CCHORS is simultaneous.
Proof
First, we will show thatdef a left-linear CCHORS
H^jis pairwise simultaneousdefk^
if it is non-overlapping. Let u^ = (;0 ; @) and v^ = ( ; 0 ; i^) be pairwise distinct
redexes in a term s, where k (j , resp.) is the arity of the head symbol of @^ (i^).
Let @ (i) be the unconditional part of @^ (i^). From Theorem 22, there exists= (; 0k ; @) and v def=
an extraction w : s 3  D [lhs(@ ); lhs(i)] of redexes u def( ; 0j ; i). Therefore, it is enough to show that D[2; lhs( i)] and D [lhs( @); 2] satisfy
the context conditions of @^ and i^, respectively.
1. If u^ and v^ are disjoint, the result is apparent since the extractions of themtake place below the disjoint positions  and , respectively; so they do not in uenceeach other.
2. Otherwise, we can assume u^ nests v^ without loss of generality. Let l^0 def= lhs(@^ )of arity m^ be an x1 ; 111 ;xm^ -closure of l^. Let mi be the arity of xi (i = 1; 111 ; m^ ). Also
let u def
= s 3  C [^l0 ] be an extraction of u in s. From the de nition, there exist xi and 2 xi Pos(l^) such that ; ; ! = . Thus, from 2 and 3 of Lemma 35, we have thatjuj ; 0m^ 0i; 1;0m ; ! and that s=;  and0 Cdef[ ]=; 0m^m^00ii; 1; 0mm are equal modulo
renaming of bound variables. So the redex v = (; 0 ; 1; 0 ; !; i) in C [ ] is thedescendant of v and we can construct an extraction of v0 from C [ ] by simulating oneof v^. Then, the resulting context is D[ ; ] from Theorem 34. Therefore, D[lhs(@ ); 2]
satis es the contextdefcondition of i^.
Suppose C [ ]= = 2(s1 ) 111 (sm^ ). Then, the extraction C [ ] 3  D[2; lhs(i)]of v^0 takes place `inside' si . Since C [ ] satis es the context condition of @^ , so does
D[2; lhs(i)].
In a similar way to the pattern HORS's case, we can show that pairwise simultaneity implies simultaneity by induction on the cardinality of the set of redexes
using Lemma 28.
Lemma 37 (Finite Developments of CCHORS). Every complete development^ ends in the same term.
of a set of simultaneous redexes of a left-linear CCHORS H
ProofThe proof is done in the same way as the pattern HORS's case, but wemust supplement the argument about the context condition. In [vOvR94], the Finite
Developments theorem is proved in the following way:
Let U = V [ fug be a set of redexes. Let L (R, resp.) be the set of the left(right-) hand sides of the rules of V , and let l (r, resp.) be the left- (right-) handside of the rule of u. Let us consider any complete U -development.
1. Suppose u is chosen in the rst rewrite step of the development. Then, therewrite step s 3  C [l] !C [l!r] C [r] !3  s0 can be simulated by s 3  D[L; l]!D[L;l!r] D[L; r] !3  s0, which also extracts V simultaneously.
2. Suppose that D[ ; r] !3! E [ ]. Let D0 [ ] be the linear context such that0
D [2; 111 ; 2]  E [2]. Then, s0 3  D0 [L0] is the extraction of the residuals of V . Let
R0 be the right-hand sides corresponding to L0 . We de ne an order  on the set ofpairs of terms and natural numbers as the lexicographic order of 3  and . When(t; i)  (t0 ; i0) and (t; i) 6= (t0; i0 ), we write (t; i)  (t0 ; i0). If holes appear n and n0iii

times in D and D0, respectively, then we have (D[R; r]; n)  (D0 [R0 ]; n0). Since  isa well-founded order, termination of the development follows.
3. By induction on , we have that any complete U -development can be simulated
by s 3  D[L; l] !D[L!R;l!r] D[R; r] !3! t, so any resulting term is equal to t.
In the case of CCHORSs, we must ascertain that s0 3  D0 [L0] in the second
item is an extraction of a set of redexes. To do that, it is enough to show that eachoccurrence of holes in D0 [ ] satis es the context condition (see De nition 32).
From the de nition, each occurrence of holes in D[ ; l] satis es the context condition. Successively, in D[ ; r] from 1 of Lemma 29, in E [ ] from 2 of Lemma 29 andin D0 [ ] from Lemma 27, each occurrence of holes satis es the context condition.
Remark. As is pointed out in [vO94], to be rigorous, we must show that the result
does not depend on the choice of the rst rewrite step in 1 in the above proof. In
fact, from Lemma 29, D[L; l] can reach D[R; r ] by the replacements in any order.
Theorem 38. A non-overlapping left-linear CCHORS has the Church-Rosser property.

Proof

By Lemma 36 and Lemma 37.

5 Unique Normal Form Property of HORS

In this section we present a new sucient condition for the unique normal form property of a pattern HORS based on the result in the previous section. This condition
requires neither left-linearity nor termination of the pattern HORS.
De nition 39. Suppose that a free variable x appears n times in a term l (n  1).
Let y1; 111 ; yn be a list of pairwise distinct free variables satisfying fy1 ; 111 ; yng \(Fvar(l) 0 fxg) = ; and x 2 fy1; 111 ; yn g. Then, the x-linearisation of l with
y1; 111 ; yn is obtained by replacing
each occurrence of x with y1 ; 111 ; yn from leftdef
to right. For a sequence  = x1 ; 111 ; xm of free variables and sequences Y1; : : : ; Ymof lists of free variables satisfying xi 2 Yi (i = 1; 111 ; m), the -linearisation of l with
Y1 ; 111 ; Ym is the x1-linearisation with Y1 of : : : of xm with Ym of l.
The following lemma is used to de ne the context-conditional linearisation of apattern HORS. The proof is routine.
Lemma 40. Let l0 ! r0 be a pattern rewrite rule. Let l0 of arity m0 be an x1 ; : : :; xmclosure of a term l. Then, there exists a unique term r such that r is an x1 ; : : :; xm closure of r.
De nition 41. Let @ def= l0 ! r0defbe a pattern rewrite rule. If ^l0, r^0 and Q satisfy
the following conditions, then @^ = ^l0 ! r^0 ( Q is called a Context-Conditionally
Linearised rule (CCL rule, for short) of @.
1. Let l0 of arity m be an x1 ; 111 ;xm-closure of l. Then, ^l0 is a ^-closure of ^l, where^l is the x1 ; 111 ; xm-linearisation of l with some sequences Y1 ; 111 ; Ym of lists offree variables, and ^ is the concatenation of Y1; 111 ; Ym.
2. Let r be thedefone in Lemma 40. Then, r^0 is a ^-closure of r.
3. Re-de ne ^ = y1; 111 ; ym^ . Then, Q is the sequence N1 ; 111 ; Nm de ned by:

if Yi = yj ; 111 ; yj+j , then Ni = fj; 111 ; j + j 0g (1  i  m) .
Note that r^def0 is a closed term since xi appears in Yi for i =def1; 111 ; m.
^ is called a
Let H = hA; ! ; Ri be a pattern HORS. Then, H^ = hA; !
 ; Ri
Context-Conditional Linearisation (CCL) of H if for any @ 2 R, there exists a CCL
rule @^ 2 R^ of @.
Any CCL is apparently left-linear from the de nition.
Example 1. For a pattern rewrite rule @ : :D( )( ) ! :E( ), the following rules are
CCL rules of @:: 0 :D()( 0 ) ! :0 E( ) ( f1; 2g;
: 0 :D( )( 0) ! : 0E( 0 ) ( f1; 2g:^ denotes a CCL of a pattern HORS
In the rest of this paper, H^ def= hA; !
 ; Ridef!
H = hA;  ; Ri.
Lemma 42. !H !H^ .
Proof
If @^ : ^l0 ! r^0 ( Q 2 H^ is a CCL rule of @ : l0 ! r0 2 H, then l0 3 ; !@^3
0; !  r from the de nition. Thus, the result is clear.
Lemma 43. Suppose that H^ has the Church-Rosser property. Then, NFH  NFH^ .
Proof
Assume NFH 6 NFH^ . Let size(t) be the number of occurrences of symbols
in term t. Let s be a term minimal wrt. size(s) satisfying s 2 NFH 0 NFH^ .
Let u^ def= (; 0k ; @^) be an H^ -redex in s, where @^ def= ^l0 ! r^0 ( N1 ; 111 ; Nm 2 R^
is a CCL rule of u^ and k is the arity of the head symbol of ^l0 . Also, let m^ be
the arity of ^l0 . Suppose that s 3  C [^l0] is the extraction of u^. From 1 of Lemma
35, s 3(; ) C [^l0 ]. Let s0 and C 0[ ] be the terms obtained from s= and C [ ]=,respectively, by replacing all unbound occurrences of bound variables with fresh freevariables. Then, we have s0 3; C 0 [^l0], and C 0 [ ] satis es the context condition of@^ . From minimality of s, we have  = . def
Therefore, we can suppose that C [] = 2(s1) 111 (sm^ ) for some s1; : : : ; sm^ from
4 of Lemma 35. Note that there is no unbound occurrence of a bound variable ins1 ; 111 ; sm^ , and that 2 does not occur in s1 ; 111 ; sm^ since C [ ] is a linear context.
Since C [ ] satis es the context condition of @^ ,for any Nj (j = 1; 111 ; m), if Nj = fi; 111 ; i + i0g, then si $3H^ 111 $3H^ si+i .
Moreover, si 2 NF! ^ for i = 1; 111 ; m^ by 2 of Lemma 35 and minimality of s. Thus,
from the Church-Rosser property of H^ ,for any Nj (j = 1; 111 ;m), if Nj = fi; 111 ; i + i0 g, then si  111  si+i .
Then, (0k ; @) is a redex of H in s from the de nition of CCL rules, which contradicts
the assumption.
De nition 44. A pattern HORS H is strongly non-overlapping if there exists a
non-overlapping CCL of H.
0

0

H

0

Theorem 45. A strongly non-overlapping pattern HORS has the unique normal
form property.

From Theorem 1 using Lemma 42, Lemma 43 and Theorem 38.
Example 2. The untyped -calculus can be translated into a pattern HORS in thefollowing way [vO94]. First, new constant symbols abs : (o ! o) ! o and app : o !
(o ! o) are introduced in order to embed untyped -terms into T(A). Then, the-rule is translated into the following pattern rule:beta : ::app(abs(: ( )))( ) ! :: ()Moreover, let us consider the following pattern rule:D : :app(app(D)( ))( ) ! :
which is a translation of the rewrite rule Dxx ! E appearing [Klo80]. With eitherof CC rules of D in example 1, we can easily verify that a pattern HORS H with
R = fbeta; Dg is strongly non-overlapping. Therefore, H has the unique normal form
property.
Proof

6 Conclusion

We presented a sucient condition for the unique normal form property of pattern
HORSs. The condition requires neither left-linearity nor termination of the HORS.
In order to investigate it, we introduced the Context-Conditional HORS and theContext-Conditional Linearisation of HORSs, and gave a sucient condition for the
Church-Rosser property of CCHORSs.
There were some results about the unique normal form property of individual
non-left-linear and non-terminating higher-order rewriting systems, e.g. [KdV89].
We presented a decidable class of HORSs having the unique normal form property.
Concerning higher-order conditional rewriting, [KvO95] derived the Church-Rosser
property from `orthogonality', which assumed some closure property of the conditions. Also, [LS93] extended the results in [Nip91] to the conditional version.
As a future work, we would like to relax the condition of strong non-overlap. We
expect that the Church-Rosser property of CCHORSs will hold even if we weaken
the non-overlap requirement to admit trivial overlap [vO94]. This will enable us totreat fbeta; eta; Dg, where the pattern rewrite rule eta is a translation of untyped
 -rule (see example 2). But this does not imply that any HORS only with trivial
overlap has the unique normal form property. Consider a pattern HORS with thefollowing rules: 89< ::app(app(app(C)(T))())() ! :: =app(app(app(C)(F))( ))( ) ! ::
: ::
::app(app(app(C)( ))( ))( ) ! :: ;which is called Parallel Conditional [KdV90]. Though this system has only trivial
overlap, any CCL of this system has non-trivial overlap.
It would be solved either by a model-theoretic approach [dV90, KdV90], or byextending the notion of compatibility of TRSs [Che81, MO95]. The former was also

used to conclude the unique normal form property of untyped -calculus with Surjective Pairing in [KdV89], whereas the latter would give a decidable condition.

Acknowledgements
We would like to thank Vincent van Oostrom for his helpful comments, and themembers of the TRS meeting for their discussions.
References[Bar84] H. P. Barendregt, editor. The Lambda Calculus, Its Syntax and Semantics. North
Holland, 1984. revised edition.
[BK84] J. A. Bergstra and J. W. Klop. Process algebra for synchronous communication.
Information and Control, Vol. 60, pp. 109{137, 1984.
[Che81] P. Chew. Unique normal forms in term rewriting systems with repeated variables.
In the 13th STOC, pp. 7{18, 1981.
[dV90] R. C. de Vrijer. Unique normal forms for combinatory logic with parallel conditional, a case study in conditional rewriting. Technical report, Vrije universiteit,
Amsterdam, 1990.
[KdV89] J. W. Klop and R. C. de Vrijer. Unique normal forms for lambda calculas withsurjective pairing. Information and Computation, Vol. 80, pp. 97{113, 1989.
[KdV90] J. W. Klop and R. de Vrijer. Extended term rewriting systems. In CTRS '90,
pp. 26{50, 1990. LNCS 516.
[Klo80] J. W. Klop. Combinatory reduction systems, 1980. PhD thesis, Rijks universiteit
Utrecht.
[KvO95] Z. Khasidashvili and V. van Oostrom. Context-sensitive conditional expression
reduction systems. Electric Notes in Computer Science, Vol. 13,, 1995.
[LS93] C. Lora-Saenz. A theoretical framework for reasoning about program construction based on extensions of rewrite systems, 1993. PhD thesis, Universitat Kaiserslautern, Germany.
[MN94] R. Mayr and T. Nipkow. Higher-order rewrite systems and their con uence.
Technical Report I9433, Insitut fur Informatik, TU Munchen, 1994.
[MO95] K. Mano and M. Ogawa. A new proof of Chew's theorem. In Theory of Rewriting
Systems and Its Application, pp. 160{177, 1995. Research report 918, RIMS,
Kyoto Univ, Kyoto.
[Nip91] T. Nipkow. Higher-order critical pairs. In LICS, pp. 342{349, 1991.
[TO94] Y. Toyama and M. Oyamaguchi. Church-Rosser property and unique normal
form property of non-duplicating term rewriting systems. In CTRS '94, pp. 316{
331, 1994.
[vO94] V. van Oostrom. Con uence for abstract and higher-order rewriting, 1994. PhD
thesis, Vrije universiteit, Amsterdam.
[vOvR94] V. van Oostrom and F. van Raamsdonk. Weak orthogonality implies con uence:
The higher-order case. In 3rd Int. sympo. on Logical Foundations of Computer
Science, pp. 379{392, 1994.
[vR96] F. van Raamdonk. Con uence and normalisation of higher-order rewriting, 1996.
PhD thesis, Vrije universiteit, Amsterdam.
[Wol93] D. A. Wolfram. The Clausal Theory of Types. Cambridge University Press, 1993.
This article was processed using the LaTEX macro package with LLNCS style