第五百六十三章 丘奇的λ演算（計(jì)算）

　　一階邏輯是一種不能量化的簡(jiǎn)單的屬性邏輯。與高階邏輯和數(shù)理邏輯不一樣。它不允許量化性質(zhì)。性質(zhì)是一個(gè)物體的特性；所以一個(gè)紅色物體被表述為有紅色的特性。

　　里面有很多“任意有”和“必須存在”這樣的符號(hào)。

　　我們可以大膽地設(shè)想，把整個(gè)數(shù)學(xué)理論內(nèi)容用一階邏輯表達(dá)式全部寫出來，成果就像是一本”天書“，一般人很難看得懂。但是，布爾巴基學(xué)派偏要這樣做，否則，似乎不夠”意思“，不過”癮“。因此，我們能夠想像，在布爾巴基的《數(shù)學(xué)基礎(chǔ)叢書》里面各種稀奇古怪的數(shù)學(xué)謂詞多得去了。對(duì)此，有人說，這純粹是形式主義，但是，也有人說，這就是現(xiàn)代數(shù)學(xué)的本來面目。

　　1935年，邱奇發(fā)明了“λ演算”，來源證明一階邏輯沒有通用判定而發(fā)明的，但對(duì)于今天的計(jì)算機(jī)科學(xué)家是一件無價(jià)的工具。

　　在函數(shù)式語言中，函數(shù)的排列更像是個(gè)鏈條，而不是我們說些的那些方程式。意思是后一個(gè)函數(shù)可以從前一個(gè)函數(shù)得出。

　　寫出一個(gè)函數(shù)后，也要寫出要帶入的變量的值，這樣在計(jì)算過程中就可以讓變量值和帶入值進(jìn)行交換就可以了。丘奇發(fā)明這種演算后，他的學(xué)生們完善了這種工具。

　　同年邱奇出版了《初等數(shù)論中的一個(gè)未解決問題》。其中包含了邱奇定理，它表明算術(shù)沒有判定程序。在理論計(jì)算機(jī)科學(xué)中，有了可計(jì)算性概念復(fù)嚴(yán)格的數(shù)學(xué)刻劃，才使證明一系列重要的數(shù)學(xué)問題的算法不可解性成為可能。

　　遞歸函數(shù)是一個(gè)自己調(diào)用自己的函數(shù)。

　　“算法可計(jì)算函數(shù)都是遞歸函數(shù)”這一丘奇論題提出，算法可計(jì)算性這個(gè)直觀概念才有了精確的數(shù)學(xué)刻劃。

　　丘奇雖然不是搞計(jì)算機(jī)的，但是他的這些工具都服務(wù)于計(jì)算機(jī)了，圖靈證明自己的圖靈機(jī)器里很多東西跟丘奇的演算理論等價(jià)。