羅賓·米爾納

簡介

1958年從劍橋大學(xué)國王學(xué)院畢業(yè)，之后的第一個工作是教師，然后在 Ferranti 公司當(dāng)程序員。回到學(xué)術(shù)界，先后在 City 大學(xué)，Swansea 大學(xué)，斯坦福大學(xué)任職。1973年回到英國愛丁堡大學(xué)，在愛丁堡大學(xué)任職期間，他開發(fā)了函數(shù)式編程語言，ML，并和他的同事一起完成了 LCF 的開發(fā)。在離開愛丁堡前，羅賓·米爾納向現(xiàn)在的愛丁堡大學(xué)信息學(xué)院提供了一筆捐款并成立了每年一次在愛丁堡大學(xué)信息學(xué)院舉行的以他名字名名的"羅賓·米爾納講座"，被邀請的演講者都是對理論計算機(jī)科學(xué)有重大貢獻(xiàn)的學(xué)者。1995年，羅賓·米爾納回到母校劍橋，并擔(dān)任劍橋大學(xué)計算機(jī)實驗室主任，現(xiàn)為劍橋大學(xué)計算機(jī)實驗室教授。1991年的圖靈獎授予給了愛丁堡大學(xué)計算機(jī)科學(xué)系教授羅賓·米爾納（Robin Milner）。他是繼威爾克斯（M.V.Wilkes, 1967）、威爾金森（J.H.Wilkinson, 1970）和霍爾（C.ARHoare, 1980）之后第四位獲此殊榮的英國科學(xué)家，這也使英國成為除美國之外獲得圖靈獎的學(xué)者最多的國家。米爾納的主要貢獻(xiàn)在計算機(jī)程序設(shè)計語言方面，他提出了形式化邏輯系統(tǒng)的一個數(shù)學(xué)模型 LCF，又主持開發(fā)了元語言 ML 并使之標(biāo)準(zhǔn)化。米爾納還利用代數(shù)方法為并發(fā)與并行計算創(chuàng)建了一種概念框架系統(tǒng) CCS，推動并促進(jìn)了并發(fā)與并行計算的發(fā)展。

學(xué)習(xí)

米爾納生于1934年1月13日，先后在伊頓公學(xué)（Eton College）、國王學(xué)院（King’s College，圖靈也曾在這個學(xué)院上學(xué)）和劍橋大學(xué)接受了高等教育，專業(yè)是數(shù)學(xué)，1957年獲得學(xué)士學(xué)位。他上大學(xué)期間曾經(jīng)接觸過由威爾克斯主持研制的世界上第一臺存儲程序式電子計算機(jī) EDSAC，在它上面編寫過程序。但當(dāng)時米爾納對計算機(jī)并沒有重視，也沒有表現(xiàn)出很大的興趣。大學(xué)畢業(yè)以后，米爾納當(dāng)了幾年中學(xué)數(shù)學(xué)教師，更是把計算機(jī)全拋在腦后。直到1960年米爾納重新規(guī)劃自己的未來，到倫敦著名的 Ferranti 公司求職。Ferranti 公司當(dāng)時正需要計算機(jī)編程人員，對有過編程經(jīng)歷的米爾納表示歡迎，但要求他“把一生都獻(xiàn)給計算機(jī)”。20世紀(jì)60年代初，計算機(jī)還沒有十分普及。計算機(jī)的深刻含意是什么，從事計算機(jī)工作有多大前途和機(jī)會，這些問題對于絕大多數(shù)人來說都是不甚清楚的。因此，對于 Ferranti 公司這一要求，米爾納也深感迷茫和困惑。所幸的是，米爾納作出了正確的選擇，進(jìn)入 Ferranti 公司，從而重返計算機(jī)領(lǐng)域，并幸運(yùn)地與計算機(jī)科學(xué)同步成長起來。但米爾納在 Ferranti 公司只干了3年，以后就轉(zhuǎn)人大學(xué)從事教學(xué)與研究。他呆過的大學(xué)包括倫敦城市大學(xué)，威爾土南部海港城市的斯旺西（Swansea）大學(xué)、美國的斯坦福大學(xué)。但長期與最后的落腳點則是愛丁堡大學(xué)，這是英國最著名、歷史最悠久的高等學(xué)府之一，有優(yōu)良的學(xué)術(shù)傳統(tǒng)，在計算機(jī)科學(xué)，尤其是人工智能領(lǐng)域，其研究工作曾長期處于世界領(lǐng)先水平。

貢獻(xiàn)

計算機(jī)程序設(shè)計語言方面

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

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

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

并發(fā)計算和并行計算

