Jaka jest korzyść z zapisu Krivine?

Widziałem, jak niektórzy ludzie używają notacji Krivine'a do aplikacji funkcji podczas prezentacji składni dla -calculus. Na przykład -term (z normalną konwencją, że aplikacja funkcji kojarzy się z lewą stroną, więc w rzeczywistości oznacza to ) jest napisane (z podobną konwencją, że w rzeczywistości oznacza ). Nie widzę sensu posiadania kolejnej pary nawiasów wokół najbardziej wewnętrznego . Dlaczego ludzie używają notacji Krivine zamiast zwykłej?$\lambda$$\lambda$$\lambda f . \lambda x . \lambda y . f\ x\ y$$\lambda f . \lambda x . \lambda y . ((f\ x)\ y)$$\lambda f . \lambda x . \lambda y . (f)\ x\ y$$\lambda f . \lambda x . \lambda y . ((f)\ x)\ y$$f$

Zakładam, że masz na myśli zapis Krivine'a z rachunku Lambda Calculus: typy i modele .

Notacja ta, stosowana jako reprezentacja danych, sprawia, że ​​wiele algorytmów na lambda jest łatwiejszych do wdrożenia i okazania się poprawnych. To znaczy, biorąc pod uwagę termin lambda$f\; e_1\; e_2\; \ldots\; e_n$, chcesz zobaczyć to jako głowę $f$wraz z listą argumentów$[e_1, e_2, \ldots, e_n]$.

Załóżmy na przykład, że chcesz porównać dwa terminy $f\;e_1\;\ldots\; e_n$ z $g\;t_1\;\ldots\;t_n$. Często najbardziej naturalne jest porównywanie głowic$f$ i $g$ po pierwsze, nawet nie patrz na $(e_i, t_i)$pary, chyba że porównanie się powiedzie. (Często pojawia się to w implementacjach unifikacji wyższego rzędu).

Zobacz artykuł Cervesato i Pfenninga „ Liniowy rachunek kręgosłupa” w celu sformalizowania tego pomysłu.

Jedna interesująca różnica pojawia się w części 2 „Reprezentatywne funkcje” rozdziału 2 książki Krivine. Trzy zakodowane w kościele są zapisane standardową notacją jako$\lambda\ x.\ \lambda\ y.\ x\ (x\ (x\ y))$. Z notacją Krivine'a (jeśli w końcu rozumiem ją poprawnie!), Piszemy zamiast tego$\lambda x\ \lambda y\ (x)(x)(x)y$.