羅賓·米爾納 - 概述

1952年從劍橋大學(xué)國(guó)王學(xué)院畢業(yè)，之后的第一個(gè)工作是教師，然后在Ferranti公司當(dāng)程序員�；氐綄W(xué)術(shù)界，先后在City大學(xué)，Swansea大學(xué)，斯坦福大學(xué)任職。1973年回到英國(guó)愛(ài)丁堡大學(xué)，在愛(ài)丁堡大學(xué)任職期間，他開(kāi)發(fā)了函數(shù)式編程語(yǔ)言，ML，并和他的同事一起完成了LCF的開(kāi)發(fā)。在離開(kāi)愛(ài)丁堡前，羅賓·米爾納向現(xiàn)在的愛(ài)丁堡大學(xué)信息學(xué)院提供了一筆捐款并成立了每年一次在愛(ài)丁堡大學(xué)信息學(xué)院舉行的以他名字名名的羅賓·米爾納演講，被邀請(qǐng)的演講者都是對(duì)理論計(jì)算機(jī)科學(xué)有重大貢獻(xiàn)的學(xué)者。1995年，羅賓·米爾納回到母校劍橋，并擔(dān)任劍橋大學(xué)計(jì)算機(jī)實(shí)驗(yàn)室主任，現(xiàn)為劍橋大學(xué)計(jì)算機(jī)實(shí)驗(yàn)室教授。

羅賓·米爾納 - 簡(jiǎn)介

1991年的圖靈獎(jiǎng)授予給了愛(ài)丁堡大學(xué)計(jì)算機(jī)科學(xué)系教授羅賓·米爾納(RobinMilner)。他是繼威爾克斯(M．V．Wilkes，1967)、威爾金森(J．H．Wilkinson，1970)和霍爾(C．A．R．Hoare，1980)之后第四位獲此殊榮的英國(guó)科學(xué)家，這也使英國(guó)成為除美國(guó)之外獲得圖靈獎(jiǎng)的學(xué)者最多的國(guó)家。米爾納的主要貢獻(xiàn)在計(jì)算機(jī)程序設(shè)計(jì)語(yǔ)言方面，他提出了形式化邏輯系統(tǒng)的一個(gè)數(shù)學(xué)模型LCF，又主持開(kāi)發(fā)了元語(yǔ)言ML并使之標(biāo)準(zhǔn)化。米爾納還利用代數(shù)方法為并發(fā)與并行計(jì)算創(chuàng)建了一種概念框架系統(tǒng)CCS，推動(dòng)并促進(jìn)了并發(fā)與并行計(jì)算的發(fā)展。

米爾納生于1934年1月13日，先后在埃頓學(xué)院(EtonCollege)、國(guó)王學(xué)院(King’sCollege，圖靈也曾在這個(gè)學(xué)院上學(xué))和劍橋大學(xué)接受了高等教育，專業(yè)是數(shù)學(xué)，1957年獲得學(xué)士學(xué)位。他上大學(xué)期間曾經(jīng)接觸過(guò)由威爾克斯主持研制的世界上第一臺(tái)存儲(chǔ)程序式電子計(jì)算機(jī)EDSAC，在它上面編寫(xiě)過(guò)程序。但當(dāng)時(shí)米爾納對(duì)計(jì)算機(jī)并沒(méi)有重視，也沒(méi)有表現(xiàn)出很大的興趣。大學(xué)畢業(yè)以后，米爾納當(dāng)了幾年中學(xué)數(shù)學(xué)教師，更是把計(jì)算機(jī)全拋在腦后。直到1960年米爾納重新規(guī)劃自己的未來(lái)，到倫敦著名的Ferranti公司求職。Ferranti公司當(dāng)時(shí)正需要計(jì)算機(jī)編程人員，對(duì)有過(guò)編程經(jīng)歷的米爾納表示歡迎，但要求他“把一生都獻(xiàn)給計(jì)算機(jī)”。

20世紀(jì)60年代初，計(jì)算機(jī)還沒(méi)有十分普及。計(jì)算機(jī)的深刻含意是什么，從事計(jì)算機(jī)工作有多大前途和機(jī)會(huì)，這些問(wèn)題對(duì)于絕大多數(shù)人來(lái)說(shuō)都是不甚清楚的。因此，對(duì)于Ferranti公司這一要求，米爾納也深感迷茫和困惑。所幸的是，米爾納作出了正確的選擇，進(jìn)入Ferranti公司，從而重返計(jì)算機(jī)領(lǐng)域，并幸運(yùn)地與計(jì)算機(jī)科學(xué)同步成長(zhǎng)起來(lái)。

