ラムダ計算 #2 簡約 - 気まぐれエンジニア日記

ラムダ計算セルフブログリレー(今命名)2日目です. 今日も平常運転, くまちゃんです. 1日目はこちら
kumachan-math.hatenablog.jp

はてなブログにはカテゴリーなるものがあって記事を分類できるらしいことがわかったので, カテゴリ名に「ラムダ計算」とつけてみました. センスのかけらもありませんね. まあそんなもんです.

どうでもいいんだけど, 記事のカテゴリ分類を自動でやってカテゴリを振ってくれたりしないかなって思ったりしました. それただのクラシフィケーションの問題ですね. というか絶対誰かやってるでしょ. ブログはみんな書いてるからデータと正解ラベルあるし, なんなら勝手にデータ増えていくから研究はしやすそうよね. 最初と最後の方にテーマやまとめとしてカテゴリ名に関連する単語が出て来やすいとかで特徴量取れるだろうし, ディープラーニングなんて重い処理しなくても解けそう.
まあ愚痴はこの辺にしておきましょうか.

昨日は, 変数やラムダ式とはなんぞやというもの定義したので, 今日から本題です. 簡約を扱います.

簡約とは, いわゆる計算を進めていく操作, 評価のことです. 5 + 3を8に置き換えるのは簡約と言えるし, 階乗関数 $f(n)$ を $n \times f(n-1)$ に置き換えるのも簡約です. まず1番最初は, 何らかのラムダ式の簡約 $L \to L'$ ができたとすると, それが全体のラムダ式にどのように作用するのかということを推論規則として定めておきます.

定義2.1. 簡約の推論規則
$V$ を変数全体の集合, $\Lambda$ をラムダ式全体の集合とする. $L, L', M, M' \in \Lambda$ , $x \in V$ とする.
$\displaystyle \frac{L \to L'}{LM \to L'M} ~~~~~~~~ \frac{L \to L'}{ML \to ML'} ~~~~~~~~ \frac{L \to L'}{\lambda x.L \to \lambda x.L'}$

1つ目と2つ目の規則から, ラムダ式が連接している時には, 右から評価しても左から評価しても良い, つまりどんな順番で評価しても良いということをいっています. これにより, ラムダ式の評価の仕方には任意性があることがわかります. これについては後述します. 3つ目の推論規則は, 束縛変数を持つラムダ式は, その中身だけを独立に評価するということを言っています.

次に, $\lambda x.L$ なるラムダ式のイメージを定式化します. このラムダ式はイメージ的には変数 $x$ を引数にとってラムダ式 $L$ を返す関数といったような感じです. それを式で表したのが $\beta$ 簡約です.

定義2.2 $\beta$ 簡約と代入
$V$ を変数全体の集合, $\Lambda$ をラムダ式全体の集合とする. $L, M \in \Lambda$ , $x \in V$ とする.
$\displaystyle (\beta)~~ \overline{(\lambda x.L)M \to L [x \mapsto M]}$

これを日本語にすると, 「束縛変数 $x$ を持つラムダ式 $L$ に別のラムダ式 $M$ を作用させることは, $L$ の中の $x$ を $M$ に置き換えることで評価できます」となります. これによって, 束縛変数への「代入」なる概念が定義できたことになります.

次に, 束縛変数の名前を変更しても良いということを $\alpha$ 変換として定めておきます.

定義2.3 $\alpha$ 変換と変数名変更
$V$ を変数全体の集合, $\Lambda$ をラムダ式全体の集合とする. $L \in \Lambda$ , $x \in V$ , $y \notin FV(L)$ とする.
$\displaystyle (\alpha)~~ \overline{\lambda x.L \to \lambda y.L[x \mapsto y]}$

これは例えば, $f(x) := x$ と $g(y) := y$ は相互に変更できるべきだということを言っています. 今まで $x$ と呼んでいた引数名を新しく $y$ と名前を変えたとしても, 何ら問題はないということです. これは計算を進める簡約ではないので, 変換と呼ばれます. ただし, $f(x) = ax + b$ のように自由変数を含む関数の場合, これは $g(a) := a\cdot a + b$ とは異なることに注意しなければいけません.

さて, 今まで $L[x \mapsto M]$ なんていう記号をさらっと使っていましたが, これは当然未定義記号です. ここで定義しておきます.

定義2.4. $L[x \mapsto M]$
$V$ を変数全体の集合, $\Lambda$ をラムダ式全体の集合とする.

$\displaystyle \forall x, y \in V, \forall L \in \Lambda, x [y \mapsto L ] := \begin{cases} L& x \equiv y \\ x & x \not\equiv y \end{cases}$

$\displaystyle \forall x, y \in V, \forall L, M \in \Lambda, (\lambda x.L)[y \mapsto M ] := \begin{cases} L& x \equiv y \\ \lambda x.L[y \mapsto M] & x \not\equiv y \land x \notin FV(M) \\ (\lambda z.L[x \mapsto z])[y \mapsto M] & \mathrm{otherwise} ~~ただし, z \notin FV(L) \cup FV(M) \\ \end{cases}$

$\displaystyle \forall y \in V, \forall L, M, N \in \Lambda, (LM)[y \mapsto N] := (L[y \mapsto N])(M[y \mapsto N])$

1番目, 3番目のルールは特に説明する必要はないでしょう. 2番目のルールは少し複雑です.

$y$ が束縛変数なら, それをどんなラムダ式に変えても意味がありません. 例えば. $f(x) = ax + b$ の $x$ という名前を今勝手に $pqr$ とかして $f(p, q, r) = a\cdot pqr + b$ としても関数の意味は変わりませんよね.

