¿Cuál es la contribución del cálculo lambda al campo de la teoría de la computación?

Solo estoy leyendo sobre el cálculo lambda para "conocerlo". Lo veo como una forma alternativa de cálculo en lugar de la máquina de Turing. Es una forma interesante de hacer cosas con funciones / reducciones (hablando en términos generales). Sin embargo, algunas preguntas me siguen molestando:

• ¿Cuál es el punto del cálculo lambda? ¿Por qué pasar por todas estas funciones / reducciones? ¿Cuál es el propósito?
• Como resultado, me pregunto: ¿qué hizo exactamente el cálculo lambda para avanzar en la teoría de la CS? ¿Cuáles fueron sus contribuciones que me permitieron tener un momento "aha" de comprender la necesidad de su existencia?
• ¿Por qué el cálculo lambda no está cubierto en textos sobre teoría de autómatas? La ruta común es pasar por varios autómatas, gramáticas, máquinas de Turing y clases de complejidad. El cálculo de Lambda solo se incluye en el plan de estudios de los cursos de estilo SICP (¿quizás no?). Pero rara vez he visto que sea parte del plan de estudios central de CS. ¿Esto implica que no es tan valioso? Tal vez no y tal vez me falta algo aquí?

Soy consciente de que los lenguajes de programación funcionales se basan en el cálculo lambda, pero no lo considero una contribución válida, ya que se creó mucho antes de que tuviéramos lenguajes de programación. Entonces, ¿de qué sirve conocer / entender el cálculo lambda, sus aplicaciones / contribuciones a la teoría?

cálculo λ tiene dos roles clave.$\lambda$

• Es una base matemática simple de comportamiento computacional secuencial, funcional y de orden superior.

• Es una representación de pruebas en lógica constructiva.

Esto también se conoce como la correspondencia Curry-Howard . Conjuntamente, la doble visión del cálculo como prueba y como lenguaje de programación (secuencial, funcional, de orden superior), fortalecido por la sensación algebraica del cálculo λ (que no es compartido por las máquinas de Turing), ha llevado a una transferencia masiva de tecnología entre la lógica, los fundamentos de las matemáticas y la programación. Esta transferencia aún está en curso, por ejemplo, en la teoría del tipo de homotopía . En particular, el desarrollo de lenguajes de programación en general, y las disciplinas de escritura en particular, es inconcebible sin $\lambda$$\lambda$$\lambda$-cálculo. La mayoría de los lenguajes de programación tienen cierto grado de deuda con Lisp y ML (por ejemplo, se inventó la recolección de basura para Lisp), que son descendientes directos del cálculo . Una segunda línea de trabajo fuertemente influenciada por el cálculo λ son los asistentes de prueba interactivos .$\lambda$$\lambda$

¿ Hay que saber cálculo para ser un programador competente, o incluso un teórico de la informática? No. Si no le interesan los tipos, los lenguajes de verificación y programación con características de orden superior, entonces probablemente sea un modelo de computación que no sea terriblemente útil para usted. En particular, si está interesado en la teoría de la complejidad, entonces el cálculo λ probablemente no sea un modelo ideal porque el paso de reducción básico ( λ x . M ) N → β M [ N / x ] es poderoso: puede hacer un número arbitrario de copias en N , entonces → $\lambda$$\lambda$

$$(\lambda x.M) N \rightarrow_{\beta} M[N/x]$$ $N$$\rightarrow_{\beta}$Es una noción básica poco realista para explicar el costo microscópico de la computación. Creo que esta es la razón principal por la cual la Teoría A no está tan enamorada del cálculo . Por el contrario, las máquinas de Turing no son muy inspirador para el desarrollo del lenguaje de programación, ya que no existen nociones naturales de la composición de la máquina, mientras que con λ -calculus, si M y N son los programas, entonces también lo es M N . Esta visión algebraica de la computación se relaciona naturalmente con los lenguajes de programación utilizados en la práctica, y gran parte del desarrollo del lenguaje puede entenderse como la búsqueda e investigación de nuevos operadores de composición de programas.$\lambda$$\lambda$$M$$N$$MN$

$\lambda$

$\lambda$$\lambda$

• $\lambda$$\mu$

• $\lambda$

• $\mu$$\lambda$

$\lambda$

¿Qué hizo exactamente el cálculo lambda para avanzar la teoría de CS?

