¿Es el cálculo Lambda puramente sintáctico?

29

He estado leyendo durante algunas semanas sobre el cálculo de Lambda, pero todavía no he visto nada que sea materialmente distinto de las funciones matemáticas existentes, y quiero saber si es solo una cuestión de notación, o si hay alguna nueva propiedades o reglas creadas por los axiomas del cálculo lambda que no se aplican a todas las funciones matemáticas. Entonces, por ejemplo, he leído que:

"Puede haber funciones anónimas" : las funciones de Lambda no son anónimas, solo se llaman lambda. Está permitido en notación matemática usar la misma variable para diferentes funciones si el nombre no es importante. Por ejemplo, las dos funciones en una conexión de Galois a menudo se llaman ambas *.

"Las funciones pueden aceptar funciones como entradas" : no es nuevo, puede hacerlo con funciones ordinarias.

"Las funciones son cajas negras" : solo las entradas y salidas también son descripciones válidas de funciones matemáticas ...

Esto puede parecer una discusión o una pregunta obstinada, pero creo que debería haber una respuesta "correcta" a esta pregunta. Quiero saber si el cálculo lambda es solo una convención de notación o sintáctica para trabajar con funciones matemáticas, o si hay diferencias sustanciales o semánticas entre las funciones lambdas y ordinarias.

Neil
fuente
2
No quiero dar una respuesta completa, pero las funciones no pueden aceptar funciones como entradas. Puedo escribir f (g (0)), pero no puedo escribir f (g, 0). Este último se llama "funcional" y requiere diferentes reglas.
Cort Ammon - Restablece a Monica el
Los funcionales @CortAmmon son funciones. Una función es solo un conjunto de pares (aunque, estrictamente hablando, es un triple (D, R, G) donde D es el dominio R es el rango y G es el gráfico (conjunto de pares), otro pequeño problema que tengo con la respuesta aceptada, pero eso no es ni aquí ni allá). Entonces, si D es un conjunto de funciones y toma pares donde el primer elemento es una función en D, entonces tiene una función. Consulte Wikipedia: "Un funcional es un mapeo [función] ..."
Neil
Es decir, todos los funcionales son funciones, no todas las funciones son funcionales. Pero todas las reglas que se aplican a las funciones se aplican a los funcionales
Neil

Respuestas:

63

Irónicamente, el título está en el punto, pero no en la forma en que parece querer decir que es "el cálculo lambda es solo una convención de notación", lo cual no es exacto.

Los términos lambda no son funciones 1 . Son piezas de sintaxis, es decir, colecciones de símbolos en una página. Tenemos reglas para manipular estas colecciones de símbolos, la reducción beta más significativa. Puede tener varios términos lambda distintos que correspondan a la misma función. 2

Abordaré tus puntos directamente.

Primero, lambda no es un nombre que se está reutilizando. No solo sería extremadamente confuso, sino que no escribimos λ(x) (o (λ x) ), que es lo que haríamos si λ fuera un nombre para una función, al igual que escribimos f(x) . En f(x) podríamos reemplazar f (si estuviera definido por un término lambda) con el término lambda produciendo algo como (λy.y)(x) significa (λy.y) es una expresión que puede representar una función, no una declaración que declara una función (llamadaλ o cualquier otra cosa). En cualquier caso, cuando sobrecargamos la terminología / notación, se hace (es de esperar) de una manera que pueda ser desambiguada a través del contexto, que ciertamente no puede ser el caso para los términos lambda.

Su siguiente punto está bien pero es algo irrelevante. Esta no es una competencia donde hay Términos y Funciones del Equipo Lambda, y solo uno puede ganar. Una aplicación importante de los términos lambda es estudiar y comprender ciertos tipos de funciones. Un polinomio no es una función, aunque a menudo los identificamos descuidadamente. Estudiar polinomios no significa que uno piense que todas las funciones deberían ser polinomios, ni es el caso de que los polinomios tengan que "hacer" algo "nuevo" para que valga la pena estudiarlos.

Las funciones teóricas establecidas no son cajas negras, aunque están completamente definidas por su relación entrada-salida. (Literalmente son la relación de entrada-salida.) Lambda términos tampoco son cajas negras y son no definen por su relación de entrada-salida. Como he mencionado antes, puede tener términos lambda distintos que produzcan la misma relación de entrada-salida. Esto también subraya el hecho de que los términos lambda no pueden ser funciones, aunque pueden inducir funciones. 2

F2 F2F24F2F2F2F22N2N

