¿Cómo se relacionan los lenguajes de programación y los fundamentos de las matemáticas?

30

Básicamente conozco tres fundamentos para las matemáticas.

  1. Teoría de conjuntos
  2. Teoría de tipo
  3. Teoría de la categoría

Entonces, ¿de qué manera están relacionados los lenguajes de programación y los fundamentos de las matemáticas?

EDITAR

La pregunta original era "Lenguajes de programación basados ​​en fundamentos matemáticos"

con el paragarph agregado de

E implementaciones de la teoría
1. Teoría de tipos en Coq
2. Teoría de conjuntos en SETL
3. Teoría de categorías en Haskell

Basado en una sugerencia, esto se cambió a "¿Cómo se relacionan los lenguajes de programación y los fundamentos de las matemáticas?"

Como esta es una de esas preguntas en las que no sabía lo suficiente sobre lo que estaba preguntando pero quería aprender algo, estoy modificando la pregunta para que sea más valiosa para el aprendizaje y para los demás, pero dejando los detalles para no hacer el La respuesta actual de Andrej Bauer parece estar fuera de tema.

Gracias por todos los comentarios y la respuesta hasta ahora, estoy aprendiendo de ellos.

Guy Coder
fuente
1
No estoy seguro si entiendo la pregunta o las suposiciones establecidas en ella. Coq no es un lenguaje de programación por lo que yo entiendo. Los programas se pueden extraer de las pruebas de Coq, pero eso no lo convierte en un lenguaje de programación. Además, la teoría de categorías y la teoría de tipos están estrechamente relacionadas, así que no estoy seguro de si podemos clasificarlas como usted. No sé sobre SETL. Vea también la lista de asistentes de pruebas en Wikipedia.
Kaveh
3
Haskell no es "una implementación de la teoría de categorías" y, en cualquier caso, los fundamentos de las matemáticas tienen un propósito diferente al de los lenguajes de programación. Si bien se puede hacer algún tipo de comparación, no es tan bueno tratar de forzar la comparación a una relación formal.
Andrej Bauer
1
Enlace relevante sobre la santa trinidad
cabeza de jardín
De interés: Fundamentos de software
Guy Coder

Respuestas:

29

[Nota: estos párrafos ahora están desactualizados.] El título de su pregunta contiene una suposición injustificada, a saber, que los lenguajes de programación están "basados ​​en fundamentos matemáticos". Este generalmente no es el caso, aunque las dos áreas tienen relaciones importantes. Una afirmación más precisa sería que (algunos) lenguajes de programación fueron diseñados usando técnicas fundamentales. Una mejor pregunta sería "¿cómo se relacionan los lenguajes de programación y los fundamentos de las matemáticas?"

La conexión más general está incorporada en las pruebas de eslogan como programas , que pueden funcionar de varias maneras. La correspondencia de Curry-Howard es la más obvia. Con él relacionamos a la vez la teoría de tipos, la lógica y la programación. Pero debe enfatizarse que la correspondencia de Curry-Howard no funciona muy bien en presencia de recursividad general (porque cada tipo se vuelve habitado), lo que admite todo lenguaje de programación de propósito general.

Una forma más sutil de hacer que las pruebas de eslogan como programas funcionen es utilizar la realizabilidad . Aquí también relacionamos pruebas y programas, pero ahora la dirección va de las pruebas a los programas: cada prueba proporciona un programa, pero no todos los programas son necesariamente una prueba.

El ejemplo principal de un lenguaje de programación basado en una base es Agda , que simplemente es una implementación de la teoría del tipo dependiente. Sin embargo, Agda no es un lenguaje de programación de propósito general porque no admite la recursividad general. Cada función en Agda es total, y hay funciones computables que no se pueden implementar en Agda. En la práctica, los programadores no notarán esto, pero notarán que Agda no permite valores indefinidos, por ejemplo, bucles infinitos.

Coq no es un lenguaje de programación sino un asistente de pruebas. Sin embargo, también tiene capacidades de extracción que proporcionan programas a partir de pruebas. Los asistentes de prueba y los lenguajes de programación no deben confundirse entre sí.

No debemos olvidar que Prolog y otros programación lógica idiomas se inspiran en la idea de que la computación es una prueba de búsqueda . Por supuesto, esto los relaciona estrechamente con la lógica.

Haskell es un lenguaje de programación de propósito general que se basa en la teoría de dominios . Es decir, su semántica es teórica de dominio porque tiene que tener en cuenta las funciones parciales y la recursividad. La comunidad de Haskell ha desarrollado una serie de técnicas inspiradas en la teoría de categorías, de las cuales las mónadas son más conocidas pero no deben confundirse con las mónadas . En términos más generales, las características de programación avanzadas generalmente se tratan con una combinación de teoría de dominio y teoría de categoría, pero esto no es algo en lo que el programador de Haskell en la calle sea experto. La llamada "categoría sintáctica" de los tipos de Haskell es la visión de un laico de cómo Haskell y la teoría de la categoría se corresponden entre sí.

