Fuleige 弗雷格
（F.L.）G. Friedrich Ludwig Gottlob Frege (1848～1925)
德國數(shù)學家、邏輯學家。1848年11月8日生于德國維斯馬,1925年7月26日卒于巴德克萊茵。1873年畢業(yè)于格丁根大學，獲博士學位。1874年起即在耶拿大學任講師，1879年任教授，1918年退休。在耶拿大學執(zhí)教的四十余年間，致力于數(shù)學基礎、數(shù)學哲學和邏輯理論的研究。
弗雷格于 1879年出版了《概念語言》一書，所謂“概念語言”是一種表意語言，用它進行推理最易于察覺隱含的前提和有漏洞的步驟。由于弗雷格認為算術定理可由純邏輯規(guī)律出發(fā)證得，為了保證推理過程的絕對嚴格性，他特地建立了這一符號語言。他成功地引入了數(shù)學中的函數(shù)概念，建立了量詞理論。這樣就構作了一種基本自足的邏輯演算即一階謂詞演算。從而給出了歷史上第一個嚴格的關于邏輯規(guī)律的公理系統(tǒng)。嗣后，他又出版了《算術基礎》（1884）和《算術的基本規(guī)律》 （卷I,1893；卷Ⅱ，1903）。在這些著作中他首創(chuàng)從邏輯出發(fā)來定義數(shù)和自然數(shù)，并從邏輯規(guī)律出發(fā)推導出一系列算術定理。盡管弗雷格明確地提出了數(shù)學可以化歸為邏輯的思想，但沒有全面地進行從邏輯推導數(shù)學的研究，因而他未能象B.A.W.羅素和A.N.懷特海在《數(shù)學原 理》中那樣精詳論證、充分展開邏輯主義的綱領（見數(shù) 學基礎），但弗雷格仍不失為邏輯主義的創(chuàng)始人之一。 邏輯主義的主要代表人物羅素，甚為稱頌弗雷格的工作。 弗雷格晚年從事數(shù)學哲學和邏輯理論的研究。
?。ㄐ煸茝模?nbsp;
弗雷格
大連理工大學 杜瑞芝
弗雷格，F(xiàn)．L．G．(Frege，F(xiàn)riedrich Ludwig Go-ttlob)1848年11月8日生于德國維斯馬(Wismar)；1925年7月26日卒于巴德克萊茵(Bad Kleinen)．數(shù)學、邏輯學、哲學．
弗雷格出生的年代正值德國民主革命開始．維斯馬是一個遠離德國政治中心的小商業(yè)城鎮(zhèn)，革命風潮對這里影響很?。ダ赘癯錾谝粋€信奉路德教的中產(chǎn)階級家庭，在血統(tǒng)上是混雜的(部分是德國的，部分是波蘭的)．其父亞歷山大?弗雷格(AlexanderFrege)開辦了一所女子學校．他去世后這所學校就由他妻子來管理．1869年，母親奧古斯特?弗雷格(Auguste Frege)送弗雷格到耶拿大學就讀．當時弗雷格就把數(shù)學作為自己的主要興趣，但也選修了化學、物理和哲學．他的老師——數(shù)學家、物理學家E．阿貝(Abbe)及時發(fā)現(xiàn)了他的才能，成為他畢生信念的支持者．在阿貝的幫助下，他離開耶拿，來到格丁根大學繼續(xù)深造．1873年，在數(shù)學家E．謝林(Schering)的指導下，弗雷格以論文“論平面上虛影的幾何圖形”(Ueber eine geometrische Darstellung derim ginaren Gebilde in der Ebene)獲得哲學博士學位．該論文通過對平面上虛影圖形性質的討論，闡明了幾何學基于直覺的觀點．他在格丁根還參加了著名哲學家R．H．洛采(Lotze)的講座．洛采的邏輯觀念，特別是他對純邏輯的看法，對弗雷格邏輯思想的形成有著重要的影響．
弗雷格在格丁根大學獲得博士學位之后，又回到耶拿大學．在阿貝的幫助下，他于1874年以論文“基于量值概念外延的演算方法”(Rechungsmethoden，die sich auf eine Erweitung desGr ssenbegriffes gr nden)獲得了無薪大學講師的資格①．在這篇論文中，弗雷格提出了用于運算的量值概念，并斷言算術真理產(chǎn)生于量值概念．1879年，弗雷格的《概念語言》問世之后，他又一次在阿貝的推薦下成為耶拿大學的編外教授．1896年成為榮譽教授．弗雷格在耶拿大學執(zhí)教40余年，講授過數(shù)學的各分支學科及有關的邏輯系統(tǒng)，舉辦過“概念符號”講座，他一直致力于數(shù)學基礎、數(shù)學哲學和邏輯理論的研究．1918年退休．
弗雷格首先是作為一位數(shù)學家和邏輯學家而聞名于世的．他在數(shù)學上的主要成就，是使自C．F．高斯(Gauss)以來所建立的數(shù)學體系更精確和完善，確立了算術演算的基本規(guī)則．他第一個建立了初步自足的命詞演算系統(tǒng)和量詞理論，首次提供了現(xiàn)代意義下的數(shù)理邏輯的一個體系，因而成為數(shù)理邏輯的奠基人．他提出數(shù)學可以化歸為邏輯的思想，成為邏輯主義的創(chuàng)始人．弗雷格還是一位杰出的哲學家．他的絕大部分著作都具有明顯的哲學特征．他認為：“一個好的數(shù)學家，至少是半個哲學家；一個好的哲學家，至少是半個數(shù)學家．”他直接把傳統(tǒng)哲學對思維內(nèi)容和認識能力的探討，轉向對語言表達形式和語言內(nèi)部框架的考慮．他認為對語言意義的分析，是哲學研究的主要任務．弗雷格對哲學任務的重新規(guī)定，標志著當代西方分析哲學的開端．因此他被譽為當代分析哲學的真正奠基者．
弗雷格的主要著作有：《概念語言》、《算術的基礎》、《函項與概念》(Function und Begriff，1891)、《論意義和所指》( ber Sinn und Bedeutung，1892)、《論概念和對象》( berBegriff und Gegenstand，1892)、《算術的基本規(guī)律》1—2卷(以下簡稱《基本規(guī)律》)．
弗雷格的科學生涯大致可以分為五個時．
在第一個時期，弗雷格主要從事純邏輯的研究．其研究成果總結在1879年出版的《概念語言》中．用數(shù)學方法研究邏輯問題，一般認為是由G．W．萊布尼茨(Leibniz)提出的文字學設想開始．他提出過有關思維演算的思想．萊布尼茨的這種先驅性想法沒有及時得到應有的發(fā)展．在淹沒了一個世紀之后，19世紀英國的兩位數(shù)學家A．德摩根(De Morgen)和G．布爾(Boole)用代數(shù)的方法建立了邏輯代數(shù)．但這種邏輯代數(shù)與亞里士多德(Ar-istotle)的形式邏輯本質上是相似的．在1874—1879年間，弗雷格攻讀了布爾學派和一些哲學邏輯學家的著作．除上文提到的洛采外，18世紀德國哲學家A．特倫德倫堡(Trendelenburg)的著作對弗雷格也有較大的影響．通過特倫德倫堡的工作使弗雷格了解到萊布尼茨關于邏輯語言的觀點．弗雷格還追隨特倫德倫堡，把他的邏輯符號系統(tǒng)稱作“概念語言”．弗雷格用心研究萊布尼茨和I．康德(Kant)的邏輯學和數(shù)學哲學方面的著作，有選擇地接受了兩位哲學家的思想．在弗雷格晚年，他是這樣描述自己的研究動機的：“我開始是搞數(shù)學．在我看來，這門科學急需更好的基礎：……語言邏輯的不完善對這種研究是一種障礙．我在《概念語言》中尋求彌補．所以，我就從數(shù)學轉向了邏輯．”
經(jīng)過5年的沉思，弗雷格完成了一部劃時代的著作——《概念語言》．在這本書里，弗雷格把從洛采和特倫德倫堡，以及從萊布尼茨和康德那里得到的觀點，變成一種全新的邏輯．這本不足80頁的小書是弗雷格的不朽之作．弗雷格在此建立的邏輯有效地終結了亞里士多德邏輯兩千多年來一直占據(jù)的統(tǒng)治地位，完成了始于幾百年前G．伽利略(Galilei)破除亞里士多德物理學的進程．在《概念語言》中，弗雷格創(chuàng)造了一種表意的語言，即“純粹思想的語言”．正如他在這本書的副標題中所說——它可以使我們完全精確地表達判斷的概念內(nèi)涵．弗雷格認為，真理分為兩種，一種真理的證明必須以經(jīng)驗事實為根據(jù)，例如物理學中的定理．另一種真理的證明似乎可以純粹從邏輯規(guī)律出發(fā)．他認為算術命題就是屬于后一種的．在探討如何根據(jù)思維的邏輯規(guī)律經(jīng)過推理以得到算術命題時，必須絕對嚴格，要防止未被查覺的直觀因素滲入，因此必須使推理過程沒有漏洞．他覺得日常語言是表達嚴密思想的障礙．當所表達的關系越復雜時，日常語言就越不能滿足要求．因此他創(chuàng)造了這種概念語言．他說，用這種語言進行推理，最有利于覺察隱含的前提和有漏洞的步驟．這種語言和日常語言相比，就好像機械手和人手相比，或者像顯微鏡和肉眼相比一樣．利用這種語言，弗雷格成功地構造了一個嚴格的邏輯演算體系．下面簡要介紹一下弗雷格邏輯演算的內(nèi)容．
1．弗雷格嚴格區(qū)別了命題的表達和斷定．他認為，我們只有能夠表達一個思想，理解一個思想，才能對它加以斷定．他引進斷定符號“├”．“├┌”表示“┌是被斷定的”．其中垂直短線“｜”稱為判斷短線，水平短線“—”稱為內(nèi)容短線．“—┌”是一個整體，它只表達可斷定的內(nèi)容，即命題的表達．而“├┌”才表示命題的斷定．如“├┌”表示“不同的磁極相互吸引”這一斷言，而“—┌”只是表達了不同磁極相互吸引這一思想，而對這一思想的正確性沒有任何判斷．
2．弗雷格明確提出真值蘊涵的思想并指出它與日常語言的區(qū)別．他采用否定和蘊涵作為基本的邏輯聯(lián)結詞．他用小豎線“ ”放在內(nèi)容短線下面表示否定．“┬┌”表示“非┌”．符號 表示“△蘊涵┌”．他列舉了┌和△的四種可能的真值組合：(1)┌肯定，△肯定；(2)┌肯定，△否定；(3)┌否定，△肯定；(4)┌否定，△否定．用符號“ ”表示以上第三種可能不實現(xiàn)而其余三個可能性中的每一個都可實現(xiàn)．弗雷格說，當┌為真時，△蘊含┌?？杀粩喽ǎ诖饲樾蜗?，△可以是任一命題，其具體內(nèi)容完全無所謂．┌和△不必有因果關系，與日常語言中的“如果……則”不同．
3．弗雷格引進一個內(nèi)容同一的符號．設┌和△為任意名稱，即不一定是命題記號，他規(guī)定，“├(┌≡△)”的意思是“名稱┌和名稱△有相同的概念內(nèi)容，使得┌總是能由△替換，反之亦然”．他還指出，由他的新符號所聯(lián)結的名稱不僅代表它們的內(nèi)容而且代表名稱自身．后來，他改用符號“=”，“=”不被看成兩個名字之間的關系，而是看成名字的指稱之間的關系．“=”用于專門的指稱，相當于等詞；用于命題的指稱(真值)，則相當于現(xiàn)在的等值符號．
4．弗雷格把數(shù)學中的函數(shù)概念引入邏輯演算，從而建立了量詞的理論．他采用變目和函項兩個術語，┌表示變目，記號Φ(┌)表達變目┌的一個不確定的函項．記號Ψ(┌，△)表達按順序所取的兩個變目┌和△的一個函項．假定如下一種函項：當它由變目填滿時，它表達可能的判斷內(nèi)容．于是，“├Φ(┌)”讀作“┌有性質Φ”，“├Ψ(┌，△)”讀作“┌與△有關系Ψ”．弗雷格使用這種符號的主要優(yōu)點是，它能夠比普通語言所提供的方式更令人滿意地表達一般性．在此基礎上，弗雷格引進了全稱量詞和存在量詞
表示“不管怎樣取函項的變目，函項總是一個事實”．即“凡a都是Φ．在這里，全稱量詞是基本概念，存在量詞則通過全稱量詞而表達為
它表達“至少有一個a是Φ”．
5．弗雷格建立了9條公理，用現(xiàn)代的符號表示為：
(1)├a→(b→a)，
(2)├(c→(b→a))→((c→b)→(c→a))，
(3)├(d→(b→a))→(b→(d→a))，
(4)├(b→a)→(┐a→ ┐b)，
(5)├ ┐┐a→a，
(6)├a→ ┐┐a，
(7)├(c=d)→(f(c)→f(d))，
(8)├c=c，
公理以外有四條變形規(guī)則：
(2)代入規(guī)則，弗雷格使用了但沒有嚴格地陳述．
假定a并不在表達式Г中出現(xiàn)，而且a僅處于Φ(a)的變目空位中．
a不在┌和△中出現(xiàn)，Φ(a)中的a只處于變目空位中．事實上，這條規(guī)則是第三條規(guī)則的推廣．
弗雷格在上述公理和規(guī)則的基礎上，進行了大量的推演，成功地構造了一種基本自足的邏輯演算，從而給出了歷史上第一個嚴格的關于邏輯規(guī)律的公理系統(tǒng)——現(xiàn)代的邏輯系統(tǒng)．它實質上包含了作為現(xiàn)代數(shù)理邏輯基礎的兩個演算系統(tǒng)——命題演算系統(tǒng)和一階謂詞演算系統(tǒng)．
不幸的是，弗雷格這本劃時代的小冊子被數(shù)學家和哲學家們忽視了．他在《概念語言》中建立的新邏輯沒有馬上被人理解．其中使用復雜而陌生的符號來表達新奇的概念，確使讀者望而生畏．德國數(shù)學家E．施羅德(Schrder)發(fā)表長篇文章，對該書進行全面批評．事實上，直到B．A．W．羅素(Russell)1901年開始發(fā)現(xiàn)弗雷格著作的價值之前，《概念語言》幾乎沒有讀者．
《概念語言》出版之后，弗雷格的創(chuàng)造生涯進入第二時期．在這一時期，弗雷格開始形成邏輯主義的觀點．在最初幾年，他由于自己的著作沒有受到重視而大受挫折，沒有發(fā)表任何作品．但他仍然在重新思考和深刻挖掘自己的哲學和數(shù)學觀點，并逐漸形成了他的數(shù)學哲學的三個主要原則：第一，他反對在數(shù)學基礎問題上的經(jīng)驗主義，否認數(shù)學來源的經(jīng)驗基礎，強調數(shù)學真理的先天性；第二，他認為數(shù)學真理是客觀的，這種客觀性基于數(shù)學的非經(jīng)驗的基礎．在他看來，客觀性是思想的必要條件；第三，他主張一切數(shù)學最終都可化歸為邏輯，數(shù)學概念可以定義為邏輯普遍要求的概念，數(shù)學公理可以從邏輯原則中得到證明．這第三條原則后來被羅素作為邏輯主義的基本主張而廣為傳播，弗雷格因此成為邏輯主義的創(chuàng)始人之一．
弗雷格在《算術的基礎》中力圖作為邏輯的延展去建立數(shù)學．為此，首先要從邏輯推出算術．為使大家能夠理解他的著作，他對自己的觀點及關于數(shù)和算術所流行的各種哲學觀點作了非形式的說明．然后他指出，要從邏輯推出算術，首先必須給出數(shù)和自然數(shù)的定義．
弗雷格接受他的前輩的觀點：所有大于1的自然數(shù)可由指出它們的前趨即用“2=1+1”，“3=2+1”一類等式來定義．但他認為，這些定義是不完全的，因為使用了“數(shù)1”和“加1”這兩個未定義的概念．他考察了從歐幾里得(Euclid)到G．康托爾(Cantor)以來的許多數(shù)學家的著作，發(fā)現(xiàn)關于數(shù)的定義是相當混亂的．他指出在此之前所見到的一切關于數(shù)的定義都含有基本的邏輯錯誤．他說：“數(shù)是什么？這是一個最根本的問題．如果我們對這個問題都不能做清楚的回答，豈不是一個笑話？”又說：“數(shù)學的本質就在于，一切能證明的都要證明，而不是通過歸納法來驗證．因此，我們也應考慮如何來證明關于正整數(shù)的命題．”
弗雷格發(fā)展了《概念語言》中關于數(shù)學序列的理論．在那里他用“遺傳性”定義了“y屬于從x開始的f-序列”和“y是x的f-后裔”，為自然數(shù)的定義和說明數(shù)學歸納法作了理論和技術上的準備．弗雷格給出的自然數(shù)的定義的核心在于使用了“一一對應”的概念：屬于兩個概念F和G的對象借助于關系Φ一一對應，如果(1)每一個屬于概念F的對象對于屬于概念G的一個對象，有關系Φ；(2)對于屬于概念G的每一個對象，存在一個屬于概念F并與前者有關系Φ的對象；(3)對所有x，y和z而言，如果x對y和z有關系Φ，那么y和z就是同樣的；(4)對所有x，y和z而言，如果x和y對z有關系Φ，那么x和y就是同樣的．
弗雷格在此基礎上構造了以下三個定義：
(1)“概念F與概念G是等數(shù)的”與“存在一個關系Φ，使得屬于概念F的對象與屬于概念G的對象一一對應”其意義是相同的．
(2)屬于概念F的數(shù)是“與概念F等數(shù)”這一概念的外延．
(3)“n是一個數(shù)”與“存在一個概念使得n是屬于它的數(shù)”其意義是相同的．
接著他又定義了“n在自然數(shù)序列中是m的直接后繼”：“存在一個概念F和一個歸于它的對象x，使得屬于概念F的數(shù)是n，屬于概念‘歸于F但不同于x’的數(shù)是m”．這實質上是后繼函數(shù)的定義．
在這些工作的基礎上，弗雷格取0作為數(shù)列的起點，提出如下定義：
0是屬于概念“不同于自身”的數(shù)，
1是屬于概念“同于0”的數(shù)，
2是屬于概念“同于0或同于1”的數(shù)，
3是屬于概念“同于0或同于1或同于2”的數(shù)，
……
可見，1在自然數(shù)序列中是0的直接后繼，2在自然數(shù)序列中是1的直接后繼，等等．
事實上，弗雷格所用到的“一一對應”概念與康托爾所謂的集合的“等價”意義是一樣的，弗雷格指出，他的數(shù)與康托爾理論中集合的“勢”或“基數(shù)”是相同的．兩個概念同數(shù)，就是兩個集合等價．概念“與概念F等數(shù)”的外延，就是與集合F等價的一切集合構成的集合．所以弗雷格實際上是把數(shù)定義為集合的集合，或類的類．利用康托爾的語言，概括弗雷格關于數(shù)的定義：
(1)一個集合的基數(shù)是所有等價于它的集合的集合．
(2)0=df?｛^｝(空集合的單元集)
1=df?｛0｝
2=df?｛0，1｝
3=df?｛0，1，2｝
弗雷格的后續(xù)函數(shù)的定義實際上是說：后續(xù)函數(shù)把等價集合的集合m映射到一個新的集合的集合Φ(m)(即n)，Φ(m)中的每一個集合是由在m中的某一個集合加上一個新分子而得到．
由此可見，自然序列中的每一個數(shù)，有一個直接后繼的數(shù)．這樣，自然數(shù)就由0和后繼函數(shù)而確定下來．
有邏輯學家評論，弗雷格的這個定義系統(tǒng)是哲學技巧中極其卓越的成就．人們也很容易理解，為什么弗雷格認為他至少使得算術化歸為邏輯是可能的．
在《算術的基礎》的最后幾頁，弗雷格指出，其他類型的數(shù)，也可以用類似的方式加以定義．實數(shù)和復數(shù)同樣可以刻畫為概念的外延．在《基本規(guī)律》的第二卷中，他闡明了這個方案是如何實施于實數(shù)的．
康托爾在1884年也給出數(shù)的定義，但弗雷格的定義比康托爾的更為精確．
弗雷格從邏輯出發(fā)定義了數(shù)和自然數(shù)，他對自然數(shù)的歸納定義也是對數(shù)學歸納法的最好說明．他認為，借助于上述定義，自然數(shù)的概念就被化歸成了邏輯的概念；自然數(shù)的理論則可以借助于上述定義和邏輯得到建立，這樣，算術理論就被“邏輯化”了．
弗雷格在他的第三時期集中精力寫作《基本規(guī)律》．原計劃寫三卷，實際上只完成兩卷(1893，1903)．弗雷格準備在這部專著中，從邏輯出發(fā)去展開除了幾何學以外的全部數(shù)學．他認為，邏輯的原則是完全可靠的，一旦完成了上述工作，數(shù)學“就被固定在一個永恒的基礎上了．”
1893年，出版了《基本規(guī)律》第一卷，它是《算術的基礎》的理論的嚴謹發(fā)展，書中改進了《概念語言》符號系統(tǒng)，提出了不同的公理，闡述了高階謂詞演算．從《概念語言》到《基本規(guī)律》，弗雷格的邏輯發(fā)生了三個主要變化：(1)他在自己的系統(tǒng)中加上了函項的值域這一概念；(2)區(qū)分了意義的兩個方面，即“所指”和“意義”；(3)更為嚴格地規(guī)定了與對象相對的函項的性質，明確提出了“第一層函項”和“第二層函項”的區(qū)別．第一層函項就是以前所定義的函項，其變目是對象，第二層函項就是函項的函項，其變目是函項，例如在Mβ(F(β))中，Mβ就是第二層函項，其變目是F．弗雷格還把概念分為第一層概念和第二層概念．這些邏輯上的變化在《基本規(guī)律》第一卷之前的5篇文章①中就已經(jīng)提出并作了解釋．
弗雷格在《基本規(guī)律》第一卷中建立了另一個邏輯系統(tǒng)——二階謂詞演算，提出了新的公理．他用‘xF(x)代表F(x)的值域，例如，若F(x)表達“x是人”，則它的值域‘xF(x)就表達“人類”．他還引進代表定冠詞的函項符號＼x．如＼’xF(x)讀為“那個具有性質F的x”．用現(xiàn)在的符號表示弗雷格的新公理如下：
在這個新系統(tǒng)中，除分離規(guī)則和代入規(guī)則之外，弗雷格還把原來系統(tǒng)的一些公理和定理作為新的推理規(guī)則．在這一系統(tǒng)中處理了命題演算，謂詞演算，類理論和關系理論，更重要的是進行了推導算術的工作．
《基本規(guī)律》第一卷出版后，再次受到冷遇．只有G．皮亞諾(Peano)在1895年作了評述，但他對這本書的內(nèi)容沒有足夠的理解．這再一次使弗雷格深感痛苦．然而，弗雷格并沒有放棄自己的目標，他繼續(xù)撰寫《基本規(guī)律》第二卷，其中主要論述實數(shù)的理論，并用較多的篇幅批評當時流行的觀點．
但是，弗雷格并沒有完成他的計劃．因為要理解數(shù)學科學的性質，除了算術以外，還必須考慮無窮集合的理論——集合論．弗雷格沒有深入研究集合論，沒有接觸到關于無窮集合的各種問題，特別是悖論問題．1902年，正當弗雷格等待《基本規(guī)律》第二卷付印的時候，他收到了羅素6月16日寫給他的信．信中首先稱頌他的工作：“就我所知，您的工作是我們時代中最好的．”“在許多具體問題上，我發(fā)現(xiàn)您的著作都進行了討論、區(qū)分和定義，這使其他邏輯學家的工作黯然失色．”具有諷刺意味的是，羅素的來信既標志著弗雷格的工作開始得到承認，也宣告了他的獨創(chuàng)性工作的終結．因為羅素在他的信中接著寫道：
“只有在一點上我遇到了困難①，……由于下述矛盾：令W為不能論斷自身的謂詞的謂詞，W可以論斷自身嗎？每種回答都隱含著它的否定①，因而人們必須得出，W不是一個謂詞．同理，沒有不包含自身的作為整體的類的類．由此我得到，在某種條件下，一個可定義的集合沒有構成一個整體．”
羅素當時并沒有完全認識到他的發(fā)現(xiàn)是怎樣嚴重地威協(xié)著弗雷格的邏輯主義綱領．但是，弗雷格本人毫無疑問地認識到這個矛盾的潛在致命力．他對羅素來信的反映迅速而強烈，他馬上復信[15]：
“您發(fā)現(xiàn)的矛盾引起了我極大的震驚，我?guī)缀蹩梢哉f是驚愕不已，因為它動搖了我建立算術基礎的企圖，……我的《基本規(guī)則》第二卷看來是有缺陷的．我無疑要補充一個附錄，對您的發(fā)現(xiàn)作出論述．”
在1903年，弗雷格出版了帶有一個后記(寫于1902年10月)的《基本規(guī)則》的第二卷．他在后記中不無悲哀地寫道：
“對于一個科學工作者來說，最不幸的事情莫過于：當他完成他的工作時，發(fā)現(xiàn)他的知識大廈的一塊基石突然動搖了．正當本書的印刷接近完成之際，伯倫特?羅素先生給我的一封信使我陷入這種境地．這封信是關于我的公理V的問題．我本人從來沒有掩蓋這條公理缺乏其他公理所具有的并必為邏輯規(guī)律所正當要求的自明性．
……
成為問題的恰恰不是我建立算術的特殊方式，而是算術是否完全可能有一個邏輯基礎．”
弗雷格的第四時期是在極度消沉中度過的．這一時期長達十幾年．最初，他相信能有補救的辦法使他的系統(tǒng)避免矛盾．他首先提出一種設想：可能有一些概念沒有相應的類．然后他用修改第Ⅴ公理的辦法來阻止羅素悖論的衍生．但是，后來邏輯學家的工作證明，他所做的努力并不足以使他的系統(tǒng)避免不一致．他還打算論述集合論的邏輯悖論(1906)．經(jīng)過幾年的努力之后，弗雷格似乎不那么相信能夠找到解決矛盾的辦法．雖然他沒有公開放棄自己的主張，但也不再做進一步的努力．至到1918年，弗雷格才徹底放棄把算術化歸為邏輯的一切希望，放棄了《基本規(guī)律》第三卷的寫作計劃．從此以后，他又進入了新的研究時期．他的研究興趣仍在數(shù)學基礎上，并很自然地轉向幾何學，提出了幾何學是整個數(shù)學的基礎的主張．弗雷格在1903年以后發(fā)表的論著很少．
雖然弗雷格的邏輯主義綱領沒有實現(xiàn)，但是他的獨創(chuàng)性工作對數(shù)學和哲學的發(fā)展都產(chǎn)生了重要影響．他的成就在有生之年沒有得到廣泛的承認，只是通過少數(shù)幾位有洞察力的人的努力，他的思想才逐漸得到理解，并通過他們的工作得到發(fā)展．
首先認識到弗雷格工作重要性的是羅素．羅素在他的《數(shù)學原理》(Principles of mathematics，1903)的附錄中，對弗雷格的邏輯進行了深入細致的研究，對弗雷格的從《概念語言》到《基本規(guī)律》第一卷等論著作了廣泛詳盡的評論．羅素發(fā)展了弗雷格的思想，他和A．N．懷特海(Whitehead)在《數(shù)學原理》(Principia mathematica，1910)中精詳論證，充分展開了邏輯主義綱領．書中可以看出弗雷格的明顯影響，甚至羅素與弗雷格不同的觀點也是受到弗雷格著作中難點的啟示而提出的．羅素表示：“在邏輯分析問題上，我們主要是從弗雷格獲得教益．”稍后，羅素的學生和朋友L．維特根斯坦(Wittgenstein)成為弗雷格的崇拜者．這位20世紀的著名思想家明確指出，他的哲學工作的兩個來源是“弗雷格的巨著和我的朋友羅索的著作”．30年代末期，由弗雷格本人的學生L．卡爾納普(Carnap)以及美國邏輯學家A．丘奇(Church)的倡導，弗雷格的邏輯理論，特別是關于意義和所指的學說重新引起人們的研究興趣[27]．1950年，《算術的基礎》英譯本出版，在使用英語的數(shù)學家中產(chǎn)生很大影響．
1918年以前，弗雷格一直安靜地生活在耶拿這座小小的大學城內(nèi)．他身材矮小，性格膽怯羞澀．弗雷格的工作長期得不到理解和承認．一般認為，他的著作對于大多數(shù)數(shù)學家來說是過于哲學化了，而對大多數(shù)哲學家來說又過于數(shù)學化了．弗雷格的著作長期受到冷遇，在相當長一段時間內(nèi)，哲學雜志和數(shù)學雜志都拒絕發(fā)表他的論文．由于得不到專業(yè)上的承認，他在耶拿大學當了好多年的編外教授．弗雷格還經(jīng)受了長遠計劃失敗的體驗．所有這一切使他變得比較內(nèi)向．他長期遠離自己的數(shù)學和哲學同事．但是，弗雷格全心全意追求真理，從不追求個人名聲；他屢受拙折而不放棄自己的奮斗目標；他勇于承認自己的失敗并另辟蹊徑提出新的主張．弗雷格這種追求真理的執(zhí)著精神和科學態(tài)度值得后人學習．
蘋果樹下的散步
歐洲有個古老的傳說：一輛著名的戰(zhàn)車，被一根山茱萸樹皮編制的繩索牢牢地捆住了。你要想取得統(tǒng)治世界的王位嗎？那就必須解開這個繩結。無數(shù)聰明、強悍的勇士滿懷希望而來，垂頭喪氣而去，因為繩結盤旋纏繞，繩頭隱藏難尋。一天，亞歷山大也慕名來到這里，他略略思索一下，便果斷地抽出寶劍，一劍把繩截成兩段。難解的繩結就這樣輕而易舉地被“解開”了。亞歷山大因此享有對整個世界的統(tǒng)治權。
1888年9月6日，人們驚喜地獲悉：十多年來許多數(shù)學家為之奮斗的著名難題——果爾丹問題，終于被一位當時尚名不見經(jīng)傳的青年人攻克了。他運用的方法和途徑是那樣的出人意料、令人折服，就像亞歷山大解開繩結一樣；也正如這位顯赫的君主在遼闊的歐亞大陸上留下曠世戰(zhàn)功，這位年輕人窮盡畢生心血和才華，在廣闊的數(shù)學領域里縱橫捭闔，遍及現(xiàn)代數(shù)學幾乎所有的前沿陣地，在整個數(shù)學的版圖上，到處都刻下他那光輝的名字。他就是數(shù)學世界的亞歷山大——大衛(wèi)?希爾伯特！
哥尼斯堡是德國一座古老而美麗的城市，康德、哥德巴赫是這座城堡的榮譽和驕傲，著名的七橋問題更使之名揚歐洲。1862年1月23日，希爾伯特就誕生在這座富有學術傳統(tǒng)的城市里。受家庭的熏陶，早在中學時代，希爾伯特對數(shù)學就表現(xiàn)出濃厚的興趣，并立志把數(shù)學作為自己奮斗的專業(yè)。
1880年秋，希爾伯特進入哥尼斯堡大學。這里的學術空氣濃厚而且自由，非常適宜希爾伯特的生活習性和學習要求。這段時間內(nèi)，他同兩位年輕的數(shù)學家的交往使他受益終生。一位是比他大3歲的胡爾維茨，在希爾伯特還是學生時，這位見多識廣的青年就已是副教授；另一位是閔可夫斯基，雖比希爾伯特小兩歲，但已榮獲巴黎科學院大獎而名揚國際。他們?nèi)灰惑w，情投意合。他們每天下午“準5點”相會于校園旁邊的蘋果樹下，互相交流彼此的學習心得、制訂計劃、探索未知領域。對于每一個重大問題，他們總是分頭準備、認真思考，并各抒己見，有時也會爭得面紅耳赤。據(jù)說，曾有一位前來哥尼斯堡大學訪問的外地學者，這天偶然經(jīng)過蘋果園，忽然聽到里面?zhèn)鞒鰩讉€人互不相讓的爭吵聲，他駐足而觀，發(fā)現(xiàn)三位年輕人比比劃劃，旁若無人。這位好心的人覺得有必要去勸解一下，但馬上就知道自己的擔心是多余的。那正是希爾伯特三人在討論問題。
蘋果樹下的小路清晰地向遠方延伸。他們通過日復一日的無數(shù)次散步，漫游了數(shù)學世界的每一個角落。這種數(shù)學家們特有的學習方式給他們其中的每一位帶來了希望、成功和友誼。
蘋果樹下的散步使希爾伯特利用有趣而又容易接受的學習方式像海綿吸水那樣接受數(shù)學知識，并以最簡潔、快速的方法到達數(shù)學研究的前沿陣地。胡爾維茨淵博、系統(tǒng)的知識，閔可夫斯基快捷、靈敏的思維，無不令希爾伯特如醉如癡，也激勵著他更加如饑似渴地學習、思考。這段時光為希爾伯特打下了牢固而全面的基礎，他也因之能在以后的歲月里頻頻出擊，并獲得數(shù)學麥加——哥廷根大學的教授席位。
英國現(xiàn)代計算機的起步的是從納粹德國的“謎”開始的?！爸i”（Enigma）是一種密碼電報機，由德國人在一戰(zhàn)和二戰(zhàn)之間研制成功。“謎”能把日常語言變?yōu)榇a，通過無線電或電話線路秘密傳送。它是一個木箱子，配有一臺打字機，箱上有26個閃爍不停的小燈泡，與打字機鍵盤的26個字母相對應?！爸i”的設計無懈可擊，有一套極精密的解碼設置，非一般的電報密碼所能比擬。在內(nèi)行人看來，平白如話，但在旁人，又是無從索解的天書。因此，這臺看似平常的機器，有了“謎”的稱號。這樣，德國的“謎”引起了英國情報部門高度的興趣。常規(guī)的解碼方式奈何不了“謎”，怎么辦？
這時，天才的數(shù)學家圖靈出現(xiàn)了。1931年圖靈進入劍橋大學國王學院，開始了他的數(shù)學天涯。一到那里，圖靈開始嶄露頭角，畢業(yè)后去美國普林斯頓大學攻讀博士學位，在那里就發(fā)明過一個解碼器（Encipher），二戰(zhàn)爆發(fā)后回到劍橋。
在劍橋，圖靈是一個婦孺皆知的怪才，常有出人意表的舉動。他每天騎自行車到離公寓3公里的一個叫布雷奇萊公園（Bletchley Park）的地方上班，因?；歼^敏性鼻炎，一遇花粉，鼻涕不止，圖靈就常戴防毒面具騎車上班，招搖過市，成為劍橋的一大奇觀。
他的自行車鏈條經(jīng)常在半道上掉落，要是換了別人，早就去車鋪修理了。而圖靈偏不，他在琢磨，發(fā)現(xiàn)這鏈條總是踏到一定的圈數(shù)時下滑，圖靈在騎車時就特別留心計算，于是能做到在鏈條下滑前一剎那戛然停車！讓旁人嘆服不已，以為是在玩雜耍。后來他居然在踏腳旁裝了一個小巧的機械計數(shù)器，到圈數(shù)時就停，好換換腦筋想些別的問題。圖靈的腦袋轉得比自行車飛輪還快。
用圖靈的腦袋來破譯德國的“謎”看來不是什么難事。二戰(zhàn)爆發(fā)后，圖靈成為英國外交部通信部門戰(zhàn)時公務員，主要負責解碼。他果然不負眾望，成功破譯了“謎”。而德國人還蒙在鼓里，還以為他們的“謎”能一直迷下去，照用不誤，泄露了大量的核心機密，在戰(zhàn)事上屢屢遭挫，戰(zhàn)后，圖靈被授予帝國勛章。至于圖靈如何破譯“謎”的，由于英國政府嚴格的保密法令，一直沒有公之于世。所以圖靈破譯“謎”也成為一個“謎”。
早在30年代初，圖靈就發(fā)表了一篇著名的論文《論數(shù)字計算在決斷難題中的應用》，他提出了一種十分簡單但運算能力極強的理想計算裝置，用它來計算所有能想象得到的可計算函數(shù)。它由一個控制器和一根假設兩端無界的工作帶組成，工作帶起著存儲器的作用，它被劃分為大小相同的方格，每一格上可書寫一個給定字母表上的符號?？刂破骺梢栽趲献笥乙苿?，控制帶有一個讀寫頭，讀寫頭可以讀出控制器訪問的格子上的符號，也能改寫和抹去這一符號。
這一裝置只是一種理想的計算模型，或者說是一種理想中的計算機。正如飛機的真正成功得力于空氣動力學一樣，圖靈的這一思想奠定了整個現(xiàn)代計算機的理論基礎。這就是電腦史上與“馮·諾依曼機器”齊名的“圖靈機”。
圖靈機被公認為現(xiàn)代計算機的原型，這臺機器可以讀入一系列的零和一，這些數(shù)字代表了解決某一問題所需要的步驟，按這個步驟走下去，就可以解決某一特定的問題。這種觀念在當時是具有革命性意義的，因為即使在50年代的時候，大部分的計算機還只能解決某一特定問題，不是通用的，而圖靈機從理論上卻是通用機。在圖靈看來，這臺機器只用保留一些最簡單的指令，一個復雜的工作只用把它分解為這幾個最簡單的操作就可以實現(xiàn)了，在當時他能夠具有這樣的思想確實是很了不起的。他相信有一個算法可以解決大部分問題，而困難的部分則是如何確定最簡單的指令集，怎么樣的指令集才是最少的，而且又能頂用，還有一個難點是如何將復雜問題分解為這些指令的問題。
此后圖靈在國家物理學實驗室（NPL）工作，并繼續(xù)為數(shù)字式計算機努力，在那里人發(fā)明了自動計算機（Automatic Computing Engine，ACE），在這一時期他開始探索計算機與自然的關系。他寫了一篇名為《智能機》的文章于1969發(fā)表，這時便開始有了人工智能的雛形。
圖靈相信機器可以模擬人的智力，他也深知讓人們接受這一想法的困難，今天仍然有許多人認為人的大腦是不可能用機器模仿的。而在圖靈認為，這樣的機器一定是存在的。圖靈經(jīng)常和其它科學家發(fā)生爭論，爭論的問題就是機器實現(xiàn)人類智能的問題，在今天我們看來這沒有什么，但是在當時這可不太容易被人接受。他經(jīng)常問他的同事，你們能不能找到一個計算機不能回答的問題，當時計算機處理多選問題已經(jīng)可以了，可是對于文章的處理還根本不可能，但今天的發(fā)展證明了圖靈的遠見，今天的計算機已經(jīng)可以讀寫一些簡單的文章了。
圖靈相信如果模擬人類大腦的思維就可以做出一臺可以思考的機器，它于1950寫文章提出了著名的“圖靈測試”，測試是讓人類考官通過鍵盤向一個人和一個機器發(fā)問，這個考官不知道他現(xiàn)在問的是人還是機器。如果在經(jīng)過一定時間的提問以后，這位人類考官不能確定誰是人誰是機器，那這個機器就有智力了。這個測試在我們想起來十分簡單，可是偉大的思想就源于這種簡單的事物之中。
現(xiàn)在已經(jīng)有軟件可以通過圖靈測試的子測試，軟件這個人類智慧的機器反映應該可以解決一些人類智力的問題。在完成ACE之前，圖靈離開了NPL，它在曼徹斯特大學開發(fā)曼徹斯特自動計算機（Manchester Automatic Digital Machine，MADAM）。他相信在2000年前一定可以制造出可以模擬人類智力的機器，圖靈開始創(chuàng)立算法，并使用MADAM繼續(xù)他的工作。
查爾斯·霍爾
---從QUICKSORT、CASE到程序設計語言程序設計語言的公理化
學過“數(shù)據(jù)結構”或“算法設計與分析”的人都知道著名的快速排序算法QUICKSORT；編過程序的人大概也都用過實現(xiàn)條件轉移的最方便的語句CASE語句。但是你知道這個算法和這個語句是誰發(fā)明的嗎?它們的發(fā)明者就是1990年IEEE計算機先驅獎和1980年圖靈獎的獲得者英國牛津大學計算機科學家查爾斯·霍爾(Charles AntonyRichard Hoare)。當然霍爾之所以獲得這兩項大獎決不僅僅是因為他發(fā)明了QUICKSORT和CASE，而是因為他在計算機科學技術的發(fā)展中，尤其是在程序設計語言的定義和設計、數(shù)據(jù)結構和算法、操作系統(tǒng)等許多方面都起了重要的作用，有一系列發(fā)明創(chuàng)造，QUICKSORT和CASE只是其中的一小部分而已。
霍爾于1934年1月11日誕生于英國南部。在坎特伯雷(Canter·bury)的國王學校(King’s Sch001)度過中學階段以后，進入牛津的莫頓學院(Merton College)學習數(shù)學，1960年取得碩士學位。之后他進入倫敦一家不大的計算機生產(chǎn)廠家Elliott Brothers公司，為該公司的Elliott 803計算機編寫庫子程序，從此開始他的計算機生涯。QUICK，SORT就是他在那個時候用原有的SHELLSORT(以算法的發(fā)明人D．L．Shell命名的通過調換并移動數(shù)據(jù)項實現(xiàn)排序的一種算法，發(fā)明于1959年)編程時分析了它的缺點而發(fā)明出來的。QUICKSORT具有“快刀斬亂麻”的特點，能迅速地對亂序作大幅度調整，特別適合于因多次追加、刪除而變得雜亂無章的數(shù)據(jù)集合。QUICKSORT是利用“分治法”(divide and conquer)進行算法設計的一個成功范例，它的發(fā)明是霍爾在計算機方面的天才的第一次顯露，受到老板的贊賞和重視。第二年，霍爾接受了一個新的任務，為公司的新機型Elliott 503設計一個新的高級語言。但就在其時，他弄到了一份Algol 60報告的復印件，還參加了一個由狄克斯特拉(E．W．D恥stra，首屆計算機先驅獎獲得者)等人在布賴頓舉辦的Algol 60培訓班，感到與其自己沒有把握地去設計一個新的語言，還不如將比較成熟的Algol 60在Elliott 503上加以實現(xiàn)?；魻柡退耐聜兊倪@個想法獲得公司同意以后，由霍爾主持設計與實現(xiàn)了Algol 60的一個子集的版本?；魻栐陂_發(fā)初首先制定了明確的目標，即系統(tǒng)要安全可靠，生成的目標碼要簡潔，工作區(qū)數(shù)據(jù)要緊湊，過程和函數(shù)的人口和出口要清晰、嚴密等，還明確了整個編譯過程采用一次掃描等原則。這樣，ElliottAl-gol的開發(fā)十分順利與成功，它在1963年中推出以后大受歡迎，成為世界各國所開發(fā)的Algol 60的各種版本中在效率、可靠性和方便性等方面的性能指標都首屈一指的一個版本，霍爾本人也從此受到國際學術界的重視。國際信息處理聯(lián)盟IFIP后來任命霍爾為2．1工作組(WorkingGroup 2．1)的負責人，這個工作組的任務是維護和發(fā)展Algol?；魻柟徊回摫娡?，主持設計了Algol X以繼承與發(fā)展Algol60。正是在AlgolX的設計中，霍爾發(fā)明了CASE語句。CASE語句具有如下形式的語法結構：
CASE E of
C1:S1；
C2:S2；
.
.
.
Cn-1:Sn-1;
Otherwise:Sn
End
其中E是一個表達式，稱為“選擇子”(Selector)，每個Ci的值為常數(shù)，稱為“分情形標號”，Si則為可執(zhí)行語句。CASE語句的含義是：若E的值等于某個Ci的值，則執(zhí)行其后的Si(i=1，2，3，…，n—1)，否則執(zhí)行Sn。某個Si或S。執(zhí)行完之后，整個CASE語句也就執(zhí)行完畢。由于CASE語句構成多路分支，程序結構清晰、直觀，所以CASE語句后來幾乎成為程序設計語言的標準，被各種語言廣泛采用。在C語言中，沒有獨立的CASE語句，但它的SWITCH語句(開關語句)實際上是在CASE語句的基礎上形成的：
switch E
{case C1:S1；
case C2:S2；
.
.
.
case Cn-1:Sn-1;
[default:Sn]
不同之處有二：一是C；可以是表達式，但計算結果必須仍是常數(shù)；二是E的結果若不等于某個Ci(i=1，2，3，…，n—1)的值，則視有無default子句，若有，執(zhí)行Sn；若無，則什么也不執(zhí)行，控制轉向SWITCH后的語句。顯然，這些都是對CASE語句的進一步改進。
霍爾于1968年離開Elliott，離開產(chǎn)業(yè)界，原因是作為學者他對程序設計浯言的形式化定義這類更偏重于學術性和理論性的課題更感興趣。離開Elliott以后，他任職過一年英國國家計算中心主任，發(fā)現(xiàn)自己也不適于從事行政管理，因此又轉入愛爾蘭的昆土大學(Queen’s University)，從事教學和研究，1977年轉入牛津大學。離開Elliott以后，霍爾在計算機科學理論的研究中發(fā)揮其特長，作出了許多創(chuàng)造性的重大貢獻。首先是1969年10月，霍爾在Communications of ACM上發(fā)表了他那篇有里程碑意義的論文“計算機程序設計的公理基礎”(An Axiomatic Basis for Computer Programming)。在這篇論文中，霍爾提出了程序設計語言的公理化定義方法，即公理語義學(axiomatic semantics)，也就是用一組公理和一組規(guī)則描寫語言應有的性質，從而使語言與具體實現(xiàn)的機器無關，而且也易于證明程序的正確性。這是繼麥卡錫(J．McCarthy，1985年計算機先驅獎獲得者)在1963年提出用遞歸函數(shù)定義程序、弗洛伊德(R．W．Floyd，1991年計算機先驅獎獲得者)在1967年提出基于程序流程圖的歸納斷言法以后，在程序邏輯研究中所取得的又一個重大技術進展?；魻柼岢龅姆椒ㄔ谶壿嬌吓c弗洛伊德提出的方法類似，但不是用流程圖而是用代數(shù)法，即控制流用以下一些結構表示：
begin al；a2；a3；…；an end
if p then a1 else a2
while p do a
后面為了方便，我們用到第一個結構時省略首尾的begin和end。
相應于弗洛伊德的驗證條件，霍爾引入下列符號：
p{a}q
其意義是：如果在執(zhí)行。之前P(叫做precondition)成立，則當α執(zhí)行完了后q(叫做postcondition)成立。
霍爾給出了以下一組證明規(guī)則(proof rule)或叫推導規(guī)則：
p’ pp{a}qq→q’
1.
p’{a}q’
這個規(guī)則中的p’→和q’→q是普通數(shù)理邏輯中的斷言命題，表示若p’(或q’)成立，則p(或q)成立。這個規(guī)則表示，若橫線以上的p’→p、p{a}q、q→q’成立，則橫線以下的p’{a}q1成立。
2．
P(e){x:=e}p(x)
這個規(guī)則表示，如果在將e賦給x之前p(e)成立，則其后p(x)成立。
3． P{a}qqr
p{a;b}r
這個規(guī)則表示的是“傳遞律”(transitive law)，即如果執(zhí)行α之前p成立，α執(zhí)行完了以后q成立；而如果執(zhí)行b之前q成立，b執(zhí)行完了以后r成立，則若在動作序列。和^執(zhí)行之前P成立，則a和b執(zhí)行完了以后r成立。
4. p∧r{a}qp∧～r(b)q
p{if r then a else b}q
這個規(guī)則中的∧和～是一般數(shù)理邏輯中的合取(conjunction)和否定(negation)連接詞。這個規(guī)則定義了if-then-else的執(zhí)行取決于precondition r的值。
5. p∧q{a}p
p{while q do a}p∧～q
這個規(guī)則定義了while循環(huán)：p是循環(huán)不變量（loop invariant），而q是終止循環(huán)的條件。
下面我們舉一個例子說明如何用霍爾建立的系統(tǒng)驗證程序的正確性。設有計算n的階乘n！的如下程序：
A: x:1;B
B: while y>0 do C
C: x:y×x;y:=y-1
則通過下列霍爾斷言可以證明上述程序是正確的，因為這些斷言都是真的，而且在霍爾的系統(tǒng)中是可以被證明的，而最后一個斷言正是我們所要尋求的結論，因此它們形成對上述階乘程序正確性的說明。
i. y>0∧x×y! =n! {x:=y×x}y>0∧x×(y-1)! =n!
[首先y>0∧x×y! =n!→y>0∧(y×x)×(y-1)! =n!]
然后用規(guī)則（2），用x代替y×x]
ii. y>0∧x×(y-1)! =n!{y:=y-1}y≥0∧x×y! =n!
[類似（i），利用規(guī)則（2）]
iii．y>0∧x×y! =n! {C}y≤0∧x×y! =n!
[對(i)和(ii)用規(guī)則(3)]
iv．Y≥0∧y=n∧x=1{B}x=n!
[因為] y=n∧x=1→x×y! =n!
又因為0！ =1，所以Y≥0∧x×y! =n! ∧y≤0→y=0∧x=n! →x×y! =n!
根據(jù)（iii），利用規(guī)則（5），令（5）中p=y≤0∧x×y! =n!，q=y>0，孥可得(iv)]
v. y≥0∧y=n{x:=1}y≥0∧y!=n∧x=1
[因為p{x:=1}p∧x=1]
vi. y≥0∧y=n{A}x=n!
[對（V）和(Vi)利用規(guī)則(3)]
因為(vi)中的precondition正好是n的初始條件，而postcondition給出了所需結果，這樣就證明了程序可算出n!。
為了給出證明，應該從程序的最后一行開始逐步后推。在這個例子中，(iii)步是最關鍵的，其中y≥0∧x×y! =n!就是循環(huán)不變量或歸納假設(induction hypothesis)。
利用霍爾提出的這種方法，已經(jīng)成功地描述了PASCAL等語言，說明了這個方法的巨大威力。但應該指出的是，霍爾的這個方法是不完備的，因為霍爾在開發(fā)和建立這個系統(tǒng)時并沒有追求系統(tǒng)的完備性，而更多地追求系統(tǒng)的實用性。
在數(shù)據(jù)類型、數(shù)據(jù)結構和操作系統(tǒng)設計等方面，霍爾也做了許多開創(chuàng)性的工作。目前廣泛流行與應用著的許多概念都源于霍爾的工作。例如，關于抽象數(shù)據(jù)類型的規(guī)格說明(Specification，也叫規(guī)約)與其實現(xiàn)是否一致，就是由霍爾于1972年公式化了的?；魻柾ㄟ^前后斷言方法用已經(jīng)定義了的(抽象)數(shù)據(jù)類型給出所要定義的新類型的抽象模型，這成為抽象數(shù)據(jù)類型規(guī)格說明的兩種主要方法之一，即模型方法(另一方法為基于異調代數(shù)理論的代數(shù)方法)。對于操作系統(tǒng)的設計與實現(xiàn)十分關鍵的monitor(監(jiān)控程序)的概念也是霍爾首先提出，并界定了它的作用與功能，即作為操作系統(tǒng)的核心，在把操作系統(tǒng)看做虛擬機擴充時，monitor是硬件的第一次擴充，它完成中斷處理、進程控制與進程通信、存儲區(qū)動態(tài)分配，建立軟時鐘，驅動設備通道，進行處理機調度。monitor為外面各層的設計提供良好的環(huán)境，并提高系統(tǒng)的安全性。
20世紀70年代后期，霍爾又深入研究了運行在不同的機器上的若干個程序之間如何互相通信、互相交換數(shù)據(jù)的問題，實現(xiàn)了面向分布式系統(tǒng)的程序設計語言CSP。在該語言中，一個并發(fā)系統(tǒng)由若干并行運行的順序進程組成，每個進程不能對其他進程的變量賦值。進程之間只能通過一對通信原語實現(xiàn)協(xié)作：Q?x表示從進程Q輸入一個值到變量x中；P!e表示把表達式e的值發(fā)送給進程戶。當戶進程執(zhí)行Q?x，同時口進程執(zhí)行戶!‘時，發(fā)生通信，e的值從Q進程傳送給戶進程的變量x。CSP語言后來成為著名的并行處理語言OCCAM(由INMOS公司為Transputer開發(fā))的基礎。20世紀80年代中期，霍爾又和布魯克斯(S．Brooks)等人合作，提出了“CSP理論”TCSP(Theory Of Communicating Sequential Processes)，它與上述CSP不同，但又有聯(lián)系，這是一個代數(shù)演算系統(tǒng)，其基本成分是事件(或動作)。進程由事件和一組算子構造而成。TCSP采用“廣播式通信”，而不像程序設計語言CSP中那樣采用握手式通信，即只有當并行運行的各進程都執(zhí)行同一動作時，才發(fā)生通信。此外，TCSP采用失敗等價作為確定進程等價的準則，這就是著名的“失敗語義”。利用失敗可以構造TCSP的指稱模型?；魻枮槭〉葍r建立了一些公理系統(tǒng)，可以對語義上的等價關系進行形式推導?；魻栐谶@方面的工作開創(chuàng)了用代數(shù)方法研究通信并發(fā)系統(tǒng)的先河，形成了所謂“進程代數(shù)”(process algebra)這一新的研究領域，產(chǎn)生了很重要的影響。
霍爾的論著極多，而且都很有份量，有很高的學術水平。有評論說，霍爾每發(fā)表一篇論文，幾乎就要改變一次人們對程序設計的認識。這雖然是一種夸張的說法，但也說明霍爾的論著確實非常重要。ACM在1983年評選出最近四分之一個世紀中發(fā)表在Communications of ACM上的有里程碑式意義的25篇經(jīng)典論文，只有兩名學者各有2篇論文人選，霍爾就是其中之一(另一名是首屆計算機先驅獎獲得者狄克斯特拉)?；魻柸诉x的兩篇論文分別是1969年10月的“計算機程序設計的公理基礎”(An Axiomatic Basis for Computer Programming，這篇論文的要點我們前面已經(jīng)介紹過了)，另一篇是1978年8月的“通信順序進程”(Communicating Sequential Processes)，該論文奠定了前述CSP語言的基礎。CSP現(xiàn)在已推廣為“混合通信／頃序進程”(Hybrid Communicating Sequential Processes)。在這個語言中，有一種特殊的語句稱為“連續(xù)構件”，可表示一個具體給定初值的微分方程；而原有的通信語句可用來表達事件的起源和發(fā)生；語言中的順序算子、條件算子等則用來刻畫連續(xù)構件和通信間的耦合關系。
值得指出的是，霍爾還和我國軟件學者、中國科學院軟件所的周巢塵研究員等合作，在20世紀80年代末由于Esprit的ProCos項目的需要而對基于時態(tài)邏輯的邏輯型混合計算模型進行了研究，在這個模型中引入了時段和切變的概念，建立了時段演算，已引起該領域同行的廣泛重視。時段用以刻畫系統(tǒng)在一個時間區(qū)間上的連續(xù)變化，而切變則表示事件的發(fā)生(離散變量的變化)。在單個時段上，借助連續(xù)數(shù)學(微分方程理論)推導系統(tǒng)的行為；而在相鄰時段間，則用時態(tài)邏輯中切變算子的規(guī)則，推導系統(tǒng)行為的轉化。這種混合計算模型對于設計要求絕對安全的軟件系統(tǒng)具有十分重大的意義。時段演算已在煤氣燃燒器、鐵路岔口控制、水位控制、自動導航、OCCAM語言的實時語義、描述調度程序的實時行為和電路設計等方面獲得成功應用。
此外，由法國學者阿勃利爾(J．R．Abrial)提出的以狀態(tài)機為模型的著名的形式規(guī)約語言Z語言，也是由霍爾所領導的研究小組加以發(fā)展并實現(xiàn)的。
霍爾出版的專著主要有以下幾種：
《操作系統(tǒng)技術》(Operating Systems Techniques，Academic Pr.,1972)
《數(shù)理邏輯和程序設計語言》(Mathematical Logic and Programming language，Prentice—Hall，1985)
《并發(fā)和通信的發(fā)展》(Development in Concurrency and Communication，Addison-Wesley，1990)
《機器推理和硬件設計》(Mechanized Reasoning and Hardware Design，Prentice·Hall，1992)
除了獲得計算機先驅獎和圖靈獎以外，霍爾還在1981年獲得AFIPS的Harry Goode獎；1985年獲得英國IEE的法拉第獎章?；魻栐鴳竭^世界的許多國家講學，中國科學院研究生院也曾于1983年邀請霍爾到北京講學，并主辦討論班。1989年霍爾當選為歐洲科學院院士。1992年新加坡政府授予霍爾“李光耀優(yōu)秀訪問學者”稱號。在2000年北京WCC大會上，霍爾應邀作了主題報告。
