为什么我们在达到这个期限后停止？ Lambda微积分

Question

我正在计算lambda Term的正常形式。我也有解决方案，所以我知道我的步骤直到“结束”是正确的。 给定的期限是

(\a.\b.(\x.a b x)(\y. b y x) a) (\f. f f)g 

和该normalform是

g g (\y. g y x)(\f. f f) 

我也得到了这一点，但后来我继续，我不明白为什么这是最后期限。我继续

g g g (\f. f f) x 

然后

g g g x x 

但显然我走的太远了，你知道为什么你应该早制止？

Answer 1

这不是一个提前停止的问题。你误解了lambda微积分的语法。

按照惯例，当我们写A B C时，我们的意思是(A B) C，而不是A (B C);即function application is left associative。

因此

g g (\y. g y x)(\f. f f) 

解析作为

((g g) (\y. (g y) x)) (\f. f f) 

特别地，(g g)施加到(\y. g y x)，而(\y. g y x)是不应用于(\f. f f)。