¿Hay alguna diferencia entre y ?

11

Actualmente estoy aprendiendo el cálculo lambda y me preguntaba sobre los siguientes dos tipos diferentes de escribir un término lambda.

  1. λxy.xy
  2. λx.λy.xy

¿Hay alguna diferencia en el significado o la forma en que aplica la reducción beta, o esas son solo dos formas de expresar lo mismo?

Especialmente esta definición de creación de pares me hizo preguntarme:

par =λxy.λp.pxy

magnético
fuente

Respuestas:

15

Estas son solo diferencias de notaciones. λxyz.t es la abreviatura de λx.λy.λz.t . No hay magia aquí.

De hecho, pero tiende a enfatizar que es una función al cambiar la forma en que escribe la definición. Pero es realmente lo mismo.pair=λxyp.pxypairtuλp.ptu

jmad
fuente
17

El primero es una abreviatura para el segundo. Es una convención sintáctica común para acortar expresiones.

Por otro lado, si tienes tuplas en el idioma, entonces hay una diferencia entre

  1. λx.λy.xy y
  2. λ(x,y).xy .

En el primer caso, puedo proporcionar un argumento único para la función y pasar la función resultante a otras funciones. En el último caso, ambos argumentos deben ser suministrados a la vez. Existe, por supuesto, una función que se puede aplicar para convertir 1 en 2 y viceversa. Este proceso se conoce como (des) curry .

La definición de que mencionas es una codificación de la noción de pares en el cálculo , en lugar de pares como un tipo de datos primitivo (como indiqué anteriormente).pairλ

Dave Clarke
fuente
2

La transformación de una función que lleva múltiples argumentos a una cadena de funciones con argumentos únicos se llama curry . Las dos funciones son esencialmente las mismas.

Artículo de Wikipedia sobre curry

Ghassen Hamrouni
fuente
8
No existe una función que tome múltiples argumentos en el cálculo lambda. es exactamente lo mismo que , no solo básicamente lo mismo. λxy.xyλx.λy.xy
sepp2k