Qual é o benefício da notação de Krivine?

Vi que algumas pessoas usam a notação de Krivine para aplicação de funções ao apresentar a sintaxe para o cálcio- . Por exemplo, o λ -termo λ f . λ x . λ y . f x y (com a convenção normal de que o aplicativo de função se associa à esquerda, significa, na verdade, λ f . λ x . λ y . ( ( f x ) y ) ) é escrito λ f . λ x . λ $\lambda$$\lambda$$\lambda f . \lambda x . \lambda y . f\ x\ y$$\lambda f . \lambda x . \lambda y . ((f\ x)\ y)$ (com uma convenção similar de que na verdade significa λ f . λ x . λ y . ( ( f ) x ) y )). Não vejo o ponto de ter outro par de parênteses em torno do f mais interno. Por que as pessoas usam a notação de Krivine em vez da usual?$\lambda f . \lambda x . \lambda y . (f)\ x\ y$$\lambda f . \lambda x . \lambda y . ((f)\ x)\ y$$f$

Suponho que você queira dizer a notação de Krivine do Lambda Calculus: Types and Models .

Essa notação, usada como representação de dados, torna muitos algoritmos em termos lambda mais simples de implementar e provar corretos. Ou seja, dado um termo lambda , você deseja visualizá-lo como umcabeçalho f , junto com umalistade argumentos [ e 1 , e 2 , … , e n ] .$f\; e_1\; e_2\; \ldots\; e_n$ $f$$[e_1, e_2, \ldots, e_n]$

Por exemplo, suponha que você queira comparar dois termos com$f\;e_1\;\ldots\; e_n$$g\;t_1\;\ldots\;t_n$$f$$g$$(e_i, t_i)$

Veja o artigo de Cervesato e Pfenning, A Linear Spine Calculus, para uma formalização dessa idéia.

$\lambda\ x.\ \lambda\ y.\ x\ (x\ (x\ y))$$\lambda x\ \lambda y\ (x)(x)(x)y$