schemeとλ計算

 この記事はISer Advent Calendar 2018 - Adventarの17日目の記事として書かれました.昨日の記事はmin-caml compiler pwn (ISer advent calendar 12/2出題)writeup - cookies.txt .scrでした.

19erの@iojjoo(twitter)です.記事など書くのははじめてですが,いい機会なので何か書いてみることにしました.よろしくお願いします.

 
 この記事は,λ計算にちょっと触れたあとに scheme の quote 構文を使って色々遊んでみた,というものです.プログラミングをちゃんと触り始めて日が浅く,コードが汚かったり読みにくかったりすると思いますが,その点は申し訳ないです.

導入,定義

 さて,λ計算に関する授業を取っていない方(19erにもしいたら)でも読めるようにしたいのと,体系を制限して話を簡単にするために,以下で少し定義を行います.

生成規則

  λ計算とは「計算」の理論を形式的に展開するための体系の一つです.形式言語理論で触れたオートマトンを考えてもらえばわかりやすいですが,計算の形式理論ではまず現在の計算状態に当たるものを用意して,それらの内有限個のものの間をあらかじめ定まった規則で遷移していく,というモデルが基本です.このとき,あらかじめ用意される状態のセットは必ずしも有限であるとは限りません(状態間の遷移は有限).λ計算では状態は次の規則で定帰納的に定まる,λ式と呼ばれる記号列で表されます:

  V を可算個の変数の集合とする;

  (変数) x \in V のとき,x はλ式

  (適用) M, Nλ式のとき, (M\ N)λ式

  (抽象) Mλ式 x \in V のとき, (\lambda x.\ M)λ式

最も外側のかっこはよく省略されます.例はラムダ計算 - Wikipediaなどを参照してください.(抽象)においてM の内側にある変数x を束縛変数と言います(ただし,より内側で束縛されていないもの).以降では全ての変数が束縛されているようなλ式(閉λ式コンビネータと呼ばれる)のみを考えます.

計算規則

 さて,次は計算(遷移)規則です.以下では,M[x:=N] は M の束縛されていない(自由な) x を全てλ式  N で置き換えたものです.

  (簡約) (\lambda x.M)\ N \rightarrow M[x:=N].

今,閉λ式のみを考えているので,難しいことは考えずに  \lambda x. を取り除いたせいで自由になってしまった x Nを代入してしまえば大丈夫です.また,この規則をλ式中の一部分(部分λ式)に適用することもあります.

 

scheme上のλ計算

 さて,これで実際に計算をしてみます.ここで,scheme の次の式を考えます.

  (define fact (lambda (x) (if (= n 0) 1 (fact (- x 1)))))

この式はが再帰を計算するのはプログラミング言語再帰を処理してくれるからですが,この再帰をもう少しだけλ計算っぽくやってみます.そのために,次のλ式を使います:

  Y = (λf. (  (f  (λx. (x x)))  (f  (λx. (x x)))  )).

