注册 登录  
 加关注
   显示下一条  |  关闭
温馨提示!由于新浪微博认证机制调整,您的新浪微博帐号绑定已过期,请重新绑定!立即重新绑定新浪微博》  |  关闭

Chun Tian (binghe)

超越自我,洞察宇宙

 
 
 

日志

 
 

ACL2,Prolog ...  

2013-12-23 02:52:32|  分类: 默认分类 |  标签: |举报 |字号 订阅

  下载LOFTER 我的照片书  |
ACL2,Prolog ... - 冰河 - Chun Tian (binghe)

后来工作上的不愉快逐渐平息了,表面上看这是团队成员间加强沟通努力消除误会的成果,实质上是以大局为重的进一步妥协,所以迟早还是会再出事的。不过我不担心,因为早已经习惯工作在剑拔弩张的环境里,在动态平衡中寻求相对稳定的价值输出了。总之一切仍在掌控之中。

过去两周里取得了一些相当不错的进展。首次在产品里实现了基于 CAS 的无锁队列,然后想出了一种符合产品代码特点的方式来解决 ABA 问题;由于希望从理论上证明无锁算法代码的正确性,这次终于下狠心去研究 ACL2 定理证明器,然后竟然第一次看懂了家中收藏已久的 ACL2 入门教材,这距离我最初得到那两本教材已经差不多快十年了;Common Lisp 程序员当然要在 Coq 和 ACL2 之间果断选择后者。使用定理证明器的关键在于认识到证明器的各种能力限制——必须学会对想要解决的问题进行正确的建模,然后只有写出适当的引理才能顺利到达证明的终点,而且跟使用编程语言写代码不同的是,定理证明器的每一个成功案例似乎都是一种高度创造性的劳动,这个领域的“最佳实践”类论文不计其数。掌握这类工具的一种对我未来的科研活动至关重要,就像语言技能一样不可或缺,所以无论花多少精力都是值得的。

甚至关于 Prolog 和逻辑型编程方面也有一点儿进展,因此我打算元旦后开始正式学习手头的一本 Prolog 教材,顺便把书中的所有 Prolog 代码在 LispWorks 的 KnowledgeWorks 和 G2 的 KB 语言里重写一遍。我的感觉是其实所有的逻辑型编程语言都是彼此等价的,区别仅在于性能和其他细节上,所以只要通过无论哪种具体语言的教材学会了逻辑型编程本身就可以把成果应用在所有同类的编程环境里了。



ACL2,Prolog ... - 冰河 - Chun Tian (binghe)

留学申请还在继续走流程,学校的反馈至少说明我邮寄的所有材料他们都收到了。现在就是一方面等待前些日子在上海考的意大利语 CILS B1 成绩,另一方面继续准备考 CILS B2。

眼下三门语言的课程(意、西、德)都在上,虽然业余没什么时间复习但好歹算是把学习成果保持住了,继续一步一个脚印地积累语言知识。明年结束掉意大利语的学习以后,继续把过去没上完的法语课上完。我的德语老师很可能会成为我在法语班里的同学,这令人期待。

圣诞节和新年就快到了,没有什么庆贺的心情,因为我的 2013 年太充实了,年终之际没有任何遗憾。我会在今年的年鉴里做个简要的总结。
  评论这张
 
阅读(2734)| 评论(10)
推荐 转载

历史上的今天

评论

<#--最新日志,群博日志--> <#--推荐日志--> <#--引用记录--> <#--博主推荐--> <#--随机阅读--> <#--首页推荐--> <#--历史上的今天--> <#--被推荐日志--> <#--上一篇,下一篇--> <#-- 热度 --> <#-- 网易新闻广告 --> <#--右边模块结构--> <#--评论模块结构--> <#--引用模块结构--> <#--博主发起的投票-->
 
 
 
 
 
 
 
 
 
 
 
 
 
 

页脚

网易公司版权所有 ©1997-2017