原因与证明

By guenchi at 2018-02-06 • 0人收藏 • 127人看过

作者:王垠


证明

我在 Cornell 的时候经常遇到这样的问题,那就是教授们一上课就在黑板上写长篇的“定理证明”,全体同学认认真真在下面抄笔记,就连只有十来个人的小课也是那样。有些写字速度慢的人就不得不带上小型录音机,把教授的课全都录下来,要不就是之后去借别人的笔记来抄。

有一次某知名教授照着讲义,背对着学生,在黑板上写了大半节课,写下好几板的证明,证明的是 simply typed lambda calculus (STLC)的 strong normalization 特性(SN)。刚写完就到下课时间了,他回过头来喘了一口气,说:“Any questions?”没有人啃声,于是他说:“很好!下课!”

几天后我问他,你证明了 STLC 有这个特性,然而你却没有告诉我它“为什么”有这个特性。他神气的看了我一眼:“你不懂吗?”我说:“你的证明我看懂了大部分,可是一个东西具有如此的性质,并不是因为你证明了它。这性质是它天生就有的,不管你是否能证明它。我想知道的是什么让 STLC 具有这个性质,而不只是证明它。”他说:“你问这样的问题有什么意义吗?你需要非常聪明,并且需要经过大量的努力才能想出这样的证明。”

原因

两年之后,我在 Indiana 上了另外一堂程序语言理论课。教授是我之前的导师 Amr Sabry。他上课从来不带讲义,貌似也没有准备,漫不经心的,却每次都能讲清楚问题的关键。于是有一天他也开始讲 STLC 的 SN 特性。他说,我不想写下这个证明让你们抄,我只告诉你们大概怎么去想。SN 的意思就是程序肯定会“终止”。所有会终止的程序,都会有一个“特征值”会随着程序的运行而减小。你需要做的就是找到 STLC 的“特征值”是什么。接着他就开始在黑板上画一个图……

过了一段时间,我不仅学会了这个“证明”,而且知道了 STLC 具有如此特性的“原因”。

证明与原因的区别

从以上的故事,以及你的亲身经历中,你也许注意到了大部分的教育过分的重视了“证明”,却忽略了比证明更重要的东西——“原因”。

原因往往比证明来得更加简单,更加深刻,但却更难发现。对于一个事实往往有多种多样的证明,然而导致这个事实的原因却往往只有一个。如果你只知道证明却不知道原因,那你往往就被囚禁于别人制造的理论里面,无法自拔。你能证明一个事物具有某种特性,然而你却没有能力改变它。你无法对它加入新的,好的特性,也无法去掉一个不好的特性。你也无法发明新的理论。有能力发明新的事物和理论的人,他们往往不仅知道“证明”,而且知道“原因”。

打个比方。证明与原因的区别,就像是犯罪的证据与它的原因的区别。证据并不是导致犯罪的原因。有了证据可以帮助你把罪犯绳之以法,可是如果你找不到他犯罪的原因,你就没法防止同样的犯罪现象再次发生。

古人说的“知其然”与“知其所以然”的区别,也就是同样的道理吧。


登录后方可回帖

登 录
信息栏

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...