Haskell でラムダ式を簡約させてみる - 3

Haskell でラムダ式を簡約させてみる - 1 - pragma666の日記
 Haskell でラムダ式を簡約させてみる - 2 - pragma666の日記

前回は自由変数の判定を行う関数を定義した。次はβ簡約の中心的な役割を担う、λ項の置換を定義する。

置換の定義

再び Hindley の教科書からの引用。置換を以下のように定義している:

定義 1.12 置換
[N/x] M について、M に含まれる x を N に置換した結果を以下に定義する：

(a) [N/x] x       = N
(b) [N/x] a       = a                   ; a は x 以外の変数、または定数
(c) [N/x] (P Q)   = ([N/x]P [N/x]Q)
(d) [N/x] (λx.P) = λx.P
(e) [N/x] (λy.P) = λy.P               ; if x /= FV(P)
(f) [N/x] (λy.P) = λy.[N/x]P          ; if x <= FV(P) && y /= FV(N)
(g) [N/x] (λy.P) = λz.[N/x][z]y]P     ; if x <= FV(P) && y <= FV(N)

ここで (e)〜(g) において y != x であり、(g) における z は FV(N P)に含まれない(新しい) 変数である。

置換はλ計算の中心的な役割を担う重要な定義である。多くの数学の論文と同じく、一連の定義、定理が続いて最後にアルゴリズムの全貌が示される、というのが Hindley の教科書のスタイルである。しかしそれでは置換の意味を理解するのがしんどいので少し先走って説明すると、

(λx.x)

というλ項は、C 言語風に書くなら

int func( int x )
{
    return x;
}

つまり入力をそのまま返す関数を示す。
C 言語では

func(y);

などして関数を呼び出す。関数 func() は y をそのまま返すので実行すると、この式は

y;

と意味的に同じである。
λ式で入力をそのまま返す処理(無名関数)を表現しようとすると (λx.x) となる。λの直後に続く x は仮引数の名前で、ドットの後に処理が書かれる。処理は x だけなので、すなわち x が返る、と読める。
func(y) に相当する関数の"呼び出し" (適用) は以下のように無名関数の後に実引数を書く：

(λx.x)y

このλ式を計算すると (λx.x) の引数 x に y が代入され、代入された値すなわち y が返るので計算結果は y となる。
ここで計算というキーワードを使ったが、単一のλ項を考えた場合、簡約とは要は、仮引数の実引数への置換である。以降、簡約を (λx.x)y -> y のように矢印 -> で示す。

さて、置換の定義に戻ると、

(a) [N/x] x = N

(a) は単純に、M = x なので、x を N に置換すれば N である。(λx.x) N -> N となる例。

(b) [N/x] a = a

(b) は M (= a) にそもそも x が含まれない。よって a のまま。(λx.a) N -> a となる例。

(c) [N/x] (P Q) = ([N/x]P [N/x]Q)

(d) [N/x] (λx.P) = λx.P

(d) は少し難しい例。λx.P における x とは、関数の仮引数名のようなものである、と先ほど述べた。例えば引数に +1 した数を返す関数を C 風に書くなら

int suc( int x ) { return x + 1 }

ここで x という名前は(所詮は仮の引数なので) 別に y でも z でも N にしても、関数としての意味は変わらない。

int suc( int N ) { return N + 1 }

しかし、意味は全く変わらないので x を N に置換する意味は無い。置換を行う意味が無いので (d) では置換を行わない。

(e) [N/x] (λy.P) = λy.P

(e)〜(g) は前提として M にあたるλ式の仮引数が x ではなく y である点に注意である。
(e) は、条件として x が P の自由変数では無い、としている。つまり x は P の中にまったく出現しないか、または束縛変数として出現するかのどちらかである。まず、まったく出現しない場合は置換の必要が無い。次に x が P の束縛変数の場合を考える。ここで、x を置換するべきか、しないべきか。定義 (e) は置換しない、と言っている。束縛されている、ということは既に独立したスコープを持つことを示している。よって置換してはならない。または置換しても意味が無い。
以下のようなλ式が、(e) の例である：

[z/x] λy.y         --> λy.y           ; x は含まれない
[z/x] λy.(λx.xx)   --> λy.(λx.xx)   ; x は束縛変数として含まれる

