-
Notifications
You must be signed in to change notification settings - Fork 68
04 數字系統
在 Lambda Calculus 中,數字和算術操作可以使用純函數來表示和實現。這些數字被稱為 Church 數字 (Church Numerals),以 Alonzo Church 命名。Church 數字的核心思想是將一個自然數表示為一個函數,該函數對參數應用一定次數的操作。
本章將介紹如何用 Lambda Calculus 表示數字及其算術操作,並使用 Python 模擬這些功能。
在 Church 數字中,自然數 ( n ) 被表示為一個高階函數:
- ( 0 ): ( \lambda f. \lambda x. x ) (對 ( f ) 應用 0 次)
- ( 1 ): ( \lambda f. \lambda x. f(x) ) (對 ( f ) 應用 1 次)
- ( 2 ): ( \lambda f. \lambda x. f(f(x)) ) (對 ( f ) 應用 2 次)
# Church 數字的定義
IDENTITY = lambda x: x
_zero = lambda f: IDENTITY # 0: 不應用函數 f
_one = lambda f: lambda x: f(x) # 1: 應用函數 f 一次
_two = lambda f: lambda x: f(f(x)) # 2: 應用函數 f 兩次
_three = lambda f: lambda x: f(f(f(x))) # 3: 應用函數 f 三次
# 測試 Church 數字
assert _zero(lambda x: x + 1)(0) == 0 # 0 不改變初始值
assert _one(lambda x: x + 1)(0) == 1 # 1 增加一次
assert _two(lambda x: x + 1)(0) == 2 # 2 增加兩次
assert _three(lambda x: x + 1)(0) == 3 # 3 增加三次
繼任者函數 (Successor) 是算術中最基本的操作,它定義為將一個自然數 ( n ) 映射到 ( n+1 )。在 Lambda Calculus 中,繼任者函數的定義如下:
[ \text{Successor}(n) = \lambda f. \lambda x. f(n(f)(x)) ]
用 Python 表示:
SUCCESSOR = lambda n: lambda f: lambda x: f(n(f)(x))
測試:
# 測試繼任者函數
assert _one(lambda x: x + 1)(0) == 1
assert SUCCESSOR(_one)(lambda x: x + 1)(0) == 2 # _one 的繼任者應為 _two
assert SUCCESSOR(_two)(lambda x: x + 1)(0) == 3 # _two 的繼任者應為 _three
加法操作可以通過將一個數字的應用次數加到另一個數字上來實現,其 Lambda Calculus 定義如下:
[ \text{Addition}(m, n) = \lambda f. \lambda x. m(f)(n(f)(x)) ]
用 Python 表示:
ADDITION = lambda m: lambda n: lambda f: lambda x: m(f)(n(f)(x))
測試:
# 測試加法
assert ADDITION(_one)(_two)(lambda x: x + 1)(0) == 3 # 1 + 2 = 3
assert ADDITION(_three)(_two)(lambda x: x + 1)(0) == 5 # 3 + 2 = 5
減法是更複雜的操作,需要用到 前任者函數 (Predecessor)。前任者的實現基於一個內部的函數構造。
[ \text{Predecessor}(n) = \lambda f. \lambda x. n(\lambda g. \lambda h. h(g(f)))(\lambda u. x)(\lambda u. u) ]
Python 實現:
PREDECESSOR = lambda n: lambda f: lambda x: n(
lambda g: lambda h: h(g(f))
)(lambda _: x)(lambda u: u)
減法則可以通過將一個數字減去另一個數字的應用次數來完成: [ \text{Subtraction}(m, n) = n(\text{Predecessor})(m) ]
Python 實現:
SUBTRACTION = lambda m: lambda n: n(PREDECESSOR)(m)
測試:
# 測試減法
assert SUBTRACTION(_three)(_one)(lambda x: x + 1)(0) == 2 # 3 - 1 = 2
assert SUBTRACTION(_three)(_three)(lambda x: x + 1)(0) == 0 # 3 - 3 = 0
乘法可以定義為將一個數字對函數的應用次數乘以另一個數字的應用次數: [ \text{Multiplication}(m, n) = \lambda f. m(n(f)) ]
Python 實現:
MULTIPLICATION = lambda m: lambda n: lambda f: m(n(f))
測試:
# 測試乘法
assert MULTIPLICATION(_two)(_three)(lambda x: x + 1)(0) == 6 # 2 * 3 = 6
assert MULTIPLICATION(_four)(_two)(lambda x: x + 1)(0) == 8 # 4 * 2 = 8
次方操作定義為將一個數字作為函數應用到另一個數字次: [ \text{Power}(x, y) = y(x) ]
Python 實現:
POWER = lambda x: lambda y: y(x)
測試:
# 測試次方
assert POWER(_two)(_three)(lambda x: x + 1)(0) == 8 # 2^3 = 8
assert POWER(_three)(_two)(lambda x: x + 1)(0) == 9 # 3^2 = 9
絕對差是兩個數字的距離,定義為兩個數字之間的差值的絕對值: [ \text{AbsDifference}(x, y) = \text{Addition}(\text{Subtraction}(x, y))(\text{Subtraction}(y, x)) ]
Python 實現:
ABS_DIFFERENCE = lambda x: lambda y: ADDITION(SUBTRACTION(x)(y))(SUBTRACTION(y)(x))
測試:
# 測試絕對差
assert ABS_DIFFERENCE(_three)(_two)(lambda x: x + 1)(0) == 1 # |3 - 2| = 1
assert ABS_DIFFERENCE(_two)(_three)(lambda x: x + 1)(0) == 1 # |2 - 3| = 1
本章介紹了 Church 數字的基本定義及其在 Lambda Calculus 中的算術操作,並用 Python 模擬了這些操作。這些操作包括:
- 繼任者
- 加法
- 減法
- 乘法
- 次方
- 絕對差
這些基於純函數的定義展示了 Lambda Calculus 強大的抽象能力,並為後續的更高階應用(如比較運算和數列生成)奠定了基礎。
從希爾伯特到圖靈的那些故事
-- 以 Python 展現這些故事背後的程式