metaclass: (Default)
metaclass ([personal profile] metaclass) wrote2009-08-03 09:09 am

Ад Computer Science

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

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

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

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

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

[identity profile] gds.livejournal.com 2009-08-03 08:01 am (UTC)(link)
в ебеня улетать нет необходимости. (а ту возможность, которая есть, использовать не обязательно. но часто интересно.)

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

[identity profile] metaclass.livejournal.com 2009-08-03 08:08 am (UTC)(link)
Не, вот я пытаюсь формально описать переходы между различными представлениями одной и той же абстрактной модели системы и ее конкретными представлениями в виде GUI, схемы БД, объектов и функций в исполняемых модулях и в итоге всегда убредаю в дебри, для выхода из которых приходится читать что-то вроде http://plato.stanford.edu/entries/type-theory/ от чего пухнет мозг :)