Discreto, Funcional, Implacable...

Como algunos ya saben, desde hace un tiempo he estado interesado en aprovechar las facilidades que trae un lenguaje funcional puro en la enseñanza de las matemáticas discretas. La primera entrada al respecto en este blog está aquí: ( Discretamente hablando: Haskell ). En esta ocasión quiero continuar con esa discusión, planteando una implementación directa del primer tema que se toca en el curso de Estructuras Discretas III de la USB: Los números enteros.

Like a sir, indeed!

Para este curso se usan las muy completas guías que realizó el profesor Yriarte (disponibles en: http://ldc.usb.ve/~yriarte/d2index.html). Que plantean muchos de los conceptos y propiedades importantes en un lenguaje fácil de entender (además que esté en Español, lo cual ayuda mucho a quien no maneja del todo el Inglés). Sin embargo, creo que se puede ir mucho más allá de una guía estática y convertirlo en una ayuda interactiva y flexible mediante el uso de un lenguaje como Haskell.

¿Por qué Haskell? Porque es un lenguaje funcional puro, de muy alto nivel, en el que las definiciones matemáticas abstractas son casi directamente plasmables de forma clara y compacta. Además, el sistema de tipos estático ayuda en gran medida a la correcta definición de las funciones y los tipos de interés. ¿Por que no algo más especializado como Coq o Idris? (Excelente sugerencia de Manuel Gómez en la entrada anterior) Las únicas razones válidas hasta el momento: tiempo y falta de experiencia. Estos lenguajes/herramientas tienen sistemas de tipo mucho más elaborados y rigurosos que permitirían mucha más confianza en las definiciones hechas. Incluso, permitirían la elaboración de pruebas simbólicas en el contexto del mismo lenguaje (ver: Idris: verifying a monoid). Sin embargo, explorar las capacidades de estos lenguajes y de como acotarlas a un nivel que sea a la vez correcto, pedagógico y práctico, es algo que tomaría tiempo y por tanto estaría sujeto a una próxima iteración de cambios.

Antes de comenzar con los temas correspondientes a Estructuras Discretas III, hacen falta algunos preliminares (idealmente, ya se hubiera usado un lenguaje como Haskell al menos en Estructuras Discretas II, pero no es el caso en esta ocasión). En particular: lo que quiere decir poder hacer aritmética sobre un tipo determinado y el tipo de los números naturales. Nótese que hablo de tipos en vez de conjuntos. ¡Esa es una de las principales ventajas del enfoque funcional! Se desliga de la fundamentación en conjuntos (heterogénea y complicada) a una fundamentación en tipos (homogénea y constructiva). Para una discusión mucho más elaborada de esto basta ver cualquier libro de teoría de tipos básica y empezar a notar todas las ventajas. Teorías de tipos más complejas dan aún más comodidades, a expensas de claridad en la presentación y por tanto se intentará mantener la presentación lo más sencilla posible (por ejemplo, la igualdad será considerada una proposición, no un tipo como es costumbre en teoría de tipos).

A continuación un archivo Haskell con la implementación de los preliminares necesarios hasta el momento:

preliminares.hs

A continuación un archivo Haskell con la implementación de los números naturales como números de Church:

naturales.hs

Una vez se han establecido los preliminares, se puede comenzar a tocar temas de Estructuras Discretas III. La primera guía de Yriarte (ver: Capítulo Uno) se trata de los números enteros. En particular, la sección 1.2 los define y plantea algunas propiedades sobre los mismos. A continuación un archivo Haskell con la implementación de los números enteros, según la guía antes mencionada:

enteros.hs

Es notable como poco a poco aumenta el nivel de abstracción hasta el punto que, en la definición de la función valor absoluto (abs), la implementación interna y complicada de números enteros se vuelve completamente transparente. ¡Esta es la belleza de una teoría constructiva!

Desventajas: Hay una inconsistencia entre la definición formal de los números enteros y la que plantea el tipo en Haskell. Los enteros son clases de equivalencia (conjunto cociente del producto N x N con respecto a la relación planteada en la ecuación 1.1). En Haskell, son tratados simplemente como miembros del producto N x N. Esto por varias razones: La guía tiene la misma inconsistencia con respecto a la definición, pues plantea las propiedades y definiciones posteriores en términos de N x N y no del conjunto cociente. Pero la más importante de las razones sería que realmente no encuentro una manera fácil e intuitiva de construir un tipo que corresponda a clases de equivalencia, sin entrar en temas muy oscuros como para una materia introductoria. (Se aceptan sugerencias en este punto).

A través de las definiciones en Haskell se puede notar una falta de estandarización en los nombres. Por ejemplo, a veces las variables son x, y, z... otras son m, n, p... y otras son a, b, c... sin motivo aparente.  Estas son importadas directamente de la guía, para no chocar con los nombres ahí utilizados. Además, algunas proposiciones son "propiedades" y otras son "teoremas". Ambas son demostrables a partir de las definiciones dadas. ¿Por qué la distinción? Ese tipo de detalles y muchas otras cosas más que me parece que faltan me hacen pensar que quizá sea más interesante, en vez de implementar un apoyo a las guían que ya existen, hacer un reboot y reescribir las guías desde un punto de vista funcional. ¡Quizá hasta un libro! Independiente del curso y general para cualquiera interesado en hacer matemáticas discretas desde un punto de vista funcional. Hasta les tengo el nombre ya (hint: el título de esta entrada es un spoiler). Se llamaría "Discreto, Funcional, Implacable..." y me imagino que la portada sería algo como un James Bond sosteniendo un arma que en realidad es un lambda. Pero esos ya son detalles no tan importantes (aunque divertidos. XD).

¿Qué opinan? ¿Va por buen camino? Gracias a muchos comentarios de diversas personas la cosa ha ido tomando forma. Me gustaría seguir recibiendo opiniones con respecto a esto para enriquecerlo y terminar con una propuesta sólida, implementable y divertida. ¡Muchas gracias a todos los que han ayudado (y a los que ayudarán. XD)!

Hasta una próxima entrada. :)