"Modular confluence modulo" (Jean-Pierre Jouannaud)

東北大の富山先生による、項書き換え系の有名な定理：二つのconfluentな項書き換え系で、関数記号や定数記号を共有しないものは modularity を持つ、の前提条件を減らして証明した、という話。Terminationする場合は簡単だが、もちろんTerminationしない場合が難しい。そのためorderを導入し、そして最初に"cleaning lemma"によってreductionが壊れる場合に対処する。おもしろかったですが、orderの話の途中で集中力が一回切れました。
ところで、J氏はフランス人の大家ですが、何故かところどころ英語が Dr. Strangeloveそっくりに聞こえてしまい、話に集中しにくかったのは秘密だ。