¿Hay una diferencia entre $ \ lambda xy.xy $ y $ \ lambda x. \ Lambda $ y.xy?

Question

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

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

¿Hay alguna diferencia en el significado o la forma de aplicar la reducción beta, o son esos solo dos maneras de expresar la misma cosa?

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

par = $ \ lambda xy. \ Lambda p.pxy $

Answer 1

Estos son sólo diferencias de notaciones. $ $ ?xyz.t es la abreviatura de $ ?x.?y.?z.t $. Aquí no hay magia.

De hecho, $ \ mbox {par} = $ ?xyp.pxy pero se tiende a enfatizar que $ \ mbox {par} \, t \, u $ es una función $ $ ?p.ptu cambiando la forma de escribir el definición. Pero en realidad es el mismo.

Answer 2

La primera es una abreviatura para el segundo. Es una convención sintáctica común a las expresiones se acortan.

Por otro lado, si usted tiene tuplas de la lengua, entonces hay una diferencia entre

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

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

La definición de $ \ text {par} $ mencionas es una codificación de la noción de pares en la $ \ lambda $ -calculus, en lugar de pares como un tipo de datos primitivo (como he insinuado más arriba).

Answer 3

La transformación de una función que toma varios argumentos a una cadena de funciones con argumentos individuales se llama currificación . Las dos funciones son esencialmente los mismos.

Artículo de Wikipedia sobre currificación