PersonalCorpus 版 (精华区)

发信人: ssos (存在与虚无·守拙), 信区: Algorithm
标  题: 关于学习计算机形式语义学的一点推介
发信站: 哈工大紫丁香 (2003年02月23日21:41:13 星期天), 站内信件

关于学习计算机形式语义学的一点推介
（附FAQ在小百合上的RE文一篇，其中给出了更详细的中文参考资料）
前一阵系版上有人问了一些关于形式语义学课程方面的问题，当时随便回了一篇，介绍
了一些参考书，之后觉得也许应该写得再详细一些，因此不揣浅薄，写了这篇介绍。不
过我自己的水平实在有限，也没有上过这方面的正规的课程，只是自己学习过一些，加
之现在的工作中经常性地涉及这些有关语义的东西，所以颇有些了解，但是其中错误和
纰漏也许是在所难免的了。
《形式语义学》这门课在南大计算机系已经有多年没有开过了，比我们高一级的师兄师
姐们（也就是98级的研究生）曾经有幸上过这门课，但是在我读研的三年内却一直没有
开。不知道以前所用的是什么讲义，不过那时的讲义估计不太可能在网上找到。去年上
半年，也就是2000－2001学年的第二学期，系里给研究生开过一门《程序设计理论》(T
he Science of Programming)，其中涉及很多有关公理语义的知识，据说那是最后一次
开那门课，不知真假。不过那门课的内容实在是太陈旧了（虽然我很尊敬主讲的老师）
，其中值得学一学的内容估计有个两到三次课就足够了，因此没有赶上的同学倒也不必
感到十分可惜。不过话说回来，不管怎样这门课还是有一点实质性的内容，而且主讲的
教师是真正了解这门课程的内容并且是很负责地在教授的，这在我们系的研究生课程中
已经不多见了。
关于《形式语义学》的参考书，英文的有很多，中文我只知道两本。一本是周巢尘写的
，很薄的一本，我不知道题目，是以前国防科大的一个朋友推荐的。此书的口碑不错，
看过周巢尘翻译的《通信.顺序.进程》（原著为C. A. Hoare）的人都应该相信此书的质
量。但是这本书是80年代写的，估计是太老了。另一本是陆汝乾写的《形式语义学》，
很厚，象字典，内容包揽了操作语义、指称语义、公理语义和代数语义，但是我以前的
导师只推荐我看其中关于petri网的内容，也就是说有关语义的部分都不要看。这本书我
读过一点，当时的感觉是确实很难读，也许是我当时水平不够吧，此后再没有碰过。此
外，据说陈意云也写过一本关于形式语义学的书，我没有见过，但是读过他的一本讲范
畴论的书，完全是翻译国外的一本讲义，连整体结构都是照搬，而且翻译得很差。我不
敢以此揣测他的形式语义学的著作（如果存在的话），但是即使他确实写过，也从来没
有人向我推荐过。
英文的参考书有很多,有几本很值得推荐：
The Formal Semantics of Programming Languages
Glynn Winskel, MIT express, 1993
我当时看的主要是这一本，写得很不错，并不难读，很多大学如Cambridge、Edinburgh
的 LFCS都将它作为首选的参考书，强烈推荐，其内容涵盖操作、指称、公理三种语义，
偏重介绍指称语义，这是现在形式语义学的主要研究方向，本系图书馆可以借到。
Semantics of Programming Languages:Structures and Techniques
Carl A. Gunter, MIT express, 1992
这本书中的数学较第一本难一些，不适合作为初学形式语义的教材（个人观点），而且
好像仅涉及指称语义。我前一阵浏览过其中的一些章节。
The Semantics of Programming Languages: an Elementary Introduction using Str
uctural Operational Semantics
Matthew Hennessy, John Wiley and Sons, 1990
这是一本主要介绍操作语义的书，写得很具体，很适合作为入门教材，只是内容涵盖范
围太窄，基本上只涉及操作语义，而且可能操作语义一些比较新的内容也没有涉及。此
书已经停印了，但可以在网上下到 电子版。
Foundations for Programming Languages
John C. Mitchell, MIT express, 1996
这是一本十分全面的介绍程序设计理论的著作，正如书的导言里所说，它可以作为多门
与程序设计理论相关的课程的教材或参考书。非常厚，我通常拿它当字典用，本系图书
馆也有的借。
上面这些书中，除了第三本以外，其他都属于MIT出版的Foundation of Computer Scie
nce 系列。这个系列非常好，虽然看上去涉及领域不多，但是如其名称所指，是计算机
科学研究的Foundation，而且大多数都是由特定的领域内很知名的教授和研究者所著，
质量还是值得信赖的。
除了这些书外，还可以在一些大学的网站上找到该课程或相关课程的一些讲义，我个人
强烈推荐Cambridge的课程讲义，Andrew Pitts 所编，结构很清晰，可以在Pitts的主页
上下载到。他的讲义主要关于操作语义和指称语义，这是现在研究程序设计理论所主要
使用的两种语义，其中操作语义现在主要应用于并发领域。公理语义现在已经很少听人
提起了，可能在一些特定领域内，如程序自动生成和验证，还有应用，我不是很清楚。
不过作为一种曾经比较主流的语义，我觉得还是应该了解一下。关于公理语义，有两本
参考书可以看看：
Predicate Calculus and Program Semantics
E. W. Dijkstra and C. S. Scholten, Springer-Verlag, 1990
The Science of Programming
David Gries, Springer Verlag, 1981
另外，目前还有一种比较流行的新兴语义，称为Game Semantics，中文译作博弈语义，
很有意思。大概的思想是将程序和程序所运行的环境分别看作player和opponent，程序
则被解释为这两者相互交互的一系列动作。举个简单的例子，任何程序都可以看作从输
入到输出的一个函数（不考虑并发），下面是player和opponent的一段对话：
O：请问P同学，你的程序的输出是什么？
P：嘿嘿，你想知道程序的输出吗？那你得先告诉我程序的输入。
O：啊，有道理的说，现在我告诉你输入是3。
P：嗯，如果输入是3的话，那么我的程序的输出是......4。
当然，这只是一个十分简单的例子，每当进入一个内部的子过程或函数时，O与P的角色
就会交换，而且这样的O、P交替的序列还要进一步被形式化，用数学的方法来表示。博
弈论现在好像很流行，而且在很多领域都有应用。我对博弈论了解不多，不过好像有一
个准则，即是要求博弈的双方都足够聪明，在实际生活中你很难做到，但是如果用计算
机模拟的话，却是可能的，而且从直觉上讲，它非常适合计算机的本性。另外，似乎通
过Game Semantics 的方法，可以构造出一个fully abstract的模型，fully abstract是
形式语义学中一个十分重要的概念，在很多形式语义学的书上都有介绍，这里不罗嗦了
。目前在Game Semantics 上研究比较活跃的两个人是Samson Abramsky 和Guy McCuske
r，在他们的主页上找到一些介绍性的文章和lecture notes。
一些浅见，望不吝指正。
----------------------------------------------------------------------------
----
附：FAQ的RE文（转自南京大学小百合站）
补充有关中文的，其实偶看得很少，主要谈谈印象吧。
1、周巢成，应为“周巢尘”，《形式语义学引论》，湖南科学技术出版社
   评论如你说述。
