任意两个表达式(「程序」)的外延相等性是不可判定的。证明如下:考虑函数 f(n),构造:f' = lambda(n). begin f(n); return 1; endg(x) = lambda(n). if(x == n) then return 1; else return f'(n)这两个函数对任意 x ≠ n 必等价,但是对 x = n 的情况,g 永远是返回的,f' 则未必,那么如果「判定两个函数外延等价」的函数 EQUIV 存在,我们就能解出停机问题: