Lambda 表达式无法定义的一个算符

By guenchi at 2018-02-04 • 0人收藏 • 169人看过

https://zhuanlan.zhihu.com/p/20049022


很多人都问我如何理解 yield 云云,事实上 yield 以及其他的类似物包括 call/cc 都是用 Lambda 演算无法定义的东西。


就比如 call/cc 吧,如果我们规定 Continuation 永不返回,或者说它是发散的,那么它的类型可以唯一指定成\alpha\rightarrow\bot,或者说\neg\alpha。那么考虑 call/cc 算子,它的类型首先肯定得满足((\alpha\rightarrow\bot)\rightarrow\beta)\rightarrow\gamma,而考察 call/cc(f) 两种可能的返回情况——通过(丢给 f 的) continuation 返回或者 f 正常返回——那么可以得到等式\alpha=\beta=\gamma,即:\mathrm{call/cc}:(\neg\alpha\rightarrow\alpha)\rightarrow\alpha。若允许 Continuation 返回,则 call/cc 的类型可定为((\alpha\rightarrow\beta)\rightarrow\alpha)\rightarrow\alpha。接下来将证明这条定律可以推出排中律(使用 LJ 推理系统):

  • α ⊢ α [I]

  • α ⊢ α ∨ ¬α [∨R](1);

  • ⊥ ⊢  [I]

  • α, ⊥ ⊢  [WL](2);

  • α, (α ∨ ¬α) → ⊥ ⊢  [→L, (1), (2)](3);

  • α, (α ∨ ¬α) → (α ∨ ¬α) → ⊥ ⊢  [→L, (1), (3)]

  • α, ((γ → β) → γ) → γ, (α ∨ ¬α) → (α ∨ ¬α) → ⊥ ⊢ ⊥ [WL]

  • ((γ → β) → γ) → γ, (α ∨ ¬α) → (α ∨ ¬α) → ⊥ ⊢ α → ⊥ [→R]

  • ((γ → β) → γ) → γ, (α ∨ ¬α) → (α ∨ ¬α) → ⊥ ⊢ α ∨ ¬α [∨R]

  • ((γ → β) → γ) → γ ⊢ ((α ∨ ¬α) → ¬(α ∨ ¬α)) → (α ∨ ¬α) [→R]

  • ((γ → β) → γ) → γ ⊢ α ∨ ¬α [MP,代换律]

换言之,如果 call/cc 是 Lambda 可表的,则意味着直觉自然演绎可以证明排中律——这显然不可能,于是 call/cc 必然是 Lambda 不可表,它必须作为单独的算符扩充到 Lambda 演算的体系里来。


登录后方可回帖

登 录
信息栏

Scheme中文社区

推荐实现 ChezScheme / r6rs / r7rs large
theschemer.org
Q群: 724577239

精华导览

社区项目

包管理器:Raven
HTTP服务器:Igropyr (希腊火)
官方插件:vscode-chez

社区目标:

完善足以使Scheme工程化和商业化的库,特别是开发极致速度的Web服务器和ANN模块。

一直以来Scheme缺少一个活跃的中文社区,同时中文资料的稀少,导致大多数因为黑客与画家和SICP而接触Scheme的朋友,在学完SICP后无事可做,不能将Scheme转换为实际的生产力。最后渐渐的放弃。
同时Chicken等实现,却因效率问题无法与其他语言竞争。本社区只有一个目的,传播Scheme的文明之火,在最快的编译器实现上,集众人之力发展出足够与其他语言竞争的社区和库。


友情链接:

Clojure 中文论坛
函数式·China


Loading...