Cálculo Lambda

El cálculo lambda fue desarrollado por Alonso Church en el año de 1930. En sí fue desarrollado para dar una definición precisa de lo que es una función.
Además el cálculo lambda también puede ser usado para definir en una forma precisa lo que es una función computable. Se dice que este ćalculo es universal ya que puede expresar y evaluar cualequier funcion computable. Por esta razón el cálculo lambda es equivalente a las máquinas de Turing, sin embargo el cálculo λ es una propuesta más cercana al software que al hardware.

El cálculo lambda trabaja con objetos llamados lambda-términos, los cuales son cadenas de símbolos como una de las siguientes forma:

• v
• λv.E₁
• (E₁ E₂)

Donde v es una variable, y donde E₁ y E₂ son lambda-términos. Y los términos de la forma λv.E₁ son abstracciones, de lo cual, les hablaré más adelante.

El cálculo lambda se puede considerar como el lenguaje universal más pequeño. Ha sido empleado también como fundamento conceptual de los lenguajes de programación.

Sintaxis
La sintaxis del Cálculo Lambda es:
<término>::= <variable> |
λ<variable>.<término> |
(<término><término>)

Esta sintaxis solo representa a las funciones con un argumento.
Si se quieren mas argumentos sería de la siguiente forma:
λx1.λ x2. .... λxn. M

Un término o expresión en el cálculo lambda se define recursivamente mediante las reglas siguientes:

• Todas las variables son términos, es decir cada una de las variables es un término.
• Suponiendo que x es una variable y t es un término, entonces (λx.t) es un término llamado abstracción lambda.
• Suponiendo que t y s son términos, entonces (ts) es un término llamado aplicación lambda.
• Ninguna otra cosa más que lo anterior, es un término.
  

Una abstracción lambda o abstracción funcional λx.t representa una función que toma solo a un argumento, además se dice que λ liga la variable x en el término t.

Por otra parte, la aplicación lambda o aplicación funcional ts representa la aplicación de un argumento s a una función t.
La aplicación lambda tiene el formato (M N) y dicha aplicación tendrá un resultado.
Para calcular el resultado de una aplicación lambda o funcional será atraves de la generación de expresiones equivalentes por la aplicación de las reglas del cálculo λ.

La relación de equivalencia entre las expresiones del cálculo λ tendrá las siguientes propiedades:

• Reflexividad M = M
  
• Simetría M = N -> N = M
  
• Transitividad M = N Λ N = P -> M = P

También tendrá las siguientes reglas:
M = N -> (M P) = (N P)
M = N -> (P M) = (P N)
M = N -> λx.N = λx.M

Ocurrencia de los términos
Dado en el siguiente término, se ejemplifica la ocurrencia:

((xy)λx.(xy))

(xy) ocurre dos veces
x ocurre tres veces
y ocurre dos veces

Ahora definiré lo que es ocurrencia ligada.
Una ocurrencia de la variable x en un término P es ligada, solamente si x ocurre en un subtérmino de P de la forma λx.M; esto se puede aplicar en el siguiente término: (λy.(yy)λx.(xy)

En sí, x y y ocurren ligadas en el término anterior, ya que este término contiene a los subtérminos:

λy.(yy) -> donde y ocurre ligada tres veces
λx.(xy) -> donde x ocurre ligada dos veces.

Ahora definiré lo que es ocurrencia libre.
Si x ocurre libre en un término de P por lo menos una vez, entonces x es una variable libre de P.
Esto es:
Bueno, en si esto es lo que trata el Cálculo Lambda.
Aquí les dejaré las referencias que utilice para este tema:

Paradigmas de Programación: Cálculo Lambda.
Cálculo Lambda.
Cálculo λ


Saludos.