给定两个lambda项,假设它们是相等的,如果它们(可能是无限的)Bohm树是。例如,在这个定义下, (Y λr.λt.(t r)) 和 (Y λr.λt.t (λt. t r) 是相等的,尽管没有正规形式,因为这两个项有相同的无限玻姆树。由于这归结为停顿问题,我们能得到的最好的就是一个概率函数。我的问题是:是否有任何有效的,最好是简单的算法,能够确定两项是否相等的一些大类的共同项?
(Y λr.λt.(t r))
(Y λr.λt.t (λt. t r)