これはYコンビネータと呼ばれるλ式で,任意のλ式 M に対して YM -> M (YM) という簡約を持ち,この性質を使うと次のように再帰ができます.

   fact = (λf. (λx. (if (= x 0) 1 (* x  (f (- x 1)...)

とすると,

  (Y fact) 2 -> (fact (Y fact)) 2 -> ~ -> (if (= 2 0) 1 (* 2  (  (Y fact)  (- 2 1)  )))

                                                    -> (* 2  (  (Y fact) (- 2 1)  ))

 赤字の部分にまた同じ簡約を繰り返せばこれで再帰ができることがわかります. 

 

評価戦略

 今,簡約の順番は自由でした.しかし,通常(プログラミング言語上など)の場合簡約の順番がちゃんと決まっていて,それを評価戦略と言います.また,ある評価戦略でそれ以上簡約出来ないλ式を標準形と言い,λ式を繰り返し簡約して標準形を求めることを評価と言います.schemeの評価戦略は値呼びというもので,この戦略は以下の簡約列をたどるので Yコンビネータを使えません:

   (Y fact) -> (fact (Y fact)) -> (fact (fact (Y fact))) -> ... 

 schemeでYコンビネータを使う場合,このような無限ループ生じないようにYの定義を少しいじれば大丈夫ですが,やはりせっかくなのでYコンビネータを使ってみたいということで,ここでは別の評価戦略を採用する方法を考えます.つまり,shceme上に別の計算体系を作ってしまって,その上で式を評価してみます.

 このとき使うのがquoteという構文です.実験の資料を参照してもらうと基本的なことがわかるのですが,今回の使い道は,λ式にquoteを適用してその抽象構文木をlist構造で取得するというものです.

計算体系の実装

 各λ式について構文木が簡単に手に入るのであれば,簡約などの定義を構造帰納法に乗せれば,形式的に実装するのは簡単です.よって以下では,計算体系の定義を帰納的に整理します.このとき,定義,実装を,代入,簡約,評価の3つに分けて考えるのが有用です.また,話を簡単にするために以下では純粋なλ式のみを考え,+, -, 1, 2, #t, if, ... などはいったんおいておきます.

 以下で用いる評価戦略は正規順序というものです.さて,まず代入の定義です.

  (base1) x \in V,\ x[x:=N] \equiv N;

  (base2) y \in V,\ y[x:=N] \equiv y;

  (step App) (L\ M) [x:=N] \equiv (L[x:=N])\ (M[x:=N]);

  (base Abs) (\lambda x. M) [x:=N] \equiv \lambda x. M;  ;内側の束縛に触らない

  (step Abs) (\lambda y. M) [x:=N] \equiv \lambda y. (M[x:=N]).

次に,簡約(\rightarrow)の定義です.

  (base1)x \in V, \Rightarrow\ x\rightarrow x;

  (base2) (\lambda x. M)\ N\ \rightarrow\ M[x:=N] ;

  (step App1) M\rightarrow M' \Rightarrow M\ N \rightarrow M'\ N

  (step App2) x \in V,\ M\rightarrow M'\ \Rightarrow\ x\ M\rightarrow x\ M'

  (step Abs) M \rightarrow M' \Rightarrow (\lambda x. M) \rightarrow (\lambda x. M')

最後に,評価です. M に上の簡約規則を用いて一回簡約したものを \operatorname{red}(M)と書きます.

   \operatorname{eval}(M)

     \operatorname{if}\ M \equiv \operatorname{red}(M)\ \operatorname{then}\ M\ \operatorname{else}\ \operatorname{eval}(\operatorname{red}(M))

 さて,あとはこれをそのままschemeの構文に落とします.以下は準備です.

(define snd (lambda (x) (car (cdr x))))
(define thrd (lambda (x) (car (cdr (cdr x)))))

(define length
  (lambda (x)
    (if (not (list? x))
	1
	(if (null? x)
	    0
	    (+ 1 (length (cdr x)))))))

lengthはリストデータに対しては長さを返し,その他のデータには1を返す関数で,λ式がどの形かを判定するのはこの length を使うと簡単です.また,listデータとして同一であるかどうかの判定は equal? でできます( = は整数の演算なので使えない).次が代入,簡約,評価の関数です.

(define sbst
  (lambda (M x N)
    (let* ((ver (car x)) (lh (length M)))                              
      (cond 
            ;Base Case
            ((= lh 1) (if (equal? M ver) N M))  
            ;Step App                                       
	    ((= lh 2) (list (sbst (car M) x N) (sbst (snd M) x N)))    
            ;Step Abs          
	    ((= lh 3) (if (equal? (snd M) x)                                                 
			   M
			   (list (car M) (snd M) (sbst (thrd M) x N))))))))

(define red (lambda (M)
	      (let ((lh1 (length M)))
		(cond 
                       ;Base Case1
                      ((= lh1 1) M)
                       ;when in App form
		      ((= lh1 2)
		       (let ((lh2 (length (car M))))
			 (cond 
                                ;Base Case2
                               ((= lh2 3) (sbst (thrd (car M)) (snd (car M)) (snd M)))
                                ;Step App
			       ((= lh2 2) (list (red (car M)) (snd M)))
			       ((= lh2 1) (list (car M) (red (snd M)))))))
                        ;Step Abs
		      ((= lh1 3) (list 'lambda (snd M) (red (thrd M))))))))

(define eval
  (lambda (M)
    (if (equal? M (red M))
	M
	(eval (red M)))))


 これで,evalを使えばquoteをかけたλ式を標準形まで簡約することが出来ます.現時点で扱えるのはλ式だけですが,λ計算の理論を使えばλ式だけで自然数の計算を行うことが出来ます.アイデアは,何かある特定の形のλ式自然数に対応させておいて,引数と出力をその形で行うと約束しておくというものです.このとき,各自然数はチャーチ数と呼ばれる閉λ式で表されます.このあたりの理論はラムダ計算 - Wikipediaがよくまとまっているので,必要であればそちらを参照してください.使う道具を以下で定めます.定義した式を後の定義に流用するときは list 構文を使わないと,変数名がそのまま quote されてしまうことに注意が必要です.

(define zero '(lambda (f) (lambda (x) x)))
(define one '(lambda (f) (lambda (x) (f x))))
(define two '(lambda (f) (lambda (x) (f (f x)))))
(define three '(lambda (f) (lambda (x) (f (f (f x))))))
(define four '(lambda (f) (lambda (x) (f (f (f (f x)))))))
(define five '(lambda (f) (lambda (x) (f (f (f (f (f x))))))))

(define suc '(lambda (n) (lambda (f) (lambda (x) (f ((n f) x))))))
(define add '(lambda (n) (lambda (m) (lambda (f) (lambda (x) ((n f) ((m f) x))))))) 
(define mult '(lambda (n) (lambda (m) (lambda (f) (lambda (x) ((n (m f)) x))))))

(define true '(lambda (x) (lambda (y) x)))
(define false '(lambda (x) (lambda (y) y)))

(define iszero (list 'lambda '(n) (list (list 'n (list true false)) true)))

(define if* '(lambda (p) (lambda (x) (lambda (y) ((p x) y)))))
(define if-iszero?
  (list 'lambda '(n)
	(list 'lambda '(x)
	      (list 'lambda '(y)
		    (list (list (list if* (list iszero 'n)) 'x) 'y)))))

(define pair '(lambda (x) (lambda (y) (lambda (p) ((p x) y)))))

(define car* (list 'lambda '(x) (list 'x true)))
(define cdr* (list 'lambda '(x) (list 'x false)))

(define ss (list 'lambda '(x) (list (list pair (list cdr* 'x)) (list suc (list cdr* 'x)))))
(define pred (list 'lambda '(n) (list car* (list (list 'n ss) (list (list pair zero) zero)))))

(define Y '(lambda (f) ((lambda (x) (f (x x))) (lambda (x) (f (x x))))))

(define fact-func
  (list 'lambda '(f)
	(list 'lambda '(x)
	      (list (list (list if-iszero? 'x)
			  one)
		    (list (list mult 'x) (list 'f (list pred 'x)))))))

(define fact (list Y fact-func))

細かい部分がよくわからない場合は気にしないでください.ここで言いたいのは,例えば (eval (list (list add two) three)) というλ式schemeで評価すると,(lambda (f) (lambda (x) (f (f (f (f (f x))))))) が表示され,(eval (list fact four)) を評価すると f を24個含むチャーチ数が表示される,というものです.five の fact は少し時間がかかりますが,ちゃんと出来ます.

計算体系の拡張

 さて,Yコンビネータを使うという目的はなんとか達成されたものの,このままでは信じられないくらい遅いです.それに加え,120の代わりに f が120個入っているλ式を返されても知らんがなという気持ちにしかなりません.これを解決する方法も作ってみたのですが,それをかくと記事が終わらないので,概略だけ書きます.

定数とその上の演算

 上の体系に1, 2, #f, #t, +, *, if, ... などの定数やその上の演算を加えた拡張を行います.やり方は簡単で,代入と簡約で新たにこれらの構文をトラップして処理するケースを付け加えればOKです.例えば,term := (quote (+ 1 2)) の形のデータをトラップして,
  (+ (snd term) (thrd term))
という式を評価すれば良いです.ここで,(quote 1) が 1 と同様の定数データとして扱われることが本質的です.つまり,(+ '1 1) を評価するとちゃんと 2 になります.ただし,('+ 1 1) などはエラー(quote前後で同じなのは定数 1, 2, #t, ...)になることと,''1 はもう同じとして扱われないことに注意が必要です.

評価戦略

 評価を手取り早く高速にするために,正規順序簡約の規則のうち(App2)と(Abs)を除きます.このままだとめちゃくちゃ早くなる代わりに簡約が途中で止まってしまうようになるので,値呼び戦略で補います.値呼びは簡約と評価の間での同時再帰で実現できます.例えば,簡約規則(base2)を,

  (Val base 2) (\lambda x. M)N \rightarrow M[x:=\operatorname{eval}(N)]

とすれば良いです.しかし,このままでは Yコンビネータが使えない元の状態に後戻りなので,値呼びをする部分を,上で追加した演算のうち自然数演算の引数と if の第一引数に限定します.こうするとちゃんと Yコンビネータが使えるまま拡張できます.試してみましたが,10の階乗くらいなら数秒でできるようになりました(正規簡約は6の階乗で全然値が帰って来なくなってしまった).「10の階乗に数秒かかる」というのがなかなかの怪文な気もしますが...


終わりに

 さて,長くなりましたがこの記事はこの辺りで終わりにします.このようなわかりにくくて長い記事を最後まで読んでいただきありがとうがざいました.自分は勘違いが多いタイプなので,〜がおかしいんじゃないかと思った場合は教えてくださるとありがたいです.本記事では純粋なλ計算の理論にはほとんど何も触ることができなかった(悲しい)ので,興味を持たれた方はぜひ何かちゃんとした本を読んでみてください.下に参考にした文献一覧をつけておきます.[1]は型無しλ計算全般について教科書的に使いました.[2]は有名な本で,λ計算を拡張するところを少しだけ参照しました.[3]は評価戦略がちゃんと書いてあってとても参考になりました.関係ないですが,様相論理のところも面白かったです.

 明日はkammer0820さんの記事です.どんな文章が生成されるのか楽しみですね.

参考文献

[1]Cardon, Hindley, 2009: Lambda-Calculus and Combinators an Introduction, Cambridge Press.
[2]Benjamin C. Pierce, 2002: Types and Programming Languages, MIT Press.
[3]萩谷昌己, 西崎真也, 2007: 論理と計算の仕組み, 岩波