¿Por qué es importante que las funciones sean anónimas en el cálculo lambda?

Estaba viendo la conferencia de Jim Weirich, titulada ' Aventuras en la programación funcional '. En esta conferencia, introduce el concepto de combinadores Y, que esencialmente encuentra el punto fijo para funciones de orden superior.

Una de las motivaciones, como él lo menciona, es poder expresar funciones recursivas usando el cálculo lambda para que la teoría de Church (cualquier cosa que sea efectivamente computable pueda ser calculada usando el cálculo lambda) permanezca.

El problema es que una función no puede llamarse simplemente así, porque el cálculo lambda no permite funciones con nombre, es decir,

no puede llevar el nombre ' ', debe definirse de forma anónima:$n$

¿Por qué es importante que el cálculo lambda tenga funciones que no tienen nombre? ¿Qué principio se viola si hay funciones con nombre? ¿O es que acabo de entender mal el video de Jim?

El teorema principal con respecto a este tema se debe a un matemático británico de finales del siglo XVI, llamado William Shakespeare . Su artículo más conocido sobre el tema se titula " Romeo y Julieta " fue publicado en 1597, aunque el trabajo de investigación se realizó unos años antes, inspirado pero precursores como Arthur Brooke y William Painter.

Su principal resultado, declarado en el Acto II. Escena II , es el famoso teorema :

¿Lo que hay en un nombre? lo que llamamos una rosa con
cualquier otro nombre olería tan dulce;

Este teorema puede entenderse intuitivamente como "los nombres no contribuyen al significado".

La mayor parte del artículo está dedicada a un ejemplo que complementa el teorema y muestra que, aunque los nombres no aportan ningún significado, son la fuente de problemas interminables.

Como en punta a cabo por Shakespeare, los nombres se pueden cambiar sin cambiar el significado, una operación que más tarde fue llamado -Conversión$\alpha$ por Alonzo Church y sus seguidores. Como consecuencia, no es necesariamente simple determinar qué se denota con un nombre. Esto plantea una variedad de problemas, como el desarrollo de un concepto de entorno donde se especifican las asociaciones de significado y nombre, y las reglas para saber cuál es el entorno actual cuando intenta determinar el significado asociado con un nombre. Esto desconcertó a los informáticos durante un tiempo, dando lugar a dificultades técnicas como el infame problema de Funarg.. Los entornos siguen siendo un problema en algunos lenguajes de programación populares, pero generalmente se considera físicamente inseguro como más específico, casi tan letal como el ejemplo elaborado por Shakespeare en su artículo.

Este problema también está cerca de los problemas planteados en la teoría del lenguaje formal , cuando los alfabetos y los sistemas formales deben definirse hasta un isomorfismo , para subrayar que los símbolos de los alfabetos son entidades abstractas , independientes de cómo se "materializan" como elementos de algún conjunto.

Este importante resultado de Shakespeare muestra también que la ciencia estaba divergiendo de la magia y la religión, donde un ser o un significado pueden tener un nombre verdadero .

La conclusión de todo esto es que, para el trabajo teórico, a menudo es más conveniente no ser gravado por nombres, a pesar de que puede parecer más simple para el trabajo práctico y la vida cotidiana. Pero recuerda que no todos los que se llaman mamá son tu madre.

Nota :
El problema fue abordado más recientemente por el lógico estadounidense del siglo XX Gertrude Stein . Sin embargo, sus colegas matemáticos todavía están reflexionando sobre las implicaciones técnicas precisas de su teorema principal :

Rose es una rosa es una rosa es una rosa.

publicado en 1913 en una breve comunicación titulada "Sacred Emily".

$\lambda$$\lambda$$\pi$$\nu x.P$$\pi$

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

$\mathsf{let} f = M \mathsf{in} N$$(\lambda f.N)M$$\lambda$

Creo que la idea es que los nombres no son necesarios. Cualquier cosa que parezca requerir nombres puede escribirse como funciones anónimas.

Puedes pensar en el cálculo lambda como lenguaje ensamblador. Alguien en una conferencia sobre ensamblaje podría decir "No hay árboles de herencia orientados a objetos en lenguaje ensamblador". Entonces puede pensar en una forma inteligente de implementar árboles de herencia, pero ese no es el punto. El punto es que no se requieren árboles de herencia en el nivel más básico de cómo se programa una computadora física.

En el cálculo lambda, el punto es que no se requieren nombres para describir un algoritmo en el nivel más básico.

Estoy disfrutando de las 3 respuestas aquí hasta ahora, especialmente el análisis de Shakespearen de @ babou, pero no arrojan luz sobre lo que creo que es la esencia de la pregunta.

El cálculo de λ une nombres a funciones cada vez que aplica una función a una función. El problema no es la falta de nombres.

"El problema es que una función no puede llamarse a sí misma simplemente" al referirse a su nombre.

(En Lisp puro, el enlace nombre -> función no está dentro del alcance del cuerpo de la función. Para que una función se llame a sí misma por su nombre, la función tendría que referirse a un entorno que se refiera a la función. Lisp puro no tiene estructuras de datos cíclicas. Impure Lisp lo hace mutando el entorno al que se refiere la función).

Como señaló @MartinBerger, la razón histórica por la que el cálculo λ no permite que una función se llame a sí misma por su nombre fue un intento de descartar la paradoja de Curry al intentar usar el cálculo λ como base de las matemáticas, incluida la lógica deductiva. Esto no funcionó ya que técnicas como el combinador Y permiten la recursión incluso sin autorreferencia.

De Wikipedia:

Si podemos definir la función r = (λ.x x x ⇒ y)entonces r r = (r r ⇒ y).

Si r res verdad, entonces yes verdad. Si r res falso, entonces r r ⇒ yes cierto, lo cual es una contradicción. Entonces, yes cierto y, como ypuede ser cualquier afirmación, cualquier afirmación puede probarse que es cierta.

r res un cálculo sin terminación. Considerada como lógica r res una expresión para un valor que no existe.