El cálculo de Lambda no parecía abstracto. Y no puedo ver el punto

18

La pregunta subyacente:

¿Qué hace el cálculo lambda por nosotros que no podemos hacer con las propiedades básicas de la función y la notación generalmente aprendidas en el álgebra de la escuela secundaria?

En primer lugar, ¿qué significa abstracto en el contexto del cálculo lambda? Mi comprensión de la palabra resumen es algo que está divorciado de la maquinaria, el resumen conceptual de un concepto.

Sin embargo, las funciones lambda, al eliminar los nombres de las funciones, evitan un cierto nivel de abstracción. Por ejemplo:

f(x) = x + 2
h(x, y) = x + 5 y

Pero incluso sin definir la maquinaria de estas funciones, podemos hablar fácilmente sobre su composición. Por ejemplo:

1. h(x, y) . f(x) . f(x) . h(x, y) or 
2. h . f . f . h

Podemos incluir los argumentos si queremos, o podemos abstraernos por completo para dar una visión general de lo que está sucediendo. Y podemos reducirlos rápidamente a una sola función. Echemos un vistazo a la composición 2. Puedo tener capas de detalles de estudiantes con las que puedo escribir dependiendo de mi énfasis:

g = h . f . f . h
g(x, y) = h(x, y) . f(x) . f(x) . h(x, y)
g(x, y) = h . f . f . h = x + 10 y + 4

Realicemos lo anterior con cálculo lambda, o al menos definamos las funciones. No estoy seguro de que esto sea correcto, pero creo que la primera y la segunda expresión aumentan en 2.

(λuv.u(u(uv)))(λwyx.y(wyx))x

Y multiplicar por 5 años.

(λz.y(5z))

En lugar de ser abstracto, esto parece entrar en la maquinaria misma de lo que significa sumar, multiplicar, etc. La abstracción, en mi opinión, significa un nivel más alto en lugar de un nivel más bajo.

Además, estoy luchando por ver por qué el cálculo lambda es incluso una cosa. ¿Cuál es la ventaja de

(λuv.u(u(uv)))(λwyx.y(wyx))x

terminado

h(x) = x + 5 y

o una notación combinada

Hxy.x+5y

o incluso la notación de Haskell

h x y = x + 5 * y

Nuevamente, ¿qué hace el cálculo lambda por nosotros que no podemos hacer con las propiedades de función estilo f (x) y la notación con la que muchos están familiarizados?

lambda-calculus programming-paradigms JDG
fuente

9

Es curioso que des un ejemplo de Haskell, ya que Haskell se basa en el cálculo lambda. El cálculo de Lambda no se trata de ninguna notación particular. Es un modelo computacional, equivalente a las máquinas de Turing, en el que "todo es una función".

Yuval Filmus

2

Sí, me dijeron que se basa en el cálculo lambda. La pregunta que todavía tengo que ver respondida de una manera que tiene sentido para mí es por qué haskell se basa en el cálculo lambda en lugar de solo. . . Los atributos básicos de las funciones que aprendí en la escuela primaria. Esa es realmente la esencia de toda esta pregunta.

JDG

66

¿No es "ningún propósito viene a mi mente" casi la definición de "abstracto"? :-)

David Richerby

1

No diría que es despectivo. Ese tratamiento de funciones es útil a través del cálculo. Pero puedo ver cómo ser interpretado como etiquetado como escuela secundaria. Lo ajustaré

JDG

66

Dudo que realmente tenga una definición formal de "notación de función de álgebra de escuela secundaria". Si tiene alguna definición para tales funciones, probablemente sea la teórica establecida que no tiene significado computacional. Parte del objetivo del cálculo lambda es comprender dicha notación en sus propios términos y, me atrevo a decirlo, abstraída de aplicaciones particulares como funciones polinómicas o cálculo.

Derek Elkins salió del SE

24

Hay muchas razones por las que el cálculo lambda es tan importante.

Una razón muy importante es que el cálculo lambda nos permite tener un modelo de computación en el que las funciones computables son ciudadanos de primera clase.

No se pueden expresar funciones de orden superior en el lenguaje del álgebra de la escuela intermedia.

Tome como ejemplo la expresión lambda

λ f . λ g . λ x . f (g (x))

$\lambda f. \lambda g. \lambda x. f(g(x))$

Esta simple expresión nos muestra que, dentro del cálculo lambda, la composición de funciones es en sí misma una función. En álgebra de secundaria, esto no se expresa fácilmente.

En el cálculo lambda, es muy fácil expresar que una función devolverá una función como resultado.

Aquí hay un pequeño ejemplo. La expresión (donde aquí supongo un cálculo lambda aplicado con suma y constantes enteras)