Esto también se aplica a los términos lambda, podemos interpretarlos como cosas distintas a las funciones. También son objetos mucho más manejables para trabajar que los conjuntos de funciones típicamente infinitas. Ambos son mucho más computacionales que las funciones arbitrarias. Puedo escribir un programa para manipular polinomios (con coeficientes que son representables al menos de manera computable) y términos lambda. De hecho, los términos lambda sin tipo son uno de los modelos originales de funciones computables. Esta perspectiva más simbólica / sintáctica, calculadora / computacional suele estar más enfatizada, especialmente para el cálculo lambda sin tipo , que las interpretaciones más semánticas del cálculo lambda. MecanografiadoLos términos lambda son cosas mucho más manejables y generalmente (pero no siempre) pueden interpretarse fácilmente como funciones teóricas establecidas, pero también pueden interpretarse en una clase de cosas aún más amplia además de funciones que el cálculo lambda sin tipo. También tienen una rica teoría sintáctica propia y una conexión muy profunda con la lógica .

1 Es posible que el problema sea al revés. Tal vez tenga una idea errónea sobre qué es una función.

DDDDDD, y para la categoría de conjuntos no hay objetos reflexivos no triviales. La historia es bastante diferente para los términos tipificados de lambda, pero aún puede ser no trivial.

3 Si tiene clara esta distinción, la analogía debería ser bastante informativa.

4 Este problema no ocurre con los campos de la característica 0, como los números complejos, reales, racionales o enteros, por lo que la distinción no es tan clara, aunque todavía existe.

Derek Elkins
fuente
8
Esta es una respuesta sorprendente, solo tengo que decir. Realmente me aclara algunos largos malentendidos. ¡Gracias!
the0ther
44
¡Ojalá pudiera responder a esto en detalle! Hay muchas cosas que me gustaría seguir. En general, esto fue muy útil para mí, y aparentemente para algunas otras personas también, así que gracias por la respuesta exhaustiva y considerada.
Neil
1
Solo hay un punto con el que tendré problemas aquí, que es su afirmación de que los polinomios no tienen que "hacer" algo "nuevo" para que valga la pena estudiarlos. ¡Por supuesto que lo hacen! Por supuesto, dependiendo de su campo, "nuevo" puede tener diferentes significados (por lo tanto, un matemático puro no distinguirá entre vectores de columna y vectores de fila porque son isomorfos, pero un estadístico puede considerar la distinción como útil para fines de cálculo). Cualquier nuevo formalismo debe justificarse a sí mismo.
Neil
2
@Neil: La nota al pie # 2 en particular ofrece evidencia muy clara de que el cálculo lambda "hace algo nuevo" que las funciones "normales" "no pueden hacer". Para un ejemplo más concreto de una expresión lambda no bien fundada, vea los combinadores de punto fijo . Los números de la Iglesia también hacen una lectura fascinante, especialmente la función predecesora.
Kevin
1
Añadiría que las lambdas como funciones no hacen nada útil. Lo único que puede hacer con una lambda es pasarle una lambda y devolverá una lambda. No tiene forma de probar lo que hace la lambda resultante. Solo puede pasarle otra lambda para obtener otra lambda a cambio. Como funciones, el conjunto de "funciones lambda" se comporta exactamente como un conjunto singleton que contiene solo la función de identidad. Es solo considerando la entrada y salida de una lambda como expresiones que puede diferenciar las lambdas.
Florian F
0

Piensa en el concepto de variables. En idiomas antiguos como básico, no tenía una asignación dinámica y necesitaba un nombre para cada variable. (Esto no es perfectamente exacto porque tenía matrices, pero la idea es que ...) en muchos problemas, debe poder asignar tantas variables como desee, sin estar limitado por la cantidad de nombres que define su programa.

Las funciones de Lambda le permiten deshacerse de la misma limitación sobre los nombres de las funciones, permitiendo que su programa defina tantas funciones como necesite y las "almacene" en las estructuras de datos complejas de Sames como otras variables. Esto no es algo que podría hacer con funciones convencionales con nombre.

Camión
fuente
¿Por qué no puedo hacer esto con funciones con nombre convencionales? Si escribo f(x)=let g(y)=x+y in g, cada matemático sabrá instantáneamente lo que significa y estará de acuerdo en que este es un objeto matemático sensible (quizás hasta algunas objeciones acerca de tener claro el dominio de f). También estarán perfectamente felices si luego escribo el conjunto {f(n) | n ∈ ℕ}, que contiene infinitas funciones y, en particular, no está limitado por tener solo un número finito de nombres para usar.
Daniel Wagner
La pregunta es sobre el cálculo lambda. Si bien está relacionado, eso no es lo mismo que las funciones lambda en los lenguajes de programación.
Andy Dent