均分推理，通过减少该功能绑结

Question

我试图总结我的周围连拍和callCC头：

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() 

我已经成功地实现了这一点：

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())) 

在这一点上，我不知道如何处理递归定义f 完成这种减少的最佳方法是什么？

Answer 1

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

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()