計算複雜性理論與計算機算法的分析與設計
計算複雜性理論是一種關於算法的分析與優化的研究,而計算機科學與技術的各個領域(計算機係統設計、程序設計、大規模集成電路與微處理技術等)無一不要用到算法,也無一不要求對用到的算法能進行優化;因之,這一理論是在計算機科學與技術的各個領域中都可以有應用的。
計算複雜性理論是70年代才發展起來的,但在用於計算技術中的有些領域時,已顯示出很大的威力。這一理論中有關計算的某些性質的研究也日益引起人們的注意。某中關於確定的計算機(或程序)與非確定的計算機(或程序)的解題能力的比較問題尤其受到重視,吸引了許多人去研究它。
目前有關的研究工作者中間絕大部分人都猜測複雜性的研究可以應用於“人工智能”。因為機器計算是有局限性的,即計算時間與存貯空間兩方麵的局限性。一類問題,如果它的複雜性超出於這種限度就將不是可解的。例如在定理機械化證明這一領域中,近年有人研究了初等幾何是否實際可判定的問題,發現它的複雜性是指數的,從而就可以斷定,它雖是理論上可判定的,卻是實際上不可判定的。
他的這種理論不同於則證明論,後者注重協調性證明及其有關的問題,而前者注重研究數學證明的結構方麵的性質包括證明複雜性所以,該理論看來與自動定理證明有關。我們可以說,理論是一種證明的理論而不是意義上的證明論。
至於可證明遞歸函數論則是在60年代中期建立起來的,其論文發表在1965年的該理論建立在50年代初所做的一項猜測上,這項猜測認為存在著一般遞歸函數,它們的一般遞歸性是不能在公理化算術中加以證明的。也以在1965年用一種非可構造性的方法證明了這種函數的存在性,而十年之後,才有人給出了具體的例子。因為這一理論顯然與程序的完全正確性證明有關;自從70年代末開始,文獻中即有人指出這一理論有可能應用於程序正確性證明,但這方麵研究的報告至今未在文獻中出現。
我們在4這個項目下所列出的技術,它的應用多年以來早已在計算機科學界為人所知了。據王浩所著《走向機械化數學》所載,他在1958年利用一種經過改進的01112611自然推理形式,在飛機上用了不到三分鍾的時間證明了《數學原理》一書前五章中的全部定理(二百多條王浩所用的算法(確切地說,它們是半遞歸的過程),僅在邏輯範圍內是有效的,但在其它一些分支中則是情況不同的。王浩後來在60年代發表的一係列論文中對於他的原來的算法提出了一些改進想法,其要點是在算法途徑之外加上策略法,他稱之為模式識別王浩的這一建議現在看來還是有用而且令人感興趣的。
提出的概念和方法看起來都是和計算機科學有關的,在這門科學中,形式化方法近來變得越來越重要-了。工作的特點在於他對於邏輯係統的縝密的研究,對嚴格性的注重和審慎地構造了邏輯係統的元理論。所有這些與程序設計理論都是有關的,而程序設計理論就是程序語言過程的與非過程的元理論。
也是研究哲學的,是19世紀著名奧地利哲學家的學生。他是在《數學原理》這部書的影響外轉向數理邏輯的工作的影響,是邏輯學華沙學派的另一創始人。
研究邏輯的主要目的是想尋找一種理想的邏輯係統,這種係統以為模型但更加精確。這個目標在1930年以後被證明是不可能達到的,但對邏輯的一些深刻見解,如關邏輯語言學的思想以及定義理論的思想,是不僅僅具有邏輯史上的意義的。
廣義命題邏輯是一種推廣了的命題邏輯理論;本體論是關於連同.的理論而部分論是關於部分的理論觀點,部分論是一種和集合論類似的理論上述理論,一種都是公理化的演繹係統。廣義命題邏輯連同本體論構成了一種統一的理論它在範圍與能力:可以成等人所著的《數學原理》招比,在華沙大學通過他的講演討論班創立了語言學。他的基本思想有件已通過受他影響的人傳播開來以及在自然語言中定義某些語言概念(如定義真理性)的困難,他用他自己的話表達了的思想。關於真理性的完備定義的精確標準。例如可歸納性、可定義性、類的抽象、集的存在等公理,可以作為定義的完備規則的部分代用品。
概念是與對象語言或被討論的理論有關的,這種對象語言不同於“兒語言”,雖然有時可以是構成“元語言”的一部分,他看出了“語言悖論”的超邏輯的“元語言”的性質,區分“語言悖論”的“邏輯悖論”,後者是可以用純邏輯或數學的語言在形式係統中表示他認為在一種非構造分層的相對化的,然而是通用的、理想地完備的,並且是語言封閉因而能包容它自身的全部語言的這樣一種語言之中,古典邏輯的法則是不能協調地成立的。
我們或許可以設計種定義檢查程序,這種程序以職給出的規則為依據,將能夠用於檢查在新設計出來的程序設計語言中的那些形式定義是否正確。
本世紀傑出的邏輯學家提出了機器,遞歸可枚舉集理論和規範係統理論,但他的同代人沒有對他的工作給予應有的重視,隻是到近年來,其工作才受到了足夠的重視。在本文中,我們將僅介紹他的規範係統理論。該理論是他在本世紀20年代創立的,但直到本世紀40年代中期才公諸於世。