【逻辑与计算理论】组合子逻辑与 Y 组合子
為什么是Y?
在前面的幾個帖子里,我已經建立了如何把lambda演算變成一個有用的系統的點點滴滴。 我們已經有了數字,布爾值和選擇運算符。我們唯一欠缺的是重復。
這個有點棘手。lambda演算使用遞歸實現循環(遞歸的解釋可以看這里)。 但是,由于在lambda演算里函數沒有名字,我們得采取一些非常手段。這就是所謂的Y組合子,又名lambda不動點運算符。
讓我們先來看看lambda演算之外的一個簡單的遞歸函數。階乘函數,這是標準的例子:
factorial(n) = 1 if n = 0 factorial(n) = n * factorial(n-1) if n > 0如果我們要用lambda演算來寫的話,我們需要幾個工具……我們需要一個測試是否為零的函數,一個乘法函數,以及一個減1的函數。
為了檢查是否為零,我們將使用一個命名函數IsZero,它有三個參數:一個數字,兩個值。如果數字為0,則返回第一個值;如果它不為0,則返回第二個值。
對于乘法——我們在制定出遞歸之前寫不出乘法。但我們可以假設目前有一個乘法函數?Mult x y。
最后,減1函數,我們用Pred x表示x的前驅——即x - 1。
所以——第一版的階乘,如果我們把遞歸調用留做空白的話,將是:
lambda n . IsZero n 1 (Mult n ( something (Pred n)))現在的問題是,我們怎么填上“something”,使其遞歸?
答案是一些所謂的組合子。一個組合子是一種特殊的高階函數,它們只引用函數應用。(一個高階函數是一個函數,它接受函數作為參數,并且返回的結果也是函數)。Y組合子非常特殊,它有近乎神奇的功能使得遞歸成為可能。它的樣子如下:
let Y = lambda y . (lambda x . y (x x)) (lambda x . y (x x))看了公式,你就就明白為什么叫它Y了,因為它的“形狀”像一個Y。為了讓這一點更清晰,有時我們把它寫成樹的形式。下面是Y組合子的樹:
?
? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ?
Y組合子的特別之處在于它應用自身來創造本身,也就是說?(Y Y) = Y (Y Y)。讓我們從(Y Y)開始看看它如何工作:
- Y Y
- 展開第一個Y:(lambda y . (lambda x . y (x x)) (lambda x . y (x x))) Y
- 現在,beta規約:(lambda x . Y (x x)) (lambda x . Y (x x))
- alpha[x/z]變換第二個lambda:(lambda x . Y (x x)) (lambda z. Y (z z))
- beta規約:Y ((lambda z. Y (z z)) (lambda z. Y (z z)))
- 展開前面的Y,并alpha[y/a][x/b]變換:(lambda a . (lambda b . a (b b)) (lambda b . a (b b))) ((lambda z . Y (z z)) ( lambda z . Y (z z)))
- beta規約:(lambda b . ((lambda z. Y (z z)) (lambda z. Y (z z))) (b b)) (lambda b . ((lambda * z. Y (z z)) (lambda z. Y (z z))) (b b))
現在,仔細看該表達式。這是(Y (Y Y))?[記得前面的(Y Y) = (lambda x . Y (x x)) (lambda x . Y (x x))吧]。所以,?Y Y = Y (Y Y),這是Y的魔力:它再造了本身。(Y Y) = Y (Y Y) = Y (Y (Y Y)),子子孫孫無窮匱也。
那么,我們如何使用這個瘋狂的玩意?
好吧,讓我們拿我們的第一次嘗試做一下修改。給它取個名字,并嘗試使用該名字重寫:
let fact = lambda n . IsZero n 1 (Mult n (fact (Pred n)))現在的問題是,“fact”不是“fact”中定義的標識符。我們如何讓“fact”引用“fact”呢?好了,我們可以做一個lambda抽象,讓“fact”函數作為參數傳過去;于是,如果我們能找到一種方法來寫“fact”,使得我們可以把它作為一個參數傳給它自己,事情就搞定了。我們稱之為metafact。
let metafact = lambda fact . (lambda n . IsZero n 1 (Mult n (fact (Pred n))))現在,如果我們可以應用metafact到本身,我們就得到了我們的階乘函數。也就是說,
fact n = (metafact metafact) n 。<= (lambda f1 . lambda t1 . t1 ? 1 : t1 * f1 (P(t1))) (lambda f2 . lambda t2 . t2 ? 1 : t2 * f2 (P(t2))) n <= (lambda t1 . t1 ? 1 : t1 * (lambda f2 . lambda t2 . t2 ? 1 : t2 * f2 (P(t2))) (P(t1))) n<= lambda n . n ? 1 : n * (lambda f2 . lambda t2 . t2 ? 1 : t2 * f2 (P(t2))) (P(n))<= lambda n . n ? 1 : n * (lambda f2 . P(n) ? 1 : P(n) * f2 (P(P(n))) ) <= lambda n . n ? 1 : n * (lambda f . (P(n) ? 1 : P(n) * f (P(P(n))) )<= lambda n . n ? 1 : n * (lambda f . f (P(n)))<= lambda f . lambda n . n ? 1 : n * f (P(n))<= f (n)這正是Y的用武之地。它讓我們可以創建一個古怪的結構,每次需要遞歸的時候都可以復制函數過來。metafact (Y metafact)將得到我們想要的。展開之,這就是:
(lambda fact . (lambda n . IsZero n 1 (Mult n (fact (Pred n))))) (Y (lambda fact . (lambda n . IsZero n 1 (Mult n (fact (Pred n))))))(Y metafact)實際上是第一個lambda中參數fact的值;當我們對它做beta規約的時候,如果n為零,那么它只是返回1,如果它不為零,那么它調用fact (Pred n)。 然后再將factbeta規約為Y metafact, 這個變換瘋狂地復制,得到輸出metafact (Y metafact) (Pred n)。
瞧,遞歸(metafact (Y metafact) = metafact (Y metafact) (Pred n))。極度扭曲的遞歸。
我第一次了解了Y組合子是在本科,1989左右,至今我仍然覺得它很神秘。我雖然也明白它是怎么來的,但我無法想象地球上怎么會有人把它給想出來!
如果你對此很長感興趣,那么我極力推薦「The Little Schemer」這本書。這是本非常棒的小書 —— 寫得象一本兒童讀物。書里要么每一頁正面是一個問題,背面就是答案,要么一頁分成兩欄,一欄問題一欄答案。書的風格輕松幽默,不僅教你Scheme編程,更教人怎么思考。
一個重要的提示:實際上有幾個不同的版本的Y組合子。也有幾種不同的lambda演算的計算方式:給定以下表達式:
(lambda x y . x * y) 3 ((lambda z . z * z) 4)我們可以按不同的順序來計算:我們可以首先對(lambda x y . x * y)做beta規約,于是有:
3 * ((lambda z . z * z) 4)或者,我們可以先beta規約((lambda z . z * z) 4):
(lambda x y . x * y) 3 (4 * 4)在這種情況下,兩種方式得到相同的結果;但事實并非總是如此。
第一種順序就是我們所說的「惰性求值」(Lazy evaluation):我們不計算函數的參數,直到我們需要使用它們。第二種叫「急切求值」(eager evaluation):我們總是在把參數傳遞給函數之前進行計算。(在實際的編程語言中,Lisp語言,Scheme,和ML使用急切求值計算lambda演算,Haskell和Miranda則使用惰性值計算lambda演算。)我上面描述的Y組合子是惰性求值。如果我們用急切求值,那么上述Y組合子是導不出來的——事實上,它會永遠地復制Y。
?
一點個人解釋
Y在定義遞歸函數中的作用
首先,在lambda演算中,函數名不是不可缺少的,沒有函數名的函數稱為「匿名函數」。lambda符號的引入就是為了去掉函數名這個冗余,使定義匿名函數成為可能。但是當需要定義的函數含有遞歸時,比如階乘factorial,也就是函數的定義部分需要引用函數自身的時候,沒有函數名意味著用lambda演算無法直接引用函數自身。怎么辦呢?
一種辦法是設計另一個函數G,它接受一個函數作為參數,返回值也是一個函數(這種參數是函數的函數稱為高階函數)。然后,我們把factorial當做參數傳給G,如果G返回的函數也是factorial的話,就圓滿了。也就是說,這個G需要滿足兩個特征:
于是,我們需要干兩件事:找到G,和找到求解G(f)=f的辦法。尋找G很簡單,既然我們想讓G(factorial)=factorial,那么把factorial定義中關于factorial的引用參數化就可以了,即:
let G = lambda f . lambda n . IsZero n 1 (Mult n ( f (Pred n)))這就是上面的metafact函數。這種構造方法可以用于構造任意遞歸函數的「G」。
然后我們需要找到求解方程G(f)=f的辦法。滿足f(x)=x的x稱為函數f的不動點,f是高階函數時也不例外。Y組合子的作用就是計算函數的不動點,它對所有的函數f都滿足f(Y(f)) = Y(f),推理如下:
Y (f) = (lambda y . (lambda x . y (x x)) (lambda x . y (x x))) f= (lambda x . f (x x)) (lambda x . f (x x)) = (lambda x . f (x x)) (lambda a . f (a a))= f ((lambda a . f (a a)) (lambda a . f (a a)))= f ((lambda x . f (x x)) (lambda x . f (x x)))= f (Y(f))于是,factorial的定義就可以寫成:
factorial n = (Y metafact) n = {[lambda y . (lambda t . y (t t)) (lambda t . y (t t))][lambda f . lambda n . IsZero n 1 (Mult n ( f (Pred n)))]} n這下不用引用自身了。
Y怎么來的
現在回到第一版的階乘。我們雖然不能直接引用自身,但可以把它作為參數傳進來,也就是說:
let fact2 = lambda f. lambda n . IsZero n 1 (Mult n ( f (Pred n)))這樣,在計算5的階乘時,我們只需要計算fact2(fact2, 5)就可以了。定義并沒有引用自身,只是在使用的時候把自己當參數傳過去。是不是很簡單?
但是,這個計算式是錯誤的:fact2的定義要求它接受兩個參數,其中參數f是只接受一個參數的函數,于是計算式中第二個的fact2在參數數量上是無法和定義中的f匹配的。那怎么辦?
不要緊,我們可以修改一下f的形式,讓它接受兩個參數。即:
let fact3 = lambda f. lambda n . IsZero n 1 (Mult n ( f [f, (Pred n)]))這下計算fact3(fact3, 5)就不會出錯了。除了這個定義有點丑……
如果對fact3做下化簡又如何呢?首先是對擁有兩個參數的f進行柯里化變換:
let fact3 = lambda h . lambda n . IsZero n 1 (Mult n ( h h (Pred n))) = lambda h . lambda n . IsZero n 1 (Mult n ( (h h) (Pred n)))這樣計算階乘的方式也相應變成了(fact3 fact3) 5。接著把(h h)用函數q代替,則有
let fact3 = lambda h . lambda n . [lambda q . IsZero n 1 (Mult n ( q (Pred n)))] (h h)= lambda h . [lambda n . lambda q . IsZero n 1 (Mult n ( q (Pred n)))] (h h)仔細觀察中括號部分,參數h對于這部分是完全自由的,于是我們可以用另一個函數定義替換之:
let f0 = lambda n . lambda q . IsZero n 1 (Mult n ( q (Pred n))) let fact3 = lambda h . f0 (h h)是不是覺得f0眼熟?沒錯,這就是metafact!不過我們先把f0放一邊,看看如何使用這個定義計算n的階乘。
factorail n = (fact3 fact3) n = (lambda h . f0 (h h)) (lambda h . f0 (h h)) n把上面的式子寫成?function_name x的形式:
factorial n = {[lambda f . (lambda h . f (h h)) (lambda h . f (h h))] f0} n注意大括號中的部分,是不是更眼熟了?這就是Y的定義。真是怎么繞都擾不過去的Y啊……
factorial n = {[lambda f . (lambda h . f (h h)) (lambda h . f (h h))] f0} n= {Y f0} n= (Y metafact) n?
從Lambda演算到組合子演算
在昨天介紹了Lambda演算中的Y組合子(Y Combinator)之后,我認為展示一些你可以用組合子做的有趣的和有用的東西會比較有意思。
讓我們來看看三個簡單的組合子:
- S:S是一個函數應用組合子:?S = lambda x y z . (x z (y z))
- K:K生成一個返回特定常數值的函數:?K = lambda x . (lambda y . x)。 (即扔掉第二個參數,返回第一個參數)
- I:恒等函數:?I = lambda x . x
乍一看,這是一個很奇怪的組合。S的應用機制尤為奇怪 —— 它并不是接受兩個參數x和y,并應用x到y,它除了x和y外還用到了第三個值z,先將x應用到z上,再將y應用到z上,最后用前者的結果應用到了后者的結果上。
這是有道理的。以下各行各做了一步規約:
S K K x = (K x) (K x) = x噗! 我們根本用不著I。我們僅用S和K就創建了I的等價。但是,這僅僅是個開始:事實上,我們可以只用S和K組合子,甚至一個變量都不用,創建任意lambda演算表達式的等價。
例如,Y組合子可以寫成:
Y = S S K (S (K (S S (S (S S K)))) K)在我們繼續深入之前,有一個重要的事情要指出。我在上面說的是,使用S K K,我們創建了I的等價,然而它并沒有規約為lambda x . x。
到目前為止,我們說在Lambda演算中,“x = y”,當且僅當x和y相同,或通過Alpha轉化后相同。(這樣lambda x y . x + y等于lambda a b . a + b?,但不等于lambda x y . y + x?)這就是所謂的內涵等價(intensional equivalence) 。 然而,另一種相等也非常有用,這就是所謂的外延等價(extensional equivalence)或外延相等(extensional equality)。外延相等時,表達式X等于一個表達式Y,當且僅當X等同Y(模Alpha),或者?for all a . X a = Y a。
從現在起,我們使用「=」表示外延相等。我們可以將任何 Lambda表達式轉換為外延相等的組合子形式。我們定義一個從Lambda 形式到組合子形式的變換函數C:
讓我們演進一下?C{lambda x y . y x}?:
- 柯里化函數:?C{lambda x . (lambda y . y x)}
- 根據規則6:?C{lambda x . C{lambda y . y x}}
- 根據規則5:?C{lambda x . S C{lambda y . y} C{lambda y . x}}
- 根據規則4:?C{lambda x . S I C{lambda y . x}}
- 根據規則3:?C{lambda x . S I (K C{x})}
- 通過規則1:?C{lambda x . S I (K x)}
- 根據規則5:?S C{lambda x . S I} C{lambda x . (K x)}
- 根據規則3:?S (K (S I)) C{lambda x . K x}
- 根據規則5:?S (K (S I)) (S C{lambda x . K} C{lambda x . x})
- 通過規則1:?S (K (S I)) (S C{lambda x . K} I)
- 根據規則3:?S (K (S I)) (S (K K) I)
現在,讓我們嘗試使用“x”和“y”作為參數傳遞給該組合子表達式,并規約:
- S (K (S I)) (S (K K) I) x y
- 讓我們創建一些別名,以方便閱讀:A = (K (S I)), B = (S (K K) I),所以我們的表達式現在成了:S A B x y
- 展開S:?(A x (B x)) y
- 讓我們去掉別名B:(A x ((S (K K) I) x)) y
- 現在讓我們去掉S:(A x ((K K) x (I x))) y
- 以及I:(A x ((K K) x x)) y
- 規約(K K) x?:(A x (K x)) y
- 展開別名A:?((K (S I)) x (K x)) y
- 規約(K (S I)) x?,得到:?((S I) (K x)) y
- 規約S:I y (K x) y
- 規約I:y (K x) y
- 最后規約(K x) y,剩下:y x
就是這樣。好玩吧?
總結
以上是生活随笔為你收集整理的【逻辑与计算理论】组合子逻辑与 Y 组合子的全部內容,希望文章能夠幫你解決所遇到的問題。
- 上一篇: 【Python】IDLE工具
- 下一篇: 【算法分析与设计】辗转相除法