羅賓·米爾納

羅賓·米爾納

羅賓·米爾納(Robin Milner),英國計算機科學家。生於1934年1月13日,1991年獲得世界計算機領域最高獎“圖靈獎”。在電腦程式設計語言方面,米爾納和戈頓等人一起提出了形式化邏輯系統的數學模型,實現了他稱之為LCF的一個系統——“可計算函式的邏輯”。另一方面的貢獻是關於並發計算(concurrentcomputing)和並行計算(parallelcomputing)。

基本介紹

  • 中文名:羅賓·米爾納
  • 外文名:Robin Milner
  • 國籍:英國
  • 出生地:英國普利茅斯
  • 出生日期:1934年1月13日
  • 逝世日期:2010年3月20日 
  • 職業:計算機科學家
  • 畢業院校:劍橋大學
  • 主要成就:1991年獲得圖靈獎
    開發了自動定理證明工具LCF
簡介,學習,貢獻,電腦程式設計語言方面,並發計算和並行計算,著作,演說,實驗室,

簡介

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

學習

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

貢獻

電腦程式設計語言方面

首先,在電腦程式設計語言方面,米爾納和戈頓(M.J.Gordon)等人一起提出了形式化邏輯系統的數學模型,實現了他稱之為LCF的一個系統——“可計算函式的邏輯”(LogicforComputableFunc-tions)。LCF不但是一種有效的建模工具,還是一種強有力的驗證工具,利用它可以方便地驗證電腦程式的正確性。由於在利用計算機解決各種各樣的具體問題時,建立正確的形式化系統在理論上和實踐上都具有重要的意義,因此米爾納的LCF受到學術界的高度評價。實際上,米爾納是受斯科特(D.Scott,1976年圖靈獎獲得者)的影響和啟發才從事這一研究的。我們前面已經介紹過,斯科特是研究自動機理論,和拉賓(M.O.Rabin)一起提出了“非確定性”有限狀態自動機的著名學者,後來在20世紀60年代又和斯特雷奇(C.Stra-chey,1916—1975)合作,提出了程式設計語言的“標誌語義模型”,為“標誌語義學”(又稱“指稱語義學”或“數學語義學”)奠定了基礎,對電腦程式設計語言的發展產生了重大的影響。斯科特曾到牛津大學訪問、講學,米爾納聽了他的講演,看了他的著作,引起了對這個問題的極大興趣,從而深入進行研究,並獲得成果。20世紀70年代初,米爾納在史丹福大學的人工智慧實驗室作訪問學者時,曾用LCF證明了那裡的一個很複雜的編譯器的正確性,受到有“人工智慧之父”之稱的麥卡錫(J.McCarthy,1971年圖靈獎獲得者)的高度評價。
在史丹福大學期間,米爾納學習了由麥卡錫主持開發的函式式人工智慧程式設計語言LISP,這使他受到很大啟發,進一步打開了他的思路和智慧之窗。回到愛丁堡大學以後,他借鑑LISP的經驗,在LCF的基礎上,花了幾年的時間,開發成功了一個更加重要的系統,即ML,也就是元語言(metalanguage),一種用來描述、表達與驗證其他語言的語言。ML是一種強多態類型的語言,一個ML程式也就是一個包含變數定義和函式作用的表達式序列,具有比LCF更強的推理能力。ML有時也被稱為函式式語言,但與純函式式語言有所不同,因為它具有引用的概念,即變數是可以賦值的。此外,它的輸入/輸出系統也引入了副作用。
ML取得成功以後,米爾納致力於使它國際化和標準化。在他的努力下,1984年成立了一個包括愛丁堡大學、劍橋大學和貝爾實驗室等知名高等學府和研究機構的專家在內的15人工作小組,採取通過電子郵件交換意見進行設計的方式工作。20世紀90年代初標準ML即SML問世。SML具有高階函式功能、I/0機制、參數化的模組系統和完善的類型系統。比如計算1+2+3+…+10的值的SML程式如下所示:
letfunsumitot=ifi=othentot
else sum(i-1)(tot+i)
insum100
end

並發計算和並行計算

