赛义甫的个人博客分享 http://blog.sciencenet.cn/u/saif 逻辑学、数学、计算科学、语言学和哲学——关于形式科学的思考

博文

哈斯凯尔·布鲁克·柯里——一个被埋没了的史诗般学者 精选

已有 11255 次阅读 2017-1-20 00:26 |个人分类:计算|系统分类:科普集锦| 布鲁克, 柯里, 哈斯凯尔, 组合逻辑

Haskell Brook Curry——美国数学家和逻辑学家,一位在数理逻辑和计算机科学历史上里程碑式的存在,其名声不如阿兰·图灵那么响亮,其影响不如库尔特·哥德尔那么广泛,但是在真实的历史中,Curry对的人类的贡献完全可以和前者比肩。如果说图灵机是现代计算机程序设计语言的基本模型,那么可计算函数就是和图灵机等价的另一种模型。组合逻辑,是Curry穷毕生精力的研究成果,这种以函数为基本元素的逻辑系统现今已成为理论计算机科学研究中一颗璀璨的明星。可能你还不知道,Curry是世界上唯一一位数学家、逻辑学家,他的姓名从头到尾全部成为计算机语言的名称:Haskell,当下最流行的函数式编程语言;Brook,是斯坦福大学开发的流处理编程语言,面向图形处理和并行计算,其设计依据ANSI C标准;Curry是一种新型的语言——混合了函数式和逻辑式两种范式的编程语言,其母体则是Haskell。Curry在某种意义上是Haskell的超集。哈斯凯尔·布鲁克·柯里,他的著作连同他的名字都成为人类智慧的象征。
本文以维基百科的英文条目——Haskell Curry为基本参考,简单介绍Haskell Brook Curry(中文译名为:柯里)的生平和学术成就。
柯里出生于1900年9月12日,逝世于1982年9月1日。柯里最大的贡献、也是他一生中投入精力最大的研究就是组合逻辑;除此之外,柯里还发现以他命名的“柯里悖论”(Curry Paradox),以及著名的“柯里-霍华德同构”(Curry-Howard isomorphism),又称“柯里-霍华德对应”(Curry-Howard correspondence);除此之外,柯里的名字,又被当做动词——currying,中文称作“柯里化”,意思是将多参数函数转化为多个单参数函数叠加的过程。
柯里16岁考入哈佛大学学医,不过中途转入数学系。本科毕业后在麻省理工学院电子工程系工作两年,后又返回哈佛学习物理,并取得硕士学位。在这期间,柯里因修读怀特海-罗素的《数学原理》课程开始对数理逻辑感兴趣,这促使他留在哈佛攻读数学专业博士学位。刚开始在他的导师George Birkoff指导下研究微分方程,但是柯里仍然放不下对数理逻辑的兴趣。1927年,柯里在普林斯顿大学获得讲师职务,期间发现了俄国学者Moses Schönfinkel在组合逻辑领域的研究,这激发起柯里极大的兴趣,并坚定了将此生投入到数理逻辑的研究当中。为此他远赴德国哥廷根,和熟悉Schönfinkel研究的两位学者Heinrich Behmann和Paul Burnays共同研究,在其导师、大名鼎鼎的希尔伯特指导下,以组合逻辑为内容完成论文获得了博士学位。期间,柯里与弗吉妮娅·维特利结婚。1929年,也就是柯里获得博士学位的前一年返回美国,并在宾州州立学院获得教职。在取得博士学位后,柯里就一直在该校任教37年。二战结束后,柯里参加了史上第一台电子计算机的研制项目。1966年,柯里从宾州学院退休,受聘于荷兰阿姆斯特丹大学。1970年在完成了他的巨篇鸿著《组合逻辑》第二卷之后,柯里从阿姆斯特丹大学退休,又返回宾州州立学院,直到逝世。
和大多数数理逻辑学家一样,柯里的研究中心也是数学基础问题,试图为数学找出一个安全的基础理论。1933年,柯里通过与John Rosser(也是一位值得提及的数理逻辑学家)通信得知了“Kleene-Rosser悖论”。这个理论由Kleene和Rosser共同研究,其结果分别证明了当时由阿隆佐·丘奇和柯里本人提出的几个形式系统的不完备性,而丘奇的系统,当时包括了λ-演算子系统,虽然整个系统不完备,但是这个子系统却是完备的。在这个证明完成之后,丘奇、Kleene和Rosser都放弃了对数学基础的研究,只有柯里坚持了下来,并声称“决不当悖论的逃兵”。
柯里对数学基础的全部希望都寄托在了“组合逻辑”上,这使他付出了毕生的精力。虽然组合逻辑的概念由Schönfinkel提出,但是大部分研究成果出自柯里,可以说柯里是组合逻辑的创建人之一。从现代角度来看,组合逻辑和λ-演算一同成为了函数式编程语言的理论基础,而后者的开创人正是阿隆佐·丘奇,不过丘奇的名声和λ-演算在很长一段时间内都盖过了柯里和组合逻辑。
1934年,柯里首次观察到蕴含式的某些形式可以转换成类型论中的某种组合子类型;24年后的1958年,柯里进一步观察到某种证明系统,例如希尔伯特式的演绎系统与组合逻辑中的标准计算模型的某些类型化片段一致,这些发现构成了发表于1960年代的柯里-霍华德同构的基础。
1942年,柯里发表了“柯里悖论”(Curry’s Paradox)。这个悖论的实质是语义悖论,亦即,其语义指称部分指向自己从而造成整句是个悖论。这个句子的结构一个if-then蕴含句:
   如果这个句子为真,那么中国与德国相邻。
