热心网友
回答时间：2023-05-09 08:21
call/cc 是非常、非常特殊的，因为它根本无法用 Lambda 演算定义。
研究中使用了扩展的演算来处理这玩意。
演算引入了一个结构算符，以及标记项（它表示将表达式标记为 ），对算符的展开满足
左结构嬗变：
右结构嬗变：
换言之，在「函数」被调用，或者被传入其他函数的时候，其体内所有和参数同标记的标记项都会以相同的形式被「调用」或者「传入其他函数」一次。算符可以将自己「外面」的东西翻到自己里面来。
在有这个算符之后，我们就能定义。在式子里就是 Continuation，我们可以看下它会变化成怎样：
被传入：
被调用：
嗯……
在 Curry-Howard 同构的层面，call/cc 对应皮尔士定律，它代表着排中律，这条定律是 Lambda 演算所对应的直觉逻辑里没有的。演算经过 C-H 同构可以得到经典逻辑。
本文如未解决您的问题请添加抖音号：51dongshi（抖音搜索懂视），直接咨询即可。
