函数式编程中cps(continuation-passing style )是什么意思?

有没有不基于lisp、c++的例子,最好是python的,也有lamdba expression嘛。
关注者
423
被浏览
39131

11 个回答

从另一个角度回答下吧。
带 callcc 的 Lambda 演算(叫\lambda\mu演算)可以经 Curry-Howard 同构到经典逻辑,而普通的\lambda演算只能同构到直觉逻辑。但是形式逻辑中有一个 Gilvenko 定理,它声称:
对任何命题p和前提\Gamma,在经典逻辑中 \Gamma\vdash p若且唯若在直觉逻辑中\Gamma\vdash\neg\neg p
在证明这个定理之后哥德尔(对,就是证明存在不确定命题的那个)和根岑(自然演绎和相继式演算的发明人)发明了双否定变换,也叫哥德尔-根岑变换,其规则是:
\alpha^{*}=(\alpha\rightarrow\bot)\rightarrow\bot
(\alpha\rightarrow\beta)^*=\alpha^* \rightarrow \beta^*
注意到哥德尔-根岑变换任意命题都和原命题经典等价,但并非直觉等价(直觉逻辑本身否认\neg\neg\alpha\rightarrow\alpha),但是按照 Gilvenko 定理,双否定命题\alpha^*若在直觉逻辑体系中可证明为真,则在经典逻辑体系里\alpha必为真,反之亦然。
那么按照 Curry-Howard 同构,\lambda\mu演算下的类型指派\Gamma\vdash e:\alpha可以经过哥德尔-根岑变换得到一个\lambda演算类型指派:\Gamma^*\vdash e^*:\alpha^*,将表达式(同构于证明过程)e变为e^*的过程就是 CPS 变换。直接照搬哥德尔-根岑变换里的类型的话,我们有如下结果:
  1. 原子 a^*=\lambda\kappa.\kappa a
  2. 调用 (EF)^*=\lambda\kappa.E^*(\lambda E'.F^* (\lambda F'.(E'F')\kappa))
  3. 抽象 (\lambda x.E)^*=\lambda\kappa.\kappa(\lambda x.\lambda k. (e^*)k)
  4. call/cc 算子\mathrm{call/cc}=\lambda\kappa.\kappa(\lambda f.\lambda k.f k k)
可以证明,E^*(\lambda x.x) =_\beta E,即:CPS 变换不改变语义。
当然这个版本的 CPS 是非常冗长的,市面上见到的那些都是在变换是之后直接做了\beta规约,删掉大堆 Redex 的。

上面这些再一次说明了,逻辑学和编程有多么紧密的联系。

其实就是把


Fuckee FindFuckee()
{
    return kula;
}

void Fuck(Fuckee fuckee, int count)
{
    for(int i=0;i<count;i++)
        fuckee.Fuck();
}

void Main()
{
    Fuck(FindFuckee(), 100);
}

改成


void FindFuckee(Action<Fuckee> continuation)
{
    continuation(kula);
}

void Fuck_(Fuckee fuckee, int count, int i, Action continuation)
{
    if(i<count) fuckee.Fuck(()=>Fuck_(fuckee, count, i+1, continuation);
    else continuation();
}

void Fuck(Fuckee fuckee, int count, Action continuation)
{
    Fuck_(fuckee, count, 0, continuation);
}

void Main(Action continuation)
{
    FindFuckee(fucker=>Fuck(fucker, 100, continuation));
}

的过程,返回值都改成了callback,相应的循环就变成了递归