智慧應用 影音
Reserch
DWebinar_20210929

「教堂」的蘭達

林一平手繪之邱奇(Alonzo Church)。林一平提供

我實作物聯網平台IoTtalk,設計一個機制,很適合執行蘭達函式(λ-function)。對於「蘭達」,我一直情有獨鍾。

在1986年9月,我在西雅圖的華盛頓大學接觸到第一堂計算機理論課。授課教授Paul Yang一直提到「教堂的蘭達、圖靈的機」,彷彿是江湖黑話,幫派切口。左顧右盼,四周的白人同學聽得津津有味,談笑有鴻儒,頻頻點頭,我則是一頭霧水,猶如雞立鶴群之白丁,也不敢發問,怕鬧笑話。

下課後衝到圖書館翻書,想搞懂啥是教堂的蘭達。最後搞懂,教堂 (Church)是人名,翻譯為「邱奇」。邱奇(Alonzo Church)是數學家,也是圖靈(Alan Mathison Turing)的指導教授。1930年,邱奇以數學邏輯為基礎,提出蘭達演算法(λ-calculus),以變數綁定和替換的規則,發展出基於函式(function)以及遞迴機制的形式系統。λ-calculus是一個通用的計算模型,強調函式變換規則的運用,而非實現它們的具體機器。

邱奇的學生圖靈也發表了一個簡單形式的抽象裝置,後人稱為「圖靈機」 (Turing Machine),是能力和蘭達演算法能力相同的計算模型。圖靈機的執行龜速,沒有實際用途,但引導後人想像,這種機器能解決運算問題。

圖靈嚴謹的證明出,我們不可能用一個演算法來決定一部指定的圖靈機是否會停機。邱奇在λ-calculus方面相等的證明比圖靈的發表早了幾個月(老師還是比較厲害)。不過圖靈的做法比邱奇直觀,更易於理解。

當年被認為不直觀的λ-calculus衍生出λ-function,反而實際應用於現代程式語言如Java、C#及Python。原因是λ-calculus清晰地定義何謂「可計算函式」。任何可計算函式都能以λ-function表達並據以求值,相當於單一磁帶圖靈機的計算過程。λ-function是匿名函式,不需要定義名稱,只有一行運算式,語法非常簡潔,功能強大,適用於小型的運算。

我設計的IoTtalk物聯網平台以Python實作,並以圖形化使用者介面將物聯網設備(感測器與制動器)以圖符(icon)形式呈現。IoT圖符間可連線,我在連線間畫了一個小圈圈。當初設計這個小圈圈,是一個產生λ-function的機制,藉此寫出優雅的函式。只可惜部分IoTtalk使用者不曉得我的苦心,老是寫馮紐曼(von Neumann)架構的駑鈍函式,我的俏媚眼做給瞎子看,只能徒呼負負。

現為交通大學資工系終身講座教授暨華邦電子講座,曾任科技部次長,為ACM Fellow、IEEE Fellow、AAAS Fellow及IET Fellow。研究興趣為物聯網、行動計算及系統模擬,發展出一套物聯網系統IoTtalk,廣泛應用於智慧農業、智慧教育、智慧校園等領域/場域。興趣多元,喜好藝術、繪畫、寫作,遨遊於科技與人文間自得其樂,著有<閃文集>、<大橋驟雨>。