なぜこの任期に達した後に停止するのですか？ラムダ微積分

Question

ラムダ項の正規形を計算しています。私も解決策を持っているので、「終わり」までのステップが正しいことを知っています。 与えられた用語は

(\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

これは早期停止の問題ではありません。ラムダ計算の構文を誤解しています。

慣例として、A B Cと書くときは、(A B) Cであり、ではありません。つまり、function application is left associativeです。

したがって

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

は(\y. g y x)が(\f. f f)に適用ないある一方

特に

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

として、(g g)は、(\y. g y x)に適用される構文解析します。