次に $y$ が自由変数であって, 変更先のラムダ式 $M$ の自由変数の中に束縛変数 $x$ が含まれていないなら, 中身のラムダ式の $y$ だけをそのまま $L$ に置き換えても良いです. 例えば, $f(x) = ax + b$ の $a$ を $c$ に変えた場合は, $ax + b$ の部分を $cx + b$ に変えればいいですが, $a$ を $x$ に変えてしまうと $f(x) = x^2 + b$ になってしまって意味が変わってしまいますよね.

この意味が変わってしまう場合, すなわち, $L$ のなかの自由変数 $y$ を $M$ に置き換えたいんだけれど, $M$ のなかに束縛変数 $x$ が含まれてしまっていたら, どうしたらいいでしょうか. この場合は簡単です. 今まで $x$ と呼んでいた束縛変数を, 今相手にしているラムダ式たちと全く関係のない新しい名前 $z$ に呼び直してしまえばいいのです. $z$ は全く関係のない名前でなければいけない, というのが
「ただし, $z \notin FV(L) \cup FV(M)$ 」
の部分に含まれています.

次に, $\eta$ 簡約と $\eta$ 展開について触れておきます. これは関数は入力となる引数のラムダ式と出力となるラムダ式が全て等しければ互いに変換できて良いだろうというルールです.

定義2.5 $\eta$ 簡約と $\eta$ 展開, 外延的等しさ
$V$ を変数全体の集合, $\Lambda$ をラムダ式全体の集合とする. $L \in \Lambda$ , $x \in V\backslash FV(L)$ とする.
$\lambda x. Lx \leftrightarrow L$
を $\eta$ 簡約, $\eta$ 展開という.

$M \in \Lambda$ を勝手に１つ取るとき,
$(\lambda x. Lx)M \to (L[x \mapsto M])(x[x \mapsto M]) \to LM$ ( $\because x \notin FV(L)$ )
また,
$(L)M \equiv LM$
となるので,
$(\lambda x. Lx)M \leftrightarrow (L)M$
を得ます. 引数となる $M$ は, ラムダ式でさえあればなんでも良いのですから, このなんでもいい引数を取り去ってしまって, $\lambda x. Lx$ と $L$ 自体を相互に変換できると考えても良いのではないか, というのが $\eta$ 簡約と $\eta$ 展開です.
言い直すと, どんな引数に対してもそれぞれ返り値が等しいのだから, 関数として相互に変換できて良いのではないかということです. この忌避数と返り値のペアが等しいという外延的等しさを認めるのが $\eta$ 簡約と $\eta$ 展開です.

さて, 簡約( $\to$ )が定義できたので, 2つのラムダ式が等しい( $=$ )という概念を定義できます.

定義2.6. ラムダ式の等しさ
ラムダ式の間の関係 $=$ を $(\rightarrow \cup \leftarrow)^*$ で定める. すなわち2つのラムダ式 $L$ と $M$ が等しいとは, $L$ に対して簡約とその逆操作である展開を施して $M$ にできることである.

例:2.7 等しいラムダ式
$(\lambda xy. xycd)ab = (\lambda x.cd)(ab)$
証明:
$(\lambda xy. xycd)ab \rightarrow (\lambda y.aycd)b \rightarrow abcd \leftarrow (\lambda x.xcd)(ab)$

ここまで簡約について, 色々とやってきましたが, 簡約を進めていくといずれこれ以上簡約できない形になることが予想できます. これを正規形といいます.

ところが, どれだけ頑張って簡約をしていったとしても, 正規系にならないラムダ式も存在します. すなわち簡約が無限に続くということです.
例を1つあげます. 簡単です.
$(\lambda x.xx)(\lambda x.xx)$
これを簡約すると
$(\lambda x.xx)(\lambda x.xx) \to yy[y \mapsto \lambda x.xx] \to (\lambda x.xx)(\lambda x.xx)$
元に戻ってしまいました. 無限ループです本当にありがとうございました.

また, 簡約の仕方は1つでないといいました. その例を1つあげてみましょう.
$\lambda u.((\lambda v.uvrs)q)p$

ご指摘を受けて修正しました.
修正前 : $\lambda u.((\lambda v.uvrs)p)q$

これは, 先に外側から見て,
$\lambda u.((\lambda v.uvrs)q)p \to (\lambda v.pvrs)q \to pqrs$

ご指摘を受けて修正しました.
修正前 : $\lambda u.((\lambda v.uvrs)p)q \to (\lambda v.pvrs)q \to pqrs$

ともできるし, 先に内側から見て,
$\lambda u.((\lambda v.uvrs)q)p \to (\lambda u.uqrs)p \to pqrs$

ご指摘を受けて修正しました.
修正前 : $\lambda u.((\lambda v.uvrs)p)q \to (\lambda u.uqrs)p \to pqrs$

ともできます. すなわち, ラムダ式の簡約には複数の「戦略」があると言えます. またこのとき, 簡約と正規形には次の3タイプに分けることができると言えます.

どのような戦略を取っても正規形に必ずなるもの. 例: $\lambda u.((\lambda v.uvrs)p)q$
どのような戦略を取っても必ずいつまでも正規形にならないもの. 例: $(\lambda x.xx)(\lambda x.xx)$
戦略によって, 正規形になったり, いつまでもならなかったりするもの. 例 $(\lambda z.y)((\lambda x.xx)(\lambda x.xx) )$

3つ目の例としてあげたものは, $\lambda z.y$ になんかの引数が食わされていると考えれば, すぐに $y$ に簡約できますが, $(\lambda x.xx)(\lambda x.xx)$ が何らかのラムダ式の引数になっていると捉えると, いつまでも簡約が終わりません. したがって, ラムダ計算においてはこの簡約戦略が非常に重要であるということがわかります.

今日はこの辺にして, 明日はラムダ計算のマクロ, 不動点結合子と再帰関数について扱います.