米爾納另一方面的貢獻(xiàn)是關(guān)于并發(fā)計算（concurrentcomputing）和并行計算（parallelcomputing）的。由于并發(fā)與并行計算與傳統(tǒng)的串行計算（sequentialcomputing）有著本質(zhì)上的不同，其復(fù)雜程度大大增加，無法用后者的方法和術(shù)語表達(dá)前者的意義。嚴(yán)格說來，所謂兩個事件是“并發(fā)”的，是指一個系統(tǒng)內(nèi)部發(fā)生的這兩個事件之間沒有因果關(guān)系，并非先后關(guān)系(當(dāng)然，有因果關(guān)系者必有先后關(guān)系，但有先后關(guān)系者不一定有因果關(guān)系)。并發(fā)概念由發(fā)明著名的“佩特里網(wǎng)”的 C.A.Petri 于1962年首先嚴(yán)格定義并建立了模型。至于“并行”，指的是利用多個處理機(jī)或其他功能部件同時工作以提高系統(tǒng)性能或可靠性，馮·諾伊曼在20世紀(jì)40年代提出細(xì)胞自動機(jī)可認(rèn)為是并行計算思想的開端。米爾納經(jīng)過深入研究，提出了一種新的觀點，把可以按任意次序在系統(tǒng)內(nèi)發(fā)生的兩個事件定義為并發(fā)事件，稱之為“交疊式并發(fā)”，而佩特里定義的嚴(yán)格并發(fā)則稱為“真并發(fā)”。在交疊式并發(fā)概念的基礎(chǔ)上，米爾納利用代數(shù)方法創(chuàng)造了一種用于建立并發(fā)與并行計算的概念框架的系統(tǒng)叫“通信系統(tǒng)演算” CCS(Calculus of communicating systems)。CCS與霍爾（C.A.R.Hoare，1980年圖靈獎獲得者）所創(chuàng)建的“通信順序進(jìn)程"CSP(Communicating Sequential Process)是最典型的兩個描述性并發(fā)模型，即進(jìn)程代數(shù)模型，都以進(jìn)程及進(jìn)程間的通信為主要描述對象，系統(tǒng)中的事件就是進(jìn)程通信，特別適合于描述分布式系統(tǒng)。CCS已經(jīng)成功地用來解釋用于書寫通信協(xié)議規(guī)約的國際標(biāo)準(zhǔn)語言 Lotos，而 Lotos 則已用于面向?qū)ο蟮?ROOA 方法中，用來描述面向?qū)ο笮枨蠖x中的抽象數(shù)據(jù)類型和進(jìn)程定義。CCS 本身雖然只有交疊式語義，但利用一些特殊的方法，如多層佩特里網(wǎng)方法，也可以建立起一個完整的真并發(fā)語義，因此具有很重要的價值。

米爾納在學(xué)術(shù)上的一個特點是十分注意打好基礎(chǔ)，精益求精。他主持開發(fā)和標(biāo)準(zhǔn)化的ML被認(rèn)為是定義得最完善，最無懈可擊，結(jié)構(gòu)最優(yōu)美、和諧而又最短小、精悍的語言之一。在作風(fēng)上，米爾納謙虛謹(jǐn)慎，從善如流，非常注意聽取和吸收合作者的意見。例如，標(biāo)準(zhǔn)ML有允許設(shè)計“大模塊”程序的功能，就是米爾納根據(jù)貝爾實驗室的麥克奎因（D.MacQueen）所提出的構(gòu)思實現(xiàn)的。ML原先是一個專用語言，意大利學(xué)者魯卡·凱德利（LucaCardelli，當(dāng)時還是一個正在寫博士論文的研究生）實現(xiàn)了ML的一個擴(kuò)充版本，使之更適合于教學(xué)。米爾納看到以后十分贊賞，在它的基礎(chǔ)上把 ML 進(jìn)一步發(fā)展為一個通用語言。米爾納的成功與他的這些優(yōu)秀品格是分不開的。

著作

米爾納的著作基本上就是他的成果的反映，主要有：《通信系統(tǒng)演算》（Calculus of Communicating Systems, Spnnger’ 1980）《通信與并發(fā)》（Communication and Concurrency, Prentice-Hall, 1989）《標(biāo)準(zhǔn)ML的定義》（The Definition of Standard ML, MITh. , 1990）《對標(biāo)準(zhǔn)ML的說明》（Commentary on Standard ML, MITpr, 1991; Revisededition, 1997）此外，1996年，米爾納和旺德（1.Wand）還合編了一本《明天的計算：計算機(jī)科學(xué)未來的研究方向》 （ComputingTomorrow: FutureResearchDirectionsinComputerScience, CambridgeUnipr. ），書中有包括米爾納自己撰寫的一篇文章在內(nèi)的總共16篇文章，都是計算機(jī)科學(xué)各方面的專家撰寫的，論述了在計算復(fù)雜性、軟件工程、并行計算、自然語言處理、數(shù)據(jù)庫、知識重用、實時計算、安全、通信、交互計算、人工智能等各分支中未來研究的方向和重要課題，很值得重視。

演說

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

實驗室

米爾納在愛丁堡大學(xué)任教20多年，并于1986年創(chuàng)建了該校的計算機(jī)科學(xué)基礎(chǔ)實驗室）（Laboratory for Foundations of Computer Science），并出任主任，英國科學(xué)與工程研究院對該所有長期的支持。最近米爾納已離開愛丁堡，轉(zhuǎn)至劍橋大學(xué)的計算實驗室。