2、陈意云，《形式语义学基础》，中国科学技术大学出版社
   也不能算很差。不过过于简单，完全不深入，好在作介绍和入门导引看看会比较轻松
。陈老师现在在中科大依然开这门课，他的主页上可以下载新的讲义。
3、屈延文，《形式语义学基础与形式说明》
   非常喜欢这个人的行文和讲法，这本书的早期版本是一本油印的北大教材，而且是两
分册，系里和学校都有，后来由科学出版社89年正式出版。
4、陆汝乾，《计算机语言的形式语义》
   这本“砖头”算是国内这方面的经典教材了，可能是软件所考研(博)的教材。陆公功
力深厚，民主德国耶拿大学数学系毕业，而且文字功底也没得说。他以前的书偶很爱看
，后来好像陆老搞人工智能了。
遗憾的是这些书都是以前出的，足见现在国内的理论研究的氛围甚至不如以前。这样的
时代，这样的发展时期也大约只能如此，怨不得什么，希望以后会好，很多人起码很诚
实地说，我们实际上只搞开发不搞科研。

--

   
<<社会契约论>>是一本好书,应当多读几遍
风味的肘子味道不错,我还想再吃它      

※ 来源:·哈工大紫丁香 bbs.hit.edu.cn·[FROM: 202.118.230.220]