Cálculo lambda

Materia : Lenguajes de Programación

Fue introducido en los 30's por Alonzo Church y Stephen Kleene con el objetivo de dar una teoría general de las funciones es un sistema formal diseñado para definir funciones, la forma de utilizarlas y la recursión. El cálculo lambda influye en lenguajes funcionales como Lisp, Haskell y ML. Es utilizado como un fundamento de lenguajes de programación porque aporta una sintaxis básica de programación, la semántica para el concepto e función en la transformación de argumentos en resultados y una forma de definir primitivas de programación.

El calculo lambda es el lenguaje de programación mas pequeño consiste en transformación simple(sustituir variables) y en definir funciones. El calculo lambda se puede decir que es equivalente a las máquinas Turing porque es capaz de evaluar y expresar cualquier función computable. Church había querido hacer un sistema formal completo para modelizar la matemática pero después separo el calculo lambda y lo ideo para que estudiara la computabilidad.

El calculo lambda usa objetos llamados lambda-términos:

v

λv.E1

(E1 E2)

• v es un nombre de variable, E1 Y E2 son lambda términos y λv.E1 se llaman abstracciones v es el parámetro formal y E1 es el cuerpo de la abstracción.
• λv.E1 es una función que recibe v como valor para sustituir y devuelve el valor de E1 para cada ocurrencia de
• (E1 E2) son llamados aplicaciones esta forma representa la llamada a la función E1 recibiendo como argumento E2.

Sintaxis del calculo lambda:

<término> ::= <variable> |

λ<variable> . <término> |

( <término> <término> )

En donde λ es la lista de argumentos y es el cuerpo de la abstraccion funcional, la sintaxis que mostré anteriormente representa una función con un solo argumento, con mas argumentos se puede representar como :

λx1. λx2. .... λxn. M

El sistema necesita que la aplicaron funcional y su resultado puedan ser evaluadas como expresiones que representen el mismo valor

(M N) = R

La regla Beta permite producir expresiones que sean equivalentes de la siguiente forma: "la manera de 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.", la forma de representarlo es a siguiente:

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

La parte de (λx .M N) se puede interpretar como sustituir la N todas las veces que ocurre x en M.

Referencias

Cálculo lambda.

Paradigmas de programación.