Home >Backend Development >Python Tutorial >函数式编程中cps（continuation-passing style ）是什么意思？

函数式编程中cps（continuation-passing style ）是什么意思？

PHP中文网Original: 2017-03-30 15:23:394335browse

有没有不基于lisp、c++的例子，最好是python的，也有lamdba expression嘛。

回复内容：

CPS把函数调用完之后接下来要执行的代码通过闭包包裹并作为函数参数调用要执行的函数。

Continuation Passing Style Revisited Part Five: CPS and AsynchronyCPS变换本质上就是调用一个函数的时候，给它传入另一个函数（所以，语言必须得支持高阶函数和闭包才行），被调函数不把结果返回调用者，而是将结果返回给通过参数传进来的那个函数。

我不清楚这个概念在别的语言里有没有实现，或者叫不同的名字。

这里有个 scheme 的例子：call/cc 探秘从另一个角度回答下吧。
带 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 变换。直接照搬哥德尔-根岑变换里的类型的话，我们有如下结果：

原子 $a^*=\lambda\kappa.\kappa a$
调用 $(EF)^*=\lambda\kappa.E^*(\lambda E'.F^* (\lambda F'.(E'F')\kappa))$
抽象 $(\lambda x.E)^*=\lambda\kappa.\kappa(\lambda x.\lambda k. (e^*)k)$
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 的。

上面这些再一次说明了，逻辑学和编程有多么紧密的联系。来个简明补充。

这是个简单函数计算输出：

  static int Times3(int x)
    {
        return x * 3;
    }
   Console.WriteLine(Times3(5));

（答案抄袭自http://www.cs.indiana.edu/cgi-pub/lkuper/c311/_media/cps-notes.scm）
定义下面四个函数（为了保持和原答案一致，其实两个就够了）

def f(var0):    
passdef g(var0, var1):    
return passdef h(var0):    
return passdef j(var0):    
return pass

其实就是把

Fuckee 
FindFuckee(){return kula;}void Fuck(Fuckee fuckee, int count){
for(int i=0;i<count;i++)
fuckee.Fuck();}void Main(){Fuck(FindFuckee(), 100);}

可以补一补逻辑学.... @Belleve的回答太抽象了，没逻辑背景的人看不懂，
我在Quora上看到一个回答写得挺好的，里面从逻辑学的角度解释的一节或许可以作为 @Belleve答案的补充：
What is continuation-passing style in functional programming?

以上就是函数式编程中cps（continuation-passing style ）是什么意思？的内容，更多相关内容请关注PHP中文网（www.php.cn）！

Statement：

The content of this article is voluntarily contributed by netizens, and the copyright belongs to the original author. This site does not assume corresponding legal responsibility. If you find any content suspected of plagiarism or infringement, please contact admin@php.cn

Previous article：如何理解 Tornado ？Next article：为什么 Python 不是 lexical scoping？

See more

函数式编程中cps（continuation-passing style ）是什么意思？

回复内容：

Related articles