Programación funcional - Cálculo Lambda

El cálculo lambda es un marco desarrollado por Alonzo Church en la década de 1930 para estudiar cálculos con funciones.

  • Function creation - Church introdujo la notación λx.Epara denotar una función en la que 'x' es un argumento formal y 'E' es el cuerpo funcional. Estas funciones pueden ser sin nombre y sin argumentos.

  • Function application - Church usó la notación E1.E2 para denotar la aplicación de la función E1 al argumento real E2. Y todas las funciones están en un solo argumento.

Sintaxis del cálculo Lambda

El cálculo de Lamdba incluye tres tipos diferentes de expresiones, es decir,

E :: = x (variables)

| E 1 E 2 (aplicación de funciones)

| λx.E (creación de funciones)

Dónde λx.E se llama abstracción Lambda y E se conoce como expresiones λ.

Evaluación del cálculo Lambda

El cálculo lambda puro no tiene funciones integradas. Evaluemos la siguiente expresión:

(+ (* 5 6) (* 8 3))

Aquí, no podemos comenzar con '+' porque solo opera con números. Hay dos expresiones reducibles: (* 5 6) y (* 8 3).

Podemos reducir cualquiera de los dos primero. Por ejemplo

(+ (* 5 6) (* 8 3)) 
(+ 30 (* 8 3)) 
(+ 30 24) 
= 54

Regla de reducción β

Necesitamos una regla de reducción para manejar λs

(λx . * 2 x) 4 
(* 2 4) 
= 8

Esto se llama reducción β.

El parámetro formal se puede utilizar varias veces:

(λx . + x x) 4 
(+ 4 4) 
= 8

Cuando hay varios términos, podemos manejarlos de la siguiente manera:

(λx . (λx . + (− x 1)) x 3) 9

El interior x pertenece al interior λ y la x exterior pertenece a la exterior.

(λx . + (− x 1)) 9 3 
+ (− 9 1) 3 
+ 8 3 
= 11

Variables libres y limitadas

En una expresión, cada aparición de una variable es "libre" (a λ) o "ligada" (a λ).

β-reducción de (λx . E) y reemplaza cada x que ocurre gratis en E con y. Por ejemplo:

Reducción alfa

La reducción alfa es muy simple y se puede realizar sin cambiar el significado de una expresión lambda.

λx . (λx . x) (+ 1 x) ↔ α λx . (λy . y) (+ 1 x)

Por ejemplo

(λx . (λx . + (− x 1)) x 3) 9 
(λx . (λy . + (− y 1)) x 3) 9 
(λy . + (− y 1)) 9 3 
+ (− 9 1) 3 
+ 8 3 
11

Teorema de Church-Rosser

El teorema de Church-Rosser establece lo siguiente:

  • Si E1 ↔ E2, entonces existe una E tal que E1 → E y E2 → E. "La reducción de cualquier forma puede producir el mismo resultado".

  • Si E1 → E2, y E2 es la forma normal, entonces hay una reducción de orden normal de E1 a E2. "La reducción de orden normal siempre producirá una forma normal, si existe".