比較兩個lambda表達式是否等價的lambda表達式怎麼寫？

---

任意兩個表達式（「程序」）的外延相等性是不可判定的。

證明如下：

考慮函數 f(n)，構造：

1. f" = lambda(n). begin f(n); return 1; end
2. g(x) = lambda(n). if(x == n) then return 1; else return f"(n)

這兩個函數對任意 x ≠ n 必等價，但是對 x = n 的情況，g 永遠是返回的，f" 則未必，那麼如果「判定兩個函數外延等價」的函數 EQUIV 存在，我們就能解出停機問題：

HALT(f, x) = let
f1 = lambda(n). begin f(n); return 1; end
g = lambda(n). if(x == n) then return 1; else return f1(n)
in EQUIV(f1, g)


顯然和停機問題不可判定矛盾。

然而對表達式加以限制之後，等價性就可判定了，如 STLC 的 beta-eta 等價性就是可判定的。

---

有人看不懂，所以我來翻譯一下 @Belleve 的答案。

停機問題是：

考慮一個牛逼的函數 can( )

const test = ( someFunction ) =&> can( someFunction ).stop ? 1 : 0 ;

const strangeFunction = ( testFunction ) =&> ( someFunction ) =&> while( testFunction( someFunction ) ){} ;


strangeFunction 是個高階函數，以 thunk 形式接受判斷函數會不會停的函數 test 和它自己：

strangeFunction( test )( strangeFunction ) ;

現在如果 strangeFunction 會停，它就不停，反之亦然，所以矛盾， test 函數里的那個 can() 我們是寫不出來的。

現在考慮一個牛逼的函數 EQUIV ，還有一個可能會死循環的函數 f ，f 會出現在 f" 里，像這樣 ：

const f" = ( n ) =&> { f( n ) ; return 1 };
const g = ( x ) =&> ( n ) =&> x==n ? 1 : f"( n ) ;


也就是說，如果你給高階函數 g 傳入的第一個參數 x 和 n 不一樣，那麼 g 會返回一個與 f" 無異的函數。但是對 x == n 的情況，g 永遠是返回 1 的，f" 在 f( n ) 死循環的情況下不返回。

我們的主要目的是用牛逼的函數 EQUIV 來干如下勾當：

const can = ( someFunction ) =&> {
const f" = ( n ) =&> { someFunction( n ) ; return 1 };
const g = ( x ) =&> ( n ) =&> x==n ? 1 : f"( n ) ;
return {stop: EQUIV( f", g ) };
}


EQUIV 會深度判斷傳入的兩個函數，如果相等就說明 someFunction 是可以停的，不相等就說明 someFunction 包含死循環。

然後最後的用法就是像上頭那樣：

const test = ( someFunction ) =&> can( someFunction ).stop ? 1 : 0 ;


是個人都知道這會導致矛盾，所以 EQUIV 不存在。

---

這個函數被證明不存在

---

其實除了 reduce 成 HALTtm，reduce 成 EMPTYtm 會好做很多。

construct EMPTYtm(M，where M accepts no string):

construct M": On input x, reject.

obviously M" accepts no string.

return EQUV(M", M)

一下就好懂了很多呢。。。不過證明 EMPTYtm 是 undecidable 比 HALTtm 稍微麻煩了一點。。。

---

推薦閱讀：