Definición de cálculo lambda

Siguiendo los conceptos matemáticos de variables libres y variables ligadas , el operador de abstracción,${\displaystyle \lambda }$Se dice que vincula su variable dondequiera que aparezca en el cuerpo de la abstracción. Se dice que las variables que caen dentro del ámbito de una abstracción están vinculadas , y la parte λ x a menudo se denomina el ligador de x . Las variables que no están vinculadas se denominan libres . Por ejemplo, la definición de la función${\displaystyle f(x)=x+y}$podría representarse como el término lambda${\displaystyle \lambda x.(x+y)}$, que contiene dos variables, x e y . La variable x está ligada por la abstracción lambda, mientras que y es libre. La variable libre y no ha sido definida y se considera desconocida. La abstracción${\displaystyle \lambda x.(x+y)}$es un término sintácticamente válido y representa una función que suma su entrada a la variable y aún desconocida . También tenga en cuenta que una variable está ligada a su abstracción "más cercana". En el siguiente ejemplo, la única aparición de${\displaystyle x}$en la expresión está delimitada por la segunda lambda:${\displaystyle \lambda xy(\lambda xz\ x)}$Una variable puede aparecer tanto libre como ligada en un término; por ejemplo${\displaystyle y}$en${\displaystyle y(\lambda yy)}$.

De manera más formal, los conjuntos de variables libres y variables ligadas de una expresión lambda,${\displaystyle M}$, se denotan como${\displaystyle \operatorname {FV} (M)}$y${\displaystyle \operatorname {BV} (M)}$y se puede definir mediante recursión sobre la estructura de los términos, como sigue: ^{[ 3 ] [ 4 ]}

Una expresión que no contiene variables libres se denomina cerrada . Las expresiones lambda cerradas también se conocen como combinadores y son equivalentes a términos en lógica combinatoria . Es común restringir la discusión solo a términos cerrados, y algunas presentaciones del cálculo lambda solo consideran términos cerrados. Por ejemplo, el término lambda que representa la identidad${\displaystyle \lambda xx}$No tiene variables libres y es cerrado.

Para mayor comodidad, se pueden omitir los paréntesis si la expresión no es ambigua. Por ejemplo, siempre se pueden omitir los paréntesis exteriores.${\displaystyle M\ N}$en lugar de${\displaystyle (M\ N)}$Sin embargo, no todos los paréntesis pueden eliminarse. Por ejemplo,

1. ${\displaystyle \lambda x.((\lambda xx)x)}$es de forma${\displaystyle \lambda xB}$y es, por lo tanto, una abstracción, mientras que
2. ${\displaystyle (\lambda x.(\lambda xx))x}$es de forma${\displaystyle MN}$y por lo tanto es una aplicación.

Los ejemplos 1 y 2 representan términos distintos, diferenciándose únicamente en la ubicación de los paréntesis. Tienen significados diferentes: el ejemplo 1 es la definición de una función, mientras que el ejemplo 2 es su aplicación. La variable lambda x es un marcador de posición en ambos ejemplos.

Aquí, el ejemplo 1 define una función.${\displaystyle \lambda xB}$, dónde${\displaystyle B}$es${\displaystyle (\lambda xx)x}$, una función anónima${\displaystyle (\lambda xx)}$, con entrada${\displaystyle x}$; mientras que el ejemplo 2,${\displaystyle M}$ ${\displaystyle N}$, es M aplicado a N, donde${\displaystyle M}$es el término lambda${\displaystyle (\lambda x.(\lambda xx))}$se está aplicando a la entrada${\displaystyle N}$que es${\displaystyle x}$Ambos ejemplos, 1 y 2, se evaluarían como la función identidad .${\displaystyle \lambda xx}$.

Para permitir una mayor concisión en estas situaciones, se suelen aplicar las siguientes convenciones:

• Se supone que las aplicaciones son asociativas por la izquierda:${\displaystyle M\ N\ P}$puede escribirse en lugar de${\displaystyle ((M\ N)\ P)}$^{[ 5 ]}
• El cuerpo de una abstracción se extiende lo más a la derecha posible :${\displaystyle \lambda xM\ N}$medio${\displaystyle \lambda x.(M\ N)}$y no${\displaystyle (\lambda xM)\ N}$Dicho de otro modo, una abstracción lambda tiene menor precedencia que una aplicación.
• Se contrae una secuencia de abstracciones:${\displaystyle \lambda x.\lambda y.\lambda zN}$se abrevia como${\displaystyle \lambda xyz.N}$^{[ 6 ] [ 7 ] [ 5 ]}
• Cuando todas las variables son de una sola letra, se puede omitir el espacio en las aplicaciones: MNP en lugar de M N P . ^{[ 8 ]}