$\lambda$$\lambda$$\lambda$

$\lambda$

$\lambda$

Sus preguntas pueden abordarse desde muchos lados. Me gustaría dejar de lado los aspectos históricos y filosóficos y abordar su pregunta principal, que considero que es la siguiente:

¿Cuál es el punto del cálculo lambda? ¿Por qué pasar por todas estas funciones / reducciones?

¿Cuál es el punto de álgebra booleana, o álgebra relacional, o lógica de primer orden, o teoría de tipo, o algún otro formalismo / teoría matemática? La respuesta es que no tienen un propósito inherente para ellos, incluso si sus diseñadores los crearon para algún propósito u otro. Leibniz, al erigir los cimientos del álgebra booleana, tenía en mente cierto proyecto filosófico ; Boole lo estudió por sus propios motivos. El trabajo de de Morgan en Álgebra Relacional también estuvo motivado por varios proyectos suyos; Peirce y Frege tenían sus propias motivaciones para crear la lógica moderna.

El punto es: cualquiera que sea la razón que la Iglesia pudo haber tenido al crear el cálculo lambda, el punto del cálculo lambda varía de un practicante a otro.

• Para alguien es una notación conveniente para hablar de cálculos; Una alternativa a las máquinas de Turing, etc.

• Para otro, es una base matemática sólida sobre la cual construir un lenguaje de programación más sofisticado (por ejemplo, McCarthy, Stanley).

• Para una tercera persona, es una herramienta rigurosa para dar la semántica de los lenguajes naturales y de programación (por ejemplo, Montague, Fitch, Kratzer).

Creo que el cálculo Lambda es un lenguaje formal que vale la pena estudiar por sí mismo. Puede aprender el hecho de que en el cálculo lambda sin tipo tenemos estas pequeñas bestias llamadas 'combinadores en Y', y cómo nos ayudan a definir funciones recursivas y hacer que la prueba de indecidibilidad sea tan elegante y simple. Puede aprender el sorprendente hecho de que existe una correspondencia íntima entre el cálculo lambda simplemente tipeado y un tipo de lógica intuicionista . Hay muchos otros temas interesantes para explorar (por ejemplo, ¿cómo deberíamos dar la semántica del cálculo lambda? ¿Cómo podemos convertir el cálculo lambda en un sistema deductivo como FOL?)

---

Echa un vistazo a Introducción de Hindley y Seldin a los combinadores y λ-Cálculo para una introducción. The Lambda Calculus de Barendregt es la biblia, así que si estás enganchado después de Hindley y Seldin, hay muchos temas de naturaleza semántica y sintáctica para explorar.

Turing argumentó que las Matemáticas pueden reducirse a una combinación de símbolos de lectura / escritura, elegidos de un conjunto finito y cambiando entre un número finito de "estados" mentales. Reificó esto en sus Máquinas Turing, donde los símbolos se registran en celdas en una cinta y un autómata realiza un seguimiento del estado.

Sin embargo, las máquinas de Turing no son una prueba constructiva de esta reducción. Argumentó que cualquier 'procedimiento efectivo' puede ser implementado por alguna máquina de Turing, y demostró que una máquina universal de Turing puede implementar todas esas otras máquinas, pero en realidad no dio un conjunto de símbolos, estados y reglas de actualización que implementen las matemáticas. en la forma en que argumentó. En otras palabras, no propuso una 'Máquina de Turing estándar', con un conjunto de símbolos estándar que podamos usar para escribir nuestras Matemáticas.

El cálculo de Lambda, por otro lado, es precisamente eso. Church estaba tratando específicamente de unificar las anotaciones utilizadas para escribir nuestras Matemáticas. Una vez que se demostró que LC y TM son equivalentes, podríamos usar LC como nuestra 'Máquina de Turing estándar' y todos podrían leer nuestros programas (bueno, en teoría;)).

Ahora, podríamos preguntarnos por qué tratar el LC como un dialecto primitivo, en lugar de un TM. La respuesta es que la semántica de LC es denotacional : los términos de LC tienen un significado 'intrínseco'. Hay números de la Iglesia, hay funciones de suma, multiplicación, recursión, etc. Esto hace que la LC esté muy bien alineada con la forma en que se practican las Matemáticas (formales), por lo que muchos algoritmos (funcionales) todavía se presentan directamente en la LC.

