λ 運算︰淵源介紹

美國數學家阿隆佐‧邱奇 Alonzo Church 對『符號邏輯』symbolic logic 的熱情與對基礎算術『形式系統』的研究持續一生。當他發現這類系統容易受到『羅素悖論』影響時，轉將所設想的『λ 運算』lambda calculus 單獨用於研究『可計算性』問題，同樣否定的回答了『判定性問題』 Decision-problem ──

一九零零年德國大數學家大衛‧希爾伯特 David Hilbert 在巴黎的國際數學家大會上作了場名為《數學問題》的演講，提出了二十三道待解決之最重要的數學問題，這就是著名的希爾伯特之二十三個問題的由來。這裡的『判定性問題』就是二十三個問題的第二題『算術公理之相容性』，一九三零年已為庫爾特‧哥德爾所否證 ──。美國 UCLA 大學 Enderton, Herbert B. 教授寫了一篇名為
《INTRODUCTION
Alonzo Church: Life and Work》的 Alonzo Church 小傳︰
…
In 1936 a pair of papers by Church changed the course of logic. An Unsolvable Problem of Elementary Number Theory presents a definition and a theorem:
“The purpose of the present paper is to propose a definition of effective calculability which is thought to correspond satisfactorily to the somewhat vague intuitive notion . . . , and to show, by means of an example, that not every problem of this class is solvable.” The “definition” now goes by the name Church’s Thesis: “We now define the notion . . . of an effectively calculable function of positive integers by identifying it with the notion of a recursive function of positive integers (or of a λ-definable function of positive integers).” (The name, “Church’s Thesis,” was introduced by Kleene.)
The theorem in the paper is that there is a set that can be defined in the language of elementary number theory (viz. the set of G ̈odel numbers of formulas of the λ-calculus having a normal form) that is not recursive—although it is recursively enumerable. Thus truth in elementary number theory is an effectively unsolvable problem.

A sentence at the end of the paper adds the consequence that if the system of Principia Mathematica is ω-consistent, then its decision problem is unsolvable. It also follows that the system (if ω-consistent) is incomplete, but of course G ̈odel had shown that in 1931.
…

λ演算是一套用來研究『函式』Function 的『抽象』Abstraction 、函式的『應用』Apply 、『變元』Variable 的『替換』Substitution 以及『函式』之『化約』reduction 的形式語言。λ演算對於泛函式程式語言的興起有著巨大的推動力，比方說人工智慧領域著名的 Lisp 語言，以及後來的 ML 語言和 Haskell 語言。更令人驚訝的是它自身就是一個『世界上最小的通用性程式語言』。由於『函式』與『變元』兩者是任何人不管想用哪種『□□程式語言』來寫『演算法』Algorithm 都需要清楚理解的概念。就讓我們踏上前人走過的足跡，回顧旅途上周遭景緻，說不定會有意外的收穫！！

首先請讀者參考在《Thue 之改寫系統《一》》一文中的『符號定義』，於此我們引用該文中談到數學裡『函數定義』的一小段︰

如此當數學家說『函數』 $f$ 的定義時︰

假使有兩個集合 $S$ 和 $T$ ，將之稱作『定義域』domain 與『對應域』codomain，函數 $f$ 是 $S \times T$ 的子集，並且滿足

$\forall x \ x \in S \ \exists ! \ y \ y \in T \ \wedge \ (x,y) \in f$

，記作 $x \mapsto y = f (x)$ ，『 $\exists \ !$ 』是指『恰有一個』，就一點都不奇怪了吧。同樣『二元運算』假使『簡記』成 $X \times Y \mapsto_{\bigoplus} \ Z$ ， $X=Y=Z=S$ ，是講︰

$z = \bigoplus ( x, y) = x \bigoplus y$ ，也是很清晰明白的呀！！

如果仔細考察 $y = f(x)$ ── 比方說 $y = x^2$ ──，那麼『函數 $f$ 』是什麼呢？『變數 $x, y$ 』又是什麼呢？如果從函數定義可以知道『變數』並不是什麼『會變的數』，而是規定在『定義域』或者『對應域』中的『某數』的概念，也就是講在該定義的『集合元素中』談到『每一個』、『有一個』和『恰有一個』…的那樣之『指稱』觀念。這能有什麼困難的嗎？假使設想另一個函數 $z = w^2$ ，它的定義域與對應域都和函數 $y = x^2$ 一樣，那麼這兩個函數是一樣還是不一樣的呢？如果說它們是相同的函數，那麼這個所說的『函數』就該是『 $\Box^2$ 』，其中 $y, z$ 『變數』只是『命名的』── 函數的輸出之數 ──，而且 $w, x$ 『變數』是『虛名的』── 函數的輸入之數 ──。如果從函數 $f$ 將『輸入的數』轉換成『輸出的數』的觀點來看，這個『輸入與輸出』本就是 $f$ 所『固有的』，所以和『輸入與輸出』到底是怎麼『命名』無關的啊！更何況『定義域或對應域』任一也都不必是『數的集合』，這時所講的『函數』或許稱作『函式』比較好，『變數』或該叫做『變元』。其次假使將多個函數『合成』composition，好比『輸出入』的串接，舉例來講，一般數學上表達成 $g(f(x)) = x^2 + 1$ ，此時假使不補足， $g(x) = x + 1$ 和 $f(x) = x^2$ ，怕是不能知道這個函數的『結構』是什麼的吧？進一步講『函數』難道不能看成『計算操作子』operator 的概念，定義著什麼是 $f + g$ 、 $f - g$ 、 $f * g$ 或 $f / g$ 的嗎？就像將之這樣定義成︰
$(f \otimes g) (x) \ =_{df} \ f(x) \otimes g(x)$

，而將函數合成這麼定義為︰
$(f (g) ) (x) \ =_{df} \ f(g(x))$

。如此將使『函數』或者『二元運算』的定義域或對應域可以含括『函數』的物項，所以說它是『泛函式』functional 的了。

再者將函式的定義域由一數一物推廣到『有序元組』turple 也是很自然的事，就像講房間裡的『溫度函數』是 $T (x, y, z)$ 一樣，然而這也產生了另一種表達的問題。假想 $f(x) = x^2 - y^2$ 、 $g(y) = x^2 - y^2$ 和 $h(x, y) = x^2 - y^2$ ，這 $f, g$ 兩個函數都是 $h$ 函數的『部份』partial 函數，構成了兩個不同的『函數族』。於是在一個運算過程中，這個表達式『 $x^2 - y^2$ 』究竟是指什麼？是指『 $f$ 』還是指『 $g$ 』呢？也許說不定是指『 $h$ 』的呢？難道說『兩平方數之差』本身就沒有意義的嗎？？因是之故，邱奇所發展的『λ 記號法』是想要『清晰明白』的『表述』一個『表達式』所說之內容到底是指的什麼。如果使用這個記號法， $f, g, h$ 記作︰