call/ccとYコンビネータ

call/ccを使って、self-applicationなしでYコンビネータを書くことができるという話
http://okmij.org/ftp/Scheme/callcc-fixpoint.txt

(define (Y f)

  ( (lambda (u) (u (lambda (x) (lambda (n) ( (f (u x)) n )))))

    (call/cc (call/cc (lambda (x) x))) ))

頭では理解できるけど、心で理解できないっ！というのは、( (lambda (x) (x x)) p )と( (call/cc call/cc) p )は「等しい」のに、(lambda (x) (x x))と(call/cc call/cc)が等しいわけではないという、このへんがcall/ccのキモさの全てを体現してるような。そのせいで、普通のYコンビネータの使い方

(define fact (Y (lambda (f) (lambda (n) (if (<= n 0) 1 (* n (f (- n 1))))))))

もできなくなってるし。いや、そもそも普通は、Yコンビネータ使わないけど

gosh>(procedure? call/cc)

#t

こいつは嘘をついてる味だぜ･･･

今までCPS変換といえば、大体CBV(call-by-velue)-CPSばっか見てたけど、CBN(call-by-name)-CPSもあるらしい

C[x] = (lambda (k) (k x))

C[(lambda (x) M)] = (lambda (k) (k (lambda (x) C[M])))

C[(M N)] = (lambda (k) (C[M] (lambda (m) (C[N] (lambda (n) ( (m n) k ))))))

C[call/cc] =

(lambda (k0)

  (k0 (lambda (f) (lambda (k) ((f (lambda (a) (lambda (k1) (k a)))) k)))))

がCBV-CPSで

C[x] = (lambda (k) (x k))

C[(lambda (x) M)] = (lambda (k) (k (lambda (x) (lambda (k2) (C[M] k2)))))

C[(M N)] = (lambda (k) (CM (lambda (v) ( (v C[N]) k ))))

C[call/cc] =

(lambda (k2)

  (k2 (lambda (f)

	(lambda (k)

	  (f (lambda (a) ( (a (lambda (q) (q (lambda (v) (lambda (c) (v k)))))) k)))))))

がCBN-CPSらしい。ふむ、違いがよく分からんし、この変換自体、心でなく頭でしか理解できない。なんというか、数学的な自然さみたいなのがねぇ。そういう時は、コンビネータに頼ればいい。UnlambdaでCPS。

CBV-CPS-callccをコンビネータで書くと

( (S I) (K ( (S ( (S (K S) ) ( (S ( (S (K S) ) ( (S (K K)) I )))
  (K ( (S (K (S (K K)))) ( (S ( (S (K S) ) ( (S (K K)) I))) (K I))))))) (K I))) )

な感じに。もっと意味がわからなく･･･

それはどうでもいい。ポイントは、実際に(call-by-value-)CPSをしてみると、(call/cc call/cc)と(lambda (x) (x x))は等しくないのに、( (call/cc call/cc) p )と( (lambda (x) (x x)) p )は等しくなるという点。

