Есть ли разница между $ lambda xy.xy $ и $ lambda x. Lambda y.xy $?

Question

В настоящее время я изучаю исчисление Lambda, и мне было интересно о следующих двух разных видах написания термина Lambda.

1. $ lambda xy.xy $
2. $ lambda x. lambda y.xy $

Есть ли какая -то разница в значении или в том, как вы применяете бета -сокращение, или это только два способа выразить одно и то же?

Особенно это определение создания пар заставило меня задуматься:

пара = $ lambda xy. lambda p.pxy $

Answer 1

Это просто различия обозначений. $ λxyz.t $ коротко для $ λx.λy.λz.t $. Здесь нет магии.

Действительно, $ mbox {pair} = λxyp.pxy $, но вы склонны подчеркнуть, что $ mbox {pair} , t , u $ - функция $ λp.ptu $, изменяя способ написания определения. Но это действительно то же самое.

Answer 2

Первый - это аббревиатура для второго. Это общая синтаксическая конвенция по сокращению выражений.

С другой стороны, если у вас есть кортежи на языке, то существует разница между

1. $ lambda x. lambda y.xy $ и
2. $ lambda (x, y) .xy $.

В первом случае я могу предоставить один аргумент функции и передать результирующую функцию на другие функции. В последнем случае оба аргумента должны быть представлены одновременно. Конечно, есть функция, которую можно применить для преобразования 1 в 2 и наоборот. Этот процесс известен как (ООН) Керри.

Определение $ text {pair} $ вы упомянули, это кодирование понятия пар в $ lambda $ -calculus, а не пары в качестве примитивного типа данных (как я намекал выше).

Answer 3

Преобразование функции, которая принимает несколько аргументов в цепочку функций с отдельными аргументами, вызывается карри. Анкет Две функции по сути одинаковы.

Статья в Википедии о карри