Por otro lado, la semántica de los programas TM es operativa : el significado se define como el comportamiento de la máquina. En este sentido, no podemos cortar una sección de la cinta y decir "esto es una suma", porque depende del contexto. El comportamiento de la máquina, cuando llega a esa sección de la cinta, depende del estado de la máquina, las longitudes / desplazamientos / etc. de los argumentos, cuánta cinta se usará para el resultado, si alguna operación anterior ha dañado esa sección de la cinta, etc. Esta es una forma horrenda de trabajar ("Nadie quiere programar una Máquina de Turing"), por eso Muchos algoritmos (imperativos) se presentan como pseudocódigo.

otras respuestas son buenas, aquí hay un ángulo / razón adicional para considerar que las mallas con otros pueden ser aún más definitivas, sin embargo, puede ser más difícil de tener en cuenta, ya que los viejos orígenes se pierden en las arenas del tiempo:

precedencia histórica!

El cálculo Lambda se introdujo al menos desde 1932 en la siguiente referencia:

• A. Church, "Un conjunto de postulados para el fundamento de la lógica", Annals of Mathematics, Series 2, 33: 346–366 (1932).

La máquina de Turing se introdujo en ~ 1936 , por lo que el cálculo Lambda es anterior a la aparición de la TM por varios años.

• Turing, AM (1936). "En números computables, con una aplicación al problema de Entscheidungs". Actas de la London Mathematical Society. 2 (1937) 42: 230–265. doi: 10.1112 / plms / s2-42.1.230

en otras palabras, una respuesta básica es que el cálculo Lambda es, en muchos sentidos, el último sistema heredado de TCS. ¡sigue existiendo de la misma manera que Cobol aunque no se desarrolle tanto en el lenguaje! parece ser el primer sistema de computación Turing Complete introducido e incluso es anterior a la idea fundamental de la integridad de Turing. Fue solo un análisis retrospectivo posterior que mostró que el cálculo de Lambda, las máquinas de Turing y el problema de la correspondencia posterior eran equivalentes e introdujeron el concepto de equivalencia de Turing y la tesis de la Iglesia-Turing .

El cálculo de Lambda es simplemente la forma de estudiar la computación desde un punto de vista centrado en la lógica más en términos de representarlo como teoremas matemáticos y derivaciones de fórmulas lógicas, etc. También muestra la profunda relación entre la computación y la recursividad y el acoplamiento más estrecho con la inducción matemática .

Este es un hecho notable porque sugiere que, en muchos sentidos, los orígenes (al menos teóricos ) de la informática fueron fundamentalmente en lógica / matemáticas , una tesis avanzada / expandida en detalle por Davis en su libro Engines of Logic / Mathematicians y los orígenes de la computadora . (por supuesto, los orígenes y el papel fundamental del álgebra booleana también refuerzan aún más ese marco histórico conceptual).

por lo tanto, dramáticamente, ¡incluso se podría decir que el cálculo Lambda es un poco como una máquina del tiempo pedagógica para explorar los orígenes de la informática!

Acabo de encontrar esta publicación y, a pesar de que mi publicación llegó bastante tarde en el día (¡año!), Pensé que quizás mi "valor de un centavo" podría ser de alguna utilidad.

Mientras estudiaba el tema en la universidad, tuve un pensamiento similar al respecto; entonces, le planteé la pregunta de "por qué" al profesor y la respuesta fue: "compiladores". Tan pronto como lo mencionó, el poder detrás de la reducción y el arte de evaluar la mejor manera de manipularla de repente hicieron que el propósito de por qué fuera y siga siendo una herramienta potencialmente útil.

Bueno, por así decirlo fue mi momento "ajá".

En mi opinión, a menudo consideramos lenguajes de alto nivel, patrones, autómatas, complejidad de algoritmos, etc. útiles porque podemos relacionarlos con la 'tarea' en cuestión; mientras que el cálculo de lamdba parece demasiado abstracto. Sin embargo, todavía hay quienes trabajan con idiomas en un nivel bajo, y me imagino que el cálculo lambda, el cálculo de objetos y otras formalizaciones relacionadas los han ayudado a comprender y tal vez desarrollar nuevas teorías y tecnologías de las que el programador promedio puede beneficiarse. De hecho, probablemente no sea un módulo central por esa razón, pero (por las razones que he dicho) habrá unos pocos, además de los académicos, que pueden encontrarlo integral en su carrera profesional en informática.