>(expand '(CPS (call/cc call/cc)))

(lambda (#:k) (#:k (lambda (#:a) (lambda (#:k1) (#:k #:a)))))

>(expand '(CPS (lambda (x) (x x))))

(lambda (#:k) (#:k (lambda (#:x) (lambda (#:k) (#:x #:x #:k)))))

で、call-by-valueとcall-by-nameで違いがあるのかという点が気になったので、CBN用にCPS,NORMマクロを書き直してテスト。

(define-syntax CBN-CPS

  (syntax-rules (lambda call/cc)

    ( (CBN-CPS (?e1 ?e2) . args)     ; application

      (CBN-NORM (lambda (k) ( (CBN-CPS ?e1) (lambda (v) ( (v (CBN-CPS ?e2) ) k )))) . args) )

    ( (CBN-CPS (lambda (x) ?e) . args)		; abstraction

      (CBN-NORM (lambda (k) (k (lambda (x) (CBN-CPS ?e)))) . args) )

    ( (CBN-CPS call/cc . args)

       (CBN-NORM (lambda (k2)

        (k2 (lambda (f)

	 (lambda (k)

	   (f (lambda (a) ((a (lambda (q) (q (lambda (v) (lambda (c) (v k)))))) k)))))))

		. args) )

    ( (CBN-CPS ?x . args)

       (CBN-NORM (lambda (k) (?x k)) . args)) ))
(define-syntax CBN-NORM

  (syntax-rules (lambda CBN-CPS)

    ( (CBN-NORM t) (CBN-NORM t () ()) )

    ( (CBN-NORM (CBN-CPS e) env stack) (CBN-CPS e env stack) )

    ( (CBN-NORM (lambda (x) e) env () )

     (let-syntax ((ren (syntax-rules ()

            ((ren ?x ?e ?env) (lambda (x) (CBN-NORM ?e ( (?x () x) . ?env ) ()))))))

       (ren x e env)) )

    ( (CBN-NORM (lambda (x) b) env ( (enve e) . stack) )

      (CBN-NORM b ((x enve e) . env) stack) )

    ( (CBN-NORM (e1 e2) env stack)

      (CBN-NORM e1 env ( (env e2) . stack )) )

    ( (CBN-NORM x () ()) x )

    ( (CBN-NORM x () ( (enve e) ...) )

       (x (CBN-NORM e enve ()) ...) )

    ( (CBN-NORM x env stack)

      (let-syntax

	((find

	   (syntax-rules (x)

	     ( (find ?x ((x ?envs ?es) . _) ?stack) (CBN-NORM ?es ?envs ?stack) )

	     ( (find ?x (_ . ?env) ?stack) (CBN-NORM ?x ?env ?stack) ))))

	(find x env stack)) )))

で、ChezSchemeで

>(expand '(CBN-CPS (call/cc call/cc)))

(lambda (#:k) (#:k (lambda (#:v) (lambda (#:c) (#:v #:k)))))
>(expand '(CBN-CPS ((call/cc call/cc) pv)))

(lambda (#:k) (pv (lambda (#:v) (#:v (lambda (#:k1) (pv #:k1)) #:k))))
>(expand '(CBN-CPS (lambda (x) (x x))))

(lambda (#:k)

  (#:k

   (lambda (#:x)

     (lambda (#:k1)

       (#:x

	(lambda (#:v)

	  (#:v

	   (lambda (#:k2)

	     (#:x #:k2)) #:k1)))))))
>(expand '(CBN-CPS ( (lambda (x) (x x)) pv)))

(lambda (#:k) (pv (lambda (#:v) (#:v (lambda (#:k1) (pv #:k1)) #:k))))

変数名は、見難いので、リネームしたけど、こうなった。

な…　何をやってるのか　わからねーと思うが おれも何をやってるのかわからなかった… 頭がどうにかなりそうだった… XコンビネータだとかYコンビネータだとか そんなチャチなもんじゃあ　断じてねえ もっと意味不明なcall/ccの片鱗を味わったぜ

ポイントは、相変わらず(call/cc call/cc)と(lambda (x) (x x))は等しくないけど、任意の引数に対して、一致するよねってとこ。ていうか、ほんとに合ってんのか、これ･･･

　　　　　　　／￣￣￣￣￣￣￣￣￣￣￣￣￣￣￣￣￣￣￣￣￣￣

　　　　　　　| アパム！アパム！自信！自信持ってこい！アパーーーム！

　　　　　　　＼＿＿＿＿＿　　＿＿＿＿＿＿＿＿＿＿＿＿＿＿＿＿

　　　　　　　　　　　　　　　　∨

　　　　　　　　　　　　　　　　　　　　　　／￣￣ ＼ ｼﾞｼﾝﾅｼ!!

　　　　　　/＼　　 　 ＿. ／ ￣￣＼ 　|＿＿＿__.|　　　　 ／￣＼

　　　　 ／|￣￣|＼/_ ヽ |＿＿＿_　|∩（・∀・；||┘　　|￣￣|￣￣|

　　　／￣￣|￣￣|￣|　 （´д｀； ||┘ ＿ユ_II＿＿＿　|￣|￣￣|￣￣|

　　 /￣￣|￣￣|￣￣|￣|（　”　つつ[三≡＿[----─ﾟ　 ￣|￣￣|￣￣|

　　/￣|￣￣|￣￣|￣￣|￣|　⌒＼⌒＼ 　||　 /￣￣|￣￣|￣￣|￣￣|￣￣|

　/￣￣|￣￣|￣￣|￣￣|￣］　＼＿）＿）..|||　|￣|￣￣|￣￣|￣￣|￣￣|￣￣

　　　　　　　　　　　　 ￣￣　　　　　　　　／|＼

今までマクロは嫌いで、Lisp系のdefmacroは相変わらず嫌いなんだけど、Scheme系のdefine-syntaxとかで定義されるやつは便利かもしれないという気がしてきた。call-by-need CPSで確認するのと、call/ccのformalな定義に従って証明するのは、宿題

どうでもいいけど、はてなで二重括弧が脚注になるのを抑止するいい方法はないのか。