(f) [N/x] (λy.P) = λy.[N/x]P

(f) は、P に x は自由変数として含まれ、N に y が自由変数として含まれないケースである。自由変数、つまり誰にも束縛されていないため x について置換をする。

[z/x] λy.x --> λy.z

(g) [N/x] (λy.P) = λz.[N/x][z]y]P

(g) は P に x が自由変数として出現し、N に y が自由変数として出現するケースである。まず仮引数名として使用されている y を、未使用な名前の変数 z に置換する。次に x を置換する。

[y/x] λy.xy --> [y/x] λz.xz --> λz.yz

Haskell による実装

先ほどの定義を多少プログラムっぽく書き直すと

-- Definition of Substitution
--
--      N      M
-- (a) [N/x] Var x       = N
-- (b) [N/x] a           = a
-- (c) [N/x] (App P Q)   = ([N/x]P [N/x]Q)
-- (d) [N/x] (Lam x P)   = Lam x P
-- (e) [N/x] (Lam y P)   = Lam y P               ; if x /= FV(P)
-- (f) [N/x] (Lam y P)   = Lam y [N/x]P          ; if x <= FV(P) && y /= FV(N)
-- (g) [N/x] (Lam y P)   = Lam z [N/x][z/y]P     ; if x <= FV(P) && y <= FV(N)

まず (a), (b) の Haskell による定義：

-- subst   M          x       N     empty
subst_i (Var n)     (Var x)   nt      e
    | n == x    = nt
    | otherwise = (Var n)

empty e は、(g) に出てくる自由変数を定義するためにある。(g) 以外では使わない。
(c) の定義は以下：

subst_i (App t1 t2) (Var x) nt      e
                = App (subst t1 (Var x)  nt) (subst t2 (Var x) nt)

次に (d) 〜 (g) の定義：

subst_i (Lam y p)   (Var x) nt      e
    | y == x                                    = (Lam y p)
    | not (elem x (fv p))                       = (Lam y p)
    | (elem x (fv p)) && (not (elem y (fv nt))) = (Lam y (subst p (Var x) nt))
    | (elem x (fv p)) && (elem y (fv nt))       = (Lam e (subst (subst_i p (Var y) (Var e) (e + 1))
                                                                  (Var x) nt ))

(g) の例(最後の定義) で、empty の e に +1 をしていることで、新たな自由変数を作っている。
最後に、これらを呼び出す元の関数の定義。

subst t1 t2 t3  = subst_i t1 t2 t3 (maximum ((fv t1) ++ (fv t2) ++ fv(t3)) + 1)

置換の式 [N/x] M について、t1 = M, t2 = x, t3 = N である。
Hindley の体後と順番が違うのでわかりにくいが、

subst 元のλ式　置換ターゲット　置換内容

みたいな感じで読むといいかも。
subst_i に渡す e は、subst の引数となる項の変数(というか数字) の最大値をもとに作成している。

subst 例

(a), (b) の例：

> subst (Var 0) (Var 0) (Var 1)
Var 1
> subst (Var 1) (Var 0) (Var 2)
Var 1

例によって数字で変数を表現しているので分かりにくいが Var 0 を V0 という変数として見立てると
最初の例は、「V0 というλ式に出てくる V0 を V1 に置き換えて」
という意味である。
ふたつ目の例は「V1 というλ式に出てくる V0 を V2 に置き換えて」
次は (c) の例：

> subst (App (Var 0) (Var 1)) (Var 0) (Var 2)
App (Var 2) (Var 1)

続いて(d) の例：

> subst (Lam 3 (App (Var 3) (Var 3))) (Var 3) (Var 4)
Lam 3 (App (Var 3) (Var 3))

(e) の例：

> subst (Lam 0 (App (Var 0) (Var 0))) (Var 1) (Var 2)
Lam 0 (App (Var 0) (Var 0))

(f) の例：

> subst (Lam 0 (App (Var 0) (Var 1))) (Var 1) (Var 2)
Lam 0 (App (Var 0) (Var 2))

最後に(g)の例：

> subst (Lam 2 (App (Var 0) (App (Var 1) (Var 2)))) (Var 1) (Var 2)
Lam 3 (App (Var 0) (App (Var 2) (Var 3)))