лямбда-исчисление: передача двух значений в один параметр без каррирования - PullRequest
7 голосов
/ 07 декабря 2011

Я не могу понять, почему в нетипизированном лямбда-исчислении допустимо следующее бета-уменьшение:

(λx.x y) (u v) -> ((u v) y)

В частности, я не могу понять, как можно передать два параметра u и v одному параметру x в части λx.x. Чтобы разрешить вышесказанное, я не должен использовать карри и иметь два параметра? Как это & ​​mdash;

(λx.(λy.(x y))) (u v)

1 Ответ

11 голосов
/ 07 декабря 2011

особенно я не могу понять, как можно передать два параметра u и v

Вы не передаете два параметра u и v.Вы передаете (u v), который является единственным значением или термином: значение u, примененное к v.

Сравните это с обычной арифметикой: вы можете применить такую ​​функцию, как sin для составного термина, такого как sin(x + 1), потому что x+1 обозначает одно значение, даже если это приложение функции + к двум аргументам x и 1.

...