[The University of Leicester]

Department of Mathematics & Computer Science



Next: Reduction and critical pairs Up: paper10 Previous: Presentations of Kan Extensions

Rewriting for Kan Extensions

The main result of the paper defines rewriting procedures on the $ P\Delta$-set

$\displaystyle T:= \bigsqcup_{B \in {\mathrm{ Ob}}\Delta} \bigsqcup_{A \in {\mathrm{ Ob}}\Gamma} XA \times P\Delta(FA,B). $

Two kinds of rewriting are involved here. The first is the familiar $ x\vert ulv \to x\vert urv$ given by a relation $ (l,r)$. The second derives from a given action of certain words on elements, so allowing rewriting $ x\vert F(a) v \to x \cdot a\vert v$. Further, the elements $ x$ and $ x \cdot a$ may belong to different sets. When such rewriting procedures complete, the associated normal form gives in effect a computation of what we call the Kan extension defined by the presentation.

Theorem 3.1   Let $ \mathcal{P}=kan \langle \Gamma \vert \Delta \vert RelB \vert X F \rangle $ be a Kan extension presentation, and let $ \mathsf{P}$, $ T$, $ R=(R_\varepsilon , R_K)$ be defined as above. Then the Kan extension $ (K,\varepsilon )$ presented by $ \mathcal{P}$ may be given by the following data:
i)
the set $ \bigsqcup_B KB = T/ \stackrel{*}{\leftrightarrow }_R$,
ii)
the function $ \overline {\tau}:\bigsqcup_B KB \to {\mathrm{ Ob}}\mathsf{B}$ induced by $ \tau:T \to {\mathrm{ Ob}}\mathsf{P}$,
iii)
the action of $ \mathsf{B}$ on $ \bigsqcup_B KB$ induced by the action of $ \mathsf{P}$ on $ T$,
iv)
the natural transformation $ \varepsilon $ determined by $ x \mapsto [x\vert i\!d_{FA}]$ for $ x \in XA, \;A \in {\mathrm{ Ob}}\mathsf{A}$.


Subsections
Next: Reduction and critical pairs Up: paper10 Previous: Presentations of 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.