計(jì)算機(jī)由來與原理？

現(xiàn)代邏輯肇始于萊布尼茨，在布爾和弗雷格處發(fā)生了分流，形成了所謂的邏輯的代數(shù)傳統(tǒng)和邏輯的語言傳統(tǒng)，然而，無論是代數(shù)傳統(tǒng)亦或者是語言傳統(tǒng)都離萊布尼茨的邏輯學(xué)綱領(lǐng)（即：“作為科學(xué)、數(shù)學(xué)和哲學(xué)”的基礎(chǔ)）相去甚遠(yuǎn)。在圖靈機(jī)理論中，圖靈核心闡述了“自動(dòng)機(jī)”和“指令表語言”這兩個(gè)概念，這兩者很好地契合了萊布尼茨關(guān)于 “理性演算”和“普遍語言”的構(gòu)想，可以說，圖靈機(jī)理論最為接近萊布尼茨的邏輯學(xué)綱領(lǐng)，也跳出代數(shù)傳統(tǒng)和語言傳統(tǒng)，另辟蹊徑，形成了一種新的“作為計(jì)算的邏輯”傳統(tǒng)（也可以稱為“計(jì)算傳統(tǒng)”）?！白鳛橛?jì)算的邏輯”實(shí)質(zhì)上是一種“主體轉(zhuǎn)向”，“以往的邏輯”是當(dāng)仁不讓地以人類為主體，研究的對(duì)象是人的思維、自然語言種種，“作為計(jì)算的邏輯”則是將計(jì)算機(jī)作為信息處理的主體，研究的是計(jì)算機(jī)的處理方式以及人與計(jì)算機(jī)的互動(dòng)關(guān)系。

關(guān)鍵詞：邏輯學(xué)；萊布尼茨綱領(lǐng)；圖靈機(jī)；作為計(jì)算的邏輯



引言
如果談及邏輯與計(jì)算的關(guān)系，大多數(shù)人都會(huì)認(rèn) 同邏輯與計(jì)算彼此緊密關(guān)聯(lián)，例如，美國計(jì)算機(jī)科學(xué)家馬納（Manna）就曾經(jīng)提出過“邏輯即計(jì)算機(jī)科學(xué)的演算”的觀點(diǎn)，此外，甚至還有人認(rèn)為“計(jì) 算本質(zhì)上就是邏輯”，例如，我國著名數(shù)理邏輯學(xué)家莫紹揆指出：“事實(shí)上，它們［程序設(shè)計(jì)］或者就是數(shù)理邏輯，或者是用計(jì)算機(jī)語言書寫的數(shù)理邏輯，或者是數(shù)理邏輯在計(jì)算機(jī)上的應(yīng)用” 。從某種意義上來說，邏輯之于計(jì)算的重要性怎么強(qiáng)調(diào)都不過分，這些主張可以通過如下論據(jù)來為之辯護(hù)：

1．從計(jì)算機(jī)的發(fā)展歷史來看，計(jì)算科學(xué)起源于邏輯學(xué)

追溯現(xiàn)代計(jì)算機(jī)科學(xué)的起源，應(yīng)該說，它與邏輯有著密不可分的關(guān)系。眾所周知，自從羅素與懷特海共同撰寫《數(shù)學(xué)原理》之后，興起對(duì)數(shù)理邏輯的研究，人們甚至期望以邏輯為基礎(chǔ)，構(gòu)建整個(gè)數(shù)學(xué)，乃至科學(xué)大廈。在這種邏輯主義的驅(qū)使下，不可避免地需要對(duì)“能行可計(jì)算”概念進(jìn)行形式化。在“能行可計(jì)算”概念的探索中，丘奇、哥德爾和圖靈幾乎在同一時(shí)間給出完全不同且又相互等價(jià)的定義。丘奇發(fā)明了Lambda演算，用來刻畫“能行可計(jì)算”。哥德爾提出“一般遞歸函數(shù)”作為對(duì)“能行可計(jì)算”的定義。圖靈則通過對(duì)一種裝置的描述，定義”能行可計(jì)算”的概念，這種裝置被后人稱作“圖靈機(jī)”，這正是現(xiàn)代計(jì)算機(jī)的理論 模型，標(biāo)識(shí)現(xiàn)代計(jì)算機(jī)科學(xué)的誕生。

2．邏輯成為計(jì)算機(jī)軟硬件系統(tǒng)的理論基礎(chǔ)

布爾邏輯成為集成電路設(shè)計(jì)的一個(gè)核心理論，正如赫爾曼·戈德斯坦所說： “正是通過它［布爾邏輯］，使得電路設(shè)計(jì)從一門藝術(shù)變成一門科學(xué)”。同時(shí)，也正是由于布爾邏輯的思想融匯在開關(guān)電路的設(shè)計(jì)中，才會(huì)在集成電路領(lǐng)域形成著名的摩爾定律，才使得集成電路和技術(shù)的創(chuàng)新發(fā)展得以實(shí)現(xiàn)。一階邏輯、邏輯類型論和Lambda演算與編程語言的深度交叉，形成了程序設(shè)計(jì)理論的核心。形式語法、類型系統(tǒng)和形式語義成為一門程序設(shè)計(jì)語言的基礎(chǔ)。邏輯的證明論模型論思 想與計(jì)算機(jī)軟硬件系統(tǒng)的互動(dòng)，構(gòu)成了計(jì)算機(jī)系統(tǒng) 正確性驗(yàn)證理論。人類基于霍爾邏輯、分離邏輯、Isabelle、Coq