日々の流転

λ. 飲み会

店員さんの裾が高めの浴衣と素足に萌え。

λ. 書き換え系について少し勉強 (「潜在帰納法と書き換え帰納法の比較」 by 小池広高 and 外山芳人)

私はどうも項書き換え系の話についてよく分かっていなくて、こないだも随分的外れなことを言ってしまった気がするので、ちょっと勉強してみようと思った。 何か短い入門的なテキストがあると良いのだけど、とりあえず手元にあった「潜在帰納法と書き換え帰納法の比較」(by 小池広高 and 外山芳人)というのを読んでみる。 以下は単なる感想で、内容の解説はない。

帰納的定理

まず、項書き換えシステムでは、帰納的定理とは任意の基底頂上で成立する等式のことを「帰納的定理」と呼ぶ。 さらっと片付けられているが、ここで少し悩んでしまった。

最初にちょっと悩んだのは、何で単に「定理」ではなくわざわざ「帰納的定理」と呼ぶのか。 任意の基底項上で成立するということはつまり始モデル(initial model)で成り立つということだけど、始モデルで成り立つ等式であっても新たな要素(junk)が加わったモデルでは成り立たない可能性があるので、帰納的定理は普通の意味での定理になっているとは限らないからか。

それから、次に悩んだのは何故「帰納的」という言葉を使うか。 ググってみると、始モデルにおける定理だからという話と、証明に一般に項の構造に関する帰納法が必要となるからという説明があるようだ。 両者は表裏の関係といっても良いので、これも納得。

潜在帰納法と書き換え帰納法

「潜在帰納法」は名前からして隠蔽代数(hidden algebra)における帰納法みたいなものだと勝手に思いこんでいたが、そうではなかった。

潜在帰納法(inductionless induction)も書き換え帰納法(rewriting induction)も、いずれも証明したい等式を追加した書き換え系が、(始モデルにおいて)元の書き換え系と同等であることを示すことによって、証明したい等式が元の書き換え系における帰納的定理であることを示す方法。

とりあえず、定義を確認して証明を一通り追いかける。 項書き換え系に詳しくないので結果については「へー」と思うだけなのだが、項書き換え系ではではこういう議論の仕方をするのね。面白い。

退行

弱正規化性、強正規化性、合流性は馴染み深い概念だけど、退行(Retrogresse)についてはまだイメージがわかないなぁ。