Uno debe, probablemente, también mencionar lenguajes de programación funcional se basa en alguna forma de escrito cálculo lambda como Haskell. Hay un poco de la categoría de la teoría pasando en los sistemas de tipo de estas lenguas, lo que puede ser un terreno familiar y una interesante aplicación de sus conocimientos matemáticos para muchos de los matemáticos.
Por otra parte, de Curry–Howard correspondencia dice que "los tipos son proposiciones" y "términos son pruebas", por lo que uno podría argumentar que la programación en estos lenguajes es la misma como la demostración de teoremas. Este enfoque es especialmente frecuente en dependiente de los lenguajes con tipos como Coq.
Pero tal vez usted no es una categoría teórico o lógico (o al menos no creo que de sí mismo de esa manera). Eso está bien - lenguajes como Haskell son todavía una gran manera de establecer los cálculos matemáticos. Esto es debido a que en Haskell, describiendo a la computadora cómo hacer los cálculos en general es muy similar a la que describen a otros matemáticos de cómo hacer los mismos cálculos!
Como un ejemplo de topología de baja dimensión, considere el siguiente fragmento de código de http://katlas.org/wiki/The_Kauffman_Bracket_using_Haskell, que calcula el Kauffman soporte de un nudo diagrama especifica el uso de la DP en la notación
kauffman :: PD -> R
kauffman [] = one
kauffman (Join a b:pd) | a == b = (-av*av-ai*ai) * kauffman pd
kauffman (Join a b:pd) | otherwise =
kauffman (map (fmap (\c -> if (c == a) then b else c)) pd)
kauffman (Cross a b c d:pd) =
ai * kauffman (Join a b:Join c d:pd)
+ av * kauffman (Join a d:Join b c:pd)
Los últimos cuatro alineado a la izquierda de las líneas de dar cuatro definiciones de la kauffman función.
La primera línea, kaufmann [] = one es un caso base de la especificación de la Kauffman soporte de diagrama vacío. La segunda línea es la regla para la eliminación de distintos círculos, y la cuarta línea es el cruce de axioma. (La tercera línea de tiradores de algunos tecnicismos en la EP notación.)
Si alguna vez has visto una charla en el Kauffman soporte (o el polinomio de Jones) que he visto estos tres axiomas, y que sobre todo tenemos que decirle a Haskell para llegar a calcular Kauffman soportes! Así que, obviamente, hay algo muy atractivo para los matemáticos pasando aquí.
Para los curiosos, algunas características específicas de Haskell (que son comunes entre estáticamente tipado de los lenguajes funcionales) que permiten a este estilo de programación son:
- evaluación diferida;
- tipo de polimorfismo;
- el tratamiento de funciones como valores de primera clase; y
- una buena algebraicas sistema de tipo de datos.
