Ад Computer Science
Aug. 3rd, 2009 09:09 amИзоморфизм Карри-Говарда
Там есть такая строка:
(EF) (где E и F — λ-выражения)
и комментарий к ней:
Я брежу или оно должно быть как-то наоборот, т.е. E - функция, а F-аргумент? Тем более что ниже, при рассмотрении типизации этого выражения оно именно так и рассматривается.
PS: И вообще, как бы это не сойти с ума от чтения подобных вещей.
Там есть такая строка:
(EF) (где E и F — λ-выражения)
и комментарий к ней:
Третья форма называется аппликацией (или применением). Она определяет попытку приложить терм E (как будто бы это аргумент функции) к терму F (как будто бы это функция).
Я брежу или оно должно быть как-то наоборот, т.е. E - функция, а F-аргумент? Тем более что ниже, при рассмотрении типизации этого выражения оно именно так и рассматривается.
PS: И вообще, как бы это не сойти с ума от чтения подобных вещей.