ロジックを勉強していたら誰もが(?)出くわす束縛変数の名前の付け替えのやつをまとめたいのよ。
以下のことを書いていて気づいたのだが、"Basic Proof Theory*1"(以下:BPT)には式 expressions や論理式 formulas の定義がない。subformulas の定義はあるので論理式の定義は暗になされているのだろうが、式はどうだろう。論理式を式に含めてよいのかどうか今のところハッキリとはわからない。もうちょっとちゃんと読み進めないと。しかしどうも含めていそうなので、以下では式の例として論理式を使っています。論理式や項 term の総称が式じゃないかなと。
BPSの3ページにこんなお約束が出てくる。
式 と が束縛変数の名前のみで異なるならば、これらを同一視する。
例えば と は同じということである。ではここで言っている同じとはどういう同じなのか。
と は見るからに同じであるが、この同じを literal identity といって と書きましょうというのがBPTのいちばん最初に出てくるお約束のうちのひとつである(2ページ)。 と の同じはα同値(α-equivalence)という。literal identity よりもおおらかな同じである*2が、議論をしやすくするためにここまでを同じとしようということである。ある式の束縛変数の名前を付け替えて別の式を作る操作は二項関係とみなせるし同値関係である。α同値を同じとみなすというのことは、我々はα同値による式の同値類およびそれらの集合である商集合に着目するというわけだ。上の例の同値類は となる。ただしアルゴリズムの実行とかそういう立場で考えると名前の付け替えを無視できない、という注意も書かれている。
この同じを認めると代入の議論がしやすくなる。代入というのは基本的には
式 の変数 に式 を代入するとは、 の自由出現を で置き換えること。
なのだが、条件として
もしくは
代入の定義に束縛変数の名前の付け替え操作も加える。
というのが必要となる(このあたりはBPSからの正確な引用ではないです。こちらでかなりイジってます)。式の意味(?)が変ってきてしまうからである。前者の条件が満たされれば後者は必要ないし後者が満たされれば前者は必要ない。しかしBPSの定義では束縛変数の名前の付け替えをしても式は変わらないので、前者の条件を満たすように適当に名前を付け替えればよいわけである。なので一般性を失わず*4代入はいつでも可能。
例。 の に を代入する。しかしこのまま を で置き換えてしまうと となり の が束縛されてしまって話が違う*5。なので予め束縛変数の名前を付け替えて とする。こうしても同じである。これに代入を実行すると となって事なきを得る。
また、この他の効能として、量化子のすぐ後の変数を量化子の出現ごとに変えられたりとか*6、束縛変数の集合と自由変数の集合を互いに素にできるというのも挙げられている(4ページ)。これらはメタ定理の証明やそれを使った証明の分析をする際に便利であると思われる。前者の例はたとえば と は同じということ。後者の例としては、 という論理式の束縛変数を見ても自由変数を見てもどちらにも が入っていてややこしいがこれと同じである にすれば束縛変数と自由変数に被りはない、というのが挙げられる。