В чем преимущество нотации Кривина?

9

Я видел, что некоторые люди используют нотацию Кривина для приложения функции при представлении синтаксиса для λ-исчисление. Например,λ-срок λf.λx.λy.f x y (с обычным соглашением, что приложение функции ассоциируется слева, так что это на самом деле означает λf.λx.λy.((f x) y)) написано λf.λx.λy.(f) x y (с похожим соглашением, которое на самом деле означает λf.λx.λy.((f) x) y). Я не вижу смысла иметь еще одну пару скобок вокруг самого внутреннегоf, Почему люди используют обозначение Кривина вместо обычного?

день
источник

Ответы:

13

Я предполагаю, что вы имеете в виду запись Кривина из Lambda Calculus: Типы и Модели .

Эта нотация, используемая в качестве представления данных, упрощает реализацию и доказывает правильность многих алгоритмов на лямбда-терминах. То есть, учитывая лямбда-терминfe1e2en, вы хотите рассматривать это как голову fвместе со списком аргументов[e1,e2,,en],

Например, предположим, что вы хотите сравнить два термина fe1en с gt1tn, Часто наиболее естественно сравнивать головыf а также g во-первых, и даже не смотреть на (ei,ti)пары, если это сравнение не удается. (Это часто встречается в реализациях объединения более высокого порядка.)

См. Статью Червесато и Пфеннинга « Линейное исчисление позвоночника» для формализации этой идеи.

Нил Кришнасвами
источник
0

Одно интересное отличие обнаруживается в разделе 2 «Представимые функции» главы 2 книги Кривин. Кодированная церковью три записана в стандартной записи какλ x. λ y. x (x (x y)), С нотацией Кривина (если я наконец понял это правильно!), Мы бы написали вместоλx λy (x)(x)(x)y,

Аарон Стамп
источник