ラムダ計算

CS

ラムダ項のベータ正規形を求めるプログラムをHaskellで書いてみた。元ネタはWadlerの論文*1にあったMirandaのプログラム。ラムダ項の評価器らしいが、ラムダ項の評価って何を求めれば良いのかがイマイチ分からなかったので、ベータ正規形に簡約するプログラムに変更する。
で、こんな感じ。

import List

data Term = Var Var | App Term Term | Abst Var Term deriving Show
type Var = [Char]

beta (Var x) = Var x
beta (App m@(Abst x m1) n) = beta (subst m1 x n)
beta (App m@(App _ _) n) = case m' of
                             (Abst _ _) -> beta (App m' n)
                             _ -> App m' (beta n)
                             where m' = beta m
beta (App m@(Var x) n) = App m (beta n)
beta (Abst x m) =  Abst x (beta m)

subst m@(Var y) x n = if x == y then n else m
subst (App m1 m2) x n = App (subst m1 x n) (subst m2 x n)
subst m@(Abst y m1) x n =  if x == y then m else Abst y' (subst (subst m1 y (Var y')) x n)
                           where (y':_) = vars \\ (nub ((free_vars n) ++ (free_vars m) ++ x:[]))

free_vars (Var x) = x:[]
free_vars (App m1 m2) = free_vars m1 ++ (free_vars m2)
free_vars (Abst x m) = filter (x /=) (free_vars m)

vars = [x:[] | x <- ['a'..'z']] ++ [x:xs | x <- ['a'..'z'], xs <- vars]

LambdaではAbstとしたのはなんとなくです。一応、最左戦略のはずだが、自信はないなあ。関数betaでAppを引数に取るところが複雑になってしまったの気に入らない。
ちゃんとベータ正規形になるか確認。しかし、関数betaは必要のないカッコを省略した形式のを読めないので、ちょっとしたラムダ項を書くのも大変である。なので、いくつかコンビネータを定義しておく。本来はカッコ省略形式を食えるように変換関数とか書くのが良いのだろうが、メンドくさいのでパスだ。このあいだSchemeで逆の関数、つまり略記形式に変換する関数、は書いたんだけどなあ。

conbI = Abst "x" (Var "x")
conbF = Abst "x" (Abst "y" (Var "y"))
conbK = Abst "x" (Abst "y" (Var "x"))
conbT = conbK
conbS = Abst "x" (Abst "y" (Abst "z" (App (App (Var "x") (Var "z")) (App (Var "y") (Var "z")))))
conbB = Abst "x" (Abst "y" (Abst "z" (App (Var "x") (App (Var "y") (Var "z")))))
conbO = App (Abst "x" (App (Var "x") (Var "x"))) (Abst "x" (App (Var "x") (Var "x")))

Haskellは大文字からはじまる変数名はダメみたいなので、conbを前につけた*2。
最初のテストは"(λxy.xyxxy)Sa"。大文字はコンビネータ(上の定義でconbを削ったものに対応する)で小文字は変数。これは井田哲雄氏の「計算モデルの基礎理論」*3という本にあった練習問題。この本は絶版らしいのだが、このあいだ運良く手に入れることができたのだ。某先生に感謝。
で、このラムダ項を代数データ型に従って書いて(長いので適当なところで改行いれてます)、それを関数betaに作用させると、下のようになった。

*Main> beta (App (App (Abst "x" (Abst "y" (App (App (App (App (Var "x") (Var "y")) (Var "x"))
 (Var "x")) (Var "y")))) conbS) (Var "a"))
App (App (App (Var "a") (Abst "b" (Abst "a" (Abst "c" (App (App (Var "b") (Var "c"))
 (App (Var "a") (Var "c"))))))) (Abst "a" (Abst "b" (Abst "c" (App (App (Var "b") (Var "c"))
 (App (App (Var "a") (Var "b")) (Var "c"))))))) (Var "a")

あっているのか、これは・・・。
なので、結果がもう少し簡単なものを。"(λxyz.x(xy)z)Ida"。これも上の本にあった練習問題。

*Main> beta (App (App (App (Abst "x" (Abst "y" (Abst "z" (App (App (Var "x")
 (App (Var "x") (Var "y"))) (Var"z"))))) conbI) (Var "d")) (Var "a"))
App (Var "d") (Var "a")

おお、これはあってるみたい。
しかし、ラムダ項書きにくいし、結果も読みにくいし、テストの方が大変だ。
一応、最左戦略であることを確かめるために"TIΩ"を試す。Ωは上の定義のconbOで、簡略が止まらないコンビネータ。最左最内戦略だと"TIΩ"は止まらないが、最左戦略なら止まる。で、結果。

*Main> beta (App (App conbT conbI) conbO)
Abst "b" (Var "b")

確かに止まった。
同様に、"FΩI"も止まる。

*Main> beta (App (App conbF conbO) conbI)
Abst "x" (Var "x")

また、卒論とまったく関係ないことに時間を費やしてしまった。とりあえず、今後は卒論に集中しよう。卒論終ったらHaskellをもうちょい勉強しようかな。せめてモナドを使えるくらいにはなりたいものだ。

*1:http://www.cs.kent.ac.uk/people/staff/dat/miranda/wadler87.pdf

*2:追記：コンビネータはcombinatorだから、前につけるのはcombだった。どこで間違えたんだか

*3:

岩波講座 ソフトウェア科学〈〔理論〕12〉計算モデルの基礎理論

岩波講座 ソフトウェア科学〈〔理論〕12〉計算モデルの基礎理論