Ад Computer Science

[metaclass]

Изоморфизм Карри-Говарда

Там есть такая строка:
(EF) (где E и F — λ-выражения)
и комментарий к ней:

Третья форма называется аппликацией (или применением). Она определяет попытку приложить терм E (как будто бы это аргумент функции) к терму F (как будто бы это функция).

Я брежу или оно должно быть как-то наоборот, т.е. E - функция, а F-аргумент? Тем более что ниже, при рассмотрении типизации этого выражения оно именно так и рассматривается.

PS: И вообще, как бы это не сойти с ума от чтения подобных вещей.

Comments

[a-lourier.livejournal.com]

Я из лекций по CS помню, что у нас по-человечески записывали Ix=x, Kab=a и т.д. Вероятно, опечатка в статье.

[kkirsanov.livejournal.com]

Заметил что в разговорах слово "безумие" чаще всего употребляется в констекста GUI и всяческих лямбд.

[metaclass.livejournal.com]

Оно так и есть.
Первое с трудом поддается вообще какому-бы то ни было теоретическому описанию(хотя если бы разрешили расстреливать юзеров и дизайнеров - поддалось бы).
А второе через пару итераций размышлений о теории улетает в нечеловеческие ебеня "размышлений о размышлениях" типа "а как бы это нам построить тип всех типов" и становится малоприменимой к реальности.

[gds.livejournal.com]

в ебеня улетать нет необходимости. (а ту возможность, которая есть, использовать не обязательно. но часто интересно.)

А касаемо статьи -- конечно опечатка.

[metaclass.livejournal.com]

Не, вот я пытаюсь формально описать переходы между различными представлениями одной и той же абстрактной модели системы и ее конкретными представлениями в виде GUI, схемы БД, объектов и функций в исполняемых модулях и в итоге всегда убредаю в дебри, для выхода из которых приходится читать что-то вроде http://plato.stanford.edu/entries/type-theory/ от чего пухнет мозг :)

[alll]

Там имхо всё корректно, если пользоваться данным там (чуть выше) определением процедуры "приложение аргумента к функции":

Используя нотацию λ-исчисления, функция с параметром x и телом E записывается как λx.E. Когда к этой функции прикладывается аргумент a (термин «прикладывается» также взят из λ-исчисления), в теле функции E на a заменяется каждое свободное вхождение x.

В данном случае, видимо, это означает, что в теле терма F все вхождения некоего формального параметра должны быть заменены на терм E.

[metaclass.livejournal.com]

Не, похоже все таки там перепутано.
Прикладывание аргумента будет выглядеть как
(λx.E а)
т.е. аргумент идет очевидно после функции.

[alll]

Там три вида термов. λx.E - это прикладывается переменная, а не выражение. А если выражение - то это случай не 2, а 3: (EF) (где E и F — λ-выражения). О чём, собственно, и речь.

[metaclass.livejournal.com]

λx.E это не прикладывание, это абстракция.
А прикладывание это (λx.E a)
Причем а в данном случае это частный случай терма F