モナド

Moggiのモナドに関する最初の論文をざっと眺めた
http://citeseer.ist.psu.edu/moggi89computational.html
以下、何となく理解したことと、理解できなかったこと。

そもそもの動機

型付ラムダ計算を、副作用・入出力・例外・非決定性を扱えるように拡張する、と書いてある。副作用etcのある関数の型付けを、ad hocなやり方ではなく、一貫性ある仕方でやる方法の一つ、ということ？

何故、圏論のmonadが絡んでくるのか

見た感じだと、要するに、関数の合成は結合的(であるべき)だ、ということに尽きると思う。結合的というのは、ある意味どっから計算してもいいよ、ということなので、参照透過であることを保証する感じ？

それを実際のプログラム言語に持ち込むメリット
謎。

圏論の枠組みで意味論を与えるのに、何のメリットがあるのか

本題とはずれるけど、ラムダ計算の圏論的な意味論を与えるのって、何か役に立つんだろうか。そうすることで、初めて証明できる事実があるとか。単に、圏論の言葉があまりにfitするので、現時点では何の役に立つか分からないけど、そのうち役立つと信じて、理論を作っておこうという精神？

項書き換え系(TRS)

Schemeで、TRSを扱う関数を書いた。その前に、単一化を書き直し。make-unifyってのは変な名前だけど。var-pは、与えられたS式が変数かどうか判定する関数。

(define (remove-if proc L)

  (cond

   ( (null? L) L )

   ( (proc (car L)) (remove-if proc (cdr L)) )

   ( else (cons (car L) (remove-if proc (cdr L))) )))
(define (make-unify var-p)

 (lambda (p q)

  (letrec

   ( (const? (lambda (x) (and (not (var-p x)) (not (pair? x)))))

     (not-occur? ;変数varが式eに現れるかどうか

      (lambda (var e) 

       (cond

	 ( (or (null? e) (const? e)) #t )

	 ( (var-p e) (if (equal? var e) #f #t) )

	 ( else (and (not-occur? var (car e)) (not-occur? var (cdr e))) ))))

     (subst-apply ;式eに代入thetaを適用

      (lambda (theta e)

       (cond

	( (const? e) e )

	( (var-p e) (let ((bind (assoc e theta))) (if bind (cdr bind) e)) )

	( else (map (lambda (x) (subst-apply theta x)) e) ))))

     (subst-compose ;代入の合成

      (lambda (theta1 theta2)

       (let*

	( (tmp (map (lambda (x) (cons (car x) (subst-apply theta2 (cdr x)))) theta1))

	  (new (remove-if (lambda (x) (equal? (car x) (cdr x))) tmp)) )

	 (append (remove-if (lambda (b) (assoc (car b) theta1)) theta2) new))))

    (main

      (lambda (p q theta)

	(cond

	 ( (not theta) #f )

	 ( (and (var-p p) (not-occur? p q)) (subst-compose theta (list (cons p q))) )

	 ( (and (var-p q) (not-occur? q p)) (subst-compose theta (list (cons q p))) )

	 ( (and (var-p p) (not (equal? p q))) #f )

	 ( (and (var-p q) (not (equal? p q))) #f )

	 ( (const? p) (if (equal? p q) theta #f) )

	 ( (const? q) #f )

	 ( else

	  (let

	    ( (eta (main (subst-apply theta (car p)) (subst-apply theta (car q)) theta)) )

	     (main (cdr p) (cdr q) eta)) ))))

    (mgu (main p q '())))

   (if mgu (lambda (e) (subst-apply mgu e)) #f))))

で、以下がTRSを扱う関数。内部でcodeを生成してevalするという強引なやり方。こういうことするなら、マクロ使うべきなんだろうけど。本当はもっといい方法があるはず。書き換えルールp->qをペア(p.q)で表現して、rulesは、書き換え規則のリスト。

(define (make-TRS rules var-p)	

 (let* ( (unify-p (make-unify var-p))

	 (arg-cur (gensym))

	 (arg-prev (gensym))

	 (arg-p (gensym))

	 (code-body

	  (list 'lambda (list arg-cur arg-prev)

	   (cons 'cond

	    (append

	     (list (list (list 'equal? arg-cur arg-prev) arg-cur))

	     (list (list (list 'not (list 'pair? arg-cur)) arg-cur))

	      (map

	       (lambda (x)

		 `( (,unify-p ',(car x) ,arg-cur)

		    => (lambda (,arg-p) (main (,arg-p (quote ,(cdr x))) ,arg-cur) ))) rules)

	     (list (list 'else `(main (map (lambda (x) (main x '())) ,arg-cur) ,arg-cur)))))))

	 (code `(lambda (e)

		  (letrec

		   ( (main ,code-body) ) (main e '())))) )

   (eval code (interaction-environment))))

で、
add(0,x)->x
add(s(x),y)->s(add(x,y))

みたいな項書き換え系と、
append(nil,x)->x
append(cons(x,y),z)->cons(x,append(y,z))

みたいなTRSに対応するのがそれぞれ

(define (variable? e) ; #\%で始まるsymbolを変数と見なす

 (with-error-handler

   (lambda (x) #f)

  (lambda () (char=? #\% (string-ref (symbol->string e) 0)))))
(let ( (nat (make-TRS '( ((add 0 %x) . %x) ((add (s %x) %y) . (s (add %x %y))) ) variable?)) )

  (nat '(add (s (s (s (s 0)))) (s (s 0)))))
(let ( (p (make-TRS

	  '(((append nil %x) . %x)

	    ((append (cons %x %y)  %z) . (cons %x (append %y %z)))) variable?)) )

  (p '(append (cons a (cons b nil)) (cons c (cons d (cons e nil))))))

と書けて、実行すると

(s (s (s (s (s (s 0))))))

(cons a (cons b (cons c (cons d (cons e nil)))))

みたいなのが、それぞれ返ってくるはず。

注意点として、make-TRSで生成したクロージャーに、var-pで変数と見なされる式を含むと、うまくいかないことがある。このへんは、変数のrenameとかしないとダメっぽい。一応、内部でどういうコードを生成しているかというと、

(define rules '(((f (f %x)) . %x) ( (g (h %x)) . (f %x) ) ))

というのを与えて、(make-TRS rules variable?)とすると、

(lambda (e)

  (letrec

   ( (main

      (lambda (G122 G123)

       (cond

	( (equal? G122 G123) G122 )

	( (not (pair? G122)) G122 )

	( (unify '(f (f %x)) G122) => (lambda (p) (main (p '%x) G122)) )

	( (unify '(g (h %x)) G122) => (lambda (p) (main (p '(f %x)) G122)) )

	( else (main (map (lambda (x) (main x '())) G122) G122) )))) )

   (main e '())))

みたいなコードを内部で作る。

あと、critical pairを見つける関数を書けば、Knuth-Bendixの完備化アルゴリズムが書けて、それができると、殆ど直接的にレゾリューション法が得られるはずだけど、operatorや関数のarityが3以上とかになると、critical pairみっけるのが大変な気がして、どうすればいいか悩み中。