diff --git a/content/_index.md b/content/_index.md index bf57927..4a89905 100644 --- a/content/_index.md +++ b/content/_index.md @@ -3,21 +3,20 @@ title: TS Guide type: docs --- -# Welcome to TS Guide +# Bievenue -The purpose of this guide is to make you familiar with Girard's recent works -through programming and exercises. +L'objectif de ce guide est de vous familiariser avec les derniers travaux +de Girard à travers la programmation et des exercices simples. -Note that everything in this guide is my own interpretation and is not -necessarily perfect faithful to Girard's point of view. +Le contenu de ce guide n'est que ma propre interprétation et n'est probablement +pas parfaitement fidèle au point de vue original de Girard. -Also keep in mind that the development of transcendental syntax is currently -very unstable. For that reason, this guide is subject to constant changes. -I created this guide because I wanted other people to be part of the process of -understanding Girard's transcendental syntax by playing with it and developing -new ideas. - -Enjoy! +Gardez aussi à l'esprit que le développement de la syntaxe transcendantale est +actuellement très instable. Ce guide sera donc sujet à de nombreux changements. +J'ai crée ce guide car je voulais que d'autres personnes puissent participer +à la compréhension et au développement de la syntaxe transcendantale en jouant +avec pour développer de nouvelles idées. +Amusez-vous bien ! Boris Eng. \ No newline at end of file diff --git a/content/docs/introduction/about.md b/content/docs/introduction/about.md new file mode 100644 index 0000000..9591e89 --- /dev/null +++ b/content/docs/introduction/about.md @@ -0,0 +1,18 @@ +--- +title: "A propos" +weight: 1 +--- + +# A propos + +## Syntaxe transcendantale + +(soon) + +## Résolution stellaire + +(soon) + +## Large star collider + +(soon) \ No newline at end of file diff --git a/content/docs/introduction/install.md b/content/docs/introduction/install.md index 17f9b4b..7aa90ef 100644 --- a/content/docs/introduction/install.md +++ b/content/docs/introduction/install.md @@ -1,16 +1,18 @@ --- -title: Install LSC +title: Installer le LSC weight: 2 --- -# Install LSC +# Installer le LSC -To install the Large Star Collider (LSC), go to this git repository: +Pour installer le Large Star Collider (LSC), aller sur ce dépôt git : https://github.com/engboris/large-star-collider -You can either compile the LSC from sources or download a released binary. -- For Linux x86-x64: https://github.com/engboris/large-star-collider/tags +Vous pouvez soit compiler à partir des sources ou alors télécharger un +exécutable pré-compilé : +- Pour Linux x86-x64: https://github.com/engboris/large-star-collider/releases -You can then write your programs on any text file and follow the instructions -in the `README.md` file of the Github repository to execute them! +Vous pouvez ensuite simplement écrire vos programmes dans n'importe quel +fichier texte et suivre les instructions dans le fichier `README.md` du dépôt +git pour exécuter vos programmes ! \ No newline at end of file diff --git a/content/docs/introduction/what.md b/content/docs/introduction/what.md deleted file mode 100644 index b0af777..0000000 --- a/content/docs/introduction/what.md +++ /dev/null @@ -1,18 +0,0 @@ ---- -title: "What it is about" -weight: 1 ---- - -# What it is about - -## Transcendental syntax - -(soon) - -## Stellar resolution - -(soon) - -## Large star collider - -(soon) \ No newline at end of file diff --git a/content/docs/playing/_index.md b/content/docs/playing/_index.md index 38bfe7f..b1b267c 100644 --- a/content/docs/playing/_index.md +++ b/content/docs/playing/_index.md @@ -1,5 +1,5 @@ --- -title: "Playing with stars" +title: "Jouer avec les étoiles" bookFlatSection: true weight: 1 --- diff --git a/content/docs/playing/configure.md b/content/docs/playing/configure.md new file mode 100644 index 0000000..dbcbb23 --- /dev/null +++ b/content/docs/playing/configure.md @@ -0,0 +1,54 @@ +--- +title: "Configurer l'interaction" +weight: 3 +--- + +# Auto-interaction + +Il peut arriver que vous vouliez autoriser le branchement de deux rayons +au sein d'une même étoile. On pourrait, par exemple obtenir l'interaction +suivante (normalement impossible) : +``` +<0,1> -f(X) +f(a) X == a +``` + +Pour cela, il suffit d'utiliser l'option `-allow-self-interaction` : +``` +lsc.exe -allow-self-interaction filename.stellar +``` + +# Debug + +## Affichage des étapes + +L'option `-show-steps` affiche chaque étape d'interaction. Ces étapes sont +calculées pour chaque sélection d'étoile de l'espace d'interaction menant à +une interaction effectivement. + +Dans le cas où plusieurs interactions sont possibles, on peut constater une +duplication. + +## Affichage de la trace + +L'option `-show-trace` affiche les détails de chaque sélection de rayons dans +l'espace d'interaction et dans la constellation de référence en précisant +quelle était la solution de l'équation entre rayons (à renommage près des +variables pour les rendre distinctes). + +## Affichage du calcul incomplet + +Par défaut, les étoiles contenant des rayons polarisés sont effacés après +exécution. De telles étoiles représentent des calculs qui n'ont pas réussi à +se compléter. + +Il est tout de même possible d'afficher ces étoiles avec l'option +`-show-unfinished-computation`. + +Ainsi, l'éxecution de la constellation `+g(a) -f(X); @+f(a)` produirait : +``` ++g(a); +``` +au lieu de la constellation vide : +``` +{} +``` \ No newline at end of file diff --git a/content/docs/playing/elementary.md b/content/docs/playing/elementary.md new file mode 100644 index 0000000..82aa28b --- /dev/null +++ b/content/docs/playing/elementary.md @@ -0,0 +1,107 @@ +--- +title: "Interactions élémentaires" +weight: 4 +--- + +# Interactions élémentaires + +Ouvrez votre éditeur de code favori et pratiquons avec le LSC ! + +## Fusion + +Une interaction simple entre deux étoiles avec transfert de la constante `a` : +``` ++f(X) X; 's1 +@-f(a); 's2 +``` + +Les deux étoiles `s1` et `s2` se sont fusionnées en interagissant le long de +`+f(X)` et `-f(a)` (d'unificateur `{X:=a}`) laissant `X{X:=a} = a` en résultat. + +On peut étendre ce transfert en traversant plusieurs étoiles : + +``` ++f1(X1) X1; +-f1(X2) +f2(X2); +-f2(X3) +f3(X3); +@-f3(a); +``` + +## Effacement + +Pour rappel, les étoiles qui contiennent des rayons polarisés sont effacés du +résultat de l'exécution. Cela permet donc de pouvoir gérer l'effacement ou la +conservation d'étoiles. + +``` ++f(X) +g(X); +@-f(a); +``` + +Ci-dessus, on a bien une interaction, mais le résultat est un rayon polarisé +qui attend d'être connecté. On obtient donc `{}` comme résultat. + +On peut rajouter une étoile afin d'obtenir un résultat : + +``` +-g(X) X; ++f(X) +g(X); +@-f(a); +``` + +## Multi-focus + +On peut utiliser plusieurs focus pour effectuer plusieurs calculs en parallèle : + +``` ++f(a); ++g(X) -g1(X); ++g1(X) -g2(X); ++g2(b); ++h(c); + +@-f(X) X; +@-g(X) X; +@-h(X) X; +``` + +## Duplication + +Il se peut qu'un même rayon de l'espace d'interaction soit compatible avec +deux rayons de deux étoiles différentes de la constellation de référence. Dans +ce cas, il y a une duplication : + +``` +-f(a); +-f(b); +@+f(X) X; 'étoile dupliquée +``` + +Une telle duplication est une "bifurcation" puisqu'elle génère deux étoiles +vues comme deux choix non-déterministes matérialisés dans deux branches +disjointes `a; b`. + +Cependant, il est aussi possible d'avoir une duplication "déterministe" au sein +d'une même étoile : + +``` ++f(a) +f(b); +g(a); @+g(b); +-f(X) -g(X) 0; 'étoile dupliquée +``` + +## Boucles + +Il est possible de faire des boucles infinies : +``` +-f(X) +f(X) 0; +@-f(X); +``` + +Mais aussi finies en faisant décroître un argument à chaque interaction et en +définissant une étoile en charge de l'arrêt de la boucle (comme en programmation +logique et fonctionnelle) : +``` ++f(0); +-f(X) +f(g(X)) 0; +@-f(g(g(g(0)))); +``` \ No newline at end of file diff --git a/content/docs/playing/exercices.md b/content/docs/playing/exercices.md new file mode 100644 index 0000000..aa5af71 --- /dev/null +++ b/content/docs/playing/exercices.md @@ -0,0 +1,14 @@ +--- +title: "Exercices" +weight: 5 +--- + +# Exercices + +## Chemins + +## Effacement partiel + +## Altération de mémoire + +## Tables de vérité \ No newline at end of file diff --git a/content/docs/playing/interaction.md b/content/docs/playing/interaction.md index f489f1a..5744905 100644 --- a/content/docs/playing/interaction.md +++ b/content/docs/playing/interaction.md @@ -3,20 +3,22 @@ title: "Interaction" weight: 2 --- -# Matchable rays +# Rayons compatibles -Usually, in the theory of term unification, we say that two terms (which are -basically rays without polarities) are *unifiable* where there a substitution -of variables making them equal. For instance `f(X)` and `f(h(Y))` are unifiable -with the substitution `{X:=h(Y)}` replacing `X` by `h(Y)`. +Dans la théorie de l'unification, on dit que deux termes +(qu'on peut voir comme des rayons sans polarités) sont *unifiables* lorsqu'il +existe une substitution des variables de telle sorte à les rendre égaux. +Par exemple, `f(X)` et `f(h(Y))` sont unifiables avec la substitution +`{X:=h(Y)}` remplaçant `X` par `h(Y)`. -We are usually interested in the most general substitution. We could have -`{X:=h(c(a)); Y:={c(a)}` but it would be less general. +Les substitutions d'intérêt sont les plus générales. Nous aurions pu considérer +la substitution `{X:=h(c(a)); Y:={c(a)}`, tout aussi valide mais inutilement +précise. -In the same fashion, we say that two rays are *matchable* when their underlying -terms (obtained by dropping polarities) are unifiable but we also want opposite -polarities to face each other instead of looking for equal symbols: we want -symbols prefixed with `+` to match same symbols but prefixed with `-`: +Dans la même idée, ici, nous disons que deux rayons sont *compatibles* lorsque +leur terme sous-jacent (obtenu par oubli des polarités) sont unifiables mais +nous voulons aussi que des symboles de fonctions de polarités opposées se +rencontrent (au lieu de considérer des symboles identiques): - `+f(X)` and `-f(h(a))` are matchable with `{X:=h(a)}`; - `f(X)` and `f(h(a))` are not matchable; @@ -26,72 +28,86 @@ symbols prefixed with `+` to match same symbols but prefixed with `-`: # Fusion -Stars are able to interact, through an operation called *fusion*, by using the -principle of Robinson's resolution rule. We define an operator `` with -connects the `i`th ray of a star to the `j`th ray of another star. +Les étoiles interagissent au travers d'une opération appelée *fusion*, en +utilisant le principe de la règle de résolution de Robinson. On définit un +opérateur `` connectant le `i`ème rayon d'une étoile au `j`ème rayon d'une +autre étoile. -Fusion is defined as follows for matchable rays `r` and `r'`: +La fusion est définie ainsi pour deux rayons compatibles `r` et `r'`: ``` r r1 ... rk <0,0> r' r1' ... rk' == theta(r1) ... theta(rk) theta(r1') ... theta(rk') ``` -where `theta` is the most general substitution induced by `r` and `r'`. +où `theta` est la substitution la plus générale induite par `r` et `r'`. -Notice that: -- `r` and `r'` interact and are annihilated; -- the two stars are merged; -- the substitution resolving the conflict between `r` and `r'` is propagated to -adjacent rays. +Remarquez que: +- `r` et `r'` sont annihilées pendant l'interaction; +- leurs deux étoiles fusionnent; +- la substitution obtenue par résolution du conflit entre `r` et `r'` est +propagée aux rayons adjacents. -For example: +Exemple : ``` X +f(X) <1,0> -f(a) == a ``` {{< hint info >}} -This corresponds to the cut rule for first-order logic except that we are -in a logic-agnostic setting (our symbols do not hold any meaning). +Cette opération de fusion correspond à la règle de compure pour la logique +du premier ordre. Cependant, la différence ici est que nous sommes dans un +cadre "alogique" (nos symboles ne portent aucun sens logique). {{< /hint >}} -# Execution +# Exécution -You have to put a focus on some stars to start a computation as in: +Il faut poser un focus sur les étoiles initiales sur lesquelles nous voulons +démarrer le calcul : ``` X1, f(X1); +a(X2 Y2); @-h(f(X3 Y3)) +a(+f(X4) h(-f(X4))); ``` -An *interaction configuration* is an expression `R |- I'` where: -- `R` is a static constellation called *reference constellation*. It corresponds -to unmarked stars; -- `I` is a dynamic constellation called *interaction space*. It corresponds to -all stars marked by a focus symbol `@`. It can be seen as a "working space". +{{< hint info >}} +Le focus est optionnel. Lorsqu'il est omis, une étoile est sélectionnée pour +nous. +{{< /hint >}} -The LSC execute constellations by looking for copies of partners in `R` for -each rays of `I`, as follows: -1. select a ray `ri` in a star `s` of `I`; -2. look for possible connections with rays `rj` belonging to stars in `R`; -3. duplicate `s` so that there is exactly one copy of `s` in `I` for every `rj`; -4. replace every copy by its fusion `s s'`, where `s'` is the star to - which `rj` belongs; -5. repeat until there is no possible interaction in `I`. +Passons à la théorie de l'exécution ! -The result of execution consists of all *neutral* stars that remain in `I`, i.e. -those without any polarized rays. Indeed, polarized stars are ignored/removed -because they correspond to *unfinished* (or stuck) computations. +Une *configuration interactive* est une expression `R |- I` où: +- `R` est une constellation statique nommée *constellation de référence*. Elle +est constituée des étoiles non marquées par `@` et elle nous servira de stock +infini d'étoiles à tirer comme on pioche dans des bacs à LEGO pour faire des +constructions; +- `I` est une constellation dynamique nommée *espace d'interaction*. Elle +est constituée de l'ensemble des étoiles marquées avec `@` et se comporte comme +un espace de travail où des constructions sont réalisées par fusion d'étoiles. -# Example +Le LSC exécute les constellations en prenant pour partenaire des copies +d'étoiles dans `R` pour les projeter et fusionner sur chaque rayon de `I` comme +suit : +1. selectionner un rayon `ri` d'une étoile `s` de `I`; +2. chercher toutes les connexions possibles avec des rayons `rj` d'étoiles `s'` + de `R`; +3. dupliquer `s` dans `I` pour chaque `rj` trouvé; +4. remplacer chaque copie de `s` par la fusion `s s'`; +5. répeter jusqu'à qu'il n'y a plus aucune interaction possible dans `I`. -We want to execute the following constellation: +Le résultat de l'exécution contient toutes les étoiles non polarisées qui +restent dans `I`. Ces étoiles non polarisées que nous ignorons correspondent +en fait à des calculs bloqués ou non terminés. + +# Exemple + +Considérons l'exécution de la constellation suivante : ``` +7(l:X) +7(r:X); 3(X) +8(l:X); @+8(r:X) 6(X); -7(X) -8(X); ``` -We distinguish an interaction space on which we focus interaction and a -reference constellation where we copy possible partners. We prefix `>>` for -selected rays. We have: +On sépare la constellation en constellation de référence et en espace +d'interaction. On préfixe par `>>` les rayons sélectionnés. Nous avons donc +les étapes suivantes : ``` +7(l:X) +7(r:X); 3(X) +8(l:X); -7(X) >>-8(X) |- >>+8(r:X) 6(X); ``` @@ -124,4 +140,4 @@ selected rays. We have: +7(l:X) +7(r:X); 3(X) +8(l:X); -7(X) -8(X) |- 3(X) 6(X); ``` -The result of the computation is `3(X) 6(X);`. \ No newline at end of file +Le résultat du calcul est une constellation contenant l'étoile `3(X) 6(X);`. \ No newline at end of file diff --git a/content/docs/playing/syntax.md b/content/docs/playing/syntax.md index 07610e4..43bf247 100644 --- a/content/docs/playing/syntax.md +++ b/content/docs/playing/syntax.md @@ -1,30 +1,31 @@ --- -title: "Syntax" +title: "Syntaxe" weight: 1 --- -# Rays +# Rayons -Either a variable (uppercase, possibly followed by digits) or a polarised (+/-) -or unpolarised (lowercase, possibly containing `_` and digits) -function symbol applied to other rays (or nothing in case of constants): +Soit une variable de la forme `[A-Z][A-Z 0-9]*` ou un symbole de fonction +polarisé ou non par `+` ou `-` de la forme `(+|-)?[a-z 0-9 _]+` appliqué à une +séquence ordonnée d'autres rayons en arguments (séquence possiblement vide dans +le cas d'une constante) : `X`, `a`, `f(X)`, `+f(X)`, `-f(-h(a, Y1), X2)`, `+add_dec(0, 2, 2)`. -Commas can be omitted: +Les virgules séparant les arguments peuvent être omises : `-f(-h(a Y1) X2)`, `+add_dec(0 2 2)`, `string(hello i am X)`. -# Cons +# Concaténation -There is a special binary infix function symbol `:` which can be used to -concatenate rays: +Un symbole de fonction binaire infixe `:` est disponible et peut être utilisé +pour écrire confortablement une concaténation de rayons : `a:X`, `a:b:b:X`, `f(a:X):+f(0:1:X):-f(Y)`. -# Stars +# Etoiles -An unordered sequence of rays ending with a semicolon `;`: +Une séquence non-ordonnée de rayons terminant par un point-virgule `;`: ``` X a +f(X); @@ -32,20 +33,25 @@ X a +f(X); # Constellations -An unordered sequence of stars: +Une séquence non-ordonnée d'étoiles : ``` X a +f(X); -f(-h(a Y1) X2); +add_dec(0 2 2); ``` -All variables are local to their stars, hence the occurrences of `X` in the -first line are distinct from the one in the second line. +Toutes les variables sont locales à leur étoile. Donc, toutes les occurrences +de `X` de la première ligne sont en fait distinctes de celles de la seconde +ligne. + +{{< hint info >}} +Il n'y a pas de sensibilité à l'indentation ou aux sauts de ligne. +{{< /hint >}} # Focus -You can prefix stars with a `@` symbol to put a *focus* over them. This will -affect the behaviour of computation: +Pour choisir des points de départ du calcul, il est possible de préfixer +certaines étoiles (de notre choix) avec un symbole de *focus* `@`. ``` @X a +f(X); @@ -53,15 +59,15 @@ affect the behaviour of computation: +add_dec(0 2 2); ``` -# Comments +# Commentaires ``` -'this is a comment on a single line -'this is another comment +'commentaire sur une seule ligne +'un autre commentaire ''' -this is a -comment on -several lines +commentaire +sur plusieurs +lignes ''' ``` \ No newline at end of file