Equational reasoning with tying the knot

I'm trying to wrap my head around Cont and callCC, by reducing this function:

s0 = (flip runContT) return $  do
    (k, n) <- callCC $ k -> let f x = k (f, x)
                             in  return (f, 0)
    lift $ print n
    if n < 3
        then k (n+1) >> return ()
        else return ()

I've managed to reach this point:

s21 = runContT (let f x = ContT $ _ -> cc (f, x) in ContT ($(f,0))) cc where
    cc = ((k,n) -> let
        iff = if n < 3 then k (n+1) else ContT ($())
        in print n >> runContT iff (_ -> return ()))

And at this point i have no idea what to do with recursive definition of f What is the best way to finish this reduction?

---

您可以按照以下步骤操作。

s21 = runContT (let f x = ContT $ _ -> cc (f, x) in ContT ($(f,0))) cc where
    cc = ((k,n) -> let
        iff = if n < 3 then k (n+1) else ContT ($())
        in print n >> runContT iff (_ -> return ())

-- runContT is the opposite of ContT

s22 =  (let f x = ContT $ _ -> cc (f, x) in ($(f,0))) cc
    where
    cc = ((k,n) -> let
        iff = if n < 3 then k (n+1) else ContT ($())
        in print n >> runContT iff (_ -> return ())

-- reordering

s23 = ($(f,0)) cc
    where
    f x = ContT $ _ -> cc (f, x)
    cc = ((k,n) -> let
        iff = if n < 3 then k (n+1) else ContT ($())
        in print n >> runContT iff (_ -> return ())

s24 = cc (f,0)
    where ...

-- beta

s25 = let iff = if 0 < 3 then f (0+1) else ContT ($())
       in print 0 >> runContT iff (_ -> return ())
    where ...

-- if, arithmetics

s26 = let iff = f 1
       in print 0 >> runContT iff (_ -> return ())
    where ...

s27 = print 0 >> runContT (f 1) (_ -> return ())
    where ...

s28 = print 0 >> runContT (ContT $ _ -> cc (f, 1)) (_ -> return ())
    where ...

s29 = print 0 >> (_ -> cc (f, 1)) (_ -> return ())
    where ...

s30 = print 0 >> cc (f, 1)
    where ...

-- repeat all the steps s24..s30

s31 = print 0 >> print 1 >> cc (f, 2)
    where ...

-- etc.

s32 = print 0 >> print 1 >> print 2 >> cc (f, 3)
    where ...

s33 = print 0 >> print 1 >> print 2 >>
      let iff = if 3 < 3 then f (3+1) else ContT ($())
       in print 3 >> runContT iff (_ -> return ())
    where ...

s34 = print 0 >> print 1 >> print 2 >> print 3 >> 
      let iff = ContT ($())
       in runContT iff (_ -> return ()))
    where ...

s35 = print 0 >> print 1 >> print 2 >> print 3 >> 
      runContT (ContT ($())) (_ -> return ())
    where ...

s36 = print 0 >> print 1 >> print 2 >> print 3 >> 
      ($()) (_ -> return ())
    where ...

s37 = print 0 >> print 1 >> print 2 >> print 3 >> 
      return ()

链接地址: http://www.djcxy.com/p/39824.html

上一篇: 游戏中心排行榜没有出现在游戏的生产版本上？

下一篇: 与结合的方程式推理