Large Star Collider

Réalisation de la résolution stellaire.

Réalisation en OCaml

Il faut dans un premier temps traduire Unification.hs en OCaml et bien commenter le programme pour réaliser l'unification entre termes. Tester le programme sur des exemples divers.

L'objectif est de réaliser un modèle de calcul appelé "résolution stellaire" qui fonctionne avec des agents indépendants appelés "étoiles" qui calculent en entrant mutuellement en interaction (de façon asynchrone et concurrente). Ces étoiles ont des termes polarisés attachés appelés rayons. L'interaction détruit les rayons connectés et propage la solution de l'équation associée aux rayons connectés aux rayons adjacents.

Il faudra dans un premier temps comprendre comment le modèle de calcul fonctionne. En particulier, il faudra comprendre la notion de graphe de dépendance, diagramme, de fusion/actualisation et d'exécution de constellation présentée dans l'article de Eng en références.

L'idée de ce projet est que ce modèle de calcul est plutôt difficile à réaliser tel que décrit par la théorie mais qu'il existe en fait une manière beaucoup plus naturelle et satisfaisante de la programmer. Il faut voir le graphe de dépendance comme une sorte d'automate qu'on peut parcourir avec des jetons (voir document PDF dans le dépôt).

Références

• Term Rewriting and All That. Baader, Franz.
• A gentle introduction to Girard's Transcendental Syntax for the linear logician. Eng.