Básicamente conozco tres fundamentos para las matemáticas.
- Teoría de conjuntos
- Teoría de tipo
- 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.
Respuestas:
[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.
fuente
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:
El documento de Turing de 1936 sobre el problema de la detención . Una construcción teórica para resolver el problema propuesto por Hilbert a principios de siglo, el problema Entscheidungs , es decir, un procedimiento automatizado para resolver problemas matemáticos.
El cálculo lambda de Church desarrollado al mismo tiempo todavía sobrevive en idiomas como lisp y schema
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:
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.
fuente