(λ f . λ g . λ x . f ((g (x))) (λ x . x + 2)

$(\lambda f. \lambda g. \lambda x. f((g(x)))(\lambda x. x+2)$

se reducirá a

λ g . λ x . g (x) + 2

$\lambda g. \lambda x. g(x)+2$

Observe también que dentro del cálculo lambda, las funciones son expresiones y no definiciones de la forma . Esto nos libera de la necesidad de nombrar funciones y distinguir entre una categoría sintáctica de expresiones y una categoría sintáctica de definiciones. $f(x) = e$

Además, cuando se hace imposible (o simplemente notoriamente engorroso) expresar funciones de orden superior, uno también tendrá problemas para asignar tipos a expresiones.

La composición de la función tiene el tipo polimórfico

\forall α . \forall β . \forall γ . (β \to γ) \to ((α \to β) \to γ)

$\forall \alpha.\forall \beta. \forall \gamma. (\beta \rightarrow \gamma) \rightarrow ((\alpha \rightarrow \beta) \rightarrow \gamma)$

en el sistema de tipos Hindley-Milner.

Un punto de venta muy fuerte para el cálculo lambda es la noción precisa de cálculo lambda mecanografiado . Los diversos sistemas de tipos para lenguajes de programación funcionales como Haskell y la familia ML se basan en sistemas de tipos para cálculos lambda, y estos sistemas de tipos ofrecen fuertes garantías en forma de teoremas matemáticos:

Si un programa está bien escrito y reduce a la residual , entonces también estará bien tipado. $e$ $e$ $e'$ $e'$

Y si está bien escrito, entonces no exhibirá ciertos errores. $e$ $e$

Las pruebas como correspondencia de programas son particularmente notables. El isomorfismo de Curry-Howard (véase, por ejemplo, https://www.rocq.inria.fr/semdoc/Presentations/20150217_PierreMariePedrot.pdf ) muestra que existe una correspondencia muy precisa entre el cálculo lambda de tipo simple y la lógica proposicional intuitiva: para cada tipo corresponde una fórmula lógica . Una prueba de corresponde a un término lambda con tipo , y una reducción beta de este término corresponde a realizar una eliminación de corte en la prueba. $T$ $\phi_T$ $\phi_T$ $T$

Insto a aquellos que sienten que el álgebra de la escuela intermedia es una buena alternativa al cálculo lambda para que desarrollen una explicación del álgebra de la escuela secundaria de tipo polimórfico de orden superior junto con una noción apropiada del isomorfismo de Curry-Howard. Si incluso puede encontrar un asistente de prueba interactivo basado en álgebra de la escuela intermedia que nos permita probar los muchos teoremas que se han formalizado utilizando asistentes de prueba basados en cálculo lambda como Coq e Isabelle, eso sería aún mejor. Entonces comenzaría a usar el álgebra de la escuela secundaria, y así, estoy seguro, lo harían muchos otros conmigo.

Hans Hüttel
fuente

Esta es una gran explicación. Es útil escuchar que las funciones de orden superior (como la composición) y la escritura están mejor representadas en el cálculo lambda. Es alentador, incluso más que esto facilita las pruebas y el código comprobable. No veo las ramificaciones de gran parte de lo que mencionó y por qué la notación tradicional es inadecuada (por ejemplo, sobre no necesitar una sintaxis de definición separada f (x) = e), sin embargo, es útil que mencione algunas de estas razones y da una idea de qué áreas son mejoradas por el cálculo lambda.

JDG

Por supuesto, se pueden introducir definiciones locales del formulario

let x = e^{'} in e

$\texttt{let}\; x = e' \; \text{in}\; e$ pero estos ya se pueden expresar en la sintaxis del cálculo lambda como

. El cálculo lambda nos permite expresar funciones sin tener que nombrarlas, tal como se puede (¡en el álgebra de la escuela secundaria!) Hablar del número

sin tener que nombrarlas por alguna variable.

(λ x . e) e^{'}

$(\lambda x.e)e'$

4

$4$

Hans Hüttel

5

$\mathbb{R}$ $\mathbb{R}$

Las funciones en el cálculo lambda son mucho más generales. La definición exacta depende de si su cálculo lambda está escrito o no. En cálculo lambda puro sin tipo, todo es una función. Esto es mucho más general que las funciones reales del cálculo.

Incluso los lenguajes de procedimiento a veces usan ideas del cálculo lambda. La función de clasificación en C acepta como parámetro una función de comparación , que utiliza para comparar elementos. El cálculo de Lambda va mucho más allá: las funciones no solo aceptan funciones como entradas, sino que también pueden generarlas.

El cálculo Lambda es un modelo de cálculo equivalente en potencia a las máquinas de Turing. Es un sistema completo en sí mismo. El cálculo lambda puro no tiene "5" o "+" como términos primitivos: se pueden definir dentro del cálculo, al igual que "5" y "+" no son primitivos de la teoría de conjuntos. (Los lenguajes de programación prácticos implementan números naturales de forma nativa por razones de eficiencia).

Sospecho que una de las razones por las que no está impresionado con el cálculo lambda es que sus ideas han impregnado tanto el discurso de programación que ya no parece innovador.

Yuval Filmus
fuente

"Sospecho que esa es una de las razones por las que no estás impresionado con el cálculo lambda" Therin miente la pregunta que estoy haciendo: ¿Qué hace el cálculo lambda por nosotros? En otras palabras, cuando no usamos cálculo lambda, qué sucede. Cuando usamos cálculo lambda, ¿qué ganamos? Si el cálculo lambda fue la primera vez que la gente pensó, ¿qué pasaría si las funciones pudieran crearlas por sí mismas, entonces es impresionante? Entre mis programas iniciales de Python hice texto que contenía funciones que luego evalué, como delegar la tarea de tomar decisiones a otra persona. Parece obvio?

JDG

Esto fue antes de que supiera mucho de nada. Simplemente pensé que era molesto escribir código una y otra vez y que la programación debería ayudarme a generar automáticamente la funcionalidad, incluidas las funciones mismas.

JDG

2

Python admite programación funcional. Los primeros lenguajes de programación no lo hicieron. Si hubiera programado en FORTRAN, no habría creado programas con texto que contenga funciones que luego evaluó. Sin siquiera darte cuenta, hiciste uso de las capacidades proporcionadas por las ideas del cálculo lambda.

Yuval Filmus

2

Eval se originó en LISP , que fue fuertemente influenciado por el cálculo lambda. Algo como esto no es posible en FORTRAN, C, COBOL y muchos otros lenguajes de programación.

Yuval Filmus

Sí, Python admite la programación funcional --- pero no estoy seguro de que su capacidad eval () haya sido inspirada por λCalc --- no debes pensar en λCalc: quiero generar automáticamente el código que puedo evaluar más tarde. Es como decir que λCalc debe pensar: "Le diré a Miranda que use su mejor criterio sobre cómo administrar su departamento", en otras palabras, obtener una función para generar sus propias funciones. No necesita λCalc para pensar en delegar tareas de alto nivel. Si desea hablar sobre la inspiración de λCalc, es un punto más apropiado para las funciones lambda, las comprensiones, etc.

JDG

4

$x^2$ $x$ $x^2$

$\lambda x.x^2$ $x^2$

$f$ $f(x) = x^2$ $f$

El uso de expresiones lambda en lenguajes de programación tiene una ventaja similar; puede escribir lo que hace la función allí donde se necesita, en lugar de tener que definir una función completamente nueva en otro lugar de su programa.

Incluso puedes ver la abstracción lambda implícita en las matemáticas; Por ejemplo, a los estudiantes de cálculo solo se les enseñan derivados de $\frac{d}{dx} x^2$ $\frac{d}{dx}$ $x^2$

$\theta : V \to V^{**}$

θ (v) (F) = F (v)

$\theta(v)(f) = f(v)$

Muchas personas encuentran esta notación de doble evaluación confusa y / o inquietante, así como este uso recursivo de la definición puntual de una función. La versión de abstracción lambda

θ = λ v . λ F . F (v)

$\theta = \lambda v . \lambda f . f(v)$

No tiene ese problema.

Finalmente, existe un teorema del sinsentido abstracto que dice "cálculo lambda simplemente tipado" es básicamente lo mismo que "categoría cerrada cartesiana", por lo que si alguna vez desea realizar cálculos en una categoría cerrada cartesiana, probablemente sea una buena idea usar simplemente escribió cálculo lambda para hacerlo.

fuente

Estoy volviendo a esta pregunta y encuentro esta respuesta genial. Gracias. Las respuestas aquí en general son realmente interesantes.

JDG

4

Diré por adelantado que no soy un experto en este tema, pero acabo de pasar un poco de tiempo estudiándolo y una de las cosas más fascinantes para mí en cualquier tema es la historia detrás de él. Entonces, para mí, comprender un poco de la historia detrás del cálculo lambda ayuda a explicar por qué es útil.

El breve resumen es que a principios del siglo XX después de que la teoría de conjuntos comenzó a despegar y las matemáticas se volvieron a concebir en función de los conjuntos, algunos matemáticos notaron que si bien una definición de teoría de conjuntos te permite afirmar que existe una determinada estructura, no te dicen cómo para construirlo y calcularlo. Entonces las definiciones de teoría de conjuntos no son constructivas . Los matemáticos comenzaron a preguntarse si había una manera de desarrollar definiciones constructivas que irían más allá de demostrar que algo es y, en cambio, probar cómo es .

Desde Wikipedia :

En matemáticas, una prueba constructiva es un método de prueba que demuestra la existencia de un objeto matemático creando o proporcionando un método para crear el objeto. Esto está en contraste con una prueba no constructiva (también conocida como prueba de existencia o teorema de existencia pura) que demuestra la existencia de un tipo particular de objeto sin proporcionar un ejemplo.

$*$

Luego se demostró que el cálculo lambda y la máquina de Turing podrían representar cualquier función computable y, por lo tanto, son equivalentes.

En teoría, cualquier función o concepto matemático puede codificarse en forma de cálculo lambda y calcularse. Esto significa que el cálculo lambda puede ser una base completamente separada para las matemáticas, aunque obviamente es extremadamente tediosa.

El cálculo de Lambda no es "útil" en el sentido de que no va a escribir código usándolo, pero sí forma la base de la semántica denotacional que se usa para describir programas y sus efectos dinámicos. Esto se usa en las discusiones sobre la corrección del programa y el significado semántico. Obviamente, también influyó mucho en el desarrollo de lenguajes de programación funcionales, que extraen todo su concepto de ejecución del cálculo lambda.

Espero que ayude.

Editar para agregar: Acabo de señalar este documento que muestra la relación entre topología, cálculo lambda y física. Leyendo brevemente me encontré con esta fantástica declaración:

Mientras que una máquina de Turing puede verse como un modelo idealizado y simplificado de hardware de computadora , el cálculo lambda es más como un modelo simple de software . ... Poéticamente hablando, el cálculo lambda describe un universo donde todo es un programa y todo son datos: los programas son datos .

El punto es que el cálculo lambda es un modelo idealizado de cómputo de software y, como tal, no está vinculado a una implementación particular en ningún lenguaje de programación. Modela computación pura .

Dave
fuente

Más sobre la historia: Breve historia del cálculo λ en la Stanford Encyclopedia of Philosophy. Tienen más entradas de las que uno puede procesar en la vida.

David Tonhofer

3

$\lambda$

Aristu
fuente

3

El cálculo Lambda no fue diseñado para ser un lenguaje de programación. De hecho, fue creado en la década de 1930, décadas antes de que incluso tuviéramos computadoras programables. Más bien, fue creado como un modelo formal para estudiar computación, en sí mismo. Si está decepcionado de la facilidad con la que expresa el código o las funciones matemáticas, eso es porque no es para eso.

Andrés
fuente

1

"décadas antes incluso teníamos computadoras programables" - mal. La computadora programable existía antes (si no las universales) y las primeras computadoras universales se construyeron durante la década de 1930.

Raphael

-2

El cálculo de Lambda existe para que se puedan crear funciones anónimas (también conocidas como lambda). Si no elimina los nombres de las funciones, el espacio de nombres puede estar abarrotado y uno puede quedarse sin los nombres de las funciones disponibles. Esto es especialmente importante cuando se trata de las llamadas "funciones de orden superior" que devuelven funciones (o punteros de función) por razones obvias.

Esencialmente, las funciones lambda son equivalentes a las variables de ámbito local. La programación funcional sin funciones lambda es análoga a la programación de procedimientos sin ninguna variable local, es decir, una idea terrible.

"por qué el cálculo lambda es incluso una cosa" a los matemáticos les encanta la redundancia. el cálculo lambda rara vez se usa en matemáticas porque, como has descubierto, la notación no es muy útil.

"Si incluso puedes encontrar un asistente de prueba interactivo basado en álgebra de la escuela intermedia que nos permita probar los muchos teoremas que se han formalizado utilizando asistentes de prueba basados en cálculo lambda como Coq e Isabelle, eso sería aún mejor. luego comience a usar el álgebra de la escuela secundaria, y así, estoy seguro, lo harían muchos otros conmigo ". ¿Has oído hablar de metamath? No hay cálculo lambda involucrado allí, puede probar muchos de los teoremas de coq / isabelle

sn
fuente

Aparte de algunas opiniones, ¿qué ofrece esta respuesta?

Raphael

@Raphael Desinformación. La mayor parte de esta respuesta ni siquiera tiene sentido. No hay escasez de nombres. Las "funciones de Lambda" no son equivalentes a las variables de ámbito local; Esto ni siquiera tiene sentido. Supongo que esto se refiere a esto let, pero si bien letpuede codificarse con funciones anónimas, claramente no puede ir a la inversa. La programación funcional no requiere "funciones lambda", por ejemplo, Backus ' FP o Sisal .

Derek Elkins se fue del SE

sobre todo quería publicar un comentario a la respuesta de Hans pero no tenía suficiente karma. así que decidí convertir el comentario en una respuesta completa

sn

El cálculo de Lambda no parecía abstracto. Y no puedo ver el punto

Respuestas: