![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
Ад Computer Science
Изоморфизм Карри-Говарда
Там есть такая строка:
(EF) (где E и F — λ-выражения)
и комментарий к ней:
Я брежу или оно должно быть как-то наоборот, т.е. E - функция, а F-аргумент? Тем более что ниже, при рассмотрении типизации этого выражения оно именно так и рассматривается.
PS: И вообще, как бы это не сойти с ума от чтения подобных вещей.
Там есть такая строка:
(EF) (где E и F — λ-выражения)
и комментарий к ней:
Третья форма называется аппликацией (или применением). Она определяет попытку приложить терм E (как будто бы это аргумент функции) к терму F (как будто бы это функция).
Я брежу или оно должно быть как-то наоборот, т.е. E - функция, а F-аргумент? Тем более что ниже, при рассмотрении типизации этого выражения оно именно так и рассматривается.
PS: И вообще, как бы это не сойти с ума от чтения подобных вещей.
no subject
no subject
no subject
Первое с трудом поддается вообще какому-бы то ни было теоретическому описанию(хотя если бы разрешили расстреливать юзеров и дизайнеров - поддалось бы).
А второе через пару итераций размышлений о теории улетает в нечеловеческие ебеня "размышлений о размышлениях" типа "а как бы это нам построить тип всех типов" и становится малоприменимой к реальности.
no subject
А касаемо статьи -- конечно опечатка.
no subject
no subject
Используя нотацию λ-исчисления, функция с параметром x и телом E записывается как λx.E. Когда к этой функции прикладывается аргумент a (термин «прикладывается» также взят из λ-исчисления), в теле функции E на a заменяется каждое свободное вхождение x.
В данном случае, видимо, это означает, что в теле терма F все вхождения некоего формального параметра должны быть заменены на терм E.
no subject
Прикладывание аргумента будет выглядеть как
(λx.E а)
т.е. аргумент идет очевидно после функции.
no subject
no subject
А прикладывание это (λx.E a)
Причем а в данном случае это частный случай терма F