现在根据蕴含真值表简单分析一下:
1. 蕴含句的前件为真、后件亦为真,那么整句为真:与事实矛盾;
2. 蕴含句的前件为真、后件为假,那么整句为假:与前件“这个句子为真”矛盾;
3. 蕴含句的前件为假、后件为真,那么整句为真:即和前件“这个句子为真”矛盾,也和后件事实矛盾;
4. 蕴含句的前件为假、后件为假,那么整句为真:和前件“这个句子为真”矛盾
因此整句是一个逻辑和语义的悖论。柯里的论文对此分别用自然语言、逻辑和集合论三种方法展示了这个悖论,因技术性太强这里就省略了。
柯里曾经写过数理逻辑的教科书《数理逻辑基础》(Foundations of Mathematical Logic)。柯里的哲学倾向偏于他的老师希尔伯特,但是后期的组合逻辑研究使他更接近直觉逻辑的观点。
柯里发表的主要著作和论文如下
组合逻辑基础:1930年,用德语写成,发表在“美国数学期刊”
可确定性的形式理论:用英语写成,第一版于1950年由Notre Dame大学出版社出版;第二版于1957年由同一出版社出版
代数逻辑教程:1952年,用法语写成,由巴黎Gauthier-Villars出版
形式主义数学哲学概览:1951年由阿姆斯特丹Elsevier出版社出版
组合逻辑·第一卷:(与Robert Feys合作)1958年用英语写成,由阿姆斯特丹North-Holland出版社出版
数理逻辑基础:1963年,用英语写成,由McGraw Hill出版;2012年由纽约Dover出版社再版
组合逻辑·第二卷:(与Robert Feys合作)1972年用英语写成,由阿姆斯特丹North-Holland出版社出版



https://blog.sciencenet.cn/blog-2349385-1028709.html

上一篇:集合论的哲学认知——读《Naive Set Theory》:有序对公理
下一篇:浅谈类型论——阶和结构
收藏 IP: 70.77.201.*| 热度|

2 吉宗祥 武夷山

该博文允许注册用户评论 请点击登录 评论 (3 个评论)

数据加载中...
扫一扫,分享此博文

Archiver|手机版|科学网 ( 京ICP备07017567号-12 )

GMT+8, 2024-3-29 02:09

Powered by ScienceNet.cn

Copyright © 2007- 中国科学报社

返回顶部