From e5d7ab02cce5e073506018783ce2a88a9c873b9c Mon Sep 17 00:00:00 2001 From: engboris Date: Wed, 13 Apr 2022 12:49:55 +0200 Subject: [PATCH] Preparation for ocaml --- README.md | 19 +++++++++++++++++-- ArithmeticsPL.hs => haskell/ArithmeticsPL.hs | 0 Main.hs => haskell/Main.hs | 0 PrettyPrinter.hs => haskell/PrettyPrinter.hs | 0 Resolution.hs => haskell/Resolution.hs | 0 Unification.hs => haskell/Unification.hs | 0 ocaml/ecrire_ici | 0 7 files changed, 17 insertions(+), 2 deletions(-) rename ArithmeticsPL.hs => haskell/ArithmeticsPL.hs (100%) rename Main.hs => haskell/Main.hs (100%) rename PrettyPrinter.hs => haskell/PrettyPrinter.hs (100%) rename Resolution.hs => haskell/Resolution.hs (100%) rename Unification.hs => haskell/Unification.hs (100%) create mode 100644 ocaml/ecrire_ici diff --git a/README.md b/README.md index 561cfca..c8b24e3 100644 --- a/README.md +++ b/README.md @@ -1,3 +1,18 @@ -# large-star-collider +# Large Star Collider -Réalisation de la résolution stellaire en Haskell. \ No newline at end of file +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.](https://hal.archives-ouvertes.fr/hal-02977750) \ No newline at end of file diff --git a/ArithmeticsPL.hs b/haskell/ArithmeticsPL.hs similarity index 100% rename from ArithmeticsPL.hs rename to haskell/ArithmeticsPL.hs diff --git a/Main.hs b/haskell/Main.hs similarity index 100% rename from Main.hs rename to haskell/Main.hs diff --git a/PrettyPrinter.hs b/haskell/PrettyPrinter.hs similarity index 100% rename from PrettyPrinter.hs rename to haskell/PrettyPrinter.hs diff --git a/Resolution.hs b/haskell/Resolution.hs similarity index 100% rename from Resolution.hs rename to haskell/Resolution.hs diff --git a/Unification.hs b/haskell/Unification.hs similarity index 100% rename from Unification.hs rename to haskell/Unification.hs diff --git a/ocaml/ecrire_ici b/ocaml/ecrire_ici new file mode 100644 index 0000000..e69de29