La teoría de conjuntos (clásica o constructiva) parece inspirar ideas en lenguaje de programación en menor medida. Por supuesto, la teoría de conjuntos constructivos tiene su conexión con la programación a través de la lógica constructiva. Alex Simpson dio una aplicación importante de la teoría intuitiva de conjuntos a los lenguajes de programación, que la utilizó para hacer que la teoría del dominio sintético funcionara. Pero esto es algo bastante avanzado, tal vez vea estas diapositivas . Jean-Louis Krivine ha desarrollado una marca muy interesante de realizabilidad para la teoría de conjuntos clásica. Esta parece una buena manera de relacionar la teoría de conjuntos clásica y la programación.

En resumen, la teoría de los lenguajes de programación utiliza técnicas fundamentales. Esto no es sorprendente, ya que consideramos que la computación es un concepto fundamental. Pero es demasiado ingenuo decir que los lenguajes de programación están "basados" en ciertos fundamentos. De hecho, la tricotomía de fundamentos "teoría de conjuntos - teoría de tipos - teoría de categorías" es nuevamente una observación útil de alto nivel que puede hacerse matemáticamente precisa de varias maneras, pero no hay nada necesario al respecto. Es un accidente histórico.

Andrej Bauer
fuente
"La idea de que el cálculo es la búsqueda de pruebas ". Estoy confundido por esta declaración. Seguramente, la búsqueda de prueba es una forma de cálculo, pero ¿no todo el cálculo es búsqueda de prueba? En el contexto de esta pregunta, también hay verificación de prueba, verificación de tipo. Más generalmente, simplemente la adición de 5 + 3. ¿Qué quieres decir con esta afirmación?
user56834
6

Este es un tema muy complejo y hay muchos libros excelentes sobre el tema, uno reciente llamado Catedral de Turings, orígenes del universo digital y también Motores de lógica, matemáticos y orígenes de la computadora .

Los lenguajes informáticos han evolucionado durante muchas décadas, pero créanlo o no, hay dos lenguajes de programación originales que muestran que las matemáticas y la informática están íntimamente entrelazadas:

Hay dos figuras clave que cruzaron los límites matemáticos y de la informática con los "lenguajes de programación":

  • La teoría de la información iniciada por Shannon muestra las profundas conexiones entre las matemáticas y la informática.

  • Otra figura clave que cruza entre las matemáticas y la informática es Von Neumann . inventó la arquitectura von neumann para almacenar programas en la memoria.

incluso "lenguajes de programación" anteriores:

  • La palabra inglesa "computadora" originalmente significaba algo más como una "calculadora" que usaba operaciones matemáticas en números y su significado se ha desplazado sustancialmente al concepto de programación de propósito general de hoy. entonces hay una conexión entre lenguajes de programación y calculadoras tempranas.
  • Las tarjetas perforadas utilizadas en telares de finales del siglo XIX y principios del XX fueron un "lenguaje de programación" para tejer patrones. Tenga en cuenta que las tarjetas perforadas se usaron para programar mainframes mucho en la década de 1960. Estos fueron vistos originalmente como "máquinas calculadoras" (¡usando matemáticas!) no como computadoras modernas de uso general.
  • Babbage y Ada Lovelace desarrollaron los primeros conceptos rudimentarios de "lenguajes de programación" a mediados de 1800 en un "motor de cálculo"
  • el álgebra booleana fue originalmente un concepto puramente matemático inventado por Boole
  • El antiguo ábaco (milenario) para el cálculo matemático es visto como un precursor de la computadora moderna. pero se podría decir que las operaciones para manipularlo eran una especie de "lenguaje de programación" (seguido por humanos)

sin embargo, en los lenguajes de programación modernos a medida que la abstracción ha aumentado y escalado, la conexión clara y directa con las matemáticas ha disminuido un poco a lo largo de las décadas, pero siempre será bastante intrínseca y, de alguna manera, se ha fortalecido. por ejemplo, los lenguajes como Java con sus tipos estrictos tienen conexiones con las matemáticas, y al comienzo a fines de la década de 1990, los lenguajes informáticos convencionales (por ejemplo, c ++, Java, Ruby, etc.) comenzaron a implementar explícitamente muchos objetos matemáticos de nivel superior como primitivos cercanos en el idiomas como conjuntos, árboles (por ejemplo, Btrees o hashmaps), etc.

vzn
fuente