Czy istnieje różnica między a ?

Obecnie uczę się rachunku lambda i zastanawiałem się nad następującymi dwoma różnymi rodzajami pisania terminu lambda.

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

Czy jest jakaś różnica w znaczeniu lub sposobie zastosowania redukcji wersji beta, czy to tylko dwa sposoby wyrażenia tego samego?

Szczególnie ta definicja tworzenia par wzbudziła we mnie zastanowienie:

para =$\lambda xy.\lambda p.pxy$

To tylko różnice w notacjach. $λxyz.t$ jest skrótem $λx.λy.λz.t$ . Brak magii tutaj.

Rzeczywiście, ale zwykle podkreślasz, że jest funkcją , zmieniając sposób pisania definicji. Ale tak naprawdę jest tak samo.$\mbox{pair}=λxyp.pxy$$\mbox{pair}\,t\,u$$λp.ptu$

Pierwszy to skrót od drugiego. Jest to powszechna konwencja składniowa do skracania wyrażeń.

Z drugiej strony, jeśli masz krotki w języku, istnieje różnica między nimi

1. $\lambda x.\lambda y.xy$ i
2. $\lambda (x,y).xy$ .

W pierwszym przypadku mogę podać pojedynczy argument funkcji i przekazać wynikową funkcję innym funkcjom. W tym drugim przypadku oba argumenty należy podać jednocześnie. Istnieje oczywiście funkcja, którą można zastosować do konwersji 1 na 2 i odwrotnie. Ten proces jest znany jako (nie) curry .

Definicja , o której wspominasz, to kodowanie pojęcia par w -calculus, a nie par jako prymitywnego typu danych (jak wskazałem powyżej).$\text{pair}$$\lambda$

Przekształcanie funkcji, która przenosi wiele argumentów do łańcucha funkcji z pojedynczymi argumentami, nazywa się curry . Dwie funkcje są zasadniczo takie same.

Artykuł w Wikipedii o curry