米爾納另一方面的貢獻是關於並發計算(concurrentcomputing)和並行計算(parallelcomputing)的。由於並發與並行計算與傳統的串列計算(sequentialcomputing)有著本質上的不同,其複雜程度大大增加,無法用後者的方法和術語表達前者的意義。嚴格說來,所謂兩個事件是“並發”的,是指一個系統內部發生的這兩個事件之間沒有因果關係,並非先後關係(當然,有因果關係者必有先後關係,但有先後關係者不一定有因果關係)。並發概念由發明著名的“佩特里網”的C.A.Petri於1962年首先嚴格定義並建立了模型。至於“並行”,指的是利用多個處理機或其他功能部件同時工作以提高系統性能或可靠性,馮·諾伊曼在20世紀40年代提出細胞自動機可認為是並行計算思想的開端。米爾納經過深入研究,提出了一種新的觀點,把可以按任意次序在系統內發生的兩個事件定義為並發事件,稱之為“交疊式並發”,而佩特里定義的嚴格並發則稱為“真並發”。在交疊式並發概念的基礎上,米爾納利用代數方法創造了一種用於建立並發與並行計算的概念框架的系統叫“通信系統演算”CCS(Calculusfor,Com-municatingSystems)。CCS與霍爾(C.A.R.Hoare,1980年圖靈獎獲得者)所創建的“通信順序進程"CSP(CommunicatingSequentialProcess)是最典型的兩個描述性並發模型,即進程代數模型,都以進程及進程間的通信為主要描述對象,系統中的事件就是進程通信,特別適合於描述分散式系統。CCS已經成功地用來解釋用於書寫通信協定規約的國際標準語言Lotos,而Lotos則已用於面向對象的ROOA方法中,用來描述面向對象需求定義中的抽象數據類型和進程定義。CCS本身雖然只有交疊式語義,但利用一些特殊的方法,如多層佩特里網方法,也可以建立起一個完整的真並發語義,因此具有很重要的價值。
米爾納在學術上的一個特點是十分注意打好基礎,精益求精。他主持開發和標準化的ML被認為是定義得最完善,最無懈可擊,結構最優美、和諧而又最短小、精悍的語言之一。在作風上,米爾納謙虛謹慎,從善如流,非常注意聽取和吸收合作者的意見。例如,標準ML有允許設計“大模組”程式的功能,就是米爾納根據貝爾實驗室的麥克奎因(D.MacQueen)所提出的構思實現的。ML原先是一個專用語言,義大利學者魯卡·凱德利(LucaCardelli,當時還是一個正在寫博士論文的研究生)實現了ML的一個擴充版本,使之更適合於教學。米爾納看到以後十分讚賞,在它的基礎上把ML進一步發展為一個通用語言。米爾納的成功與他的這些優秀品格是分不開的。

著作

米爾納的著作基本上就是他的成果的反映,主要有:
《通信系統演算》(CalculusofCommunicatingSystems,Spnnger’1980)
《通信與並發》(CommunicationandConcurrency,Prentice-Hall,1989)
《標準ML的定義》(TheDefinitionofStandardML,MITh.,1990)
《對標準ML的說明》(CommentaryonStandardML,MITpr,1991;Revisededition,1997)
此外,1996年,米爾納和旺德(1.Wand)還合編了一本《明天的計算:計算機科學未來的研究方向》 (ComputingTomorrow:FutureResearchDirectionsinComputerScience,CambridgeUnipr.),書中有包括米爾納自己撰寫的一篇文章在內的總共16篇文章,都是計算機科學各方面的專家撰寫的,論述了在計算複雜性、軟體工程、並行計算、自然語言處理、資料庫、知識重用、實時計算、安全、通信、互動計算、人工智慧等各分支中未來研究的方向和重要課題,很值得重視。

演說

米爾納在接受圖靈獎時發表了題為“互動的原理”(ElementsofInteraction)的演說,並接受了記者的採訪。演說全文以及與記者的對話刊載於1996年1月的CommunicationsofACM,78~97頁。在與記者的談話中,米爾納表達了這樣一個觀點,即計算機科學既是理論性很強的科學,又是與套用和實踐密切聯繫著的科學。因此,任何希望在這一領域取得成功的年輕人,必須十分重視把理論與實踐結合起來。他送給年輕人這樣一個忠告:“不要丟失連線!”(Don’tlosethelink!)。大家知道,“連線”(link)在計算機專業中是一個十分基本而重要的概念,任何高級語言程式在編譯以後如果不經過連線,都是不能運行的。因此米爾納用這句話來勉勵年輕的計算機科學工作者,真是意味深長的。

實驗室

米爾納在愛丁堡大學任教20多年,並於1986年創建了該校的計算機科學基礎實驗室(LaboratoryforFoundationsofComputersci-ence),並出任主任,英國科學與工程研究院對該所有長期的支持。最近米爾納已離開愛丁堡,轉至劍橋大學的計算實驗室。他目前的電子信箱為:
Robin.Milner@cl.cam.ac.uk

相關詞條

熱門詞條

聯絡我們