精华区文章阅读

发信人: Lerry (坐壮:望苗:思汉@贵族与猫族斗争到底), 信区: Algorithm
标  题: ['91]Robin Milner
发信站: 哈工大紫丁香 (2002年04月26日07:52:25 星期五), 站内信件

[1991]米尔纳--标准元语言(ML)的开发者 (吴鹤龄)
(Ref: http://it.sohu.com/itpeople/Milner.html
      http://www.acm.org/awards/turing_citations/milner.html)
=============================================================================
   1991年度的图灵奖授予了爱丁堡大学计算机科学系教授罗宾·米尔纳(Robin
   Milner)。米尔纳是继M.V.Wilkes(1967)、J.H.Wilkinson(1970)、
   C.A.R.Hoare(1980)之后第四位获此殊荣的英国科学家，这也使英国成为除美国
   之外获得图灵奖学者最多的国家。

   米尔纳生于1934年1月，在皇家学院(King's College)和剑桥大学接受了高等教育
   ，专业是数学，1957年获得学士学位。他上大学期间，米尔纳曾经接触过EDSAC计
   算机(Electronic Delay Storage Automatic Calculator，这是由Wilkes等研制
   的世界上第一台存储程序式电子计算机，也是世界上最早的商品化计算机型号之
   一)，米尔纳应用它编写过解的程序。但当时，米尔纳对计算机并没有重视，也
   没有表现出很大的兴趣。大学毕业以后，米尔纳当了几年中学数学教师，更是把
   计算机全抛在脑后，直到1960年米尔纳重下决心，到伦敦著名的Ferranti公司求
   职。Ferranti公司当时正需要计算机编程人员，对有过编程经历的米尔纳表示欢
   迎，但要求他“把一生都献给计算机”。

   20世纪60年代初，计算机尚未普及，计算机的深刻含意是什么，从事计算机工作
   有多大前途和机会，这对绝大多数人来说都是不甚清楚的事。因此，对
   于Ferranti公司这一要求，米尔纳也深感悦和震惊。所幸的是，米尔纳作出了
   正确的选择，进入Ferranti公司，从而重返计算机领域，并幸运地与计算机科
   学同步成长起来。

   米尔纳在Ferranti公司只干了3年，以后就一直在大学从事教学和研究，其中包
   括伦敦城市大学，威尔士南部海港城市的斯旺西(Swansea)大学。他还在美国斯
   坦福大学工作过2年，但长期的落脚点则是爱丁堡大学，这是英国最著名、历史
   最悠久的高等学府之一，有优良的学术传统，在计算机科学，尤其是人工智能等
   领域，其研究工作曾长期处于世 □ 荨剪平。

   米尔纳的主要贡献有以下几个方面：

   首先，在计算机程序设计语言方面，米尔纳提出了形式化逻辑系统的数学模型，
   实现了他称之为 LCF的一个系统“可计算函数的逻辑”(Logic for Computable
   Functions)。 LCF不但是一种建模工具，还是一种验证工具，利用它可以验证计
   算机程序的正确性。由于在利用计算机解决各种各样的具体问题时，建立正确的
   形式化系统有著重要的意义，米尔纳的 LCF受到学术界高度的评价。实际上，米
   尔纳是受D.Scott(1976年度图灵奖获得者，我们以后将专门介绍)的影响和启发
   才从事这一研究的。Scott是研究自动机理论的著名学者，在60年代提出了标志
   语义模型(Denotational Semantic Model)，对计算机程序设计语言的发展产生
   了重大的影响。Soatt曾到牛津大学访问、讲学，米尔纳听了他的讲演，看了他
   的著作，引起自己对这个问题或力凡影的很大兴趣，从而深入推进有关课题并获
   得成果。70年代初，米尔纳在斯坦福的人工智能实验室时，曾用LCF证明了那里
   的一个很复杂的编译器的正确性，受到有“人工智能之父”之称的 J.McCarthy
   的高度评价。

   在斯坦福，米尔纳学习了由McCarthy主持开发的函数式人工智能程序设计语
   言LISP，这使他进一步打开了思路。回到爱丁堡大学以后，他利用LISP的经验，
   在LCF的基础上，花了12年的时间，主持开发成功了一个更加重要的系统 ML，也
   就是元语言(metalanguage)，一种用来描述、表达与验证其他语言的语言。ML中
   包含了比LCF更强的推理能力。

   ML取得成功以后，米尔纳又致力于使它国际化和标准化。在他的努力下，成立了
   一个由世界各国的专家在内的15人工作小组，采取通过电子邮件交换意见进行设
   计的方式工作标准ML已于20世纪90年代初完成。

   米尔纳另一方面的贡献是并发计算 (concurrent computing)和并行计
   算(parallel computing)。由于并行计算机与传统的串行计算(sequential
   computing)有著本质上的不同，其复杂程度大大增加，无法用后者的方法和术语
   表达前者的意义。米尔纳经过深入研究，利用代数方法创造了一种用于建立并发
   与并行计算的概念框架的系统——CCS(Calculus for Communicating Systems)
   。CCS不但是可用于描述并行计算的一种方法，本身也是一种具体的并行程序设
   计语言。已经成功地用CCS解释了目前广泛使用的描述通信协议的语言LOTOS的规
   格说明(specification)。

   米尔纳在学术上的一个特点是十分注意打好基础，精益求精。他主持开发和标准
   化的ML被认为是定义得最完善、最无懈可击、结构最优美、和谐而又最短小、精
   悍的语言之一。在作风上，米尔纳谦虚谨慎，从善如流，非常注意听取和吸收
   合作者的意见。例如，标准ML有允许设计“大模块” 程序的功能，就是米尔纳根
   据Bell实验室的MacQueen所提出的构思实现的。ML原先是一个专用语言，意大利
   学者LucaCardelli(当时还是一茈缜b写博士论文的研究生)实现了ML的一个扩充
   版本，使之更适合于教学。米尔纳看到以后十分赞赏，在它的基础上把ML进一
   步发展为一个通用语言。米尔纳的成功与他的品格是分不开的。

   米尔纳的著作基本上就是他的成果的反映，主要有：

   《系统间通信的原理》(Calculusof Communicating Systems》
   ，Springer,1980)

   《通信与并发》(《Communicationand Concurrency》， Prendtice Hall
   ，1989)

   《标准ML的定义》《TheDefinition of StandardML》， MITPr,1990)

   《对标准ML的说明》(《Commentaryon Standard ML》
   ，MITPr,1991;reviseded,1997)

   此外，1996年，米尔纳和I.Wand合编了一本《明天的计算：计算机科学未来的研
   究方向(《Computing Tomorrow:FutureResearchDirectionsinComputerScience》
   ，CambridgeUni.Pr.)，书中有包括米尔纳自己撰写的一篇文章在内的总共16篇
   由各方面专家写的文章，论述了有关计算机科学在计算复杂性、软件工程、并
   行计算、自然语言处理、数据库、知识重用、实时计算、安全、通信、交互计算
   、人工智能等各个分支中未来研究漱阆V和重要课题。本书和我们以前介绍过的
   由J.Hartmanis主编的《Computingthe Future——ABroad Agenda for Computer
   cienceand Engineering》(NationalAcademicPr.1992 见“图灵奖得主简介”之
   六)有异曲同工之妙，很值得重视。

   米尔纳在接受图灵奖时发表了题为“交互的原理”(Elements of Interaction)
   的演说，并接受了记者的采访。演说全文以及与记者的对话刊载于1993年1月的
   《Communications of ACM》， 78～97页。在与记者的谈话中，米尔纳表达了这
   样一个观点：计算机科学既是理论性很强的科学，又是与应用和实践密切联系
   著的科学。因此，任何希望在这一领域取得成功的年轻人，必须十分重视把理论
   与实践结合起来。他送给年轻人这样一个忠告：“不要丢失连接!
   ”(Don?tlosethelink!)

   米尔纳目前是剑桥大学计算机实验室教授，其电子信箱为
   ：Robin.Milner@cl.cam.ac.uk。
=============================================================================
Robin Milner

   Citation
          For three distinct and complete achievements: 1) LCF, the
          mechanization of Scott's Logic of Computable Functions,
          probably the first theoretically based yet practical tool for
          machine assisted proof construction; 2) ML, the first language
          to include polymorphic type inference together with a type-safe
          exception-handling mechanism; 3) CCS, a general theory of
          concurrency. In addition, he formulated and strongly advanced
          full abstraction, the study of the relationship between
          operational and denotational semantics.
=============================================================================

--
当一个女孩儿觉得她不太容易了解那个男人的时候，她会爱他。

※ 来源:·哈工大紫丁香 bbs.hit.edu.cn·[FROM: 218.7.32.75]
※ 修改:·Lerry 於 04月26日07:55:48 修改本文·[FROM: 218.7.32.75]

Algorithm 版 (精华区)