A new proof of Chew's theorem(Theory of Rewriting Systems and Its Applications)
Ken Mano, Mizuhito Ogawa · Institutional Repositories DataBase (IRDB) · 1995
We present a new proof of Chew's theorem, which states that normal forms are unique up to conversion in compatible term rewriting systems.$\mathrm{L}\mathrm{e}\mathrm{t}arrow$ be an abstract reduction system that is a binary relation on some underlying domain.The symmetric closure, the reflexive transitive closure, and the reflexive transitive symmetric closure $\mathrm{o}\mathrm{f}arrow$ are written $\mathrm{a}\mathrm{s}rightarrow,$ $arrow^{*}$ and $rightarrow^{*}$ , respectively.If there is no $a'$ such that $aarrow a'$ , then $a$ is a normal form of the reduction system.A sequence $a_{1}rightarrow\cdotsrightarrow a_{n}$ is called a proof.A subsequence of the form $a'arrow aarrow a"$ is called a peak.A reduction $\mathrm{s}\mathrm{y}\mathrm{s}\mathrm{t}\mathrm{e}\mathrm{m}arrow$ has the unique normal form property (UN) if $arightarrow^{*}a'\Rightarrow a\equiv a'$ for each pair of normal forms $a,$ $a'$ .We say-has the Church-Rosser property $(\mathrm{C}\mathrm{R})$ if, for any $arightarrow^{*}a'$ , there exists $b$ such that $aarrow^{*}b$ and $a'arrow^{*}b$ .Let $F$ be a set of function symbols, and let $V$ be a countably infinite set of variables.The set of all terms built from $F$ and $V$ is defined as usual.The set of variables occurring in a term $t$ is denoted by $V(t)$ .Let $\square$ be a fresh special constant symbol.A context $C[]$ is a term in $F\cup\square$ and $V$ .When $C[]$ is a context with $n\square ' \mathrm{s}$ and $t_{1},$ $\cdots,$ $t_{n}$ are terms, $C[t_{1}, \cdots, t_{n}]$ denotes the term obtained by replacing all $\square$ in $C[]$ with $t_{i}$ in a left-to-right manner.Let $t$ be terms $\mathrm{s}.\mathrm{t}$ .$t\equiv C[s1$ with a context $C[]$ and a non-variable term $s$ .If $s$ and $t'$ are unifiable with a most general unifier $\theta$ , then $C[s\theta]$ is called a superposition of $t$ and $t'$ .Positions of a term are encoded in the sequences of natural numbers.The set of positions of a term $t$ is denoted by $P(t)$ .For a position $p\in P(t),$ $t/p$ is the subterm occurring at $p$ in $t$ .For terms $t,$ $s$ and a position $p\in P(t),$ $t|parrow s]$ is the term obtained by replacing the subterm at $p$ in $t$ with $s$ .ForThe longest common prefix of $p_{1}$ and $p_{2}$ is denoted by $\wedge(p_{1},p_{2})$ .A term rewriting system (TRS) is a finite set $R$ of rewrite rules.A rewrite rule is a pair of terms denoted by $larrow r$ satisfying (1) $l$ is not a variable and (2) $V(l)\supseteq V(r)$ .The reduction $\mathrm{s}\mathrm{y}\mathrm{s}\mathrm{t}\mathrm{e}\mathrm{m}arrow R$ on the set of terms is defined from a TRS $R$ as follows: $arrow R=$ { $C1^{l}\theta]arrow {}_{R}C[r\theta]|C[]$ is a context, $\theta$ is a substitution, and $larrow r\in R$ }.A term $l\theta$ is called a redex of $R$ if $larrow r\in R$ .For a reduction $\alpha$ : $C[l\theta]{}_{arrow R}C[r\theta]$ , the position of the redex $l\theta$ in $C[l\theta]$ is denoted by $p(\alpha)$ .When we think of a pair of rules $S$ and $S'$ , we assume that $S$ and $S'$ are standardized apart, i.e., the variables in $S$ and $S'$ are renamed appropriately so that $S$ and $S'$ do not share variables.Let $C[]$ be a context with $n\square ' \mathrm{s}$ , and let $t_{i}rightarrow^{*}t'Ri$ be proofs in $R$ for $1\leq i\leq n$ .The embedding of the proofs into $C[]$ is the following:Rewrite rules $S$ and $S'$ are overlay if a superposition of $l$ and $l'$ exists only in a root-to-root case, i.e., the context $C[]$ in the definition of superposition is $\square$ .If $S$ and $S'$ are overlay and $r\sigma\equiv r'\sigma$ for all unifiers a of $l$ and $l'$ , then $S$ and $S'$ are almost non-overlapping.Definition 2.1 A term $\overline{t}$ is a linearization of a term $t$ if (1) $\overline{t}$ is linear, and (2) there is a substitution a $\mathrm{s}.\mathrm{t}$ .$\overline{t}\sigma=t$ and $x\sigma\in V$ for all $x\in V$ .For a rewrite rule $larrow r,\overline{l}arrow\overline{r}$ is called a linearization of $larrow r$ , if the following properties hold: .$\overline{l}$ is a linearization of $l\mathrm{s}.\mathrm{t}.\overline{l}\sigma=l$, and .$\overline{r}\sigma=r$ .Definition 2.2 ([Che81, clV90]) Rewrite rules $S$ and $S'$ are said to be compatible3 if there exist $1\mathrm{i}\mathrm{n}\mathrm{e}\mathrm{a}\mathrm{r}\mathrm{i}\mathrm{z}\mathrm{a}\mathrm{t}\mathrm{i}_{0}11\mathrm{s}$ $\overline{S},\overline{S}'$ of S. $S'$ such that $\overline{S}$ and $\overline{S}'$ are almost non-overlapping.A TRS $R$ is colnpatible if each pair of rules is compatible.3 De Vrijel's terminology $[\iota 1\mathrm{V}90]$ is usecl llele.Tlle corresponding notion in Chew's $01\mathrm{i}\mathrm{g}\mathrm{i}_{1}1\mathrm{a}\iota$ }) $\mathrm{a}\mathrm{p}\mathrm{e}\iota$ is $' \mathrm{s}\uparrow_{1}\mathrm{o}\mathrm{n}\mathrm{g}$ ] $\mathrm{y}\mathrm{I}\mathrm{l}\mathrm{C}$ ) $11-\mathrm{O}\mathrm{V}\mathrm{e}1$ ] $\mathrm{a}_{\mathrm{I})]}$ ) $\mathrm{i}\mathrm{n}\mathrm{g}$ a $11(|$ compatible".