束縛そくばくと自由変数じゆうへんすうの基本きほん

1導入どうにゅう

この講義こうぎでは、λ項こうの構文こうぶんを定義ていぎし、変数へんすうの各かく出現しゅつげんを束縛出現そくばくしゅつげんまたは自由出現じゆうしゅつげんに分類ぶんるいする。変数名へんすうめいだけでは分類ぶんるいできず、その出現位置しゅつげんいちと束縛子そくばくしの作用域さよういきが必要ひつようである。

2構文こうぶんと構文木こうぶんぎ

可算無限かさんむげんな変数集合へんすうしゅうごうを $\text{[PARSE ERROR: Undefined("Command("mathcal")")]}V$\mathcal V とする。型かたなしλ項こうの集合しゅうごう $\mathrm{\Lambda }$\Lambda は次つぎの生成規則せいせいきそくで再帰的さいきてきに定義ていぎする。

$x$x は変数へんすう、$MN$M\;N は適用てきよう、$\lambda x.M$\lambda x.M はλ抽象ちゅうしょうである。括弧かっこを省略しょうりゃくするとき、適用てきようは左結合ひだりけつごうとし、λ抽象ちゅうしょうの本体ほんたいは可能かのうな限かぎり右みぎまで延長えんちょうする。したがって $MNP=\left(MN\right)P$M\;N\;P=(M\;N)\;P であり、$\lambda x.MN=\lambda x.\left(MN\right)$\lambda x.M\;N=\lambda x.(M\;N) である。

3束縛子そくばくし・作用域さよういき・出現しゅつげん

$\lambda x.M$\lambda x.M の $\lambda x$\lambda x を $x$x の束縛子そくばくしbinder、部分項ぶぶんこう $M$M をその作用域さよういきscopeという。構文木こうぶんぎにおける変数へんすう $x$x の葉はの出現しゅつげんが、ある $\lambda x$\lambda x の本体ほんたいに含ふくまれるとき、その出現しゅつげんは束縛そくばくされる。該当がいとうする束縛子そくばくしが複数ふくすうある場合ばあいは、構文木上こうぶんぎじょうで最もっとも近ちかい束縛子そくばくしがその出現しゅつげんを束縛そくばくする。いずれの $\lambda x$\lambda x の作用域さよういきにも属ぞくさない $x$x の出現しゅつげんは自由じゆうである。

「束縛そくばくされる」という性質せいしつは変数名へんすうめいでなく出現しゅつげんに属ぞくする。例たとえば

では、左端さたんの $x$x は自由出現じゆうしゅつげんであり、右端うたんの $x$x は内側うちがわの $\lambda x$\lambda x による束縛出現そくばくしゅつげんである。また

では、内側うちがわの本体ほんたいにある $x$x は内側うちがわの束縛子そくばくしに、最後さいごの $x$x は外側そとがわの束縛子そくばくしに束縛そくばくされる。この現象げんしょうを遮蔽しゃへいshadowingという。

4自由変数集合じゆうへんすうしゅうごう

$\mathrm{F}\mathrm{V}\left(M\right)$\mathrm{FV}(M) は $M$M に自由出現じゆうしゅつげんを持もつ変数名へんすうめいの集合しゅうごうであり、構文こうぶんに沿そって次つぎのように定義ていぎする。

例たとえば、

$\mathrm{F}\mathrm{V}\left(M\right)=\text{[PARSE ERROR: Undefined("Command("varnothing")")]}$\mathrm{FV}(M)=\varnothing である項こうを閉項へいこうclosed term、それ以外いがいを開項かいこうopen termという。閉項へいこうであることは、変数へんすうの各出現かくしゅつげんがいずれかの束縛子そくばくしに束縛そくばくされることと同値どうちである。

5確認かくにん

$M=\lambda x.\left(x\right(\lambda y.xy\left)z\right)$M=\lambda x.(x\;(\lambda y.x\;y)\;z) では、二ふたつの $x$x の出現しゅつげんは外側そとがわの $\lambda x$\lambda x に束縛そくばくされ、$y$y の出現しゅつげんは $\lambda y$\lambda y に束縛そくばくされ、$z$z の出現しゅつげんだけが自由じゆうである。したがって $\mathrm{F}\mathrm{V}\left(M\right)=\left\{z\right\}$\mathrm{FV}(M)=\{z\} である。次つぎの講義こうぎでは、この出現しゅつげんごとの分類ぶんるいを用もちいて捕縛ほばくを回避かいひする置換ちかんを定義ていぎする。

6関連かんれんリンク