王垠:原因与证明_最新动态_新闻资讯_程序员俱乐部

中国优秀的程序员网站程序员频道CXYCLUB技术地图
热搜:
更多>>
 
您所在的位置: 程序员俱乐部 > 新闻资讯 > 最新动态 > 王垠:原因与证明

王垠:原因与证明

 2013/5/19 14:58:50    程序员俱乐部  我要评论(0)
  • 摘要:证明我在Cornell的时候经常遇到这样的问题,那就是教授们一上课就在黑板上写长篇的“定理证明”,全体同学认认真真在下面抄笔记,就连只有十来个人的小课也是那样。有些写字速度慢的人就不得不带上小型录音机,把教授的课全都录下来,要不就是之后去借别人的笔记来抄。有一次某知名教授照着讲义,背对着学生,在黑板上写了大半节课,写下好几板的证明,证明的是simplytypedlambdacalculus(STLC)的strongnormalization特性(SN)
  • 标签:原因

  证明

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

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

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

  原因

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

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

  证明与原因的区别

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

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

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

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

发表评论
用户名: 匿名