¿Cálculo lambda fuera de la programación funcional?

Question

Soy un estudiante universitario y actualmente estamos estudiando el cálculo de Lambda. Sin embargo, todavía me cuesta entender exactamente por qué esto es útil para mí. Me doy cuenta de que si haces un montón de programación funcional, podría ser útil, sin embargo, creo que realmente no es necesario para aprender la programación funcional, ¿qué piensas?

En segundo lugar, ¿hay algún uso para el cálculo de lambda dentro del ámbito de la informática pero fuera de los lenguajes de programación funcional?

Answer 1

El cálculo de Lambda es fundamental en la lógica, la teoría de la categoría, la teoría de tipos, la verificación formal ... básicamente, cualquier cosa que ver con la semántica del lenguaje de programación y la lógica formal. Es un formalismo tan fundamental que las personas que trabajan en estos campos ni siquiera cuestionan el beneficio de él.

Creo que es extremadamente útil para comprender la programación funcional porque le brinda la esencia de la programación funcional. Funciones, aplicación, sustitución. En base a esto, puede desarrollar sus habilidades en razonamiento sobre programas funcionales y transformaciones de ellas. Las funciones de orden superior son muy fáciles.

Claro que podría aprender la programación funcional sin el cálculo de Lambda, pero nunca entenderá realmente la programación funcional sin él.

Answer 2

Está pidiendo una aplicación fuera de la informática y la lógica. Eso se encuentra fácilmente, por ejemplo, en la topología algebraica, es conveniente tener una categoría cartesiana cerrada de espacios, ver Categoría conveniente de espacios topológicos en nlab. El lenguaje formal correspondiente a las categorías cerradas cartesianas es precisamente el $ lambda $ -calculus. Permítanme ilustrar con un ejemplo muy simple cómo esto es útil.

Primero, como ejercicio de calentamiento, suponga que alguien le pregunta si la función $ f: mathbb {r} to mathbb {r} $ definida por $ f (x) = x^2 e^x + log (1 + x^2) $ es diferenciable. En realidad, no tiene que demostrar que lo es, solo observa que es una composición de funciones diferenciables, por lo tanto, diferenciable. En otras palabras, llegó a una conclusión fácil basada en el forma de definición.

Ahora para el ejemplo real. Supongamos que alguien le pregunta si la función $ f: mathbb {r} to mathbb {r} $ definida por $$ f (x) = left ( lambda f: mathcal {c} ( mathbb {r} ). es continuo. Nuevamente, podemos responder inmediatamente "sí" porque la función se define usando $ lambda $ -calculus y comenzando desde mapas continuos $ max $, $ int $, $ sin $, etc.

Varias extensiones del $ lambda $ -calculus hacen posible hacer el mismo tipo de cosas en otras áreas. Por ejemplo, porque un topos suaves es una categoría cerrada cartesiana, cualquier mapa que se define usando el $ lambda $ -calculus, que comienza a partir de derivadas y la estructura del anillo de los reales (y puede tirar la función exponencial si lo desea) es automáticamente suave. (En realidad, el empuje principal de los topos lisos es la existencia de infinitesimales nilpotentes que le permiten decir significativamente cosas como "Diseñamos un disco en triángulos isósceles infinitamente delgados".

Answer 3

Una forma de ver $ lambda $ -calculus es como un modelo simple y breve de programas de parámetros. Parametriza el código en casi cualquier lenguaje de programación que tenga funciones, procedimientos o métodos, y en cualquier lenguaje que tenga módulos o que le permita parametrizar tipos. La parametrización es una forma de reutilización. Debido a que $ lambda $ -calculus es tan simple, los puntos en común entre muchos lenguajes de programación que le permiten parametrizar el código, se destacan especialmente claramente.

Ciertamente es posible ser un muy buen programador sin saber sobre $ lambda $ -calculus, pero te estás perdiendo algo hermoso que también es muy útil.

Answer 4

Microsoft Linq (consulta integrada del lenguaje) Injerta las capacidades de programación funcional en lenguajes de procedimiento. Hace un uso extenso y bastante directo de $ lambda $ -calculus para desenredar dependencias y porciones segregadas del árbol de expresión que se pueden delegar al servidor de la base de datos. Esta es una aplicación extremadamente práctica con alto valor comercial.

He escrito una pequeña aplicación comercial utilizando un lenguaje funcional y puedo asegurarle que, aunque vale la pena para los académicos e investigadores, son menos útiles comercialmente que sus primos de procedimiento. Realmente es una cuestión de caballos para cursos, y lo más práctico de todo es un idioma que puede ser procesal o funcional según sea necesario. Como consecuencia, las capacidades funcionales que se introdujeron (a C#) en apoyo de LINQ, como $ lambda $ -expresiones, obtienen bastante uso fuera del contexto de las consultas de bases de datos.

Entonces, cuando finalmente te encuentres obligado a hacer cosas desagradables porque te gustaría que te paguen, puedes encontrar $ lambda $ -calculus más útil de lo que esperabas, aunque seguramente estás no estar utilizando un lenguaje funcional.

Answer 5

Sin saber más al respecto, escucho que los lingüistas están usando el cálculo de lambda.

http://www.sfu.ca/~jeffpell/ling406/lambdaabstractionoh.pdf, https://files.nyu.edu/cb125/public/lambda/