天天看點
傳回

計算的表示僞哲學家λ 演算自然數的表示邏輯的表示序對的表示進一步思考參考資料

僞哲學家

當提到「計算」這個詞的時候，我們會想到什麼，是想到「計算機」，或是「圖靈機」，又或是操控計算機的「彙編語言」，還是說「1 + 1」這樣的算式？這些都是計算，但它們都是計算的一種表示而非計算本身，計算本身是一個更加本質的東西，可以認為是一種柏拉圖型相，或是理念，剛剛說到的東西都是對它的摹仿。

比如我們說到「4」的時候，我們在用「4」這個符号去摹仿「4」這個理念，這個理念可以用「4」來摹仿，也可以用「四」，也可以用「four」，具體是什麼不重要，重要的是你不會走在路上突然見到一個「4」，而是會見到一個類似「4」的東西。那既然可以用這樣一個來自阿拉伯的符号來摹仿數字，那是否有其他的方式來摹仿呢？更一般地說，是否有其他的計算表示方式，并以此來實作我們在彙編語言，C，Java，等語言中表示的計算呢？下面将介紹一個圖靈完備的計算模型，稱為 λ 演算（lambda calculus）1，該計算的表示由 Alonzo Church 在 20 世紀 30 年代發明，它可被稱為是最小的通用程式設計語言。

λ 演算

λ 演算非常簡練，而且相對于圖靈機的計算模型來說非常優雅，其核心在于表達式（expression）。一個名字（name）又被稱為變量（variable），是一個辨別符（identifier），可以是任意的字母，如：a, b, c 等。而表達式的定義如下：

\[\begin{array}{rcl} \text{<expression>} & := & \text{<name> | <function> | <application>} \\ \text{<function>} & := & \lambda~\text{<name>.<expression>} \\ \text{<application>} & := & \text{<expression><expression>} \\ \end{array}\]

至于變換規則則總共有三條，更加具體的描述可參考維基百科 2：

α - conversion: 改變綁定變量的名稱不影響函數本身；

β - reduction: 将函數應用于其參數；

η - conversion: 兩個函數對于所有的參數得到的結果都一緻，當且僅當它們是同一個函數。

本文後面的部分均使用 Scheme 語言來描述這些計算，在 Scheme 中，有非常類似 λ 演算中表達式的表示，例如一個函數 \lambda x.y 将在 Scheme 中表示為 (lambda (x) y)，而将函數應用于參數 x~y 将在 Scheme 中表示為 (x y)。最大的差別可能在于，在 λ 演算中，(x) 和 x 一樣，而在 Scheme 中，前者會變成一個對函數 x 的調用，而後面則是 x 本身。

自然數的表示

在考慮如何表示數之前，先思考一下數是什麼，前面已經說了，數是一種理念，我們在去摹仿這個理念的時候，一般是做兩件事，一是定義一些基本運算，将數進行組合擷取新的數，比如四則運算；二是通過和上下文結合，用來表達某個意思，比如三個蘋果，走了一步等。這樣看來，隻要能抽象出這兩點，具體用什麼來表示似乎就不重要了，其中一個方式就是邱奇數 3。

在這種表示法下，數字被表現為一個函數應用于一個值多少次。也就是說，所謂的「0」，就是一個函數應用一個值 0 次，即

x

，「1」是應用 1 次，即

(f x)

，「2」則是先應用 1 次，再對作用後的傳回值再應用 1 次，即

(f (f x))

，以此類推。首先，要先有一個初始，也就是所謂的「0」，用 Scheme 表示如下：

(define ZERO
  (lambda (f)
    (lambda (x) x)))

複制

注意，這裡的

(define ZERO ...)

隻是給了後面的表達式一個名字，而非像 C 語言一樣聲明一個變量，這個過程完全是引用透明的，也就是此後任何出現

ZERO

的地方都可以用這裡定義的部分直接代換。下面是函數

succ

的定義，作用是求一個邱奇數的後繼（successor），即所謂的給一個數加「1」。

(define succ
  (lambda (n)
    (lambda (f)
      (lambda (x) (f ((n f) x))))))

複制

此時，我們已經可以用這個方式表示所有的自然數了，舉例而言：

; (f x)
(define ONE (succ ZERO))

; (f (f x))
(define TWO (succ (succ ZERO)))

; (f (f (f x)))
(define THREE (succ TWO))

複制

前面說了，數隻有在給定的上下文中才會有其意義，否則隻是一個概念而已，這裡為了友善計算機列印，可以将其設定為對我們常用的阿拉伯數字的轉換：

(define trans
  (lambda (n)
    ((n (lambda (x) (+ x 1))) 0)))

複制