但米爾納在Ferranti公司只干了3年，以后就轉(zhuǎn)人大學(xué)從事教學(xué)與研究。他呆過(guò)的大學(xué)包括倫敦城市大學(xué)，威爾土南部海港城市的斯旺西(Swansea)大學(xué)，美國(guó)的斯坦福大學(xué)，但長(zhǎng)期與最后的落腳點(diǎn)則是愛(ài)丁堡大學(xué)，這是英國(guó)最著名、歷史最悠久的高等學(xué)府之一，有優(yōu)良的學(xué)術(shù)傳統(tǒng)，在計(jì)算機(jī)科學(xué)，尤其是人工智能領(lǐng)域，其研究工作曾長(zhǎng)期處于世界領(lǐng)先水平。

羅賓·米爾納 - 個(gè)人貢獻(xiàn)

首先，在計(jì)算機(jī)程序設(shè)計(jì)語(yǔ)言方面，米爾納和戈頓(M．J．Gordon)等人一起提出了形式化邏輯系統(tǒng)的數(shù)學(xué)模型，實(shí)現(xiàn)了他稱之為L(zhǎng)CF的一個(gè)系統(tǒng)——“可計(jì)算函數(shù)的邏輯”(LogicforComputableFunc-tions)。LCF不但是一種有效的建模工具，還是一種強(qiáng)有力的驗(yàn)證工具，利用它可以方便地驗(yàn)證計(jì)算機(jī)程序的正確性。由于在利用計(jì)算機(jī)解決各種各樣的具體問(wèn)題時(shí)，建立正確的形式化系統(tǒng)在理論上和實(shí)踐上都具有重要的意義，因此米爾納的LCF受到學(xué)術(shù)界的高度評(píng)價(jià)。實(shí)際上，米爾納是受斯科特(D．Scott，1976年圖靈獎(jiǎng)獲得者)的影響和啟發(fā)才從事這一研究的。我們前面已經(jīng)介紹過(guò)，斯科特是研究自動(dòng)機(jī)理論，和拉賓(M．O．Rabin)一起提出了“非確定性”有限狀態(tài)自動(dòng)機(jī)的著名學(xué)者，后來(lái)在20世紀(jì)60年代又和斯特雷奇(C．Stra-chey，1916—1975)合作，提出了程序設(shè)計(jì)語(yǔ)言的“標(biāo)志語(yǔ)義模型”，為“標(biāo)志語(yǔ)義學(xué)”(又稱“指稱語(yǔ)義學(xué)”或“數(shù)學(xué)語(yǔ)義學(xué)”)奠定了基礎(chǔ)，對(duì)計(jì)算機(jī)程序設(shè)計(jì)語(yǔ)言的發(fā)展產(chǎn)生了重大的影響。斯科特曾到牛津大學(xué)訪問(wèn)、講學(xué)，米爾納聽(tīng)了他的講演，看了他的著作，引起了對(duì)這個(gè)問(wèn)題的極大興趣，從而深人進(jìn)行研究，并獲得成果。20世紀(jì)70年代初，米爾納在斯坦福大學(xué)的人工智能實(shí)驗(yàn)室作訪問(wèn)學(xué)者時(shí)，曾用LCF證明了那里的一個(gè)很復(fù)雜的編譯器的正確性，受到有“人工智能之父”之稱的麥卡錫(J．McCarthy，1971年圖靈獎(jiǎng)獲得者)的高度評(píng)價(jià)。

在斯坦福大學(xué)期間，米爾納學(xué)習(xí)了由麥卡錫主持開(kāi)發(fā)的函數(shù)式人工智能程序設(shè)計(jì)語(yǔ)言LISP，這使他受到很大啟發(fā)，進(jìn)一步打開(kāi)了他的思路和智慧之窗�；氐綈�(ài)丁堡大學(xué)以后，他借鑒LISP的經(jīng)驗(yàn)，在LCF的基礎(chǔ)上，花了幾年的時(shí)間，開(kāi)發(fā)成功了一個(gè)更加重要的系統(tǒng)，即ML，也就是元語(yǔ)言(metalanguage)，一種用來(lái)描述、表達(dá)與驗(yàn)證其他語(yǔ)言的語(yǔ)言。ML是一種強(qiáng)多態(tài)類型的語(yǔ)言，一個(gè)ML程序也就是一個(gè)包含變量定義和函數(shù)作用的表達(dá)式序列，具有比LCF更強(qiáng)的推理能力。ML有時(shí)也被稱為函數(shù)式語(yǔ)言，但與純函數(shù)式語(yǔ)言有所不同，因?yàn)樗�具有引用的概念，即變量是可以賦值的。此外，它的輸入／輸出系統(tǒng)也引入了副作用。

