人物簡介
(1936-2001)Robert W.Floyd
歷屆圖靈獎得主基本上都有高學歷、高學位,絕大多數有博士頭銜。這是可以理解的,因為創新型人才需要有很好的文化素養,豐富的知識底蘊,因而必須接受良好的教育。但事情總有例外,1978年圖靈獎獲得者、史丹福大學計算機科學系教授羅伯特·弗洛伊德就是一位“自學成才的計算機科學家”(a Self-Taught Computer Scientist)。
弗洛伊德1936年6月8日生於紐約。說他“自學成才”並不是說他沒有接受過高等教育,他是芝加哥大學的畢業生,但學的不是數學或電氣工程等與計算機密切相關的專業,而是文學,1953年獲得文學士學位。
20世紀50年代初期美國經濟不太景氣,找工作比較困難,因學習文學而沒有任何專門技能的弗洛伊德在就業上遇到很大麻煩,無奈之中到西屋電氣公司當了二年計算機操作員,在IBM650機房值夜班。我們知道,早期的計算機都是以批處理方式工作的,計算機操作員的任務就是把程式設計師編寫好的程式在卡片穿孔機(這是脫機的輔助外部設備)上穿成卡片,然後把卡片疊放在讀卡機上輸入計算機,以便運行程式。因此,操作員的工作比較簡單,同打字員類似,不需要懂計算機,也不需要懂程式設計。但弗洛伊德畢竟是一個受過高等教育的人,又是一個有心人,幹了一段時間的操作員,很快對計算機產生了興趣,決心弄懂它,掌握它,於是他借了有關書籍資料在值班空閒時間刻苦學習鑽研,有問題就虛心向程式設計師請教。白天不值班,他又回母校去聽講有關課程。這樣,他不但在1958年又獲得了理科學士學位,而且逐漸從計算機的門外漢變成計算機的行家裡手。
1956年他離開西屋電氣公司,到芝加哥的裝甲研究基金會(Armour Research Foundation),開始還是當操作員,後來就當了程式設計師。1962年他被麻薩諸塞州的Computer Associates公司聘為分析員。此時與Warsall合作發布Floyd-Warshall算法。1965年他應聘成為卡內基—梅隆大學的副教授,3年後轉至史丹福大學。1970年被聘任為教授。
之所以能這樣快地步步高升,關鍵就在於弗洛伊德通過勤奮學習和深入研究,在計算機科學的諸多領域:算法,程式設計語言的邏輯和語義,自動程式綜合,自動程式驗證,編譯器的理論和實現等方面都作出創造性的貢獻。其中包括:1962年,弗洛伊德完成了Algol 60編譯器的開發,成功投入使用,這是世界上最早的Algol 60編譯器之一,而且弗洛伊德在這個編譯器的開發中率先融入了最佳化的思想,使編譯所生成的目標代碼占用空間少,運行時間短。弗洛伊德最佳化編譯的思想對編譯器技術的發展產生了深刻的影響。隨後,他又對語法分析進行了系統研究,優先文法(precedence grammar),限界上下文文法(bounded context grammar)等都是弗洛伊德在首先提出來的。優先文法解決了自底向上的語法分析中的首要任務:如何找到“句柄”,也就是當前需要進行歸約的符號串。弗洛伊德通過對不同的符號定義不同的優先權,解決了這個問題。限界上下文文法則通過對上下文無關文法G中的兩個推導:
*
S→βArβαγ
+
S→δαε
進行比較以確定α是否是δαε的句柄,以及產生方式A→α是否是唯一可進行歸約的產生式。弗洛伊德經過研究,給出其充分必要條件為:β和δ的最後m個符號相同,丁和o/的最初n個終結符相同。這樣一個上下文無關文法G就稱為(m,n)限界上下文文法。
在算法方面,弗洛伊德和威廉士(J.Williams)在1964年共同發明了著名的堆排序算法HEAPSORT,這是與英國學者霍爾 (C.A.R.Hoare,1980年圖靈獎獲得者)發明的QUICKSORT齊名的高效排序算法之一。此外還有直接以弗洛伊德命名的求最短路的算法,這是弗洛伊德利用動態規劃(dynamic programming)的原理設計的一個高效算法。
在程式設計方面,計算機科學家非常關心的一個重要問題是如何表達和描述程式的邏輯,如何驗證程式的正確性。1967年,在美國數學會AMS舉行的套用數學討論會上,弗洛伊德發表了那篇引起轟動並產生了深遠影響的論文,即“如何確定程式的意義”(Assigning Meanings to Programs)。這篇論文在程式邏輯研究的歷史上,是繼麥卡錫(J.McCarthy,1971年圖靈獎獲得者)在1963年提出用遞歸函式作為程式的模型這一方法以後最重大的一個進展。
麥卡錫倡導的方法對於一般程式,包括大型軟體確實是行之有效的,但它有一個不足,即對於許多以命令方式編寫的軟體,其中包括賦值語句,條件語句,用While實現循環的語句……對這樣的程式用遞歸定義的函式去證明其正確性就很不方便了。正是為了解決這個問題,弗洛伊德在上述論文中提出了一種基於流程圖的表達程式邏輯的方法。這個方法的主要特點就是在流程圖的每一弧線上放置一個“標記”(tag),也就是一個邏輯斷言,並且保證只要當控制經過這個弧線時該斷言一定成立。弗洛伊德的主要貢獻在於解決了基於這種標記的形式系統的細節,證明了這種系統的完備性,解決了如何證明程式終結的問題。弗洛伊德還引入了驗證條件的概念,包括流程圖的一個組成部分(方框、圓框等)及其人口和出口處的標記。為了證明帶標記的流程圖的正確性,只要證明其中每一組成部分的驗證條件成立就行了。弗洛伊德提出的方法被叫做“歸納斷言法”(inductive assertion method),或前後斷言法(pre·and post-assertion method)。在框圖每個斷點i上所加的邏輯斷言即標記就叫i點的歸納斷言,說明程式執行經過此點時在各輸入變數x和各程式變數丁之間應存在的關係,以謂詞Pi(x,y)的形式表示。若程式從斷點i經過路段。到下一斷點j的驗證條件以Ra(x,y)表示,丁的值在。上的變化以ha(x,y)表示,則只要能證明下式恆真:
(∨x)(∨y)[pi(x,y)∧Ra(x,y) Pj(x,ha(x,y))]
程式從i到j的部分正確性也就證明了。
雖然用歸納斷言法不能證明程式的完全正確性,因為它必須以程式能夠終結為前提,但由於弗洛伊德在論文中同時也考慮了如何證明程式終結的問題,因此弗洛伊德的歸納斷言法也就有了普遍的意義。
學術成就
弗洛伊德在同年發表於《ACM學報》(Journal of ACM)10月號上的另一篇論文中,還第一次把“不確定性”概念引入程式。所謂“不確定性程式”(non deterministic program)就是根據操作規則有多種操作可供選擇,而只選其中之一搜尋下去的程式。這對人工智慧問題的研究具有十分重要的意義。
此外,弗洛伊德還和伊萬斯(R. 0.Evans,因設計世界上第一個類比推理程式Analogy而聞名於世的學者。Analogy是可以判定幾何圖形是否類似的人工智慧程式)一起設計了一種稱為產生式語言的特殊的程式設計語言FPL(Floyd-Evans Production Language),用來編寫計算機語言的語法分析程式。之所以稱它為產生式語言,是因為用它編寫的程式由一系列產生式(或稱歸約式)組成。實際上,用 FPL編好語法分析程式以後,如果再插入語義子程式,就可以構成一個完整的編譯器。用FPL語言編寫的程式簡稱PP程式,由以下5個部分按自左至右順序組成:
⒈標號(可有可無);
⒉棧頂符號串;
⒊前看符號串(或稱視窗符號串);
⒋歸約符號;
⒌語義動作。
執行一個PP程式的方法是:依次檢視各PP的第三部分。若某PP的第三部分和輸入的前看符號串一致,則進一步檢視此PP的第四部分,若非空,表示要進行歸約,此時把它的第二部分和當前實際的棧頂符號串相比。如果能匹配上,則實行歸約,即刪去實際的棧頂符號串,用第四部分代替之,然後執行第五部分的動作。若此PP的第四部分為空,表示當前無歸約可做,直接執行第五部分的動作即可。
弗洛伊德是1978年12月4日在華盛頓舉行的ACM年會上接受圖靈獎的。
他發表了題為“程式設計的風範”(The Paradigms of Programming)的演說。演說全文刊於Communications of ACM,1979年8月,455-460頁,也可見《前20年的ACM圖靈獎演說集》(ACM Turing Award Lectures——The First 20Years:1966—1985,ACM Pr.),131—142頁。
弗洛伊德在演說中對結構化程式設計,遞歸協同例程(recursive coroutine),動態程式設計,基於規則的系統,狀態變換機制(state-transition mechanism)等各種不同程式設計風範進行了比較,並介紹了自己在研究工作中如何根據具體情況套用不同風範的例子,很給人以啟示。時間雖然已過去20多年,他的例子也許有些過時,但他的觀點至今仍然是有效的。