以文本方式查看主题 - 中文XML论坛 - 专业的XML技术讨论区 (http://bbs.xml.org.cn/index.asp) -- 『 理论计算机科学 』 (http://bbs.xml.org.cn/list.asp?boardid=64) ---- 数理逻辑大师们[转帖] (http://bbs.xml.org.cn/dispbbs.asp?boardid=64&rootid=&id=30781) |
-- 作者:chzhuang -- 发布时间:4/18/2006 3:16:00 PM -- 数理逻辑大师们[转帖] 小庄编:回顾计算机科学的发展,我们可以清晰地发展数理逻辑一直是计算机科学的理论基础和发展动力。如果没有这些数理逻辑学家的工作,没有这些计算机科学大师的工作,我们就没有电脑,也就没有网络,我们今天就不能在这里用电脑玩游戏上网收发邮件QQ聊天之类。所以,应该向这些大师致敬!他们是莱布尼兹(同时也是哲学家物理学家),弗雷格(同时也是分析哲学的创始人),希尔伯特(上世纪的大数学家),哥德尔(两个不完全定理提示了人类智力的限度),邱奇(递归论的创始人),图灵(图灵机的创始人现代计算机科学的创始人),麦卡锡(人工智能之父同时也是非经典逻辑的发展者),霍尔(公理语义学的创始人用逻辑来分析程序理论) Fuleige 弗雷格
[此贴子已经被作者于2006-4-18 16:06:16编辑过]
|
-- 作者:chzhuang -- 发布时间:4/18/2006 3:17:00 PM -- ●希尔伯特,D.(Hilbert,David,1862~1943) 希尔伯特,D.(Hilbert,David,1862~1943)德国数学家,生于东普鲁士哥尼斯堡(前苏联加里宁格勒)附近的韦劳。中学时代,希尔伯特就是一名勤奋好学的学生,对于科学特别是数学表现出浓厚的兴趣,善于灵活和深刻地掌握以至应用老师讲课的内容。1880年,他不顾父亲让他学法律的意愿,进入哥尼斯堡大学攻读数学。1884年获得博士学位,后来又在这所大学里取得讲师资格和升任副教授。1893年被任命为正教授,1895年,转入格廷根大学任教授,此后一直在格廷根生活和工作,于是930年退休。在此期间,他成为柏林科学院通讯院士,并曾获得施泰讷奖、罗巴切夫斯基奖和波约伊奖。1930年获得瑞典科学院的米塔格-莱福勒奖,1942年成为柏林科学院荣誉院士。希尔伯特是一位正直的科学家,第一次世界大战前夕,他拒绝在德国政府为进行欺骗宣传而发表的《告文明世界书》上签字。战争期间,他敢干公开发表文章悼念“敌人的数学家”达布。希特勒上台后,他抵制并上书反对纳粹政府排斥和迫害犹太科学家的政策。由于纳粹政府的反动政策日益加剧,许多科学家被迫移居外国,曾经盛极一时的格廷根学派衰落了,希尔伯特也于1943年在孤独中逝世。 希尔伯特是对二十世纪数学有深刻影响的数学家之一。他领导了著名的格廷根学派,使格廷根大学成为当时世界数学研究的重要中心,并培养了一批对现代数学发展做出重大贡献的杰出数学家。希尔伯特的数学工作可以划分为几个不同的时期,每个时期他几乎都集中精力研究一类问题。按时间顺序,他的主要研究内容有:不变式理论、代数数域理论、几何基础、积分方程、物理学、一般数学基础,其间穿插的研究课题有:狄利克雷原理和变分法、华林问题、特征值问题、“希尔伯特空间”等。在这些领域中,他都做出了重大的或开创性的贡献。希尔伯特认为,科学在每个时代都有它自己的问题,而这些问题的解决对于科学发展具有深远意义。他指出:“只要一门科学分支能提出大量的问题,它就充满着生命力,而问题缺乏则预示着独立发展的衰亡和终止。”在1900年巴黎国际数学家代表大会上,希尔伯特发表了题为《数学问题》的著名讲演。他根据过去特别是十九世纪数学研究的成果和发展趋势,提出了23个最重要的数学问题。这23个问题通称希尔伯特问题,后来成为许多数学家力图攻克的难关,对现代数学的研究和发展产生了深刻的影响,并起了积极的推动作用,希尔伯特问题中有些现已得到圆满解决,有些至今仍未解决。他在讲演中所阐发的想信每个数学问题都可以解决的信念,对于数学工作者是一种巨大的鼓舞。他说:“在我们中间,常常听到这样的呼声:这里有一个数学问题,去找出它的答案!你能通过纯思维找到它,因为在数学中没有不可知。”三十年后,1930年,在接受哥尼斯堡荣誉市民称号的讲演中,针对一些人信奉的不可知论观点,他再次满怀信心地宣称:“我们必须知道,我们必将知道。”希尔伯特的《几何基础》(1899)是公理化思想的代表作,书中把欧几里得几何学加以整理,成为建立在一组简单公理基础上的纯粹演绎系统,并开始探讨公理之间的相互关系与研究整个演绎系统的逻辑结构。1904年,又着手研究数学基础问题,经过多年酝酿,于二十年代初,提出了如何论证数论、集合论或数学分析一致性的方案。他建议从若干形式公理出发将数学形式化为符号语言系统,并从不假定实无穷的有穷观点出发,建立相应的逻辑系统。然后再研究这个形式语言系统的逻辑性质,从而创立了元数学和证明论。希尔伯特的目的是试图对某一形式语言系统的无矛盾性给出绝对的证明,以便克服悖论所引起的危机,一劳永逸地消除对数学基础以及数学推理方法可靠性的怀疑。然而,1930年,年青的奥地利数理逻辑学家哥德尔(K.Gödel,1906~1978)获得了否定的结果,证明了希尔伯特方案是不可能实现的。但正如哥德尔所说,希尔伯特有关数学基础的方案“仍不失其重要性,并继续引起人们的高度兴趣”。希尔伯特的著作有《希尔伯特全集》(三卷,其中包括他的著名的《数论报告》)、《几何基础》、《线性积分方程一般理论基础》等,与其他合著有《数学物理方法》、《理论逻辑基础》、《直观几何学》、《数学基础》 希尔伯特问题研究进展 问 题 推动发展的领域 解 决 情 况 1.连续统假设 公理化集合论 1963年,Paul J.Cohen[美国]在下述意义下证明了第一问题是不可解的,即:连续统假设的真伪不可能在Zermelo-Fraenkel公理系统内判明。 2.算术公理的相容性 数学基础 Hilbert证明算术公理相容性的设想,后来发展为系统“Hilbert计划”,但1931年Godel的“不完备定理”提出用“元数学”证明算术公理相容性之不可能。数学相容性问题至今尚未解决。 3.两等高等底的四面体体积之相等 几何基础 这问题很快(1900年)即由Hilbert的学生M.Dehn给出肯定解答。 4.直线作为两点间最短距离问题 几何基础 这问题提得过于一般。Hilbert之后,许多数学家致力于构造和探讨各种特殊的度量几何,在研究第四问题上取得很大进展,但问题并未完全解决。 5.不要定义群的函数的可微性假设的李群概念 拓扑群论 经过漫长的努力,这个问题于1952年由Glenson、Montgomery、Zippin等人[美国]最后解决,答案是肯定的。 6.物理公式的数学处理 数学物理 在量子力学、热力学等部门,公理化方法已获很大成功,但一般地说,公理化的物理意味着什么,仍是需探讨的问题。至于概率论的公理化,已由A.H.K o лМ o r o p oB[前苏联,1933]等人建立。 7.某些数的无理性与超越性 超越数论 1934年,A.O.г e M ж o H д[前苏联]和Schneider[德国]各自独立解决了这问题的后半部分,即对于任意代数数α≠0,1和任意代数无理数β≠0证明了α攩β攪的超越性,1966年这一结果又被A.Baker等人大大推广和发展了。
苹果树下的散步 1888年9月6日,人们惊喜地获悉:十多年来许多数学家为之奋斗的著名难题——果尔丹问题,终于被一位当时尚名不见经传的青年人攻克了。他运用的方法和途径是那样的出人意料、令人折服,就像亚历山大解开绳结一样;也正如这位显赫的君主在辽阔的欧亚大陆上留下旷世战功,这位年轻人穷尽毕生心血和才华,在广阔的数学领域里纵横捭阖,遍及现代数学几乎所有的前沿阵地,在整个数学的版图上,到处都刻下他那光辉的名字。他就是数学世界的亚历山大——大卫•希尔伯特! 哥尼斯堡是德国一座古老而美丽的城市,康德、哥德巴赫是这座城堡的荣誉和骄傲,著名的七桥问题更使之名扬欧洲。1862年1月23日,希尔伯特就诞生在这座富有学术传统的城市里。受家庭的熏陶,早在中学时代,希尔伯特对数学就表现出浓厚的兴趣,并立志把数学作为自己奋斗的专业。 1880年秋,希尔伯特进入哥尼斯堡大学。这里的学术空气浓厚而且自由,非常适宜希尔伯特的生活习性和学习要求。这段时间内,他同两位年轻的数学家的交往使他受益终生。一位是比他大3岁的胡尔维茨,在希尔伯特还是学生时,这位见多识广的青年就已是副教授;另一位是闵可夫斯基,虽比希尔伯特小两岁,但已荣获巴黎科学院大奖而名扬国际。他们三位一体,情投意合。他们每天下午“准5点”相会于校园旁边的苹果树下,互相交流彼此的学习心得、制订计划、探索未知领域。对于每一个重大问题,他们总是分头准备、认真思考,并各抒己见,有时也会争得面红耳赤。据说,曾有一位前来哥尼斯堡大学访问的外地学者,这天偶然经过苹果园,忽然听到里面传出几个人互不相让的争吵声,他驻足而观,发现三位年轻人比比划划,旁若无人。这位好心的人觉得有必要去劝解一下,但马上就知道自己的担心是多余的。那正是希尔伯特三人在讨论问题。 苹果树下的小路清晰地向远方延伸。他们通过日复一日的无数次散步,漫游了数学世界的每一个角落。这种数学家们特有的学习方式给他们其中的每一位带来了希望、成功和友谊。 苹果树下的散步使希尔伯特利用有趣而又容易接受的学习方式像海绵吸水那样接受数学知识,并以最简洁、快速的方法到达数学研究的前沿阵地。胡尔维茨渊博、系统的知识,闵可夫斯基快捷、灵敏的思维,无不令希尔伯特如醉如痴,也激励着他更加如饥似渴地学习、思考。这段时光为希尔伯特打下了牢固而全面的基础,他也因之能在以后的岁月里频频出击,并获得数学麦加——哥廷根大学的教授席位。 善疑名问会将学习引向深入,开放性的学习方式有利于塑造创造性的品质,相互影响、彼此促进的环境是培养人才群体的基本要素。这是“苹果树下的散步”给予的启迪。难道我们今天的教育、教学就不可以有所借鉴吗 |
-- 作者:chzhuang -- 发布时间:4/18/2006 3:17:00 PM -- 哥德尔 中国科学院软件研究所 张锦文 作者:张锦文 文章来源:中数网 点击数: 601 更新时间:2004-5-17
|
-- 作者:chzhuang -- 发布时间:4/18/2006 3:23:00 PM -- 邱奇-图灵论题 邱奇-图灵论题(The Church-Turing thesis)是计算机科学中以数学家阿隆佐•邱奇(Alonzo Church)和阿兰•图灵命名的论题。该论题最基本的观点表明,所有计算或算法都可以由一台图灵机来执行。以任何常规编程语言编写的计算机程序都可以翻译成一台图灵机,反之任何一台图灵机也都可以翻译成大部分编程语言程序,所以该论题和以下说法等价:常规的编程语言可以足够有效的来表达任何算法。该论题被普遍假定为真,也被称为邱奇论题或邱奇猜想 和图灵论题。 目录 • 1 本论题之等价形式 • 2 本论题之起源 • 3 本论题之成功 • 4 哲学内涵 • 5 补充材料 • 6 参考文献 本论题之等价形式
|
-- 作者:chzhuang -- 发布时间:4/18/2006 3:26:00 PM -- 阿伦·图灵 作者:liny信息来源:XY Studio编辑:EmilMatthew 更新时间:2003-4-10 -------------------------------------------------------------------------------- 正如美国电脑界有冯·诺依曼一样,在英国电脑的进展中,也有一个有巨大影响力的天才,他就是阿伦·图灵(Alan Turing)。此人对于电脑技术的发展,有着无可替代的影响。 英国现代计算机的起步的是从纳粹德国的“谜”开始的。“谜”(Enigma)是一种密码电报机,由德国人在一战和二战之间研制成功。“谜”能把日常语言变为代码,通过无线电或电话线路秘密传送。它是一个木箱子,配有一台打字机,箱上有26个闪烁不停的小灯泡,与打字机键盘的26个字母相对应。“谜”的设计无懈可击,有一套极精密的解码设置,非一般的电报密码所能比拟。在内行人看来,平白如话,但在旁人,又是无从索解的天书。因此,这台看似平常的机器,有了“谜”的称号。这样,德国的“谜”引起了英国情报部门高度的兴趣。常规的解码方式奈何不了“谜”,怎么办? 这时,天才的数学家图灵出现了。1931年图灵进入剑桥大学国王学院,开始了他的数学天涯。一到那里,图灵开始崭露头角,毕业后去美国普林斯顿大学攻读博士学位,在那里就发明过一个解码器(Encipher),二战爆发后回到剑桥。 在剑桥,图灵是一个妇孺皆知的怪才,常有出人意表的举动。他每天骑自行车到离公寓3公里的一个叫布雷奇莱公园(Bletchley Park)的地方上班,因常患过敏性鼻炎,一遇花粉,鼻涕不止,图灵就常戴防毒面具骑车上班,招摇过市,成为剑桥的一大奇观。 他的自行车链条经常在半道上掉落,要是换了别人,早就去车铺修理了。而图灵偏不,他在琢磨,发现这链条总是踏到一定的圈数时下滑,图灵在骑车时就特别留心计算,于是能做到在链条下滑前一刹那戛然停车!让旁人叹服不已,以为是在玩杂耍。后来他居然在踏脚旁装了一个小巧的机械计数器,到圈数时就停,好换换脑筋想些别的问题。图灵的脑袋转得比自行车飞轮还快。 用图灵的脑袋来破译德国的“谜”看来不是什么难事。二战爆发后,图灵成为英国外交部通信部门战时公务员,主要负责解码。他果然不负众望,成功破译了“谜”。而德国人还蒙在鼓里,还以为他们的“谜”能一直迷下去,照用不误,泄露了大量的核心机密,在战事上屡屡遭挫,战后,图灵被授予帝国勋章。至于图灵如何破译“谜”的,由于英国政府严格的保密法令,一直没有公之于世。所以图灵破译“谜”也成为一个“谜”。 早在30年代初,图灵就发表了一篇著名的论文《论数字计算在决断难题中的应用》,他提出了一种十分简单但运算能力极强的理想计算装置,用它来计算所有能想象得到的可计算函数。它由一个控制器和一根假设两端无界的工作带组成,工作带起着存储器的作用,它被划分为大小相同的方格,每一格上可书写一个给定字母表上的符号。控制器可以在带上左右移动,控制带有一个读写头,读写头可以读出控制器访问的格子上的符号,也能改写和抹去这一符号。 这一装置只是一种理想的计算模型,或者说是一种理想中的计算机。正如飞机的真正成功得力于空气动力学一样,图灵的这一思想奠定了整个现代计算机的理论基础。这就是电脑史上与“冯·诺依曼机器”齐名的“图灵机”。 图灵机被公认为现代计算机的原型,这台机器可以读入一系列的零和一,这些数字代表了解决某一问题所需要的步骤,按这个步骤走下去,就可以解决某一特定的问题。这种观念在当时是具有革命性意义的,因为即使在50年代的时候,大部分的计算机还只能解决某一特定问题,不是通用的,而图灵机从理论上却是通用机。在图灵看来,这台机器只用保留一些最简单的指令,一个复杂的工作只用把它分解为这几个最简单的操作就可以实现了,在当时他能够具有这样的思想确实是很了不起的。他相信有一个算法可以解决大部分问题,而困难的部分则是如何确定最简单的指令集,怎么样的指令集才是最少的,而且又能顶用,还有一个难点是如何将复杂问题分解为这些指令的问题。 此后图灵在国家物理学实验室(NPL)工作,并继续为数字式计算机努力,在那里人发明了自动计算机(Automatic Computing Engine,ACE),在这一时期他开始探索计算机与自然的关系。他写了一篇名为《智能机》的文章于1969发表,这时便开始有了人工智能的雏形。 图灵相信机器可以模拟人的智力,他也深知让人们接受这一想法的困难,今天仍然有许多人认为人的大脑是不可能用机器模仿的。而在图灵认为,这样的机器一定是存在的。图灵经常和其它科学家发生争论,争论的问题就是机器实现人类智能的问题,在今天我们看来这没有什么,但是在当时这可不太容易被人接受。他经常问他的同事,你们能不能找到一个计算机不能回答的问题,当时计算机处理多选问题已经可以了,可是对于文章的处理还根本不可能,但今天的发展证明了图灵的远见,今天的计算机已经可以读写一些简单的文章了。 图灵相信如果模拟人类大脑的思维就可以做出一台可以思考的机器,它于1950写文章提出了著名的“图灵测试”,测试是让人类考官通过键盘向一个人和一个机器发问,这个考官不知道他现在问的是人还是机器。如果在经过一定时间的提问以后,这位人类考官不能确定谁是人谁是机器,那这个机器就有智力了。这个测试在我们想起来十分简单,可是伟大的思想就源于这种简单的事物之中。 现在已经有软件可以通过图灵测试的子测试,软件这个人类智慧的机器反映应该可以解决一些人类智力的问题。在完成ACE之前,图灵离开了NPL,它在曼彻斯特大学开发曼彻斯特自动计算机(Manchester Automatic Digital Machine,MADAM)。他相信在2000年前一定可以制造出可以模拟人类智力的机器,图灵开始创立算法,并使用MADAM继续他的工作。 图灵对生物也十分感兴趣,他希望了解生物的各个器官为什么是这个样子而不是那个样子,他不相信达尔文的进化论,他觉得生物的发展与进化没什么关系。对于生物学,他也用它钟爱的数学进行研究,它的研究对他进行计算机的研究有促进作用。它把生物的变化也看做是一种程序,也就是图灵机的基本概念,按程序进行。最后,这位伟大的计算机先驱于1954年6月7日去世,他终生未娶。 |
-- 作者:chzhuang -- 发布时间:4/18/2006 3:32:00 PM -- 呵呵,顺序放错了,这个要放最前面,按时间顺序。 莱布尼兹 出生于书香门第的莱布尼兹是德国一位博学多才的学者。他的学识涉及哲学、历史、语言、数学、生物、地质、物理、机械、神学、法学、外交等领域。并在每个领域中都有杰出的成就。然而,由于他独立创建了微积分,并精心设计了非常巧妙而简洁的微积分符号,从而使他以伟大数学家的称号闻名于世。莱布尼兹对微积分的研究始于31岁,那时他在巴黎任外交官,有幸结识数学家、物理学家惠更斯等人。在名师指导下系统研究了数学著作,1673年他在伦敦结识了巴罗和牛顿等名流。从此,他以非凡的理解力和创造力进入了数学前沿阵地。 牛顿从运动学角度出发,以“瞬”(无穷小的“0”)的观点创建了微积分。他说dx和x相比,如同点和地球,或地球半径与宇宙半径相比。在其积分法论文中,他从求曲线所围面积积分概念,把积分看作是无穷小的和,并引入积分符号∫,它是把拉丁文Summa的字头S拉长。他的这个符号,以及微积分的要领和法则一直保留到当今的教材中。莱布尼兹也发现了微分和积分是一对互逆的运算,并建立了沟通微分与积分内在联系的微积分基本定理,从而使原本各处独立的微分学和积分学成为统一的微积分学的整体。 莱布尼兹是数学史上最伟大的符号学者之一,堪称符号大师。他曾说:“要发明,就要挑选恰当的符号,要做到这一点,就要用含义简明的少量符号来表达和比较忠实地描绘事物的内在本质,从而最大限度地减少人的思维劳动,”正像印度--阿拉伯数字促进算术和代数发展一样, 莱布尼兹所创造的这些数学符号对微积分的发展起了很大的促进作用。欧洲大陆的数学得以迅速发展,莱布尼兹的巧妙符号功不可灭。除积分、微分符号外,他创设的符号还有商“a/b”,比“a:b”,相似“∽”,全等“≌”,并“∪”,交“∩”以及函数和行列式等符号。 牛顿和对微积分的创建都作出了巨大的贡献,但两人的方法和途径是不同的。牛顿是在力学研究的基础上,运用几何方法研究微积分的;莱布尼兹主要是在研究曲线的切线和面积的问题上,运用分析学方法引进微积分要领的。牛顿在微积分的应用上更多地结合了运动学,造诣精深;但莱布尼兹的表达形式简洁准确,胜过牛顿。在对微积分具体内容的研究上,牛顿先有导数概念,后有积分概念;莱布尼兹则先有求积概念,后有导数概念。除此而外,牛顿与莱布尼兹的学风也迥然不同。作为科学家的牛顿,治学严谨。他迟迟不发表微积分著作《流数术》的原因,很可能是因为他没有找到合理的逻辑基础,也可能是“害怕别人反对的心理”所致。但作为哲学家的莱布尼兹大胆,富于想象,勇于推广,结果造成创作年代上牛顿先于莱布尼兹10年,而在发表的时间上,莱布尼兹却早于牛顿三年。 虽然牛顿和莱布尼兹研究微积分的方法各异,但殊途同归。各自独立地完成了创建微积分的盛业,光荣应由他们两人共享。然而在历史上曾出现过一场围绕发明微积分优先权的激烈争论。牛顿的支持者,包括数学家泰勒和麦克劳林,认为莱布尼兹剽窃了牛顿的成果。争论把欧洲科学家分成誓不两立的两派:英国和欧洲大陆。争论双方停止学术交流,不仅影响了数学的正常发展,也波及自然科学领域,以致发展到英德两国之间的政治摩擦。自尊心很强的英国民族抱住牛顿的概念和记号不放,拒绝使用更为合理的莱布尼兹的微积分符号和技巧,致命英国在数学发展上大大落后于欧洲大陆。一场旷日持久的争论变成了科学史上的前车之鉴。 莱布尼兹的科研成果大部分出自青年时代,随着这些成果的广泛传播,荣誉纷纷而来,他也越来越变得保守。到了晚年,他在科学方面已无所作为。他开始为宫廷唱赞歌,为上帝唱赞歌,沉醉于研究神学和公爵家族。莱布尼兹生命中的最后7年,是在别人带给他和牛顿关于微积分发明权的争论中痛苦地度过的。他和牛顿一样,都终生未娶。1761年11月14日,莱布尼兹默默地离开人世,葬在宫廷教堂的墓地。
|
-- 作者:chzhuang -- 发布时间:4/18/2006 3:41:00 PM -- 约翰.麦卡锡 --"人工智能之父"和LISP语言的发明人 1971年的图灵奖授予提出"人工智能"这一术语并使之成为一个重要的学科领域的斯坦福大学教授约翰. 麦卡锡( John McCarthy)。 麦卡锡1927年9月4日生于波士顿。他的父亲是一个爱尔兰移民,做过木匠和渔夫,同时也是一个发明家和工会积极分子,拥有捻船缝机和桔汁冷冻机两项专利。麦卡锡的母亲是来自立陶宛的犹 太人,热心于*女*权运动,当过记者。夫妻两人在20世纪30年代都曾参加美国共产党。受父母的影响,麦卡锡对社会问题也比较关注,参与过在加州的Palo Alto 创办自由大学的活动,倡议过修改"人*权*法*案"(the Bill of Rights,这是美国于1789年通过的对美国宪法的第一次修正案)。但与他在计算机科学上所做的工作和贡献相比,麦卡锡主要还是一个科学家而非社会活动家。此外,麦卡锡还喜欢攀登、跳伞、驾驶滑翔机等有刺激性和危险性的运动,曾和他的第二任妻子维拉.沃特森(Vera Watson)一起攀登过世界上不少大山高峰。沃特森是一位程序员,也是世界知名的女登山运动员,是第一位独自攀上西半球第一高峰、位于阿根廷和智利边界的安第斯山脉的阿空加瓜山(海拔6960米)的女性,后来在一次攀登位于尼泊尔中部的阿那波尔那峰(海拔8 075米)的妇女探险活动中不幸遇难牺牲。 麦卡锡是一个天赋很高的人,还在上初中时,他就弄了一份加州理工大学的课程目录,按目录自学了大学低年级的高等数学教材,做了教材上的所有练习题。这使他1944年进入加州理工学院以后可以免修头两年的数学,并使他虽因战时环境(第二次世界大战当时正在进行之中,美国也在珍珠港事件后宣布参战)要在军队中充任一个小职员,占去了部分时间,仍得以在1948年按时完成学业。然后到普林斯顿大学研究生院深造,于1951年取得数学博士学位。麦卡锡留校工作两年以后转至斯坦福大学,也只呆了两年就去达特茅斯学院任教(达特茅斯学院位于新罕布什尔州的汉诺威)。在那里,他发起了并成功举办了成为人工智能起点的有历史意义的"达特茅斯会议"。1958年麦卡锡到MIT任职,与明斯基(L. Minsky,1969年图灵奖获得者)一起组建了世界上第一个人工智能实验室,并第一个提出了将计算机的批处理方式改造成为能同时允许数十甚至上百用户使用的分时方式(time-sharing)的建议,并推动MIT成立组织开展研究。其结果就是实现了世界上最早的分时系统--基于IBM 7094的CTSS和其后的MULTICS。麦卡锡虽因主持该课题的负责人产生矛盾而于1962年离开MIT重返斯坦福,未能将此项目坚持到底,但学术界仍公认他是分时概念的创始人。麦卡锡到斯坦福后参加了一个基于DEC PDP -1的分时系统的开发,并在那里组建了第二个人工智能实验室。 麦卡锡对人工智能的兴趣始于他当研究生的时候。1948年9月,他参加了一个"脑行为机制"的专题讨论会,会上,冯.诺伊曼发表了一篇关于自复制自动机制论文,提出了可以复制自身的机器的设想,这激起了麦卡锡的极大兴趣和好奇心,自此就开始尝试在计算机上模拟人的智能。1949年他向冯.诺伊曼谈了自己的想法,后者极表赞成和支持,鼓励他搞下去。在达特茅斯会议前后,麦卡锡的主要研究方向是计算机下棋。下棋程序的关键之一是如何减少计算机需要考虑的棋步。麦卡锡经过艰苦探索,终于发明了著名的α-β搜索法中,麦卡锡将结合的产生与求评价函数值(或称返上值或倒推值)两者巧妙地结合起来,从而使某些子树结点根本不必产生与搜索(这谓之"修剪"--pruning或cutoff)。之所以称为α-β搜索法,是因为将处于取最大值级的结点的返上值或候选返上值PBV(Provisional Back-up Value)称为该结点的α值,而将处于取最小值级的结点的候选返上值或返上值称为该结点的β值。 这样,在求得某结点以下的α值时,就可与其先辈结点的α值相比较,若α≥β, 则可终止该结点以下的搜索,即从该结点处加以修剪,这叫β修剪;而在求得某结点以下的β值时,就可与其先辈结点的α值相比较,若β≤α,则可终止该结点以下的搜索,即从该结点处加以修剪,这叫α修剪。为了说明α-β修剪,我们举一个最简单的例子。设在取火柴棍的游戏中,A、B两人轮流从N根火柴中取1根或2根,不得多取,也不能不取。取走最后一根火柴者胜。用A(n)、B(n)表示轮到A或B时有n根火柴的状态,当n = 5时轮到A取,则如下图所示,A有两种可能,一是取2根火柴进入B(3),另一是取1根火柴进入B(4)。显然,进入B(3)后,不管B取几根,A必胜,故A必走这一步,余下的分支不必再搜索了。α-β搜索法至今仍是解决人工智能问题中一种常用的高效方法。 至于达特茅斯会议,当东道主的麦卡锡是主要发起人,另外3个发起人是当时在哈佛大学的明斯基(1969年图灵奖获得者),IBM公司的罗杰斯特(N. Rochster),信息论的创造人香农。麦卡锡发起这个会议时的目标非常宏伟,是想通过10来个人2个有共同努力设计出一台具有真正智能的机器。会议的经费是洛克菲勒基金会资助的,包括每个代表1200美元加上外地代表的往返车票。会议的原始目标虽然由于不切实际而不可能实现,但由于麦卡锡在下棋程序尤其是α-β搜索法上所取得的成功,以及卡内基-梅隆大学的西蒙(H. A.Simon)和纽厄尔(A. Newell,这两人是1975年图灵奖获得者)带来了已能证明数学名著《数学原理》一书第二章52个定理中的38个定理的启发式程序"逻辑理论家"LT(Logic Theorist),明斯基带来的名为Snarc的学习机的雏形(主要学习如何通过迷宫),这使会议参加者仍能充满信心地宣布"人工智能"这一崭新学科的诞生。 1959年,麦卡锡基于阿隆索.邱奇(Alonzo Church)的λ-演算和西蒙、纽厄尔首创的"表结构",开发了著名的LISP语言(LISt Processing language),成为人工智能界第一个最广泛流行的语言。LISP是一种函数式的符号处理语言,其程序由一些函数子程序组成。在函数的构造上,和数学上递归函数的构造方法十分类似,即从几个基本函数出发,通过一定的手段构成新的函数。LISP语言还具有自编译能力。具体说来,LISP有以下几个主要特点: 1. 计算用的符号表达式而不是数; 2. 具有表处理能力,即用链表形式表示所有的数据; 3. 控制结构基于函数的复合,以形成更复杂的函数; 4. 用递归作为描述问题和过程的方法; 5. 用LISP语言书写的EVAL函数既可作为LISP语言的解释程序,又可以作为语言本身的形式定义; 6. 程序本身也同所有其他数据一样用表结构形式表示。 已经证明,LISP的这些特点是解决人工智能核心问题的关键。此外,精巧的表机制也是进一步简化LISP程序设计的方便而有力的工具,因此,LISP自发明以来,已经被广泛用于数学中的符号微积分计算,定理证明,谓词演算,博奕论等领域。它和后来由英国伦敦大学的青年学生柯瓦连斯基(R. Kowaliski)提出、由法国马赛大学考尔麦劳厄(A. Colmerauer)所领导的研究小组于1973年首先实现的逻辑式语言PROLOG(PROgramming in LOGic)并称为人工智能的两大语言,对人工智能的发展起了十分深远的意义也吸引了负责设计Algol语言的国际委员会,麦卡锡因此而被吸收为该委员会的成员。Algol中后来采纳了LISP关于递归和条件表达式这些思想。 麦卡锡在20世纪50年代末研究的另一个课题是如何程序能接受劝告从而改善其自身的性能。为此他提出过一个名为Advice Taker的系统的设想。有资料说,这是世界上第一个体现知识获取工具思想的系统,1968年建成。实际上,这个系统并未最后完成,只是完成了一部分,用LISP语言建立起了一个具有常识(common sense)的软件,能理解告诉它的是什么,并能评估其行动的后果。但正是在Advice Taker的开发过程中,启发麦卡锡提出了用"分时系统"代替"批处理系统"的建议,使计算机的使用方式引发了一场革命。 除了人工智能方面的研究和贡献这外,麦卡锡也是最早对程序逻辑进行研究并取得成果的学者之一。1963年他发表的论文"计算的数学理论的一个基础"一文(收录于P. Braffort和D. Hirschberg编辑的《计算机程序设计和形式系统》--Computer Programming and Formal Systems, North Holland, 33-70页)集中反映了他这方面的成果。麦卡锡在这篇论文中系统地论述了程序设计语言形式化的重要性,以及它同程序正确性、语言的正确实现等问题的关系,并提出在形式语义研究中使用抽象语法和状态向量等方法,开创了"程序逻辑(logics of programs)研究的先河。程序逻辑就是一种"语言",用这种语言可以无二义地表达程序的各种性质,其语义规定了该语言中各种表达式的意义,而它的一组规则则用同意义相关的方式去操作这些表达式以计算该语言中的各种断言(assertation)的真值。研究程序的逻辑对于帮助人们了解软件是否合理十分重要,它可以用于程序的逻辑对于帮助人们了解软件是否合理十分重要,它可以用于程序验证(program verification),自动程序设计,为优化和审计而进行的程序分析等方面。麦卡锡在上述论文中提出的方法是用递归函数作为程序的模型。他以两个链表(list)的"附加"(append)操作为例说明可以用递归的方法定义这个函数,并可以用形式化的方法证明链表的附加操作是满足结合律的(associative law ),即x @ (y @ z) = (x @ y) @ z。麦卡锡进而证明了用一系列递归定义的函数就完全可能建造大型的软件系统,并用归纳法证明这些系统所具有的性质。麦卡锡所提出的方法是有关程序逻辑研究中第一个比较系统而成熟的方法,曾被广泛地采用。 20世纪70年代以后,麦卡锡又开始研究非单调逻辑。在经典逻辑中,由已知事实推出的结论,决不会在已知事实增加时反而丧失其有效性,因此是"单调的"(monotonic)。但在人类思维过程中,由于信息的不完全和认识的局限性,常常有随着事物的发展变化,原有结论被否定和取消的情况,这就导致了所?"非单调逻辑"(nonmonotonic logic)。非单调逻辑中有一类是基于最小化语义的最小化非单调逻辑。1980年,麦卡锡在一篇论文中提出了"限制逻辑"或称"限界逻辑",成为这类非单调逻辑中比较成功的一个体系(见J. McCarthy:Circumscription--a form of nonmonotonic reasoning. Artificial Intelligence ,Vol.13,1980,27-39页)。限制逻辑的基本思想是:"限制"某个谓词P也就是排除以P的原有事实为基础所建立的大部分模型,而只保留有关P的最小模型。这与人类思考问题时总是在某些条件限制下考虑,也就是只考虑所涉及的个体或关系,而决不去涉及其他个体或关系,是比较相符的。1986年,麦卡锡在AI杂志上就限制逻辑的应用发表了进一步的研究论文:"限制逻辑在常识知识形式化中的应用"(Applications of Circumscription to Formalizing Common Sense Knowledge, AI, Vol.28,1986,89-116页),对倡导常识推理和常识研究起了十分重要的作用。 麦卡锡的主要著作有: 《自动机研究》(Automata Studies, Princeton Uni. Pr.,1956,与香农合编) 《信息学:科学美国人之书》(Information:A Scientific American Book, Freeman, 1966) 《形式化的常识:麦卡锡论文选集》(Formalizing Common Sense:Papers by John McCarthy , Ablex Pub. Co., 1990, 蒝. Lifschitz 编辑) 除了获得图灵奖以外,麦卡锡在1988年获得由日本INAMORI基金会所设立的KYOTO奖,这个奖主要奖励在高科技方面作出杰出贡献的科学家,麦卡锡是这个奖的第5位获得者。1990年麦卡锡获得美国全国科学奖章 (National Medal of Scien- -ce)。 麦卡锡的图灵奖演说题为"人工智能研究的现状"(The Present State of Research on Artificial Intelligence)。但不知什么原因,这篇演说没有发表。在《前20年的图灵奖演说集》(ACM Turing Award Lectures--The First 20 Years:1966-1985 ,ACM Pr.)中,则以"附录"(postscript)的形式约请麦卡锡另写了一篇"人工苣一般原理"(Generality in Artificial Intelligence),刊于该书257-268页。 麦卡锡现仍在斯坦福大学计算机科学系任教,其电子信箱为: jmc@cs.stanford.edu 出自《ACM图灵奖——计算机发展史的缩影》(高等教育出版社)
|
-- 作者:chzhuang -- 发布时间:4/18/2006 3:43:00 PM -- Rule of Simplicity (by C.A.R. Hoare) - - "There are a number of ways of constructing a software design. One way is to make it so simple that there are obviously no deficiencies, and the other way is to make it so complicated that there are no obvious deficiencies." -- C.A.R. Hoare ---从QUICKSORT、CASE到程序设计语言程序设计语言的公理化 学过“数据结构”或“算法设计与分析”的人都知道著名的快速排序算法QUICKSORT;编过程序的人大概也都用过实现条件转移的最方便的语句CASE语句。但是你知道这个算法和这个语句是谁发明的吗?它们的发明者就是1990年IEEE计算机先驱奖和1980年图灵奖的获得者英国牛津大学计算机科学家查尔斯·霍尔(Charles AntonyRichard Hoare)。当然霍尔之所以获得这两项大奖决不仅仅是因为他发明了QUICKSORT和CASE,而是因为他在计算机科学技术的发展中,尤其是在程序设计语言的定义和设计、数据结构和算法、操作系统等许多方面都起了重要的作用,有一系列发明创造,QUICKSORT和CASE只是其中的一小部分而已。 霍尔于1934年1月11日诞生于英国南部。在坎特伯雷(Canter·bury)的国王学校(King’s Sch001)度过中学阶段以后,进入牛津的莫顿学院(Merton College)学习数学,1960年取得硕士学位。之后他进入伦敦一家不大的计算机生产厂家Elliott Brothers公司,为该公司的Elliott 803计算机编写库子程序,从此开始他的计算机生涯。QUICK,SORT就是他在那个时候用原有的SHELLSORT(以算法的发明人D.L.Shell命名的通过调换并移动数据项实现排序的一种算法,发明于1959年)编程时分析了它的缺点而发明出来的。QUICKSORT具有“快刀斩乱麻”的特点,能迅速地对乱序作大幅度调整,特别适合于因多次追加、删除而变得杂乱无章的数据集合。QUICKSORT是利用“分治法”(divide and conquer)进行算法设计的一个成功范例,它的发明是霍尔在计算机方面的天才的第一次显露,受到老板的赞赏和重视。第二年,霍尔接受了一个新的任务,为公司的新机型Elliott 503设计一个新的高级语言。但就在其时,他弄到了一份Algol 60报告的复印件,还参加了一个由狄克斯特拉(E.W.D耻stra,首届计算机先驱奖获得者)等人在布赖顿举办的Algol 60培训班,感到与其自己没有把握地去设计一个新的语言,还不如将比较成熟的Algol 60在Elliott 503上加以实现。霍尔和他的同事们的这个想法获得公司同意以后,由霍尔主持设计与实现了Algol 60的一个子集的版本。霍尔在开发初首先制定了明确的目标,即系统要安全可靠,生成的目标码要简洁,工作区数据要紧凑,过程和函数的人口和出口要清晰、严密等,还明确了整个编译过程采用一次扫描等原则。这样,ElliottAl-gol的开发十分顺利与成功,它在1963年中推出以后大受欢迎,成为世界各国所开发的Algol 60的各种版本中在效率、可靠性和方便性等方面的性能指标都首屈一指的一个版本,霍尔本人也从此受到国际学术界的重视。国际信息处理联盟IFIP后来任命霍尔为2.1工作组(WorkingGroup 2.1)的负责人,这个工作组的任务是维护和发展Algol。霍尔果然不负众望,主持设计了Algol X以继承与发展Algol60。正是在AlgolX的设计中,霍尔发明了CASE语句。CASE语句具有如下形式的语法结构: CASE E of C1:S1; C2:S2; . . . Cn-1:Sn-1; Otherwise:Sn End 其中E是一个表达式,称为“选择子”(Selector),每个Ci的值为常数,称为“分情形标号”,Si则为可执行语句。CASE语句的含义是:若E的值等于某个Ci的值,则执行其后的Si(i=1,2,3,…,n—1),否则执行Sn。某个Si或S。执行完之后,整个CASE语句也就执行完毕。由于CASE语句构成多路分支,程序结构清晰、直观,所以CASE语句后来几乎成为程序设计语言的标准,被各种语言广泛采用。在C语言中,没有独立的CASE语句,但它的SWITCH语句(开关语句)实际上是在CASE语句的基础上形成的: switch E {case C1:S1; case C2:S2; . . . case Cn-1:Sn-1; [default:Sn] 不同之处有二:一是C;可以是表达式,但计算结果必须仍是常数;二是E的结果若不等于某个Ci(i=1,2,3,…,n—1)的值,则视有无default子句,若有,执行Sn;若无,则什么也不执行,控制转向SWITCH后的语句。显然,这些都是对CASE语句的进一步改进。 霍尔于1968年离开Elliott,离开产业界,原因是作为学者他对程序设计浯言的形式化定义这类更偏重于学术性和理论性的课题更感兴趣。离开Elliott以后,他任职过一年英国国家计算中心主任,发现自己也不适于从事行政管理,因此又转入爱尔兰的昆土大学(Queen’s University),从事教学和研究,1977年转入牛津大学。离开Elliott以后,霍尔在计算机科学理论的研究中发挥其特长,作出了许多创造性的重大贡献。首先是1969年10月,霍尔在Communications of ACM上发表了他那篇有里程碑意义的论文“计算机程序设计的公理基础”(An Axiomatic Basis for Computer Programming)。在这篇论文中,霍尔提出了程序设计语言的公理化定义方法,即公理语义学(axiomatic semantics),也就是用一组公理和一组规则描写语言应有的性质,从而使语言与具体实现的机器无关,而且也易于证明程序的正确性。这是继麦卡锡(J.McCarthy,1985年计算机先驱奖获得者)在1963年提出用递归函数定义程序、弗洛伊德(R.W.Floyd,1991年计算机先驱奖获得者)在1967年提出基于程序流程图的归纳断言法以后,在程序逻辑研究中所取得的又一个重大技术进展。霍尔提出的方法在逻辑上与弗洛伊德提出的方法类似,但不是用流程图而是用代数法,即控制流用以下一些结构表示: begin al;a2;a3;…;an end if p then a1 else a2 while p do a 后面为了方便,我们用到第一个结构时省略首尾的begin和end。 相应于弗洛伊德的验证条件,霍尔引入下列符号: p{a}q 其意义是:如果在执行。之前P(叫做precondition)成立,则当α执行完了后q(叫做postcondition)成立。 霍尔给出了以下一组证明规则(proof rule)或叫推导规则: p’ pp{a}qq→q’ 1. p’{a}q’ 这个规则中的p’→和q’→q是普通数理逻辑中的断言命题,表示若p’(或q’)成立,则p(或q)成立。这个规则表示,若横线以上的p’→p、p{a}q、q→q’成立,则横线以下的p’{a}q1成立。 2. P(e){x:=e}p(x) 这个规则表示,如果在将e赋给x之前p(e)成立,则其后p(x)成立。
3. P{a}qq{b}r p{a;b}r 这个规则表示的是“传递律”(transitive law),即如果执行α之前p成立,α执行完了以后q成立;而如果执行b之前q成立,b执行完了以后r成立,则若在动作序列。和^执行之前P成立,则a和b执行完了以后r成立。
4. p∧r{a}qp∧~r(b)q p{if r then a else b}q
这个规则中的∧和~是一般数理逻辑中的合取(conjunction)和否定(negation)连接词。这个规则定义了if-then-else的执行取决于precondition r的值。
5. p∧q{a}p p{while q do a}p∧~q 这个规则定义了while循环:p是循环不变量(loop invariant),而q是终止循环的条件。 下面我们举一个例子说明如何用霍尔建立的系统验证程序的正确性。设有计算n的阶乘n!的如下程序: A: x:1;B B: while y>0 do C C: x:y×x;y:=y-1 则通过下列霍尔断言可以证明上述程序是正确的,因为这些断言都是真的,而且在霍尔的系统中是可以被证明的,而最后一个断言正是我们所要寻求的结论,因此它们形成对上述阶乘程序正确性的说明。 i. y>0∧x×y! =n! {x:=y×x}y>0∧x×(y-1)! =n! [首先y>0∧x×y! =n!→y>0∧(y×x)×(y-1)! =n!] 然后用规则(2),用x代替y×x] ii. y>0∧x×(y-1)! =n!{y:=y-1}y≥0∧x×y! =n! [类似(i),利用规则(2)] iii.y>0∧x×y! =n! {C}y≤0∧x×y! =n! [对(i)和(ii)用规则(3)] iv.Y≥0∧y=n∧x=1{B}x=n! [因为] y=n∧x=1→x×y! =n! 又因为0! =1,所以Y≥0∧x×y! =n! ∧y≤0→y=0∧x=n! →x×y! =n! 根据(iii),利用规则(5),令(5)中p=y≤0∧x×y! =n!,q=y>0,孥可得(iv)] v. y≥0∧y=n{x:=1}y≥0∧y!=n∧x=1 [因为p{x:=1}p∧x=1] vi. y≥0∧y=n{A}x=n! [对(V)和(Vi)利用规则(3)] 因为(vi)中的precondition正好是n的初始条件,而postcondition给出了所需结果,这样就证明了程序可算出n!。 为了给出证明,应该从程序的最后一行开始逐步后推。在这个例子中,(iii)步是最关键的,其中y≥0∧x×y! =n!就是循环不变量或归纳假设(induction hypothesis)。 利用霍尔提出的这种方法,已经成功地描述了PASCAL等语言,说明了这个方法的巨大威力。但应该指出的是,霍尔的这个方法是不完备的,因为霍尔在开发和建立这个系统时并没有追求系统的完备性,而更多地追求系统的实用性。 在数据类型、数据结构和操作系统设计等方面,霍尔也做了许多开创性的工作。目前广泛流行与应用着的许多概念都源于霍尔的工作。例如,关于抽象数据类型的规格说明(Specification,也叫规约)与其实现是否一致,就是由霍尔于1972年公式化了的。霍尔通过前后断言方法用已经定义了的(抽象)数据类型给出所要定义的新类型的抽象模型,这成为抽象数据类型规格说明的两种主要方法之一,即模型方法(另一方法为基于异调代数理论的代数方法)。对于操作系统的设计与实现十分关键的monitor(监控程序)的概念也是霍尔首先提出,并界定了它的作用与功能,即作为操作系统的核心,在把操作系统看做虚拟机扩充时,monitor是硬件的第一次扩充,它完成中断处理、进程控制与进程通信、存储区动态分配,建立软时钟,驱动设备通道,进行处理机调度。monitor为外面各层的设计提供良好的环境,并提高系统的安全性。 20世纪70年代后期,霍尔又深入研究了运行在不同的机器上的若干个程序之间如何互相通信、互相交换数据的问题,实现了面向分布式系统的程序设计语言CSP。在该语言中,一个并发系统由若干并行运行的顺序进程组成,每个进程不能对其他进程的变量赋值。进程之间只能通过一对通信原语实现协作:Q?x表示从进程Q输入一个值到变量x中;P!e表示把表达式e的值发送给进程户。当户进程执行Q?x,同时口进程执行户!‘时,发生通信,e的值从Q进程传送给户进程的变量x。CSP语言后来成为著名的并行处理语言OCCAM(由INMOS公司为Transputer开发)的基础。20世纪80年代中期,霍尔又和布鲁克斯(S.Brooks)等人合作,提出了“CSP理论”TCSP(Theory Of Communicating Sequential Processes),它与上述CSP不同,但又有联系,这是一个代数演算系统,其基本成分是事件(或动作)。进程由事件和一组算子构造而成。TCSP采用“广播式通信”,而不像程序设计语言CSP中那样采用握手式通信,即只有当并行运行的各进程都执行同一动作时,才发生通信。此外,TCSP采用失败等价作为确定进程等价的准则,这就是著名的“失败语义”。利用失败可以构造TCSP的指称模型。霍尔为失败等价建立了一些公理系统,可以对语义上的等价关系进行形式推导。霍尔在这方面的工作开创了用代数方法研究通信并发系统的先河,形成了所谓“进程代数”(process algebra)这一新的研究领域,产生了很重要的影响。 霍尔的论著极多,而且都很有份量,有很高的学术水平。有评论说,霍尔每发表一篇论文,几乎就要改变一次人们对程序设计的认识。这虽然是一种夸张的说法,但也说明霍尔的论著确实非常重要。ACM在1983年评选出最近四分之一个世纪中发表在Communications of ACM上的有里程碑式意义的25篇经典论文,只有两名学者各有2篇论文人选,霍尔就是其中之一(另一名是首届计算机先驱奖获得者狄克斯特拉)。霍尔人选的两篇论文分别是1969年10月的“计算机程序设计的公理基础”(An Axiomatic Basis for Computer Programming,这篇论文的要点我们前面已经介绍过了),另一篇是1978年8月的“通信顺序进程”(Communicating Sequential Processes),该论文奠定了前述CSP语言的基础。CSP现在已推广为“混合通信/顷序进程”(Hybrid Communicating Sequential Processes)。在这个语言中,有一种特殊的语句称为“连续构件”,可表示一个具体给定初值的微分方程;而原有的通信语句可用来表达事件的起源和发生;语言中的顺序算子、条件算子等则用来刻画连续构件和通信间的耦合关系。 值得指出的是,霍尔还和我国软件学者、中国科学院软件所的周巢尘研究员等合作,在20世纪80年代末由于Esprit的ProCos项目的需要而对基于时态逻辑的逻辑型混合计算模型进行了研究,在这个模型中引入了时段和切变的概念,建立了时段演算,已引起该领域同行的广泛重视。时段用以刻画系统在一个时间区间上的连续变化,而切变则表示事件的发生(离散变量的变化)。在单个时段上,借助连续数学(微分方程理论)推导系统的行为;而在相邻时段间,则用时态逻辑中切变算子的规则,推导系统行为的转化。这种混合计算模型对于设计要求绝对安全的软件系统具有十分重大的意义。时段演算已在煤气燃烧器、铁路岔口控制、水位控制、自动导航、OCCAM语言的实时语义、描述调度程序的实时行为和电路设计等方面获得成功应用。 此外,由法国学者阿勃利尔(J.R.Abrial)提出的以状态机为模型的著名的形式规约语言Z语言,也是由霍尔所领导的研究小组加以发展并实现的。 霍尔出版的专著主要有以下几种: 《操作系统技术》(Operating Systems Techniques,Academic Pr.,1972) 《数理逻辑和程序设计语言》(Mathematical Logic and Programming language,Prentice—Hall,1985) 《并发和通信的发展》(Development in Concurrency and Communication,Addison-Wesley,1990) 《机器推理和硬件设计》(Mechanized Reasoning and Hardware Design,Prentice·Hall,1992) 除了获得计算机先驱奖和图灵奖以外,霍尔还在1981年获得AFIPS的Harry Goode奖;1985年获得英国IEE的法拉第奖章。霍尔曾应邀到过世界的许多国家讲学,中国科学院研究生院也曾于1983年邀请霍尔到北京讲学,并主办讨论班。1989年霍尔当选为欧洲科学院院士。1992年新加坡政府授予霍尔“李光耀优秀访问学者”称号。在2000年北京WCC大会上,霍尔应邀作了主题报告。 顺便提一下,霍尔所开创的进程代数,我国学者给予了高度重视和深入研究,并有创新。国防科技大学李舟军博土已撰写出《进程代数导论——理论及应用》一书,被列入“中创软件丛书"2001年度计划即将出版。
|
-- 作者:amny -- 发布时间:4/18/2006 7:52:00 PM -- 不错!!! |
-- 作者:yangfeather -- 发布时间:4/19/2006 1:34:00 AM -- ? [此贴子已经被作者于2006-4-19 7:56:49编辑过]
|
-- 作者:chzhuang -- 发布时间:4/19/2006 7:57:00 AM -- 谢谢yang兄指正: 1、他们两位相对没这么大吧,但在目前来说,他们参与的基于逻辑的人工智能,和基于逻辑的程序理论,分别代表了数理逻辑在当代的两个重要发展方向呀。 2、呵呵,这是前因后果的问题。如果没有图灵机,连电脑都没有,还怎么玩游戏?!当然,不是说游戏也是他们编的,编游戏还要有很好的创意和美工音乐等等。 3、算法与复杂性当然很重要了,但是要刻画计算的极限或者进一步追求计算的能力,这些工作很多是数理逻辑领域的吧。即使在复杂性领域,计算复杂性与递归论也是息息相关的呀。在算法领域,要保证算法的具体化(程序)的正确性,也经常要用数理逻辑来保证它的正确性和可靠性呀。 4、呵呵,列出霍尔,主要是他的公理语义学方面的创新。他的进程代数CSP我现在不太懂。 |
-- 作者:chinake -- 发布时间:4/19/2006 10:05:00 AM -- 作者区分数理逻辑的标准是什么哪?好几位大师都没有提到,Hilbert是否可以称为数理逻辑大师?他的成就主要在数学,而不是逻辑学,但是他成就了Godel。 |
-- 作者:chzhuang -- 发布时间:4/19/2006 11:03:00 AM -- 这个跟个人兴趣和视野有关呀,不可能面面俱到。HILBERT当然称得上数理逻辑大学了,他提出问题,哥德尔解决问题。有时候,我们甚至分不清“提出问题”重要,还是“解决问题”重要。更何况,他也是形式主义的奠基人。我用的教材《logic for mathematicians》也是用形式主义的方法来讲数理逻辑的。 |
-- 作者:xixi8356 -- 发布时间:5/29/2006 3:02:00 PM -- 相当不错 |
-- 作者:Kysio -- 发布时间:1/11/2010 10:15:00 PM -- 好高兴自己开始学数量逻辑了,真希望以后做出点成绩来。 |
W 3 C h i n a ( since 2003 ) 旗 下 站 点 苏ICP备05006046号《全国人大常委会关于维护互联网安全的决定》《计算机信息网络国际联网安全保护管理办法》 |
214.844ms |