數理邏輯與計算機科學有密切關係,前者在後者之中有應用。此點已被有關的科學家公認。
數理邏輯是計算機科學所必耑的西德著名計算機科學家在1983年發表的一篇文章中說:“形式化是計算機科學所必需的止如數學是古典工程科學所必需的”。
美國著名機科學家在前些年也曾經說:“我們打理由希望,到下個世紀,邏輯和計算機的關係將和上-世紀吋數學分析和科學的關係那樣富有成果。”數理邏輯可以在計算機科:用這是因為推理和計算這兩種過程適有本質聯係的近公式來說明兩者之間的聯係:受控的推理:數理邏輯中的概之和需經過發展,才能在計算機科學中有用。
由於不考慮效率的高而效宇卻是算機科學中至關重要的問題,所以數理邏輯中的許多力―法不能簡單地移植到計算機科學中,而要加以發展。比如在可計算性理論中所討論的可計算性是理論的可計算性,如作為計算機科學一個分支的計算複雜性理論卻是研究實際可計算件的(也就是在現實計算機上實際可計算的廣因之.不能認為邏輯中許多研究成果可以簡單地移植到計算機科學中,而常常是需要發展新的邏輯理論,發現新的邏輯方法。
而且計算機科學的新概念一般來源於對計算係統反複進行實驗的結果,而不是單純來自對計算係統的反思。
英國愛丁堡大學教授在最近說:“我們現在提出的研究課題是新的。新就新在下列的雙重論題:計算係統的設計隻有建立在理論上時才能成功,而一種理論中的重要概念隻有通過不斷地應用才能產生。《計算是一種實驗科學嗎》。
在同一篇論文中又說:“就我個人而言,我深信不僅在哲學式的研究中,而且在計算機科學的研究中理論和實驗是不可分的”。
這種理論與實驗的可分性是計算機科學的特征。
形式化方法本身是有局限性的,用之不逬,會導致邏輯矛盾。
數理邏輯中形式化方法的發展史的研究在這方麵是有用的。
著名計算機科學家目前正在從事如何在計算機科學中避免邏輯矛盾的研究。據說,他正在寫本名為《程序設計的邏輯基礎》的書。
數理邏輯需要開拓新的領域,而邏輯在計算機科學中的應用就是這樣的領域。
計算技術中提出了大量的邏輯問題,邏輯程序設計語言的設計與“推理機”(這是新一代計算機的核心部分)的研製就是這一類的問題。
卿等人近年提出的關於“常識中的推理”(即日常生活中的推理,如“非單調邏輯”)是又一個例子。
邏輯與計算機科學的關係並非單純是前者有許多現成的概念和方法在後者之中有應用,而是後者提出的問題將推動前者發展出新的方法和理論。
變換型程序設計的邏輯基礎
引言
由慕尼黑學派創立,通常被稱作“變換型程序設計”的這一套方法,貼切地節略在縮"通過規範說明和變換的程序開發中,這是一個項目的名字,該項目是歐洲信息程遠景規劃,領導的一個戶項目。這套方法由兩部分組成。
通過變換產生可執行的程序
注意上述過程與能行可定義函數類到能行可計算函數類的轉換過程之間的顯著相似性,是件有意思的事。回憶起來,能行可定義函數的定義~即函數可由一方程係統能行地定義一一實際上比能行可計算函數的定義要來得早些。一件邏輯史上的事實是,在一封給上帝的信中提出能行可定義函數的定義,後者將其改造為今天所說的遞歸函數最初設想的能行可定義函數在近年的文獻中有時被稱作“遞歸函數”。