¿Cuáles son algunos artículos disponibles sobre conexiones entre IA y cálculo lambda / teoría de tipos o razonamiento automatizado?

Tengo algunas sugerencias, pero no estoy seguro de que caigan en la “IA clásica”.

Lo primero que me vino a la mente fue HLearn, que es una biblioteca de Haskell para el aprendizaje automático que le permite trabajar con distribuciones como estructuras algebraicas, lo que genera algunos algoritmos nuevos y un código más agradable. Hay un documento de ICML, así como muchos más recursos en la página de GitHub. Sospecho que esto está muy lejos de lo que quieres en la “IA clásica”, así que no sé si se ajusta a tu curso, pero es un proyecto fascinante sobre el que vale la pena leer.

Algo más cercano a la lógica y la verificación para IA, leería sobre sistemas reactivos y especialmente sobre lógica temporal lineal (LTL), programación reactiva funcional (FRP) y la conexión entre los dos. La programación reactiva es una forma natural de modelar un agente que puede interactuar con su entorno, por lo que creo que puede adaptarse tanto a sus intereses como al tema de su curso. FRP es un conjunto ordenado de abstracciones para tratar y razonar sobre sistemas reactivos en un lenguaje funcional. Puede encontrar un montón de documentos generales sobre el tema, pero creo que vale la pena mirar aplicaciones específicas relevantes para la IA como la robótica.

LTL es un tipo de sistema lógico formal para modelar el tiempo . A menudo se usa para cosas como especificar y verificar el comportamiento de sistemas concurrentes, pero también aparece en robótica. No presto mucha atención a las cosas fuera de la esfera PL, pero este documento sobre LTL para la planificación del movimiento parece relevante. LTL también está relacionado con FRP, donde puede darnos una forma formal de razonar sobre la semántica de FRP y también corresponde a él a través del isomorfismo de Curry-Howard. Desafortunadamente, no conozco ningún documento accesible sobre esto, pero podría echar un vistazo a los tipos de LTL FRP para ver cómo LTL ayuda a definir los tipos estáticos para FRP y estas prácticas diapositivas sobre el isomorfismo de Curry-Howard entre los dos.

Una pequeña complicación es que hay múltiples modelos para FRP que involucran abstracciones sutilmente diferentes y es probable que se encuentre con documentos sobre ambos. (De hecho, ambos surgen en las cosas que he vinculado: los documentos de mecanografía hablan sobre Arrowized FRP y las diapositivas hablan sobre Classic FRP). Entonces, si decides mirar FRP, tendrás que hacer una investigación básica por adelantado para descubrir lo que está sucediendo y será bastante difícil.