Teoría de categorías y analizadores: se necesitan referencias

Como estoy interesado en los analizadores (principalmente en las gramáticas de expresión de analizadores), me pregunto si hay algún trabajo que ofrezca un tratamiento categórico del análisis. Cualquier referencia sobre aplicaciones de la teoría de categorías al análisis es muy apreciada.

Mejor,

¡Una de las primeras aplicaciones de la teoría de categorías a un tema fuera de la geometría algebraica fue analizar! Las palabras clave que desea orientar su búsqueda son "cálculo de Lambek" y "gramática categorial".

En términos modernos, Joachim Lambek inventó la lógica lineal no conmutativa para modelar la estructura de las oraciones. La idea básica es que puedes dar partes básicas del discurso como tipos, y luego (por ejemplo) atribuir adjetivos en inglés a un tipo de función que lleva frases nominales a frases nominales. (por ejemplo, "verde" se ve como una función que lleva sustantivos a sustantivos, lo que significa que "huevos verdes" está bien escrito, ya que "huevos" es un sustantivo).

La linealidad surge del hecho de que un adjetivo toma exactamente una frase nominal como argumento, y la no conmutatividad surge del hecho de que el orden de las palabras en las oraciones es importante. Por ejemplo, el argumento sustantivo de un adjetivo viene después del adjetivo ("huevos verdes"), mientras que la frase sustantiva de una frase preposicional va antes de las frases preposicionales ("huevos verdes con salsa de tomate"). En términos categóricos, desea una categoría monoidal (no simétrica) que esté cerrada a la izquierda y a la derecha. Entonces el tipo es el tipo de frase que tiene el tipo B , cuando está precedido por una A a la izquierda, y B / A es el tipo de frase que tiene el tipo$A\setminus{}B$$B$$A$$B/A$$B$ cuando lo sucede a la derecha, y el tipo A ∗ B es el tipo de una frase hecha mediante la concatenación de algo de tipo a con algo de tipo B .$A$$A \ast B$$A$$B$

Resulta que las gramáticas Lambek son equivalentes a los lenguajes libres de contexto, aunque aparentemente este es un resultado bastante difícil: mostrar CFG es un subconjunto de gramáticas Lambek es fácil, pero Pentus no estableció la otra dirección en 1991.

Un buen ejercicio ^ H ^ H ^ Hpublicación para el lector (es decir, no lo he probado, pero creo que sería genial intentarlo) es usar el cálculo de Lambek para reformular la presentación de Valiant del análisis CYK a través de la multiplicación de matriz booleana , en forma categórica condiciones. Como motivación, cito el artículo de Lambek de 1958 The Mathematics of Sentence Structure :

El cálculo presentado aquí es formalmente idéntico a un cálculo construido por GD Findlay y el presente autor para una discusión de las asignaciones canónicas en álgebra lineal y multilineal.

Parece que (sin contexto) el análisis a la Parsec se expresa naturalmente en términos declase de tipo Aplicativo . A su vez, esta clase está bien descrita por los llamados functores monoidales laxos fuertes , que se mencionan en esta muy buena pregunta de teoría y en esta buena pregunta de stackoverflow .

En términos más generales, los analizadores Parsec son mónadas , tan conocidos tanto en la teoría CS como en la teoría de categorías que no voy a dar referencias a menos que me lo pidan.