La α-conversión ( alpha -conversion), a veces conocida como α-renombrado, ^{[ 10 ]} permite cambiar los nombres de las variables vinculadas. Por ejemplo, la α-conversión de${\displaystyle \lambda xx}$podría producir${\displaystyle \lambda yy}$Los términos${\displaystyle x}$y${\displaystyle y}$Los términos que difieren únicamente por la conversión alfa se denominan α-equivalentes , lo que refleja la intuición de que la elección particular de una variable ligada en una abstracción no suele ser relevante. Con frecuencia, en el cálculo lambda, los términos α-equivalentes se consideran equivalentes.

Las reglas precisas para la conversión alfa no son del todo triviales. Primero, al convertir alfa una abstracción, las únicas ocurrencias de variables que se renombran son aquellas que están vinculadas por la misma abstracción. Por ejemplo, una conversión alfa de${\displaystyle \lambda x.\lambda xx}$podría resultar en${\displaystyle \lambda y.\lambda xx}$pero no podría resultar en${\displaystyle \lambda y.\lambda xy}$. Este último tiene un significado diferente al original. Esto es análogo a la noción de programación de ocultamiento de variables .

En segundo lugar, la conversión alfa no es posible si resultara en que una variable sea capturada por una abstracción diferente. Por ejemplo, si reemplazamos${\displaystyle x}$con${\displaystyle y}$en${\displaystyle \lambda x.\lambda yx}$, obtenemos${\displaystyle \lambda y.\lambda yy}$, lo cual no es en absoluto lo mismo. En la notación de índice de De Bruijn , cualesquiera dos términos α-equivalentes son sintácticamente idénticos, y de esta manera no puede producirse confusión.

Ver ejemplo:

Sustitución, por escrito${\displaystyle E[V:=R]}$es el proceso de reemplazar todas las ocurrencias libres de la variable${\displaystyle V}$en la expresión${\displaystyle E}$con expresión${\displaystyle R}$La sustitución en términos del cálculo lambda se define mediante recursión en la estructura de los términos, como sigue (nota: x e y son variables, mientras que M y N son cualquier expresión λ).

• ${\displaystyle x[x:=N]=N}$ ; con${\displaystyle N}$sustituido por${\displaystyle x}$,${\displaystyle x}$se convierte${\displaystyle N}$
• ${\displaystyle y[x:=N]=y}$si${\displaystyle x\neq y}$ ; con${\displaystyle N}$sustituido por${\displaystyle x}$,${\displaystyle y}$(que no lo es)${\displaystyle x}$) restos${\displaystyle y}$
• ${\displaystyle (M_{1}\ M_{2})[x:=N]=(M_{1}[x:=N])(M_{2}[x:=N])}$ ; la sustitución distribuye a ambos lados de una solicitud
• ${\displaystyle (\lambda xM)[x:=N]=\lambda xM}$ Una variable ligada a una abstracción no es sustituible; sustituir dicha variable deja la abstracción inalterada.
• ${\displaystyle (\lambda yM)[x:=N]=\lambda y.(M[x:=N])}$si${\displaystyle x\neq y}$y${\displaystyle y\notin FV(N)}$; la sustitución de una variable que no está ligada a una abstracción se realiza en el cuerpo de la abstracción, siempre que la variable abstraída${\displaystyle y}$es " fresco " para el término de sustitución${\displaystyle N}$, lo que significa que no aparece entre las variables libres de${\displaystyle N.}$

Por ejemplo,${\displaystyle (\lambda xx)[y:=y]=\lambda x.(x[y:=y])=\lambda xx}$, y${\displaystyle ((\lambda xy)x)[x:=y]=((\lambda xy)[x:=y])(x[x:=y])=(\lambda xy)y}$.

La condición de frescura (que requiere que${\displaystyle y}$no está en las variables libres de${\displaystyle N}$) es crucial para asegurar que la sustitución no cambie el significado de las funciones. La situación en la que se sustituye${\displaystyle x}$Se suponía que debía ser libre pero terminó siendo atado, una situación conocida como captura.${\displaystyle x}$Para sustituir en una abstracción lambda, a veces es necesario convertir la expresión a α. Por ejemplo, esta sustitución${\displaystyle (\lambda xy)[y:=x]\neq \lambda x.(y[y:=x])=\lambda xx}$es erróneo porque convertiría la función constante en una función.${\displaystyle \lambda xy}$en la identidad${\displaystyle \lambda xx}$. La sustitución correcta consiste en renombrar la variable ligada utilizando la α-equivalencia, en este caso${\displaystyle (\lambda x.y)[y:=x]=(\lambda z.y)[y:=x]=\lambda z.(y[y:=x])=\lambda z.x}$.

