新的希望
2017-02-12 19:18:27| 分类：
默认分类
| 标签：
|举报
|字号大中小 订阅
本文简要介绍我自从2017年初以来新的变化和学业上的主要进展。
我目前属于博洛尼亚大学2014年入学，目前已在编外（Fuori corso / out of course）的学生。我的成绩单其实不算难看，很多课程都是满分30分，其中还有3门课是最高分（30L）可以体现出教授对我的充分肯定。其实我校计算机系的给分标准相对较高，学生通过数次考试以后最终拿到高分并不难，甚至某些选修课程只要完成了教授要求的全部工作即可轻松拿到满分，就好像只要肯选修就已经很值得表扬了似的。所以通过成绩单本身并不一定能看出学生的实际学习能力。但我眼下还真的是除了成绩单以外别的什么更像样的也没有了。
这段时间来最大的成就是基本上学会了
HOL 定理证明器的使用，顺便也能看懂其他定理证明器（主要是 Coq 和 Isabelle）的代码了，然后一下子证出了上百个小定理。但是到目前为止对应的课程项目还没完成。自从定理证明入门了以后，我产生了很多新的想法：1. HOL 形式化概率论的改进，外加大数定律的形式化证明。2. 图论的一般性形式化（目前为止的类似工作都跟标准教科书上的定义相去甚远，难以扩展和重用）。3. 编程语言的静态分析，可以作为我过去暂时放弃的一门课的课程项目。4. 并行理论（CCS, LCS）的形式化验证工具。但由于我还不是很熟悉 HOL 现有的定理库，实际操作过程中发现哪怕向前走一小步都举步维艰。所以我决定还是从长计议，先通过迁移 Coq 代码和移植古老的 HOL 代码来进一步熟悉工具，然后再开始证明新的定理。
尽管在定理证明方面并没有拿到学分，但我对 Lambda 演算、类型系统等理论计算机基础知识的理解毫无疑问地加深了，而且这比光是枯燥地看教材和课程笔记理解得更加深入。相关的回报就是我在1月16日那天顺利通过了 FLI（计算机科学的逻辑基础）的口试，又得到一个宝贵的6学分。回想我在突然发现考试可以注册了以后仅有5天的复习时间，于是临时决定放手一搏，不通过也没关系，但竟然顺利通过了，分数也还不错（28）。这门课是系主任亲自教的，把关算是比较严格的。
相比之下我在高等概率论上花的功夫更多，用 LaTeX 整理了 70 页的电子笔记，内容胜过单独任何一本教科书。但在2月8日的第三次考试尝试中还是失败了。复杂的上层定理是理解了，偏偏卡在了基础定理上。回想考试那天我西装革履，充满自信，而且还是先去上了一节梵语课，下课后立即赶赴考场。轻松的心态溢于言表。这一次我有10天的复习时间，也充分准备了，但是不得不承认还是有没能很好理解的所有知识点。教授比较严格，但也无可厚非，我能看出他是希望我再进一步学习一下的，绝对没有因为我不是数学系的学生而鄙视我的意思。我事后发邮件表示会再去听一轮他的数学课，这次彻底理解所有讲授定理的证明，并且是教授自己的证明版本。
下面谈谈梵语的学习进展。今年我时间充裕了，不用工作了，重新开始跟随学校课程学习梵语时感觉比以往学得好多了。我手里有往年已通过课程的中国同学借我的笔记，所以书本上每个例句的标准答案我都有。这样一来就方便多了，至少不用走什么弯路了，然后我再用整理出我自己的电子版本，用 InDesign CS6 做多种语言的混合排版。梵语的学习过程中，必须对那些精心挑选出来的例句加以反复研究，因为只有这样才能真正记住那些繁复的词法和语法规则。我过去就是因为脱离了例句，结果既不能记住重要的词汇，也反复都背部下来各种动词和名词的变化规则，反反复复记住了一些然后再很快忘掉，走了不少弯路。而如今我总算掌握窍门了。只要保持下去，今年5月课程结束的时候我有充分的信心通过梵语的考试。
我在梵语上的学习目标当然不仅仅满足于通过考试——也就是正确地分析所有学过的例句（包括记住所有例句中用到的词汇），我的最终目标是把古印度的梵语语法著作里描述的梵语语法规则形式化，或者说以某种形式输入计算机，以期直接得到一个能否解析梵语语句的软件系统。这项工作的任务十分艰巨，因为首先必须基于梵语的现代语法学会这门语言，能够熟练地手工分析句子，然后还必须能看懂古代语法书——Panini《八章书》和 Diksita《最后定论的月光》，最后才能开始着手代码层面的工作。利用定理证明器的推理能力来自动推导梵语语法仅在理论上是可行的，实际如何操作我目前全无想法。用 Lisp 从头写一个针对梵语古代语法的规则引擎也只是理论可行，这一切都要先熟悉了古代语法究竟都说了些什么才行。
从 Diksita《最后定论的月光》第一卷的目录结构来看，梵语语法中关于词的各种构造占据相当大的篇幅（接近2/3），而这些内容在其他语言里往往根本就不写入语法，不同的词汇仅作为词典里不相关的原子来处理。但梵语则不同，尤其是名目繁多的各类复合词在实际句子中使用之多已经达到了登峰造极的地步，不能正确理解复合词就几乎无法阅读任何实际的梵语书籍，相比之下我过去背了很多年都背不下来的简单名词变格法在整个梵语语法体系里也就5%不到的样子。
作为一个已经快到 35 岁的二手学者。我最向往的几门高层次知识（梵语、数学、形式化方法/定理证明）由于我的资质愚钝和这些知识本身的复杂性，我都没有学好，可以说远没有达到“学会了”的程度。但是时间和金钱却不等人，我必须在今年里毕业，要么读博士要么找工作，只有先活下来才有机会继续深入学习那些我为之神往的知识，只有先活下来才有机会继续感受人类文明。我现在每天脑子里想的就只是这些知识，以及尽快推进我的各项课程进度好早日毕业，其他的一切都是次要的。女人现在对我来说则是最不重要的。
评论这张
转发至微博
转发至微博
关闭
玩LOFTER，免费冲印20张照片，人人有奖！
我要抢>
<#--最新日志，群博日志-->
<#--推荐日志-->
<#--引用记录-->
<#--博主推荐-->
<#--随机阅读-->
<#--首页推荐-->
<#--历史上的今天-->
<#--被推荐日志-->
<#--上一篇，下一篇-->
<#-- 热度 -->
<#-- 网易新闻广告 -->
<#--右边模块结构-->
<#--评论模块结构-->
<#--引用模块结构-->
<#--博主发起的投票-->
评论