Cálculo Lambda

CÁLCULO LAMBDA

Es una teoría fundamental de aplicación y abstracción para el estudio de tipos ya que puede verse como una gramática para términos de un lenguaje.

El cálculo lambda permite decidir si una expresión pertenece o no al lenguaje.

El cálculo lambda surge antes que los lenguajes de programación de alto nivel a raíz del estudio realizado por Alonso Church en la década del 30

La relevancia del cálculo lambda en ciencias de la computación sólo se apreció en 1960, cuando las propiedades básicas en lenguajes de alto nivel se estudiaron, observándose el potencial que tiene el cálculo lambda en la especificación de los lenguajes de programación

El cálculo lambda puro tiene una sintaxis pequeña compuesta solamente de tres constructores: variables, aplicación de funciones y creación de funciones

El cálculo lambda puro no tiene tipos. Las funciones pueden aplicarse sin restricciones, pero teniendo en cuenta el ámbito, el paso de parámetros y las estrategias de evaluación.

gramática de términos.

M := x | ( M1 M2 ) | ( λx. M)

Dice que un término puede ser una variable x, una aplicación (M1 M2) de la función M1 a M2 o una abstracción (λX.M).

λx. M: función con parámetro x y cuerpo M

Note que las funciones se escriben junto a sus argumentos.

λx.M <---->abstracción <----> definición de función.

Determinación de parámetros y cuerpo de la función.

xy <----> aplicación <----> invocación.

Se está invocando la función x con parámetro y, donde y es una función o una variable.

Se usan las letrasj, x, y, z para variables y M, N, P, Q para términos. La letra e se utiliza para constantes básicas y funciones constantes.

El cálculo lambda permite estudiar las propiedades de las funciones, de tal forma que se constituye en la teoría que formaliza los lenguajes funcionales, facilitando la rigurosa evaluación y prueba de expresiones.

La regla del cálculo lambda que permite generar expresiones que satisfagan la relación de equivalencia se denomina Regla Beta

La Regla Beta establece como sustituir en el cuerpo de la abstracción funcional cada ocurrencia de la variable que hace de argumento nominal por el argumento efectivo de la aplicación funcional correspondiente.

EJEMPLO

(λx .M N) = [N/x] M

La parte derecha de la expresión se interpreta como: "El término que se obtiene de introducir N en lugar de x, toda vez que x ocurre libre en M”

OCURRENCIA DE UN TERMINO

Definición. Ocurrencia de P en Q

Si P ocurre en M o N ---> P ocurre en (M N)

Si P ocurre en M o P es igual a x ---> P ocurre en λx.M

EJEMPLO

( (x y) λx.(x y) )

(x y) ocurre dos veces

x ocurre tres veces

y ocurre dos veces

Los conceptos son los de ocurrencia libre y ligada de un variable.

Una ocurrencia de la variable x en un término P es ligada sí y solo sí, x ocurre en un subtérmino de P de la forma λx.M

Si x ocurre libre al menos un vez en un término P, entonces x es una variable libre de P.

EJEMPLO

((λy.(x y) z) λx.(x λx.(x y)))

(x y) ocurre 2 veces

x ocurre 5 veces, 4 veces ligada y 1 vez libre

y ocurre 3 veces, 2 veces ligada y 1 libre

z ocurre una vez libre

Por lo tanto:

variables libres: x, y, z

variables ligadas: x, y

BRIAN ALEJANDRO FLORES SILVA

INSTITUTO TECNOLÓGICO SUPERIOR DE IRAPUATO

PROGRAMACIÓN LÓGICA Y FUNCIONAL