無型むがたλ計算けいさんの基本きほん

1導入どうにゅう

この講義こうぎでは、無型むがたλ計算けいさんの構文こうぶんとβ簡約かんやくを説明せつめいする。置換ちかんによる変数捕獲へんすうほかくを回避かいひするため、自由変数じゆうへんすうとα同値どうちをβ簡約かんやくより先さきに確認かくにんする。ここでは型判断かたはんだんを導入どうにゅうしない。

21. 構文こうぶんと結合規則けつごうきそく

変数へんすうの集合しゅうごうを可算無限集合かさんむげんしゅうごうとする。λ項こう $t$t は次つぎの文法ぶんぽうで帰納的きのうてきに定義ていぎする。

$\lambda x.t$\lambda x.t は $x$x を束縛そくばくするλ抽象ちゅうしょう、$ts$t\;s は適用てきようである。適用てきようは左結合ひだりけつごうであり、λ抽象ちゅうしょうの本体ほんたいは可能かのうな限かぎり右みぎへ延長えんちょうする。したがって、$tuv=\left(tu\right)v$t\;u\;v=(t\;u)\;v、$\lambda x.tu=\lambda x.\left(tu\right)$\lambda x.t\;u=\lambda x.(t\;u) である。

32. 自由変数じゆうへんすうとα同値どうち

自由変数集合じゆうへんすうしゅうごう $\mathrm{F}\mathrm{V}\left(t\right)$\mathrm{FV}(t) を次つぎで定義ていぎする。

束縛変数そくばくへんすうの一貫いっかんした改名かいめいだけが異ことなる項こうをα同値どうちとする。たとえば、$\lambda x.x{=}_{\alpha }\lambda z.z$\lambda x.x =_\alpha \lambda z.z である。ただし、$z$z が本体ほんたいで自由じゆうに出現しゅつげんする場合ばあい、$x$x を $z$z に改名かいめいできない。

43. 捕獲回避置換ほかくかいひちかん

$t[x:=s]$t[x:=s] は、$t$t における $x$x の自由出現じゆうしゅつげんを $s$s で置換ちかんする項こうである。$$x\notin \mathrm{F}\mathrm{V}\left(t\right)$$x\notin\mathrm{FV}(t) なら $$t[x:=s]=t$$t[x:=s]=t とする。変数へんすうと適用てきようでは構造こうぞうに沿そって定義ていぎし、λ抽象ちゅうしょうでは次つぎの条件じょうけんを用もちいる。

最後さいごの場合ばあいでは、$t$t と $s$s のどこにも出現しゅつげんせず、$x$x とも異ことなる新あたらしい変数へんすう（fresh variable）$z$z を選択せんたくする。たとえば、$(\lambda y.x)[x:=y]$(\lambda y.x)[x:=y] をそのまま $\lambda y.y$\lambda y.y とすると、置換項ちかんこうの自由変数じゆうへんすう $y$y が捕獲ほかくされる。先さきにα改名かいめいして、$(\lambda y.x)[x:=y]{=}_{\alpha }(\lambda z.x)[x:=y]=\lambda z.y$(\lambda y.x)[x:=y]=_\alpha(\lambda z.x)[x:=y]=\lambda z.y とする。

54. β簡約かんやくと正規形せいきけい

$(\lambda x.t)s$(\lambda x.t)\;s という部分項ぶぶんこうをβ簡約基かんやくきといい、捕獲回避置換ほかくかいひちかんによって次つぎのように簡約かんやくする。

項こうの任意にんいの位置いちにあるβ簡約基かんやくきを一段いちだん簡約かんやくできる。β簡約基かんやくきを含ふくまない項こうをβ正規形せいきけいという。

一方いっぽう、$\mathrm{\Omega }=(\lambda x.xx)(\lambda x.xx)$\Omega=(\lambda x.x\;x)(\lambda x.x\;x) のβ簡約基かんやくきは項全体こうぜんたいだけであり、その簡約かんやくは $\mathrm{\Omega }{\to }_{\beta }\mathrm{\Omega }$\Omega\to_\beta\Omega に戻もどる。したがって、どの簡約列かんやくれつもβ正規形せいきけいへ到達とうたつしない。無型むがたλ計算けいさんでは停止性ていしせいを一般いっぱんに保証ほしょうできない。

65. 評価戦略ひょうかせんりゃく

β簡約かんやくは簡約基かんやくきの選択順せんたくじゅんを規定きていしない。最左外側さいさひだりそとがわの簡約基かんやくきを選択せんたくする正規順序せいきじゅんじょと、最左内側さいさひだりうちがわの簡約基かんやくきを選択せんたくする適用順序てきようじゅんじょでは、停止挙動ていしきょどうが異ことなりうる。

正規順序せいきじゅんじょでは外側そとがわを先さきに簡約かんやくして $a$a に到達とうたつする。適用順序てきようじゅんじょでは $\mathrm{\Omega }$\Omega の簡約かんやくを反復はんぷくするため停止ていししない。これは戦略せんりゃくの停止性ていしせいの差さであり、β簡約規則かんやくきそくそのものの差さではない。β正規形せいきけいが存在そんざいする項こうについて、正規順序せいきじゅんじょはそれに到達とうたつする。

76. η変換へんかんとの区別くべつ

$x\notin \mathrm{F}\mathrm{V}\left(f\right)$x\notin\mathrm{FV}(f) のとき、$\lambda x.fx{=}_{\eta }f$\lambda x.f\;x=_\eta f とするη変換へんかんは、関数かんすうの外延的がいえんてきな同一視どういつしを表あらわす。これは関数適用かんすうてきようを実行じっこうするβ簡約かんやくとは別べつの規則きそくである。

8まとめ

無型むがたλ計算けいさんの計算けいさんは、α同値どうちを考慮こうりょした捕獲回避置換ほかくかいひちかんによるβ簡約かんやくである。正規形せいきけいの存在そんざいと、特定とくていの評価戦略ひょうかせんりゃくが停止ていしすることは区別くべつする必要ひつようがある。