曇りなき眼で見定めブログ

学生です。勉強したことを書いていく所存です。リンクもコメントも自由です! お手柔らかに。。。更新のお知らせはTwitter@cut_eliminationで

Basic Proof Theory 読書記録 其の二 束縛変数の名前の付け替えのやつ

 ロジックを勉強していたら誰もが(?)出くわす束縛変数の名前の付け替えのやつをまとめたいのよ。

 以下のことを書いていて気づいたのだが、"Basic Proof Theory*1"(以下:BPT)には式 expressions や論理式 formulas の定義がない。subformulas の定義はあるので論理式の定義は暗になされているのだろうが、式はどうだろう。論理式を式に含めてよいのかどうか今のところハッキリとはわからない。もうちょっとちゃんと読み進めないと。しかしどうも含めていそうなので、以下では式の例として論理式を使っています。論理式や項 term の総称が式じゃないかなと。

 

 BPSの3ページにこんなお約束が出てくる。

{\mathcal E}{\mathcal E'} が束縛変数の名前のみで異なるならば、これらを同一視する。

 例えば \forall xFx\forall yFy同じということである。ではここで言っている同じとはどういう同じなのか。

 \forall xFx と \forall xFx は見るからに同じであるが、この同じを literal identity といって \forall xFx \equiv \forall xFx と書きましょうというのがBPTのいちばん最初に出てくるお約束のうちのひとつである(2ページ)。\forall xFx\forall yFy同じα同値(α-equivalence)という。literal identity よりもおおらかな同じである*2が、議論をしやすくするためにここまでを同じとしようということである。ある式の束縛変数の名前を付け替えて別の式を作る操作は二項関係とみなせるし同値関係である。α同値を同じとみなすというのことは、我々はα同値による式の同値類およびそれらの集合である商集合に着目するというわけだ。上の例の同値類は \{\forall xFx, \forall yFy, \forall zFz, ...\} となる。ただしアルゴリズムの実行とかそういう立場で考えると名前の付け替えを無視できない、という注意も書かれている。

 この同じを認めると代入の議論がしやすくなる。代入というのは基本的には

式 {\mathcal E} の変数 x に式 {\mathcal E'} を代入するとは、 x の自由出現を {\mathcal E'} で置き換えること。

 なのだが、条件として

{\mathcal E'} 中のどの自由変数も {\mathcal E'} の変数束縛する演算子*3で束縛されてはならない。

もしくは

代入の定義に束縛変数の名前の付け替え操作も加える。

というのが必要となる(このあたりはBPSからの正確な引用ではないです。こちらでかなりイジってます)。式の意味(?)が変ってきてしまうからである。前者の条件が満たされれば後者は必要ないし後者が満たされれば前者は必要ない。しかしBPSの定義では束縛変数の名前の付け替えをしても式は変わらないので、前者の条件を満たすように適当に名前を付け替えればよいわけである。なので一般性を失わず*4代入はいつでも可能。

 例。\forall x(Fx \land Gy)yfx を代入する。しかしこのまま yfx で置き換えてしまうと \forall x(Fx \land Gfx) となり fxx が束縛されてしまって話が違う*5。なので予め束縛変数の名前を付け替えて \forall z(Fz \land Gy) とする。こうしても同じである。これに代入を実行すると \forall z(Fz \land Gfx) となって事なきを得る。

 また、この他の効能として、量化子のすぐ後の変数を量化子の出現ごとに変えられたりとか*6、束縛変数の集合と自由変数の集合を互いに素にできるというのも挙げられている(4ページ)。これらはメタ定理の証明やそれを使った証明の分析をする際に便利であると思われる。前者の例はたとえば \forall xFx \land \forall xGx と \forall xFx \land \forall yGy同じということ。後者の例としては、Fx \land \forall xGx という論理式の束縛変数を見ても自由変数を見てもどちらにも x が入っていてややこしいがこれと同じである Fx \land \forall yGy にすれば束縛変数と自由変数に被りはない、というのが挙げられる。

*1:

*2:何故なら \forall xFx と \forall xFx は literal identity であるうえに α同値でもあるのが、 \forall xFx\forall yFy はα同値ではあるが literal identity ではない。こういうケースがあるので。

*3:「変数束縛をする演算子はこれとこれとこれ」みたいに明記はされていないのですが、おそらく量化子とラムダ演算子と考えておけばよいかと。

*4:これがよくわからないんすよ。

*5:Gfx って見にくいけどBPSノーテーションだとこんな感じです。

*6:冒頭の"式"に対する疑問ですが、ここで量化子の例が挙げられているのでたぶん論理式も含みます。