其中傳入給邱奇數

n

的函數是一個給阿拉伯數字加一的函數，之後再傳入的被作用對象是阿拉伯數字

，故結果就是該邱奇數的概念對應的阿拉伯數字。此時，在 REPL 中可以這樣進行轉換：

>>> (trans ONE)
1
>>> (trans (succ (succ ONE)))
3

複制

除了這樣依賴于上下文的意義，數字的作用還有一些預定義的運算。其中，加法的運算最為簡單直接：

(define plus
  (lambda (m)
    (lambda (n)
      (lambda (f)
        (lambda (x) ((m f) ((n f) x)))))))

複制

也就是，對于兩個邱奇數

n

，

m

而言，其求和之後的邱奇數是

l

，當給

l

一個函數

f

和一個參數

x

之後，它會先将

f

和

x

傳給

n

得出結果後再将

f

和結果傳給

m

，這樣

f

就在

x

上作用了所謂「m + n」次了。

>>> (trans ((plus ONE) TWO))
3

複制

類似地，乘法的定義也相當直覺：

(define mult
  (lambda (m)
    (lambda (n)
      (lambda (f) (m (n f))))))

複制

也就是将

f

作用

n

次這件事重複作用

m

次，這也正是乘法的意義：

>>> (trans ((mult TWO) THREE))
6

複制

如果想得到一個邱奇數的前驅（predecessor）則比之前的計算要困難多了，可以表示如下：

(define pred
  (lambda (n)
    (lambda (f)
      (lambda (x)
        (((n (lambda (g)
               (lambda (h) (h (g f))))) (lambda (u) x)) (lambda (u) u))))))

複制

則有：

>>> (trans (pred THREE))
2

複制

當然，這個

pred

的表示非常令人困惑，但可以使用代換模型直接驗證，考慮将将該函數應用于

ONE

，再将結果應用于

f

和

x

。那麼，首先肯定是不能将

ONE

直接應用于

f

了，這裡将

ONE

應用于另一個函數，這個函數是：

(lambda (g)
  (lambda (h) (h (g f))))

複制

其中的

f

是傳入的

f

，此時

ONE

會傳回另一個函數：

(lambda (y)
  ((lambda (g)
     (lambda (h) (h (g f)))) y))

複制

即：

(lambda (y)
  (lambda (h) (h (y f))))

複制

這裡為了避免和傳入的

x

沖突，将

x

替換為

y

。然後将這個結果應用于另一個函數：

(lambda (u) x)

複制

其中的

x

是傳入的

x

，結果為：

(lambda (h) ((lambda (u) x) f))

複制

即：

(lambda (h) (h x))

複制

這個結果又被應用到了另一個函數上：

((lambda (h) (h x)) (lambda (u) u))

複制

即：

x

複制

即

(pred ONE)

的定義如下：

(lambda (f)
  (lambda (x) x))

複制

也就是說

(pred ONE)

就是

ZERO

。

一但有了這些對自然數的運算，負數、浮點數都是可以定義的，畢竟我們使用的計算機也是通過一些約定的記法來表示負數和浮點數的。

邏輯的表示

上一節說明了如何用函數來表示數的概念，這一節将用函數來表示邏輯與斷言。同樣地，首先要思考的是，我們一般使用的

True

和

False

到底是用來做什麼的。事實上，邏輯不是為了判斷對錯，而是對條件分支的選擇，它說明了有兩種情況，在一種情況下選擇一種分支，在另一種情況下選擇另一分支，另外還需要在其上進行邏輯運算的算子（與或非）。注意到 C 語言其實是沒有布爾值這個類型的，但是依然不影響

if

的使用，因為 C 裡面可以用其他類型的值來進行邏輯運算，在

if

裡也可以用這些結果來進行分支的選擇。

是以，我們可以這樣來定義布爾值，下面這個定義法被稱為邱奇布爾值：

(define TRUE
  (lambda (x) (lambda (y) x)))

(define FALSE
  (lambda (x) (lambda (y) y)))

複制

也就是說，給定兩個分支，

TURE

會選擇第一個，而

FALSE

會選擇第二個。至于邏輯運算可以基于這個表示方式進行定義，比如與運算定義如下：

