Add techniques
This commit is contained in:
parent
b9acdebbe9
commit
65241154a0
|
|
@ -1,5 +1,5 @@
|
||||||
---
|
---
|
||||||
title: "Introduction"
|
title: "Introduction"
|
||||||
bookFlatSection: true
|
bookFlatSection: true
|
||||||
weight: 1
|
weight: 10
|
||||||
---
|
---
|
||||||
|
|
|
||||||
|
|
@ -1,18 +0,0 @@
|
||||||
---
|
|
||||||
title: "A propos"
|
|
||||||
weight: 1
|
|
||||||
---
|
|
||||||
|
|
||||||
# A propos
|
|
||||||
|
|
||||||
## Syntaxe transcendantale
|
|
||||||
|
|
||||||
(soon)
|
|
||||||
|
|
||||||
## Résolution stellaire
|
|
||||||
|
|
||||||
(soon)
|
|
||||||
|
|
||||||
## Large star collider
|
|
||||||
|
|
||||||
(soon)
|
|
||||||
|
|
@ -0,0 +1,6 @@
|
||||||
|
---
|
||||||
|
title: "Large star collider"
|
||||||
|
weight: 30
|
||||||
|
---
|
||||||
|
|
||||||
|
(soon)
|
||||||
|
|
@ -0,0 +1,6 @@
|
||||||
|
---
|
||||||
|
title: "Résolution stellaire"
|
||||||
|
weight: 20
|
||||||
|
---
|
||||||
|
|
||||||
|
(soon)
|
||||||
|
|
@ -0,0 +1,6 @@
|
||||||
|
---
|
||||||
|
title: "Syntaxe transcendantale"
|
||||||
|
weight: 10
|
||||||
|
---
|
||||||
|
|
||||||
|
(soon)
|
||||||
|
|
@ -1,5 +1,5 @@
|
||||||
---
|
---
|
||||||
title: "Jouer avec les étoiles"
|
title: "Jouer avec les étoiles"
|
||||||
bookFlatSection: true
|
bookFlatSection: true
|
||||||
weight: 1
|
weight: 20
|
||||||
---
|
---
|
||||||
|
|
|
||||||
|
|
@ -1,6 +1,6 @@
|
||||||
---
|
---
|
||||||
title: "Configurer l'interaction"
|
title: "Configurer l'interaction"
|
||||||
weight: 3
|
weight: 40
|
||||||
---
|
---
|
||||||
|
|
||||||
# Auto-interaction
|
# Auto-interaction
|
||||||
|
|
|
||||||
|
|
@ -1,6 +1,6 @@
|
||||||
---
|
---
|
||||||
title: "Interactions élémentaires"
|
title: "Interactions élémentaires"
|
||||||
weight: 4
|
weight: 50
|
||||||
---
|
---
|
||||||
|
|
||||||
# Interactions élémentaires
|
# Interactions élémentaires
|
||||||
|
|
|
||||||
|
|
@ -1,6 +1,6 @@
|
||||||
---
|
---
|
||||||
title: "Interaction"
|
title: "Exécution"
|
||||||
weight: 2
|
weight: 30
|
||||||
---
|
---
|
||||||
|
|
||||||
# Rayons compatibles
|
# Rayons compatibles
|
||||||
|
|
@ -1,6 +1,6 @@
|
||||||
---
|
---
|
||||||
title: "Exercices"
|
title: "Exercices"
|
||||||
weight: 5
|
weight: 60
|
||||||
---
|
---
|
||||||
|
|
||||||
# Exercices
|
# Exercices
|
||||||
|
|
@ -88,7 +88,7 @@ la sortie `+a(X)` vers `b` (en plus de l'affichage de `a`). Et on ajoute une
|
||||||
On utilise l'étoile `-a(X) -b(Y) c(va(X) vb(Y));`.
|
On utilise l'étoile `-a(X) -b(Y) c(va(X) vb(Y));`.
|
||||||
{{< /details >}}
|
{{< /details >}}
|
||||||
|
|
||||||
## Circuits booléens
|
## Logique booléenne
|
||||||
|
|
||||||
On veut simuler des formules booléennes (plus précisément des circuits) par des
|
On veut simuler des formules booléennes (plus précisément des circuits) par des
|
||||||
constellations. Chaque question utilise le résultat de la question précédente.
|
constellations. Chaque question utilise le résultat de la question précédente.
|
||||||
|
|
@ -174,11 +174,8 @@ de l'équivalence logique sachant que `X <=> Y = (X => Y) /\ (X => Y)`.
|
||||||
```
|
```
|
||||||
{{< /details >}}
|
{{< /details >}}
|
||||||
|
|
||||||
5. En utilisant l'étoile `+share(X X X);`, définir le circuit booléen pour
|
6. Définir une constellation représentant la formule du tiers `X \/ ~X`.
|
||||||
la formule du tiers exclu qui prend une unique entrée, la partage au travers de
|
Afficher la table de vérité correspondant à cette formule.
|
||||||
deux sorties avec l'une qui passe par une porte NOT et pour rejoindre l'autre
|
|
||||||
sortie à travers une porte OR. Afficher la table de vérité correspondant à ce
|
|
||||||
circuit.
|
|
||||||
|
|
||||||
{{< details title="Solution" open=false >}}
|
{{< details title="Solution" open=false >}}
|
||||||
```
|
```
|
||||||
|
|
@ -186,20 +183,23 @@ circuit.
|
||||||
+and(0 0 0); +and(0 1 0); +and(1 0 0); +and(1 1 1);
|
+and(0 0 0); +and(0 1 0); +and(1 0 0); +and(1 1 1);
|
||||||
+or(0 0 0); +or(0 1 1); +or(1 0 1); +or(1 1 1);
|
+or(0 0 0); +or(0 1 1); +or(1 0 1); +or(1 1 1);
|
||||||
|
|
||||||
+and2(0 X 0); +and2(1 X X);
|
|
||||||
+or2(0 X X); +or2(1 X 1);
|
|
||||||
|
|
||||||
-not(X Y) -or(Y Z R) +impl(X Z R);
|
|
||||||
-not(X Y) -or2(Y Z R) +impl2(X Z R);
|
|
||||||
|
|
||||||
-impl(X Y R1) -impl(Y X R2) -and(R1 R2 R) +eqq(X Y R);
|
|
||||||
-impl2(X Y R1) -impl2(Y X R2) -and2(R1 R2 R) +eqq2(X Y R);
|
|
||||||
|
|
||||||
+share(X X X);
|
|
||||||
|
|
||||||
'excluded middle
|
'excluded middle
|
||||||
-share(X X1 X2) -not(X1 R1) -or(R1 X2 R2) +ex(R2);
|
-not(X R1) -or(R1 X R2) +ex(X R2);
|
||||||
|
|
||||||
@-ex(X) table_ex(X);
|
@-ex(X R) table_ex(X R);
|
||||||
|
```
|
||||||
|
{{< /details >}}
|
||||||
|
|
||||||
|
7. Déterminer pour quelles valeurs de `X`, `Y` et `Z` la formule `X /\ ~(Y \/ Z)`
|
||||||
|
est vraie.
|
||||||
|
|
||||||
|
{{< details title="Solution" open=false >}}
|
||||||
|
```
|
||||||
|
+not(0 1); +not(1 0);
|
||||||
|
+and(0 0 0); +and(0 1 0); +and(1 0 0); +and(1 1 1);
|
||||||
|
+or(0 0 0); +or(0 1 1); +or(1 0 1); +or(1 1 1);
|
||||||
|
|
||||||
|
' X /\ ~(Y \/ Z)
|
||||||
|
@-or(Y Z R1) -not(R1 R2) -and(X R2 1) x(X) y(Y) z(Z);
|
||||||
```
|
```
|
||||||
{{< /details >}}
|
{{< /details >}}
|
||||||
|
|
@ -1,6 +1,6 @@
|
||||||
---
|
---
|
||||||
title: Installer le LSC
|
title: Installer le LSC
|
||||||
weight: 2
|
weight: 10
|
||||||
---
|
---
|
||||||
|
|
||||||
# Installer le LSC
|
# Installer le LSC
|
||||||
|
|
@ -1,6 +1,6 @@
|
||||||
---
|
---
|
||||||
title: "Syntaxe"
|
title: "Syntaxe"
|
||||||
weight: 1
|
weight: 20
|
||||||
---
|
---
|
||||||
|
|
||||||
# Rayons
|
# Rayons
|
||||||
|
|
|
||||||
|
|
@ -1,5 +1,5 @@
|
||||||
---
|
---
|
||||||
title: "Techniques"
|
title: "Techniques"
|
||||||
bookFlatSection: true
|
bookFlatSection: true
|
||||||
weight: 1
|
weight: 30
|
||||||
---
|
---
|
||||||
|
|
|
||||||
|
|
@ -1,6 +0,0 @@
|
||||||
---
|
|
||||||
title: "Composition"
|
|
||||||
weight: 5
|
|
||||||
---
|
|
||||||
|
|
||||||
(soon)
|
|
||||||
|
|
@ -3,4 +3,53 @@ title: "Conditions"
|
||||||
weight: 2
|
weight: 2
|
||||||
---
|
---
|
||||||
|
|
||||||
(soon)
|
# Conditions booléennes
|
||||||
|
|
||||||
|
Selon les compatibilités entre les rayons, des choix sont faits. Par exemple,
|
||||||
|
en vérifiant une valeur de vérité :
|
||||||
|
|
||||||
|
```
|
||||||
|
-true result(the condition is true);
|
||||||
|
-false result(the condition is false);
|
||||||
|
@+true;
|
||||||
|
```
|
||||||
|
|
||||||
|
On une étoile par clause de condition et l'entréé dans une condition (ou le
|
||||||
|
choix d'une étoile) dépend de la compatibilité entre les rayons. C'est en fait
|
||||||
|
le mécanisme de base de la résolution stellaire.
|
||||||
|
|
||||||
|
# Conditions complexes
|
||||||
|
|
||||||
|
Ce principe peut se généraliser à n'importe quel rayon. La constellation
|
||||||
|
suivante :
|
||||||
|
|
||||||
|
```
|
||||||
|
+not(0 1); +not(1 0);
|
||||||
|
+and(0 X 0); +and(1 X X);
|
||||||
|
+or(0 X X); +or(1 X 1);
|
||||||
|
-not(X Y) -or(Y Z R) +impl(X Z R);
|
||||||
|
|
||||||
|
-cond(X Y) -impl(X Y 1) ok;
|
||||||
|
|
||||||
|
@+cond(0 1);
|
||||||
|
```
|
||||||
|
|
||||||
|
peut-être lue comme "si X implique Y alors afficher ok".
|
||||||
|
|
||||||
|
# Cas d'échec
|
||||||
|
|
||||||
|
Remarquez qu'il n'est pas (nativement) possible de représenter le `else` de la
|
||||||
|
programmation. Il est donc nécessaire de capturer tous les cas manuellement
|
||||||
|
lorsque l'on souhaite être exhaustif :
|
||||||
|
|
||||||
|
```
|
||||||
|
+not(0 1); +not(1 0);
|
||||||
|
+and(0 X 0); +and(1 X X);
|
||||||
|
+or(0 X X); +or(1 X 1);
|
||||||
|
-not(X Y) -or(Y Z R) +impl(X Z R);
|
||||||
|
|
||||||
|
-cond(X Y) -impl(X Y 1) ok;
|
||||||
|
-cond(X Y) -impl(X Y 0) not_ok;
|
||||||
|
|
||||||
|
@+cond(0 1);
|
||||||
|
```
|
||||||
|
|
@ -3,4 +3,87 @@ title: "Récupération de données"
|
||||||
weight: 1
|
weight: 1
|
||||||
---
|
---
|
||||||
|
|
||||||
(soon)
|
# Récupération de données
|
||||||
|
|
||||||
|
Dans cette section sont décrites des techniques exploitant les mécanismes de la
|
||||||
|
résolution stellaire afin de réaliser des opérations souhaitables pour un
|
||||||
|
programmeur.
|
||||||
|
|
||||||
|
## Retour d'interaction
|
||||||
|
|
||||||
|
Les rayons non polarisés ou *neutres* ne peuvent pas interagir mais se
|
||||||
|
retrouvent en résultat de l'exécution. Il sont donc utilisés pour récupérer des
|
||||||
|
informations sur le calcul effectué.
|
||||||
|
|
||||||
|
On peut les utiliser pour suivre les interactions effectives avec des sortes de
|
||||||
|
messages de debug. Par exemple, si on a cette constellation calculant pour
|
||||||
|
quelles valeurs la formule `X /\ ~(Y \/ Z)` est vraie :
|
||||||
|
|
||||||
|
```
|
||||||
|
+not(0 1); +not(1 0);
|
||||||
|
+and(0 0 0); +and(0 1 0); +and(1 0 0); +and(1 1 1);
|
||||||
|
+or(0 0 0); +or(0 1 1); +or(1 0 1); +or(1 1 1);
|
||||||
|
|
||||||
|
' X /\ ~(Y \/ Z)
|
||||||
|
@-or(Y Z R1) -not(R1 R2) -and(X R2 1) x(X) y(Y) z(Z);
|
||||||
|
```
|
||||||
|
|
||||||
|
On pourrait ajouter un rayon neutre pour vérifier quel calcul a été effectué
|
||||||
|
pour le connecteur `not` :
|
||||||
|
|
||||||
|
```
|
||||||
|
+not(0 1) debug(not(0 1)); +not(1 0) debug(not(1 0));
|
||||||
|
+and(0 0 0); +and(0 1 0); +and(1 0 0); +and(1 1 1);
|
||||||
|
+or(0 0 0); +or(0 1 1); +or(1 0 1); +or(1 1 1);
|
||||||
|
|
||||||
|
' X /\ ~(Y \/ Z)
|
||||||
|
@-or(Y Z R1) -not(R1 R2) -and(X R2 1) x(X) y(Y) z(Z);
|
||||||
|
```
|
||||||
|
|
||||||
|
## Redirection
|
||||||
|
|
||||||
|
Il est aussi possible d'utiliser des rayons polarisés afin de déléguer
|
||||||
|
le transfert de message à une autre constellation dédiée :
|
||||||
|
|
||||||
|
```
|
||||||
|
+not(0 1) +debug(0 1); +not(1 0) +debug(1 0);
|
||||||
|
+and(0 0 0); +and(0 1 0); +and(1 0 0); +and(1 1 1);
|
||||||
|
+or(0 0 0); +or(0 1 1); +or(1 0 1); +or(1 1 1);
|
||||||
|
|
||||||
|
' debug
|
||||||
|
-debug(X R) debug(not(X R));
|
||||||
|
|
||||||
|
' X /\ ~(Y \/ Z)
|
||||||
|
@-or(Y Z R1) -not(R1 R2) -and(X R2 1) x(X) y(Y) z(Z);
|
||||||
|
```
|
||||||
|
|
||||||
|
Cela permet en particulier un traitement générique.
|
||||||
|
|
||||||
|
## Langage naturel
|
||||||
|
|
||||||
|
En utilisant des constantes, il est possible de mimer le langage naturel, chose
|
||||||
|
très pratique pour l'affichage de résultats :
|
||||||
|
|
||||||
|
```
|
||||||
|
message(hello world);
|
||||||
|
```
|
||||||
|
|
||||||
|
Cette astuce utilise le fait que les constantes sont ordonnées lorsqu'elles
|
||||||
|
sont en arguments d'un symbole de fonction.
|
||||||
|
|
||||||
|
## Interpolation de chaîne
|
||||||
|
|
||||||
|
En rajoutant des variables, il est en fait possible d'afficher des messages
|
||||||
|
génériques :
|
||||||
|
|
||||||
|
```
|
||||||
|
+not(0 1) +debug(0 1); +not(1 0) +debug(1 0);
|
||||||
|
+and(0 0 0); +and(0 1 0); +and(1 0 0); +and(1 1 1);
|
||||||
|
+or(0 0 0); +or(0 1 1); +or(1 0 1); +or(1 1 1);
|
||||||
|
|
||||||
|
' debug
|
||||||
|
-debug(X R) debug(the result of not(X) is R);
|
||||||
|
|
||||||
|
' X /\ ~(Y \/ Z)
|
||||||
|
@-or(Y Z R1) -not(R1 R2) -and(X R2 1) x(X) y(Y) z(Z);
|
||||||
|
```
|
||||||
|
|
@ -3,4 +3,26 @@ title: "Digging"
|
||||||
weight: 4
|
weight: 4
|
||||||
---
|
---
|
||||||
|
|
||||||
(soon)
|
# Digging
|
||||||
|
|
||||||
|
Les polarités internes permettent des mécanismes intéressants comme le fait
|
||||||
|
de faire apparaître des rayons polarisés lors de l'interaction.
|
||||||
|
|
||||||
|
Utiliser l'option `-allow-unfinished-computation` sur la constellation suivante
|
||||||
|
:
|
||||||
|
|
||||||
|
```
|
||||||
|
+f(+g(a));
|
||||||
|
@-f(X) X;
|
||||||
|
```
|
||||||
|
|
||||||
|
On remarque l'apparition d'un rayon `+g(a)` qui pourrait être utilisé pour
|
||||||
|
interagir avec un autre rayon :
|
||||||
|
|
||||||
|
```
|
||||||
|
+f(+g(a));
|
||||||
|
-g(X) result(X);
|
||||||
|
@-f(X) X;
|
||||||
|
```
|
||||||
|
|
||||||
|
Nous avons en quelque sorte déterré `+g(a)`.
|
||||||
|
|
@ -1,6 +1,87 @@
|
||||||
---
|
---
|
||||||
title: "Boucles convergeantes"
|
title: "Boucles"
|
||||||
weight: 3
|
weight: 3
|
||||||
---
|
---
|
||||||
|
|
||||||
(soon)
|
Il est possible de construire des boucles dans le cas où des étoiles
|
||||||
|
peuvent être réutilisées.
|
||||||
|
|
||||||
|
# Boucles divergentes improductive
|
||||||
|
|
||||||
|
Il est recommandé d'utiliser l'option `-show-steps` pour cette partie.
|
||||||
|
|
||||||
|
```
|
||||||
|
-f(X) +f(X);
|
||||||
|
@+f(X);
|
||||||
|
```
|
||||||
|
|
||||||
|
Dans l'exemple ci-dessus, on se concentre sur `@+f(X);` pour se connecter
|
||||||
|
à `-f(X)` et ainsi produire `+f(X)` sur lequel on se focalise puis on
|
||||||
|
recommence en utilisant la première étoile, et ce indéfiniement.
|
||||||
|
|
||||||
|
La boucle existe car il existe une compatibilité dans la première étoile
|
||||||
|
entre son premier rayon `-f(X)` et son second rayon `+f(X)` permettant sa
|
||||||
|
duplication et sa réutilisation.
|
||||||
|
|
||||||
|
# Boucles divergentes productives
|
||||||
|
|
||||||
|
En remplaçant le second rayon de `-f(X) +f(X);` de sorte à le rendre strictement
|
||||||
|
plus grand (en nombre de symboles) que le premier, il est possible de rendre
|
||||||
|
la boucle productive : elle ajoute de plus en plus de symboles. Par exemple :
|
||||||
|
|
||||||
|
```
|
||||||
|
-f(X) +f(s(X));
|
||||||
|
@+f(X);
|
||||||
|
```
|
||||||
|
|
||||||
|
Remarque : si on avait fait l'inverse avec
|
||||||
|
|
||||||
|
```
|
||||||
|
-f(s(X)) +f(X);
|
||||||
|
@+f(X);
|
||||||
|
```
|
||||||
|
|
||||||
|
on serait resté avec une boucle improductive qui dit simplement que ce nous
|
||||||
|
donnons (le `X` de `@+f(X)` ici) doit être identifié à `s(X)` mais au final
|
||||||
|
on produit du `X` sans utiliser le symbole `s` qui disparaît.
|
||||||
|
|
||||||
|
# Boucles convergeantes
|
||||||
|
|
||||||
|
Afin d'avoir une boucle convergente, il faut proposer des ressources sur
|
||||||
|
lesquelles on se focalise et avoir une boucle qui les consomme.
|
||||||
|
|
||||||
|
## Décroissance
|
||||||
|
|
||||||
|
On peut par exemple proposer une pile de symboles `s` dépilée par une étoile
|
||||||
|
de boucle :
|
||||||
|
|
||||||
|
```
|
||||||
|
-f(0) end;
|
||||||
|
-f(s(X)) +f(X);
|
||||||
|
@+f(s(s(s(0))));
|
||||||
|
```
|
||||||
|
|
||||||
|
Remarque : on a ajouté une étoile `-f(0) end` pour repérer le moment où la
|
||||||
|
boucle laisse `0` (on a retiré tous les `s`) pour ensuite produire `end` en
|
||||||
|
sortie.
|
||||||
|
|
||||||
|
## Boucle for
|
||||||
|
|
||||||
|
En utilisant ces mécanismes, on peut simuler la boucle `for` de la programmation
|
||||||
|
impérative en ajoutant des rayons à l'étoile de boucle.
|
||||||
|
|
||||||
|
Voici une constellation qui affiche trois fois `hello` avec la valeur de
|
||||||
|
compteur associée :
|
||||||
|
|
||||||
|
```
|
||||||
|
-f(0) end;
|
||||||
|
-f(s(X)) +f(X) message(hello X);
|
||||||
|
@+f(s(s(s(0))));
|
||||||
|
```
|
||||||
|
|
||||||
|
# Cas général
|
||||||
|
|
||||||
|
Dans cette section, nous avons seulement considéré des étoiles de boucles
|
||||||
|
binaires mais il est tout à fait possible d'imaginer des choses plus compliquées
|
||||||
|
avec plusieurs étoiles qui forment plusieurs embranchements pour ensuite
|
||||||
|
réutiliser une étoile déjà utilisée.
|
||||||
|
|
@ -3,4 +3,10 @@ title: "Permissions"
|
||||||
weight: 6
|
weight: 6
|
||||||
---
|
---
|
||||||
|
|
||||||
|
# Permissions
|
||||||
|
|
||||||
|
## Composition
|
||||||
|
|
||||||
|
## Composition conditionnée
|
||||||
|
|
||||||
(soon)
|
(soon)
|
||||||
Loading…
Reference in New Issue