1樓：
憑藉我原始的樸素的對lambda驗算的認知來講
我認為兩個化簡（Partial evaluation）後的lambda表示式能夠比較結構（AST）是否等同
但不能證明兩個結構不一致的lambda表示式的行為是否一致
2樓：hhhhhhhhh
其實除了 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 稍微麻煩了一點。。。
3樓：Belleve
任意兩個表示式（「程式」）的外延相等性是不可判定的。
證明如下：
考慮函式 f(n)，構造：
f' = lambda(n). begin f(n); return 1; end
g(x) = lambda(n). if(x == n) then return 1; else return f'(n)
這兩個函式對任意 x ≠ n 必等價，但是對 x = n 的情況，g 永遠是返回的，f' 則未必，那麼如果「判定兩個函式外延等價」的函式 EQUIV 存在，我們就能解出停機問題：
HALT(f
,x)=
letf1
=lambda(n
).beginf(
n);return1;
endg
=lambda(n
).if(x
==n)then
return1;
else
returnf1(
n)inEQUIV(f1
,g)顯然和停機問題不可判定矛盾。
然而對表示式加以限制之後，等價性就可判定了，如 STLC 的 beta-eta 等價性就是可判定的。
Java 8的新特性lambda表示式是否比匿名內部類具有更好的可讀性？
ylxfc 可讀性上，撒加已經說得很明白了，這裡補充下lambda跟匿名內部類的區別 對於大多數剛剛接觸jdk8的同學來說，應該都會認為lambda表示式其實就是匿名內部類的語法糖 包括我自己，在剛剛接觸的時候，也是這樣認為的 但實際上二者還是存在不少差異，其中最主要的兩點就是標識性和作用域。首先，...
如何比較兩個 LaTeX 表示的數學表示式在語義上等價？
藥罐子千里冰封 假設你沒有使用一些自然語言特性，而是使用類似型別論的那種所有符號都有計算的定義的基本元素寫出來的。然後這不是個 TeX 問題，而是符號計算的問題。如果你的表示式裡用到的運算組合出來是 Strongly normalize 的，那麼你只需要 normalize 你的表示式然後判斷 sy...
如何定義乙個可以接受lambda表示式作為引數的函式？
狐狸 include template struct isFunctor std false type template struct isFunctor std true type template struct isLambda isFunctor struct FakeLambda void ...