Call-By-Name 不过是带定界控制的 Call-By-Value

定界控制算子 shift0 展现出多样能力：它可表达分层单子效应，或等价地，代数效应。我们鲜知其也能表达 lambda 演算！我们提出 \Lambda_\ $，一种扩充了 shift0 与控制定界符$ $ $并带有精心构造归约理论的 call-by-value lambda 演算，使得带有 beta 与 eta 归约的 lambda 演算可通过一个 continuation-passing style 翻译的右逆同构地嵌入$ \Lambda_$ $中。虽然 lambda 演算的 call-by-name 归约可平凡地模拟其 call-by-value 版本，我们表明 shift0 与$ $ $的加入是表达力的黄金中点：足以模拟 beta 与 eta 归约，同时仍允许反向模拟。作为推论，演算$ \Lambda\mu_v $、$ \lambda_$ $、$ \Lambda_$ $与$ \lambda $ 在方程意义上均相对应。