人気ブログランキング | 話題のタグを見る

ラムダ計算で遊ぶ


ラムダ計算のインタープリタを作ったが、作りっぱなしでは面白くないので、A Tutorial Introduction to the Lambda Calculus をネタにラムダ計算によるプログラムをいろいろ試してみることにする。読解形式にはしないで、気ままにラムダ計算のプログラムを引用してラムダ計算機で実験していく。

ラムダ計算は「世界で最小の汎用プログラム言語」と呼ばれているようだが、すぐに思いつくのは次のような identity function くらいしかない。これは、単に引数を一つ取り、それを戻り値として返すだけだから何の面白みもない。

$ runghc Lambda.hs
lambda> (lx.x)
(lx.x)
lambda> ((lx.x) a)
a

ラムダ計算機ではこのように β 簡約を自動でできるが、ラムダ式の入力は括弧を省略しない形式でないとできない。したがって、参考書に出てくる括弧を省略した、λxy.MNL は (lx.(ly.((M N) L) というように括弧を補充する必要がある。

ラムダ計算では論理の真理値を定義できる。論理値の true と false は次のように定義される。

true = λxy.x
false = λxy.y

ラムダ計算機では (= var term) 式で変数 var にラムダ式 term を束縛できる。変数名は alphaNum なので数字と英数字の文字列になる。数字だけの変数にすることもできる。

lambda> (= true (lx.(ly.x)))
lambda> (= false (lx.(ly.y)))
lambda> true
(lx.(ly.x))
lambda> false
(lx.(ly.y))

true は引数 x y をとり、第1引数 x を返す関数だ。false は引数 x y をとり y を返す。

lambda> ((true a) b)
a
lambda> ((false a) b)
b

なぜこれが true と false なのだろうと不思議に感じるが、true と false がこのように定義されていると、if c then a else b という if ~ then ~ else 式が次のように簡単に定義できる。

if = λcxy.cxy

lambda> (=if (lc.(lx.(ly.((c x) y)))))
lambda> (((if true) a) b)
a
lambda> (((if false) a) b)
b

これでラムダ計算機もめでたく、条件分岐を記述できるようになった。

論理値が導入できたので論理記号も定義したい。NOT は次のように定義できる。

NOT = λx.xFT

true と false の別名 T と F を作って上の NOT を実装してみる。

lambda> (= T true)
lambda> (= F false)
lambda> (= NOT (lx.((x F) T)))
lambda> (NOT true)
(lx.(ly.y)) ..... false
lambda> (NOT false)
(lx.(ly.x)) ..... true

AND と OR の定義は次のようになる。

AND = λxy.xyF
OR = λxy.xTy

lambda> (= AND (lx.(ly.((x y) F))))
lambda> ((AND true) false)
(lx.(ly.y))
lambda> ((AND true) true)
(lx.(ly.x))

lambda> (= OR (lx.(ly.((x T) y))))
lambda> ((OR true) false)
(lx.(ly.x))
lambda> ((OR false) false)
(lx.(ly.y))

含意の定義は次のようになる。

lambda> (= IMPLY (lx.(ly.((OR (NOT x)) y))))
lambda> ((IMPLY true) true)
(lx.(ly.x))
lambda> ((IMPLY true) false)
(lx.(ly.y))

ラムダ計算機もだんだんプログラム言語らしくなってきた。一見不可解な true と false の定義で条件分岐や論理演算が定義できるのが面白い。

ラムダ計算機を使っていると、はるか昔にマイコンに機械語のプログラムを打ち込んでLEDを点滅させて感動していたときのことが思い出される。ラムダ計算の理論的なことは置いておいても、ラムダ計算機をいじるのは楽しい。

by tnomura9 | 2019-09-08 07:26 | Haskell | Comments(0)
<< ラムダ計算で遊ぶ 2 Monad Transform... >>