Théorie des catégories et analyseurs - références recherchées

Étant donné que je suis intéressé par les analyseurs (principalement les grammaires d'expression des analyseurs), je me demande s'il y a du travail qui donne un traitement catégorique de l'analyse. Toute référence sur les applications de la théorie des catégories à l'analyse syntaxique est très appréciée.

Meilleur,

L'une des toutes premières applications de la théorie des catégories à un sujet en dehors de la géométrie algébrique a été l'analyse syntaxique! Les mots-clés que vous souhaitez guider votre recherche sont "Lambek calculus" et "grammaire catégorielle".

En termes modernes, Joachim Lambek a inventé une logique linéaire non commutative afin de modéliser la structure des phrases. L'idée de base est que vous pouvez donner des parties de base du discours comme ayant des types, puis (par exemple) attribuer aux adjectifs anglais un type de fonction prenant des phrases nominales en phrases nominales. (Par exemple, «vert» est considéré comme une fonction qui prend des noms en noms, ce qui signifie que «œufs verts» est bien typé, car «œufs» est un nom).

La linéarité découle du fait qu'un adjectif prend exactement une phrase nominale comme argument, et la non-commutativité découle du fait que l'ordre des mots dans les phrases est important. Par exemple, l'argument du nom d'un adjectif vient après l'adjectif ("œufs verts"), alors que l'expression nominale d'une phrase prépositionnelle précède les phrases prépositionnelles ("œufs verts avec du ketchup"). En termes catégoriques, vous voulez une catégorie monoïdale (non symétrique) qui est fermée à gauche et à droite. Donc le type est le type d'une phrase qui a le type B , lorsqu'elle est précédée d'un A à gauche, et B / A est le type d'une phrase qui a le type B lorsqu'elle est remplacée par A à droite, et le type A ∗ B est le type d'une phrase faite en concaténant quelque chose de type A avec quelque chose de type$A\setminus{}B$$B$$A$$B/A$$B$$A$$A \ast B$$A$$B$ .

Il s'avère que les grammaires Lambek sont équivalentes aux langages sans contexte, bien qu'apparemment ce résultat soit assez difficile - montrer que les CFG sont un sous-ensemble de grammaires Lambek est facile, mais l'autre direction n'a été établie qu'en 1991 par Pentus.

Un bon exercice ^ H ^ H ^ Hpublication pour le lecteur (c'est-à-dire que je ne l'ai pas essayé, mais je pense que ce serait cool d'essayer) est d'utiliser le calcul de Lambek pour reformuler la présentation de Valiant de l'analyse CYK via la multiplication de matrice booléenne , en catégories termes. Comme motivation, je cite un article de Lambek de 1958 intitulé Les mathématiques de la structure des phrases :

Le calcul présenté ici est formellement identique à un calcul construit par GD Findlay et le présent auteur pour une discussion des mappages canoniques en algèbre linéaire et multilinéaire.

Il semblerait que (sans contexte) l'analyse syntaxique à la Parsec soit naturellement exprimée en termes de classe de type Applicative . À son tour, cette classe est bien décrite par les foncteurs monoïdes dits laxistes forts , qui sont mentionnés dans cette très belle question de théorie et cette belle question de stackoverflow .

Plus généralement, les analyseurs Parsec sont des monades , qui sont si bien connues à la fois dans la théorie CS et la théorie des catégories que je ne vais pas donner de références sauf si on me le demande.