Update
This commit is contained in:
parent
bbf21e9201
commit
6be1fcd5c7
|
|
@ -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.
|
||||
|
|
@ -0,0 +1,18 @@
|
|||
---
|
||||
title: "A propos"
|
||||
weight: 1
|
||||
---
|
||||
|
||||
# A propos
|
||||
|
||||
## Syntaxe transcendantale
|
||||
|
||||
(soon)
|
||||
|
||||
## Résolution stellaire
|
||||
|
||||
(soon)
|
||||
|
||||
## Large star collider
|
||||
|
||||
(soon)
|
||||
|
|
@ -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 !
|
||||
|
|
@ -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)
|
||||
|
|
@ -1,5 +1,5 @@
|
|||
---
|
||||
title: "Playing with stars"
|
||||
title: "Jouer avec les étoiles"
|
||||
bookFlatSection: true
|
||||
weight: 1
|
||||
---
|
||||
|
|
|
|||
|
|
@ -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 :
|
||||
```
|
||||
{}
|
||||
```
|
||||
|
|
@ -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))));
|
||||
```
|
||||
|
|
@ -0,0 +1,14 @@
|
|||
---
|
||||
title: "Exercices"
|
||||
weight: 5
|
||||
---
|
||||
|
||||
# Exercices
|
||||
|
||||
## Chemins
|
||||
|
||||
## Effacement partiel
|
||||
|
||||
## Altération de mémoire
|
||||
|
||||
## Tables de vérité
|
||||
|
|
@ -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 `<i,j>` 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 `<i,j>` 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 <i,j> 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 <i,j> 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);`.
|
||||
Le résultat du calcul est une constellation contenant l'étoile `3(X) 6(X);`.
|
||||
|
|
@ -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
|
||||
'''
|
||||
```
|
||||
Loading…
Reference in New Issue