Path Rewriting SystemとPR-Precategories
パス書き換え系（Path Rewriting System; PRS）は項書き換え系（TRS）の一般化。次のものから構成される。
- 0セルの集合V
- 1セルの集合E、VとEでグラフになる。
- 書き換えと呼ばれる2セルの集合
- 書き換えの結合（合成）と代数的な法則
f, g, hなどが1セルだととして、隣接する（グラフの意味で）で1セルの列[f, g, h]などをパスと呼ぶ。パスに含まれる1セルの個数を長さとする。[]は長さ0のパス、[f]は長さ1のパス。書き換えα:F⇒G は、共端（バエズの用語では平行）なパスF, Gのあいだを結ぶ。Fの長さ=n, Gの長さ=m もとき、αをn-m書き換えと呼ぶ。
2セルである書き換え達の反射的推移的閉包を考える。この閉包の2セルも書き換えと呼ぶ。αがFからGへの広義の書き換えのとき、α:F⇒* G と書く。
F, Gが共端なパスとして、α:F⇒* G、β:G⇒* G があるとき、F≡G と書いて、FとGは合同と呼ぶ。α:F⇒* H、β:G⇒* H となるα, β, Hがあるとき、F〜G と書いて、FとGはj弱合同と呼ぶ。書き換え系が合流性を持つなら、弱合同は同値関係になる。
次に、特殊なパス書き換え系を考える。書き換えは、0セル（の一部）でインデックスされた1-0書き換えと、長さ2のパス（の一部）でインデックスされた2-1書き換えが与えられている。これをもとに、長さnのパス（の一部）に対して、n-(n-1)書き換えが構成できる。この書き換えに基づいて、弱合同を定義できる。このとき、
- 最初に与えられて書き換えの集合は、単位律と結合律を満たす。
- 弱合同は同値関係になる。
このような性質を持つPRSをPRプレ圏（PR-precategory）と呼ぶ。PRプレ圏があれば、そのパス圏を弱合同で割り算して圏を構成できる。この圏が、もとのPRプレ圏の自由圏となる。自由圏を作る関手は、ベキ等モナドになる。