(define and
  (lambda (p)
    (lambda (q) ((p q) (lambda (x) (lambda (y) x)))))

複制

即：

(define and
  (lambda (p)
    (lambda (q) ((p q) FALSE)))

複制

也就是，如果

p

為真，将會由

q

來選擇分支，如果

p

為假，則由

FALSE

來選擇條件分支。至于或和非也類似定義：

(define or
  (lambda (p)
    (lambda (q) ((p TRUE) q))))

(define not
  (lambda (p) ((p FALSE) TRUE)))

複制

當然也可以轉成一個可以被列印的形式：

>>> ((((and (not FALSE)) TRUE) 'true) 'false)
true

複制

序對的表示

一個序對（pair）就是一個二進制組（2-tuple），這是一個非常簡單而且非常強大的結構構件，如果在 C 中，表示形式大概是這樣的：

struct Pair {
  void* first;
  void* second;
}

複制

這個表示方法是一個很典型的方式，它可以很顯然地看出資料是如何存放的，但事實上，為了獲得一個序對，我們根本不用關心資料是如何存放的，我們關心的是如何建構一個序對，然後如何将組成序對的元素取出來，換言之，我們希望有

(first ((pair x) y))

就是

x

，

(second ((pair x) y))

就是

y

。裡面具體是怎樣的，并不值得關心，也就是我們隻是需要一個 constructor 和兩個 selector 而已。邱奇序對編碼（Church encoding for pairs）的表示如下：

(define pair
  (lambda (x)
    (lambda (y)
      (lambda (f) ((f x) y)))))

(define first
  (lambda (p) (p (lambda (x) (lambda (y) x)))))

(define second
  (lambda (p) (p (lambda (x) (lambda (y) y)))))

複制

使用之前定義的

TRUE

和

FALSE

：

(define first (lambda (p) (p TRUE)))

(define second (lambda (p) (P FALSE)))

複制

這個表示方式非常令人驚訝，因為資料看起來像是存在于一片虛無之中，語言在執行的時候建構了 closure，但是看起來似乎就像把函數傳來傳去，資料就這樣在其中隐匿、出現。

pair

函數接收了兩個元素之後就傳回了另一個函數，這個函數接收一個選擇函數，然後

pair

就将兩個元素交由選擇函數進行選擇，而

first

和

second

則将對應的選擇函數交給這個函數，擷取到對應的資料。

有了這樣一個東西，我們隻要再有一個能夠表示 list 末尾的東西就可以建構一個 list 了。将這個東西命名為

NIL

，将判斷一個元素是否為

NIL

的函數命名為

nil?

。

NIL

具體是個什麼東西不重要，最重要的是，将

nil?

應用于一個序對将傳回

FALSE

而将

nil?

應用于

NIL

将傳回

TRUE

，可以表示如下：

(define NIL (lambda (x) TRUE))

(define nil?
  (lambda (p) (p (lambda (x)
                   (lambda (y) FALSE))))))

複制

nil?

接受一個序對或是一個

NIL

，并傳遞給他一個接受兩個參數再傳回

FALSE

的函數，如果是一個序對，那麼結果必然是

FALSE

，而如果是

NIL

，那麼這個函數則不會被調用，而是

NIL

直接傳回了

TRUE

。這樣就表示了

NIL

。那麼建構有兩個元素的 list 的方法可以表示為：

(lambda (x) (lambda (y) ((pair x) ((pair y) NIL))))

複制

這樣一個 list 的建構方式就是連結清單，通過 pair，可以建構更為複雜的資料結構。

進一步思考

在這種計算模型下除法如何實作？遞歸如何實作？這些都是更為進階的話題，在 Wikipedia 上有更詳細的說明 4 5。

計算是一個非常本質的東西，跳出固有的思維來看，能産生更多的思考。

參考資料

  1. Raul Rojas - A Tutorial Introduction to the Lambda Calculus ↩
  2. λ 演算 - 維基百科 ↩
  3. 邱奇數 - 維基百科 ↩
  4. Church encoding - Wikipedia ↩
  5. Lambda calculus - Wikipedia ↩

/* * * CONFIGURATION VARIABLES: EDIT BEFORE PASTING INTO YOUR WEBPAGE * * */ var disqus_shortname = 'ZhiruiLi'; // required: replace example with your forum shortname /* * * DON'T EDIT BELOW THIS LINE * * */ (function() { var dsq = document.createElement('script'); dsq.type = 'text/javascript'; dsq.async = true; dsq.src = 'https://' + disqus_shortname + '.disqus.com/embed.js'; (document.getElementsByTagName('head')[0] || document.getElementsByTagName('body')[0]).appendChild(dsq); })(); /* * * DON'T EDIT BELOW THIS LINE * * */ (function () { var s = document.createElement('script'); s.async = true; s.type = 'text/javascript'; s.src = 'https://' + disqus_shortname + '.disqus.com/count.js'; (document.getElementsByTagName('HEAD')[0] || document.getElementsByTagName('BODY')[0]).appendChild(s); }()); comments powered by Disqus

上一篇: 長視訊的日子，過得不如短視訊舒坦
下一篇: 深度探索C++對象模型【第三章2】