¿Es la programación funcional una rama de las matemáticas?

Question

En ¿Teoría principalmente relacionada con el cálculo lambda?, F. G. Dorais escribió sobre la idea de que el cálculo lambda define un dominio de las matemáticas:

Eso nunca se mantendría a menos que haya otra buena razón. Además, el cisma entre ciencias de la computación y matemáticas es muy reciente, yo sostendría que "programación funcional" es en realidad un término matemático, hablando históricamente. Más importante aún, sería incorrecto usar un término diferente al de aquellos que lo utilizan principalmente, es decir, los científicos de la computación teóricos, que por cierto son matemáticos muy competentes.

Creo que la idea es que la superposición entre el tipo de matemáticas constructivas que sigue la correspondencia fórmula-como-tipos, y la programación funcional pura es tan sustancial que el núcleo de los dos temas es esencialmente el mismo sujeto.

¿Es cierto esto?

Answer 1

Entonces, soy un científico informático trabajando en esta área y mi percepción es la siguiente:

No puedes hacer un buen trabajo en programación funcional si eres ignorante de la conexión lógica, punto. Sin embargo, mientras que "pruebas-como-programas" es un eslogan maravilloso, que captura un hecho sumamente importante sobre la estructura a gran escala del tema, no captura todos los hechos sobre los aspectos de la programación.

La razón es que cuando vemos un término lambda como un programa, nos importan adicionalmente sus propiedades intensionales (como el uso de espacio y tiempo de ejecución), mientras que en matemáticas solo nos importan las propiedades extensionales (es decir, la relación que computa). Bubble sort y merge sort son la misma función bajo la lente de la igualdad $\beta\eta$, pero ningún científico informático puede creer que sean el mismo algoritmo.

Espero, por supuesto, que algún día estos factores intensionales ganen significado lógico de la misma manera que las propiedades extensionales ya lo tienen. Pero aún no hemos llegado allí.

[*] Por cierto: Aquí estoy usando "intensional" y "extensional" en un sentido diferente al utilizado en la teoría de tipos de Martin-Löf.

Answer 2

Creo que la mayoría de las personas aquí estarían de acuerdo en que la Teoría de Categorías es parte de las matemáticas.

El estudio de los lenguajes de programación funcional de tipo fuerte es realmente solo el estudio de las categorías cerradas cartesianas, por lo que pienso que esta parte particular de la programación funcional es matemáticas legítimas. Y la Teoría del Dominio es el estudio de la categoría de órdenes parciales completos con inferior, por lo que también la incluiría.

No creo que extendería eso a lenguajes no tipados o de tipado dinámico (LISP). Además, probablemente elegiría un término distinto a "programación funcional", ya que rara vez los subcampos de las matemáticas se nombran con gerundios ("lenguajes funcionales de tipo fuerte" es probablemente el más preciso, pero un poco largo).

Answer 3

Hay trabajo en usar la teoría de categorías monoidales en la programación funcional en lenguajes como Haskell. Además de simplemente utilizar las ideas e implementarlas, desarrollan nuevos marcos para la teoría, nuevas aplicaciones de los teoremas y presentaciones de la teoría. Digo que esto es una rama de las matemáticas, pero es una escala variable dependiendo de cómo la trates.