ML取得成功以后，米爾納致力于使它國(guó)際化和標(biāo)準(zhǔn)化。在他的努力下，1984年成立了一個(gè)包括愛(ài)丁堡大學(xué)、劍橋大學(xué)和貝爾實(shí)驗(yàn)室等知名高等學(xué)府和研究機(jī)構(gòu)的專家在內(nèi)的15人工作小組，采取通過(guò)電子郵件交換意見(jiàn)進(jìn)行設(shè)計(jì)的方式工作。20世紀(jì)90年代初標(biāo)準(zhǔn)ML即SML問(wèn)世。SML具有高階函數(shù)功能、I／0機(jī)制、參數(shù)化的模塊系統(tǒng)和完善的類型系統(tǒng)。比如計(jì)算1+2+3+…+10的值的SML程序如下所示：

letfunsumitot=ifi=othentot

elsesum(i-1)(tot+i)

insum100

end

米爾納另一方面的貢獻(xiàn)是關(guān)于并發(fā)計(jì)算(concurrentcomputing)和并行計(jì)算(parallelcomputing)的。由于并發(fā)與并行計(jì)算與傳統(tǒng)的串行計(jì)算(sequentialcomputing)有著本質(zhì)上的不同，其復(fù)雜程度大大增加，無(wú)法用后者的方法和術(shù)語(yǔ)表達(dá)前者的意義。嚴(yán)格說(shuō)來(lái)，所謂兩個(gè)事件是“并發(fā)”的，是指一個(gè)系統(tǒng)內(nèi)部發(fā)生的這兩個(gè)事件之間沒(méi)有因果關(guān)系，并非先后關(guān)系(當(dāng)然，有因果關(guān)系者必有先后關(guān)系，但有先后關(guān)系者不一定有因果關(guān)系)。并發(fā)概念由發(fā)明著名的“佩特里網(wǎng)”的C．A．Petri于1962年首先嚴(yán)格定義并建立了模型。至于“并行”，指的是利用多個(gè)處理機(jī)或其他功能部件同時(shí)工作以提高系統(tǒng)性能或可靠性，馮·諾伊曼在20世紀(jì)40年代提出細(xì)胞自動(dòng)機(jī)可認(rèn)為是并行計(jì)算思想的開(kāi)端。米爾納經(jīng)過(guò)深入研究，提出了一種新的觀點(diǎn)，把可以按任意次序在系統(tǒng)內(nèi)發(fā)生的兩個(gè)事件定義為并發(fā)事件，稱之為“交疊式并發(fā)”，而佩特里定義的嚴(yán)格并發(fā)則稱為“真并發(fā)”。在交疊式并發(fā)概念的基礎(chǔ)上，米爾納利用代數(shù)方法創(chuàng)造了一種用于建立并發(fā)與并行計(jì)算的概念框架的系統(tǒng)叫“通信系統(tǒng)演算”CCS(Calculusfor，Com-municatingSystems)。CCS與霍爾(C．A．R．Hoare，1980年圖靈獎(jiǎng)獲得者)所創(chuàng)建的“通信順序進(jìn)程"CSP(CommunicatingSequentialProcess)是最典型的兩個(gè)描述性并發(fā)模型，即進(jìn)程代數(shù)模型，都以進(jìn)程及進(jìn)程間的通信為主要描述對(duì)象，系統(tǒng)中的事件就是進(jìn)程通信，特別適合于描述分布式系統(tǒng)。CCS已經(jīng)成功地用來(lái)解釋用于書(shū)寫(xiě)通信協(xié)議規(guī)約的國(guó)際標(biāo)準(zhǔn)語(yǔ)言Lotos，而Lotos則已用于面向?qū)ο蟮腞OOA方法中，用來(lái)描述面向?qū)ο笮枨蠖�義中的抽象數(shù)據(jù)類型和進(jìn)程定義。CCS本身雖然只有交疊式語(yǔ)義，但利用一些特殊的方法，如多層佩特里網(wǎng)方法，也可以建立起一個(gè)完整的真并發(fā)語(yǔ)義，因此具有很重要的價(jià)值。 米爾納在學(xué)術(shù)上的一個(gè)特點(diǎn)是十分注意打好基礎(chǔ)，精益求精。他主持開(kāi)發(fā)和標(biāo)準(zhǔn)化的ML被認(rèn)為是定義得最完善，最無(wú)懈可擊，結(jié)構(gòu)最優(yōu)美、和諧而又最短小、精悍的語(yǔ)言之一。在作風(fēng)上，米爾納謙虛謹(jǐn)慎，從善如流，非常注意聽(tīng)取和吸收合作者的意見(jiàn)。例如，標(biāo)準(zhǔn)ML有允許設(shè)計(jì)“大模塊”程序的功能，就是米爾納根據(jù)貝爾實(shí)驗(yàn)室的麥克奎因(D．MacQueen)所提出的構(gòu)思實(shí)現(xiàn)的。ML原先是一個(gè)專用語(yǔ)言，意大利學(xué)者魯卡·凱德利(LucaCardelli，當(dāng)時(shí)還是一個(gè)正在寫(xiě)博士論文的研究生)實(shí)現(xiàn)了ML的一個(gè)擴(kuò)充版本，使之更適合于教學(xué)。米爾納看到以后十分贊賞，在它的基礎(chǔ)上把ML進(jìn)一步發(fā)展為一個(gè)通用語(yǔ)言。米爾納的成功與他的這些優(yōu)秀品格是分不開(kāi)的。

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

