Учитывая два лямбда-члена, скажем, они равны, если их (возможно, бесконечные) деревья Бома равны. Согласно этому определению, например, (Y λr.λt.(t r)) и (Y λr.λt.t (λt. t r) равны, несмотря на то, что они не имеют нормальной формы, потому что оба члена имеют одинаковые бесконечные деревья Бома. Поскольку это сводится к проблеме остановки, лучшее, что мы можем иметь, - это вероятностная функция. Мой вопрос: существует ли эффективный, предпочтительно простой алгоритм, способный определить, равны ли два λ-члена для некоторого большого класса общих терминов?