En general, el incumplimiento de la condición de frescura se puede remediar renombrando alfa primero, con una variable fresca adecuada. La sustitución se define de forma única hasta la α-equivalencia. La mayoría de las implementaciones de sustitución usan la conversión alfa automáticamente para evitar la captura durante la sustitución, una operación llamada sustitución que evita la captura . En lenguajes de programación con ámbito estático, la sustitución que evita la captura se puede usar para implementar la resolución de nombres manejando cuidadosamente el sombreado de variables en ámbitos contenedores . Otra estrategia es requerir el renombrado alfa en el programa fuente para hacer que la resolución de nombres sea trivial . Si se usa la indexación De Bruijn , entonces la conversión alfa ya no es necesaria, ya que no habrá colisiones de nombres. Los nombres de las variables tampoco son necesarios si se usa una función universal, como en Iota y Jot .

La β-reducción ( reducción beta ) captura la idea de aplicación de la función. La β-reducción se define en términos de sustitución: la β-reducción de${\displaystyle ((\lambda V.E)\ E')}$es${\displaystyle E[V:=E']}$. La regla de reducción β establece que una aplicación de la forma${\displaystyle (\lambda x.t)s}$se reduce al término${\displaystyle t[x:=s]}$. La notación${\displaystyle (\lambda x.t)s\to t[x:=s]}$se utiliza para indicar que${\displaystyle (\lambda x.t)s}$β-se reduce a${\displaystyle t[x:=s]}$La β-reducción captura la idea de aplicación de funciones (también llamada llamada a función) e implementa la sustitución de la expresión del parámetro real por la variable del parámetro formal. La β-reducción puede considerarse equivalente al concepto de reducibilidad local en la deducción natural , a través del isomorfismo de Curry-Howard .

Por ejemplo, para cada${\displaystyle s}$,${\displaystyle (\lambda x.x)s\to x[x:=s]=s}$Esto demuestra que${\displaystyle \lambda x.x}$realmente es la identidad. De manera similar,${\displaystyle (\lambda x.y)s\to y[x:=s]=y}$, lo cual demuestra que${\displaystyle \lambda x.y}$es una función constante. Suponiendo alguna codificación de${\displaystyle 2,7,\times }$, tenemos la siguiente β-reducción:${\displaystyle ((\lambda n.\ n\times 2)\ 7)\rightarrow 7\times 2}$.

De manera más formal, la reducción β se puede realizar en la abstracción lambda sin renombrar alfa solo si no hay nombres de variables libres en el parámetro real y ligados en el cuerpo: ^{[ a ]}

${\displaystyle FV(y)\cap BV(b)=\{\}\to (\lambda x.b)\ y=b[x:=y]}$

Se puede utilizar el cambio de nombre alfanumérico en${\displaystyle b}$cambiar el nombre de los nombres que están libres en${\displaystyle y}$pero limitado en${\displaystyle b}$, para cumplir con la condición previa para esta transformación. Ver ejemplo:

Si observamos más de cerca, las sustituciones clave son:

${\displaystyle {\begin{array}{r}((\lambda x.z\ x)(\lambda y.z\ y))[z:=(x\ y)]{\text{(blocked - will capture)}}\\((\lambda a.z\ a)(\lambda b.z\ b))[z:=(x\ y)]{\text{(allowed - no capture)}}\end{array}}}$

En este ejemplo,

1. En el β-redex,
   1. Las variables libres son,${\displaystyle \operatorname {FV} (x\ y)=\{x,y\}}$
   2. Las variables ligadas son,${\displaystyle \operatorname {BV} ((\lambda x.z\ x)(\lambda y.z\ y))=\{x,y\}}$
2. La reducción β ingenua cambió el significado de la expresión porque x e y del parámetro real quedaron capturados cuando las expresiones se sustituyeron en las abstracciones internas.
3. El cambio de nombre alfa eliminó el problema al modificar los nombres de x e y en la abstracción interna para que fueran distintos de los nombres de x e y en el parámetro real.
   1. Las variables libres son,${\displaystyle \operatorname {FV} (x\ y)=\{x,y\}}$
   2. Las variables ligadas son,${\displaystyle \operatorname {BV} ((\lambda a.z\ a)(\lambda b.z\ b))=\{a,b\}}$
4. La reducción β procedió entonces con el significado previsto.

La reducción η ( reducción eta ) convierte de${\displaystyle \lambda x.(fx)}$a${\displaystyle f}$, dado que${\displaystyle x}$no parece libre en${\displaystyle f}$El problema de utilizar una reducción η cuando f tiene variables libres se muestra en este ejemplo:

Este uso inapropiado de la reducción η cambia el significado al dejar x en ${\displaystyle \lambda y.y\,x}$no sustituido.

La η-reducción a menudo se combina con su inversa, la η-expansión, que convierte desde${\displaystyle f}$a${\displaystyle \lambda x.(fx)}$, nuevamente dado que${\displaystyle x}$no parece libre en${\displaystyle f}$Los dos procesos en conjunto se denominan η-conversión . La η-conversión expresa la idea de extensionalidad , ^{[ 12 ]} que en este contexto significa que dos funciones son iguales si y solo si dan el mismo resultado para todos los argumentos. La η-conversión puede considerarse equivalente al concepto de completitud local en la deducción natural , a través del isomorfismo de Curry-Howard .