[The University of Leicester]

Department of Mathematics & Computer Science



Next: Completion procedure Up: Rewriting for Kan Extensions Previous: Rewriting for Kan Extensions

Reduction and critical pairs

To work with a rewrite system $ R$ on $ T$ we will require certain concepts of order on $ T$. We give properties of orderings $ >_X$ on $ \bigsqcup_A XA$ and $ >_P$ on $ \mathrm{Arr}\mathsf{P}$ to enable us to construct an ordering $ >_T$ on $ T$ with the properties needed for the rewriting procedures. Given an admissible well-ordering $ >_T$ on $ T$ it is possible to discuss when a reduction relation generated by a rewrite system is compatible with this ordering. It is a standard result that if a reduction relation is compatible with an admissible well-ordering, then it is Noetherian. A Noetherian reduction relation on a set is confluent if it is locally confluent (Newman's Lemma [16]). By standard abuse of notation the rewrite system $ R$ will be called complete when $ \to_R$ is complete. Hence, if $ R$ is compatible with an admissible well-ordering on $ T$ and $ \to_R$ is locally confluent then $ \to_R$ is complete. By orienting the pairs of $ R$ with respect to the chosen ordering $ >_T$ on $ T$, $ R$ is made to be Noetherian. The problem remaining is testing for local confluence of $ \to_R$ and changing $ R$ in order to obtain an equivalent confluent reduction relation. We explain the notion of critical pair for a rewrite system for $ T$, extending the traditional notion to our situation. In particular the overlaps involve either just $ R_T$, or just $ R_P$ or an interaction between $ R_T$ and $ R_P$.

A term $ crit\in T$ is called critical if it may be reduced by two or more different rules. A pair $ (crit1,crit2)$ of distinct terms resulting from two single-step reductions of the same term is called a critical pair. A critical pair for a reduction relation $ \to_R$ is said to resolve if there exists a term $ res$ such that both $ crit1$ and $ crit2$ reduce to a $ res$, i.e. $ crit1 \stackrel{*}{\to}_R res$, $ crit2 \stackrel{*}{\to}_R res$. If $ t=x\vert b_1 \cdots b_n$, then a part of $ t$ is either a term $ x\vert b_1 \cdots b_i$ for some $ 1 \leqslant i \leqslant n$ or a word $ b_i b_{i+1} \cdots b_j$ for some $ 1 \leqslant i \leqslant j \leqslant n$. Let $ (rule1,rule2)$ be a pair of rules of the rewrite system $ R=(R_T,R_P)$ where $ R_T \subseteq T \times T$ and $ R_P \subseteq \mathrm{Arr}\mathsf{P}\times \mathrm{Arr}\mathsf{P}$. Then the rules are said to overlap when $ rule1$ and $ rule2$ may both be applied to the same term $ t$ in such a way that there is a part $ c$ of the term that is affected by both the rules. There are five types of overlap for this kind of rewrite system, as shown in the following table:


# rule1 in rule2 in overlap critical pair
(i) $ (s_1,u_1)$ $ R_T$ $ (s_2,u_2)$ $ R_T$ $ s_2=s_1\cdot q$ for some $ q \in \mathrm{Arr}\mathsf{P}$ $ (u_1\cdot q,u_2 )$
(ii) $ (l_1, r_1)$ $ R_P$ $ (l_2,r_2)$ $ R_P$ $ l_1=pl_2q$ for some $ p,q \in \mathrm{Arr}\mathsf{P}$ $ (r_1,pr_2q)$
(iii)         $ l_1q=pl_2$ for some $ p,q \in \mathrm{Arr}\mathsf{P}$ $ (r_1q,pr_2)$
(iv) $ (s_1,u_1)$ $ R_T$ $ (l_1, r_1)$ $ R_P$ $ s_1\cdot q= s\cdot l_1$ for some $ s \in T, q \in \mathrm{Arr}\mathsf{P}$ $ (u_1\cdot q, s \cdot r_1)$
(v)         $ s_1 =s \cdot (l_1q)$ for some $ s \in T, q \in \mathrm{Arr}\mathsf{P}$ $ (u_1, s \cdot r_1q)$
Overlap table
Next: Completion procedure Up: Rewriting for Kan Extensions Previous: Rewriting for Kan Extensions

[University Home] [MCS Home] [University Index A-Z] [University Search] [University Help]

Author: A. Heyworth, tel: +44 (0)116 252 3884
Last updated: 2000-11-24
MCS Web Maintainer
This document has been approved by the Head of Department.
© University of Leicester.