lambda cálculo: hacer pasar dos valores a un único parámetro sin currying

Question

no puedo entender por qué se permite la siguiente reducción beta en untyped cálculo lambda:

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

Específicamente I no puede entender cómo se puede pasar dos parámetros u y v a un solo parámetro x en la parte λx.x. Para permitir lo anterior ¿no debería usar currying y tener dos parámetros? Al igual que este —

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

Answer 1

específicamente no puedo entender cómo se puede pasar dos parámetros u y v

usted no está pasando dos parámetros u y v. Está pasando (u v), que es un único valor o término: el valor de u aplicado a v.

comparar esto con la aritmética ordinaria: se puede aplicar una función tal como sin a un término compuesto como sin(x + 1) porque x+1 denota un solo valor, a pesar de que es la aplicación de la función + a dos argumentos x y 1.