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

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

ここからはラムダ式を Haskell で表現していく。
そのためには幾つかの定義が必要だが、全ての定義は Hindley の著書 Lambda-Calculus and Combinators: An Introduction から拝借させて頂いた。

Lambda-Calculus and Combinators: An Introduction

この本は(洋書ではあるが)ステップを踏んでラムダ式が何であるか説明があるので、お勧め。前述した高橋先生の著書では、ラムダ式の説明は2ページそこそこであるが、この本では1章をまるまる使っての説明となる。

ラムダ項

ここからは Hindley による定義を、Haskell で実装していく。

定義 1.1 ラムダ項
(a) 全ての変数と定数はラムダ項である
(b) M と N がラムダ項であれば (M N) はラムダ項である( application )
(c) M がラムダ項で x が変数であれば (λx.M) はラムダ項である

例：

(a) (λv0.(v0 v00))
(b) (λx.(x y))
(c) ((λy.y)(λx.(x y)))
(d) (x(λx.(λx.x)))
(e) (λx.(y z))

上記はすべてラムダ項である。

Haskell による定義は以下：

-- Definition of Term
--
data Term = 
    Var Int
  | App Term Term 
  | Lam Int Term deriving Show

変数は Var 1, Var 2 のように示す。
x, y のように文字列を使っても良いのだが、ユニークであれば何でも良いので数字にした。数字のほうが入力しやすいし。
以下は Haskell で定義したラムダ項の例である：

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

x を Var 0, y を Var 1, z を Var 2 に見立てると、上の例は上から x, y, x z, λx.x y, (λx.x y)(λx.x) の意味となる。

自由/束縛変数

続いて Hindley の本では、自由/束縛変数についての定義が続く。

定義1.11 自由/束縛変数
λ項 P に出現する変数 x を以下のように定義する：
1. P に含まれる λy.M の M に x が含まれる場合、bound
2. P に λx.M が含まれる場合、bound and binding
3. それ以外、x は free = 自由変数

例：

(((x v)(λy.(λz.(y v))))w)

左から順に、x, v は free.
次の y は bound and binding,
z も bound and binding,
次の y は、この項より前に出てくるλy.() のスコープなので bound,
v は free, w は free.

P に含まれる全ての自由変数を関数 FV(P) で得られるとすると、

FV(((x v)(λy.(λz.(y v))))w) = {x, v, w}

となる。
別の例で

FV((λy.y x(λx.y(λy.z)x))v w) = {x, z, v, w}

この例では、x は複数回出現し、出現する位置によって bound, bound and binding, free となるが FV は全ての自由変数を返す関数であるため x は FV の返り値に含まれる。

少しプログラムっぽく FV を定義すると、以下のようになる：

-- --------------------------------------------------------------------
-- Definition of FV
--
-- FV(M) =   {M}                if M is Var
--         | FV(M1) U FV(M2)    if M = App M1 M2
--         | FV(N) / {x}        if M = Lam x.N
--

Haskell による定義は以下：

fv_i (Var m)     = m : []
fv_i (App m1 m2) = fv_i m1 ++ fv_i m2
fv_i (Lam x n)   = [ v | v <- fv_i n, v /= x]

uniq [] = []
uniq (x :xs) | elem x xs     = uniq xs
             | otherwise     = x : uniq xs

fv (t) = uniq (fv_i t)

> let t1 = (Lam 0 (Var 0))
> fv(t1)
[]
> let t2 = (Lam 0 (Var 1))
> fv(t2)
[1]

数字ではやはり少し見にくいので多少工夫をすると

gv (Var n)  = n

v   = Var 1
w   = Var 2
x   = Var 3
y   = Var 4
z   = Var 5

これらを定義した後で

> let t3 = (App (App v w) (App (Lam (gv x) (App x y)) (App (Lam (gv y) (App z y)) z) ))
> fv(t3)
[1,2,4,5]

変数を数字に置き換えてるので分かりにくいが、これは

FV((v w) ((λx.x y)((λy.z y)z))) = [v w y z]

のことである。よって自由変数は x (= 3) 以外の v, w, y, z となる。