[The University of Leicester]

Department of Mathematics & Computer Science



Next: Example of a GAP Up: Rewriting for Kan Extensions Previous: Reduction and critical pairs

Completion procedure

We show: (i) how to find overlaps between rules of $ R$; (ii) how to test whether the resulting critical pairs resolve; (iii) that if all the critical pairs resolve then this implies $ \to_R$ is confluent; and (iv) that critical pairs which do not resolve may be added to $ R$ without affecting the equivalence relation $ R$ defines on $ T$. We have now set up and proved everything necessary for a variant of the Knuth-Bendix procedure, which will add rules to a rewrite system $ R$ resulting from a presentation of a Kan extension, to attempt to find an equivalent complete rewrite system $ R^C$. The benefit of such a system is that $ \to_{R^C}$ then acts as a normal form function for $ \stackrel{*}{\leftrightarrow }_{R^C}$ on $ T$.

Theorem 3.2   Let $ \mathcal{P}= \langle \Gamma \vert \Delta \vert RelB \vert X \vert F \rangle $ be a finite presentation of a Kan extension $ (K,\varepsilon )$. Let $ P:=P \Delta$, $ T:= \bigsqcup_{{\mathrm{ Ob}}\Delta} \bigsqcup_{{\mathrm{ Ob}}\Gamma} XA \times \mathsf{P}(FA, B)$, and let $ R$ be the initial rewrite system for $ \mathcal{P}$ on $ T$. Let $ >_T$ be an admissible well-ordering on $ T$. Then there exists a procedure which, if it terminates, will return a rewrite system $ R^C$ which is complete with respect to the ordering $ >_T$ and such that the equivalence relations $ \stackrel{*}{\leftrightarrow }_R$, $ \stackrel{*}{\leftrightarrow }_{R^C}$ coincide.

The above procedure which attempts completion of a presentation of a Kan extension has been implemented in GAP3.

Next: Example of a GAP Up: Rewriting for Kan Extensions Previous: Reduction and critical pairs

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