《通信系統(tǒng)演算》(CalculusofCommunicatingSystems，Spnnger’1980)

《通信與并發(fā)》(CommunicationandConcurrency，Prentice-Hall，1989)

《標(biāo)準(zhǔn)ML的定義》(TheDefinitionofStandardML，MITh．，1990)

《對(duì)標(biāo)準(zhǔn)ML的說(shuō)明》(CommentaryonStandardML，MITpr，1991；Revisededition，1997)

此外，1996年，米爾納和旺德(1．Wand)還合編了一本《明天的計(jì)算：計(jì)算機(jī)科學(xué)未來(lái)的研究方向》 (ComputingTomorrow：FutureResearchDirectionsinComputerScience，CambridgeUnipr．)，書(shū)中有包括米爾納自己撰寫(xiě)的一篇文章在內(nèi)的總共16篇文章，都是計(jì)算機(jī)科學(xué)各方面的專家撰寫(xiě)的，論述了在計(jì)算復(fù)雜性、軟件工程、并行計(jì)算、自然語(yǔ)言處理、數(shù)據(jù)庫(kù)、知識(shí)重用、實(shí)時(shí)計(jì)算、安全、通信、交互計(jì)算、人工智能等各分支中未來(lái)研究的方向和重要課題，很值得重視。

米爾納在接受圖靈獎(jiǎng)時(shí)發(fā)表了題為“交互的原理”(ElementsofInteraction)的演說(shuō)，并接受了記者的采訪。演說(shuō)全文以及與記者的對(duì)話刊載于1993年1月的CommunicationsofACM，78～97頁(yè)。在與記者的談話中，米爾納表達(dá)了這樣一個(gè)觀點(diǎn)，即計(jì)算機(jī)科學(xué)既是理論性很強(qiáng)的科學(xué)，又是與應(yīng)用和實(shí)踐密切聯(lián)系著的科學(xué)。因此，任何希望在這一領(lǐng)域取得成功的年輕人，必須十分重視把理論與實(shí)踐結(jié)合起來(lái)。他送給年輕人這樣一個(gè)忠告：“不要丟失連接!”(Don’tlosethelink!)。大家知道，“連接”(link)在計(jì)算機(jī)專業(yè)中是一個(gè)十分基本而重要的概念，任何高級(jí)語(yǔ)言程序在編譯以后如果不經(jīng)過(guò)連接，都是不能運(yùn)行的。因此米爾納用這句話來(lái)勉勵(lì)年輕的計(jì)算機(jī)科學(xué)工作者，真是意味深長(zhǎng)的。

米爾納在愛(ài)丁堡大學(xué)任教20多年，并于1986年創(chuàng)建了該校的計(jì)算機(jī)科學(xué)基礎(chǔ)實(shí)驗(yàn)室(LaboratoryforFoundationsofComputersci-ence)，并出任主任，英國(guó)科學(xué)與工程研究院對(duì)該所有長(zhǎng)期的支持。最近米爾納已離開(kāi)愛(ài)丁堡，轉(zhuǎn)至劍橋大學(xué)的計(jì)算實(shí)驗(yàn)室。他目前的電子郵箱為：

Robin．Milner@cl．cam．a(chǎn)c．uk