Generación de optimizaciones del compilador a partir de pruebas es un documento maravilloso. Los autores dicen que se enfrentaron al problema, se atascaron y luego intentaron razonarlo utilizando la teoría de categorías. Tomaron el camino obvio, aislaron la nueva idea, diseñaron el algoritmo abstracto y lo aplicaron a su caso concreto.
¿Qué otros ejemplos como éste conoce, en los que la teoría de categorías haya desempeñado claramente un papel en la producción de un algoritmo no trivial?
El hermoso y ya clásico papel Teoremas gratis de Philip Wadler introduce -o mejor dicho, elabora muy ricamente- la idea de que el conocimiento del tipo de una función puede utilizarse para descubrir algunas de sus propiedades. En ese artículo, el lenguaje es el de los cálculos lambda tipados, pero en trabajos posteriores él y otros lo reformularon, de forma muy natural, en el lenguaje de la teoría de categorías (transformaciones naturales laxas y cosas así)
Las propiedades de las funciones deducidas de sus tipos de ese modo pueden ser y son utilizadas por los compiladores de lenguajes funcionales en el proceso de optimización.
Más tarde. Por supuesto, todo el "movimiento mónada" visto en el contexto de los lenguajes funcionales también es un ejemplo, así como lo de la "flecha" posterior. La biblioteca de analizadores sintácticos autooptimizados de S. Doaitse Swierstra, que es algo inequívocamente categórico, es un ejemplo extraordinario de las abstracciones de la teoría de categorías puestas en uso para tratar problemas algorítmicos de la vida real.
Me alegro de que te haya gustado el periódico. Pensé que te gustaría saber que los algoritmos de mis dos artículos sobre PLDI se diseñaron utilizando un marco teórico categorial que creé para los tipos existenciales (la mitad de los cuales resultaron ser opfibraciones, pero yo no las conocía en ese momento). Otros me lo han pedido, así que finalmente cedo y publico el trabajo en curso en mi página de Lenguaje ensamblador tipado orientado a objetos inferible , ya que ese es el problema que me impulsó a hacer el marco una vez que me quedo atascado. Sólo tienes que buscar "Cuantificación Existencial Inferible". Espero que os guste.
Una cosa que voy a señalar es que, según mi experiencia, la teoría "algorítmica" de categorías (en contraposición a la teoría "teórica de tipos" y la teoría "semántica" de categorías) se basa en gran medida en la teoría concreta de categorías. Al fin y al cabo, muchos algoritmos trabajan con conjuntos estructurados de algún tipo. Por tanto, las técnicas disponibles para un algoritmo a menudo dependen de si la categoría concreta es topológica o algebraica, más que de si es cerrada. Hay muchas cosas que muestran qué tipo de estructuraciones preservan cosas como la existencia de pushouts y pullbacks, pero creo que sería muy interesante (y útil) identificar también qué tipo de estructuraciones preservan la constructibilidad/decidibilidad de pushouts y pullbacks. Sabiendo eso, podríamos construir algoritmos para un dominio simplemente mostrando cómo se puede construir el dominio a partir de una secuencia de estructuraciones que preserven la constructibilidad y que, en consecuencia, garanticen la presencia de las estructuras particulares requeridas por el algoritmo. Si alguien conoce ya una investigación de este tipo, me interesaría mucho verla.
I-Ciencias es una comunidad de estudiantes y amantes de la ciencia en la que puedes resolver tus problemas y dudas.
Puedes consultar las preguntas de otros usuarios, hacer tus propias preguntas o resolver las de los demás.
