La belleza del Cálculo lambda

En una entrada anterior escribí sobre el impacto del Calculo lambda en la Ciencias de la Computación, hoy quiero escribir sobre la belleza del Cálculo lambda, El Cálculo lambda es un modelo matemático, que sirve para describir a todas las funciones computables y es equivalente a las máquinas de Turing. Las computadoras actuales tienen un diseño basado en las máquinas de Turing. La definición de una máquina de Turing es muy "pomposa"/tediosa/larga, pues se da en términos de seis cosas( dependiendo del libro el numero de estas puede variar) éstas son: Un conjunto de estados, un conjunto de estados finales, un estado inicial, un símbolo especial (el blanco), un alfabeto de entrada, un alfabeto de salida, y la definición de una función delta de transiciones. La descripción de una maquina de Turing que suma números enteros puede ser muy larga. Por otro lado la definición del calculo lambda es muy sencilla, de hecho "peca" de sencilla, la definición es:

L ::= Var | L L | lambda Var.L

Var:: x1,x2,x3,x4,......

Es decir los términos del Cálculo lambda son: Variables, Aplicaciones (L L) y abstracciones. La sencillez de la definición es sorprendente, pero su equivalencia con las máquinas de Turing también.

Philip Walder escribe en su artículo Proofs are Programs : "Como el Universo físico parece estar construido de un número pequeño de partículas y fuerzas básicas , el Universo computacional parece estar construido de sólo tres tipos de términos y una regla de reducción"

La regla de reducción a la que hace referencia Walder es la beta reducción, la cual es una regla muy sencilla, parecida a la substitución en la lógica de primer orden.


Estas son algunas de las razones por las que el Cálculo lambda es mi modelo favorito de computo.