Pourquoi nous arrêtons-nous après avoir atteint ce terme? Lambda Calculus

Question

Je calcule la forme normale d'un Terme lambda. J'ai aussi la solution donc je sais que mes étapes jusqu'à la "fin" étaient justes. Le terme donné est

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

et normalform de c'est

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

J'ai aussi cela, mais je continuais et je ne comprends pas pourquoi c'est le terme final. Je continuais avec

g g g (\f. f f) x 

puis

g g g x x 

Mais apparemment je suis allé trop loin, ne savez-vous pourquoi vous êtes censé arrêter plus tôt?

Answer 1

Il ne s'agit pas de s'arrêter plus tôt. Vous interprétez mal la syntaxe du lambda-calcul. Par convention, lorsque nous écrivons A B C, nous entendons (A B) C, et non ; c'est-à-dire function application is left associative.

Par conséquent

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

parse comme

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

En particulier, (g g) est appliqué à (\y. g y x), alors que (\y. g y x) est pas appliquée à (\f. f f).