Introduction

Bienvenue sur le guide du langage Stellogen.

Notez que ce guide est très expérimental et est suceptible de changer régulièrement. Le langage présenté est tout aussi instable.

Je suis intéressé par toutes opinions, recommandations, suggestions ou simples questions. N'hésitez pas à me contacter à boris.eng@proton.me.

Bonne lecture !

Comment tout a commencé

Stellogen a été créé à partir des recherches de Boris Eng pour comprendre le programme de syntaxe transcendantale de Jean-Yves Girard.

La syntaxe transcendantale propose un nouveau fondement pour la logique et le calcul étendant la correspondance de Curry-Howard. Dans ce nouveau programme, les entités logiques comme les preuves, les formules ou des concepts comme la vérité sont redéfinis/construits à partir d'un modèle de calcul élémentaire appelé "résolution stellaire", qui est une sorte de langage de programmation logique très flexible.

Dans le but de pouvoir expérimenter avec ces idées, Eng a développé un interpréteur appelé "Large Star Collider (LSC)" permettant d'exécuter des expressions de la résolution stellaire. Il a initiallement été développé en Haskell puis finalement redéveloppé en OCaml.

Plus tard, il a été remarqué qu'un langage de metaprogrammation était nécessaire pour travailler convenablement avec ces objets et notamment écrire des preuves de la logique linéaire (ce qui était le projet initial). C'est de là qu'est né le langage Stellogen.

Le langage Stellogen s'est ensuite détaché petit à petit de la syntaxe transcendantale pour développer ses propres concepts.

Philosophie

Connectique du sens

Les types, spécifications, algorithmes et formules logiques sont des questions que l'on pose. Elles portent une intention qui est subjective. Les programmes sont des réponses à ces questions. Elles sont portées par une dynamique objective: elles peuvent être implicites et se développer vers une forme explicite irreductible (c'est l'exécution vers un résultat du calcul).

La grande question est : comment savoir si l'on est face à une réponse à une question. Il nous faudrait une connectique de l'interaction entre question et réponse.

Iconoclasme et décentralisation

Traditionnellement, la logique et les systèmes de types définissent des systèmes avec :

des classes d'entités (individus du premier ordre et relations);
des règles sémantiques (le compilateur/l'interpréteur est responsable du sens des expressions et l'utilisateur manipule ces expressions en suivant ce sens);
des interactions interdites;
des interactions autorisées.

Il y a donc une préconception logique. En particulier, les compilateurs et interpréteurs détiennent le pouvoir sémantique : ils définissent quelles questions peuvent être posées et comment juger si l'on a une réponse.

Stellogen tente de redonner le pouvoir sémantique à l'utilisateur, devenant responsable de la création du sens par des briques élémentaires qui composent à la fois les programmes et les types/formules/specifications. Les interpréteurs et compilateurs sont ensuite responsables d'un noyau basique assurant la bonne connexion entre ces briques mais aussi de la méta-programmation. Nous passons ainsi d'un rôle d'autorité sémantique à un rôle protocolaire et administratif de l'évaluateur.

Le sens par l'expérience

Pour savoir si un programme a un certain type (si une réponse satisfait une question), on procède ainsi :

on construit un type par un ensemble de tests à passer qui sont eux-mêmes des programmes;
on construit un "juge" qui détermine ce que signifie "passer un test";
on connecte un programme à chaque test du type et on vérifie si le juge valide toutes les interactions.

Cela nous donnes des garanties non-systémiques et locales similaires aux commandes "assert" en programmation. Nous pourrions choisir de se mettre dans des contextes où l'on organiserait des types et contraintes pour former un système.

Un ordre dans le chaos

Le modèle de calcul de briques élémentaires avec lequel nous travaillons pourrait être qualifié de chaotique. Il est possible d'écrire des choses peu intuitives au résultat peu prédictible. Dans certains cas, la propriété de confluence n'est même pas valide (deux ordres d'exécutions mènent à deux résultats différents).

Il y a deux manières d'obtenir un ordre dans le chaos:

l'émergence naturelle, locale par la création de garanties locales sur des bouts de programmes;
l'imposition d'un système fermé définissant des restrictions/contraintes et dans lequel seul certains types peuvent être utilisés.

Stellogen souhaite laisser les deux possibilités ouvertes. Le premier choix permettrait une grande flexibilité et le second donnerait l'avantage de l'efficacité et de l'ergonomie tout en ayant des garanties plus fortes.

Vérification partielle

Du point de vue de la programmation, et plus particulièrement des méthodes formelles, Stellogen est motivé par une vérification "partielle" s'opposant aux vérifications totales où l'on modéliserait entièrement un programme et ses propriétés pour obtenir des preuves formelles.

Stellogen se concentre sur l'expressivité de contraintes locales qui pourraient être globalisées dans un système.

Démarrer

Pour installer l'interprêteur Stellogen, aller sur ce dépôt git :

https://github.com/engboris/stellogen

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/stellogen/releases

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.

Pour un aperçu rapide, n'hésitez pas à explorer :

Si vous êtes prêts, allons-y !

Unification de termes

Syntaxe

Dans la théorie de l'unification, nous écrivons des termes. Ce sont soit :

des variables (commençant par une majuscule comme X, Y ou Var);
des fonctions de la forme f(t1, ..., tn) où f est un symbole de fonction (commençant par une minuscule ou un chiffre) et les expressions t1, ..., tn sont d'autres termes.

Tous les identifiants (que cela soit pour les variables ou symboles de fonction) peuvent contenir les symboles _ et ? (mais pas au début). Par exemple : is_empty? et X_1.

Exemples de termes. X, f(X), h(a, X), parent(X), add(X, Y, Z).

On peut aussi omettre la virgule séparant les arguments d'une fonction étant donné que leur absence ne produit pas d'ambiguïté. On écrirait donc h(a X) à la place de h(a, X).

Principe

Dans la théorie de l'unification, on dit que deux termes sont unifiables lorsqu'il existe une substitution des variables les rendant identiques. Par exemple, f(X) et f(h(Y)) sont unifiables avec la substitution {X:=h(Y)} remplaçant X par h(Y).

Les substitutions qui nous intéressent sont celles qui 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.

Une autre façon de voir les choses est de voir cela comme brancher des termes ensemble pour vérifier s'ils sont compatibles se branchent correctement :

une variable X se branche avec tout ce qui ne contient pas X comme sous-terme, sinon nous aurions une dépendance circulaire, comme entre X et f(X);
une fonction f(t1, ..., tn) est compatible avec f(u1, ..., un) où ti est compatible avec ui pour tout i.
f(X) et f(h(a)) sont compatibles avec {X:=h(a)};
f(X) et X sont incompatibles;
f(X) et g(X) sont incompatibles;
f(h(X)) et f(h(a)) sont compatibles avec {X:=a}.

Etoiles et constellations

Rayons

Le langage de résolution stellaire étend la notion de terme avec la notion de rayon. Un rayon est un terme où les symboles de fonction sont polarisés avec :

+ (polarité positive);
- (polarité négative);
rien (polarité nulle ou absence de polarité).

La compatibilité entre les rayons suit les mêmes règles que l'unification des termes sauf que :

au lieu de demander l'égalité f = g des symboles de fonction lorsque f(t1, ..., tn) est confronté à g(u1, ..., un), on demande que f et g aient une polarité opposée (+ contre -);
les symboles sans polarités ne peuvent pas interagir.

Par exemple :

+f(X) et -f(h(a)) sont compatibles avec {X:=h(a)};
f(X) et f(h(a)) sont incompatibles;
+f(X) et +f(h(a)) sont incompatibles;
+f(+h(X)) et -f(-h(a)) sont compatibles avec {X:=a};
+f(+h(X)) et -f(-h(+a)) sont compatibles avec {X:=+a}.

Chaînes de caractère

Stellogen permet aussi de définir des constantes spéciales représentant des chaînes de caractères :

"this is a string literal"

Séquences

Il est possible d'utiliser un symbole infixe spécial : comme dans :

+w(0:1:0:1:e).

Il est possible de le parenthéser pour préciser la priorité (à droite par défaut) :

+w((0:(1:(0:(1:e))))).
+w((((0:1):0):1):e).

Etoiles

Avec les rayons, nous pouvons former des étoiles. Ce sont des collections non ordonnées de rayons qui peuvent être entourées de crochets :

+f(X) -f(h(a)) +f(+h(X))

[+f(X) -f(h(a)) +f(+h(X))]

L'étoile vide est notée [].

Constellations

Les constellations sont des séquences non ordonnées d'étoiles séparées par le symbole ; et se terminant par un . :

+f(X) X; +f(+h(X) a f(b)).

Elles peuvent être entourées d'accolades :

{ +f(X) X; +f(+h(X) a f(b)) }.

Les variables sont locales à leur étoile. Cela peut être rendu explicite ainsi :

+f(X1) X1; +f(+h(X2) a f(b)).

La constellation vide est notée {}.

Les constellations sont en fait les plus petits objets que nous pourront manipuler. C'est elles qui pourront être exécutées comme on exécute un programme.

Exécution de constellations

Fusion d'étoiles

Les étoiles interagissent entre elles par une opération appelée fusion (que l'on pourrait qualifier de protocole d'interaction), en utilisant le principe de la règle de résolution de Robinson.

La fusion entre deux étoiles

r r1 ... rk

r' r1' ... rk'

le long de leurs rayons r et r' est définie par une nouvelle étoile :

theta(r1) ... theta(rk) theta(r1') ... theta(rk')

où theta est la substitution la plus générale induite par r et r'.

Remarquez que:

r et r' sont annihilées pendant la fusion;
les deux étoiles fusionnent;
la substitution obtenue par résolution du conflit entre r et r' est propagée aux rayons adjacents.

Exemple. La fusion entre X +f(X) et -f(a) fait interagir +f(X) et -f(a) ensemble pour propager la substitution {X:=a} sur l'unique voisin X. Le résultat est donc X{X:=a} soit a.

Cette opération de fusion correspond à la règle de coupure pour la logique du premier ordre (correspondant aussi à la règle de résolution). Cependant, la différence ici est que nous sommes dans un cadre "alogique" (nos objets ne portent aucun sens logique).

Exécution

Cela marche à peu près comme pour la résolution d'un puzzle ou un jeu de fléchettes. Vous avez une constellation faites de plusieurs étoiles. Choisissez des étoiles initiales puis des copies des autres étoiles seront jetées dessus pour interagir par fusion. L'opération continue jusqu'à qu'il n'y ait plus d'interactions possibles (saturation). La constellation obtenue à la fin est le résultat de l'exécution.

Plus formellement, nous séparons une constellation en deux parties pour l'exécuter :

l'espace d'états, un espace d'étoiles qui seront cibles de l'interaction;
l'espace d'actions qui sont des étoiles qui vont interagir avec les étoiles de l'espace d'états.

On pourrait représenter cette séparation ainsi avec l'espace d'actions à gauche et l'espace d'états à droite, séparées avec le symbole |- :

a1 ... an |- s1 ... sm

L'exécution procède de la façon suivante :

selectionner un rayon r d'une étoile d'état s;
chercher toutes les connexions possibles avec des rayons r' d'étoiles d'action a;
dupliquer s à droite pour chaque tel rayon r' trouvé car il y a plusieurs interactions possibles à satisfaire;
remplacer chaque copie de s par la fusion entre a et s;
répéter jusqu'à qu'il n'y a plus aucune interaction possible l'espace d'états.

Focus

Les étoiles d'état sont préfixées par un symbole @ :

@+a b; [-c d].

+a b; [@-c d].

Exemple

Considérons l'exécution de la constellation suivante :

@+a(0(1(e)) q0);
-a(e q2) accept;
-a(0(W) q0) +a(W q0);
-a(0(W) q0) +a(W q1);
-a(1(W) q0) +a(W q0);
-a(0(W) q1) +a(W q2).

Pour l'exemple, on entoure par >> et << les rayons sélectionnés. Nous avons donc l'étapes suivante :

-a(e q2) accept;
-a(0(W) q0) +a(W q0);
-a(0(W) q0) +a(W q1);
-a(1(W) q0) +a(W q0);
-a(0(W) q1) +a(W q2);
@+a(0(1(e)) q0).

Nous avons la séparation suivante :

-a(e q2) accept;
-a(0(W) q0) +a(W q0);
-a(0(W) q0) +a(W q1);
-a(1(W) q0) +a(W q0);
-a(0(W) q1) +a(W q2)
|-
+a(0(1(e)) q0)

Sélectionnons le premier rayon de la première étoile :

>>-a(e q2)<< accept;
-a(0(W) q0) +a(W q0);
-a(0(W) q0) +a(W q1);
-a(1(W) q0) +a(W q0);
-a(0(W) q1) +a(W q2)
|-
+a(0(1(e)) q0)

Il ne peut pas se connecter à +a(0(1(e)) q0) car le premier argument e est incompatible avec 0(1(e)). Cependant, il peut interagir avec les deux étoiles suivantes (mais pas la dernière à cause d'une incompatibilité entre q0 et q1). Nous effectuons une duplication et fusion suivante entre :

-a(0(W) q0) +a(W q0);
-a(0(W) q0) +a(W q1);

+a(0(1(e)) q0)

donnant la substitution {W:=1(e)} et le résultat :

+a(1(e) q0);
+a(1(e) q1)

Nous obtenons donc l'étape suivante :

-a(e q2) accept;
-a(0(W) q0) +a(W q0);
-a(0(W) q0) +a(W q1);
-a(1(W) q0) +a(W q0);
-a(0(W) q1) +a(W q2)
|-
+a(1(e) q0);
+a(1(e) q1)

La seconde étoile d'état +a(1(e) q1) ne peut interagir avec aucune étoile d'action. Cependant on peut se focaliser sur +a(1(e) q0).

-a(e q2) accept;
-a(0(W) q0) +a(W q0);
-a(0(W) q0) +a(W q1);
-a(1(W) q0) +a(W q0);
-a(0(W) q1) +a(W q2)
|-
>>+a(1(e) q0)<<;
+a(1(e) q1)

Il peut se connecter à -a(1(W) q0) avec comme substitution {W:=e} :

-a(e q2) accept;
-a(0(W) q0) +a(W q0);
-a(0(W) q0) +a(W q1);
-a(1(W) q0) +a(W q0);
-a(0(W) q1) +a(W q2)
|-
+a(e q0);
+a(1(e) q1)

Plus aucune interaction n'est possible. Le résultat de l'exécution est donc :

+a(e q0);
+a(1(e) q1)

Définir des constellations

Définitions statiques

On peut nommer des constellations que l'on écrit directement. Les identifiants suivent les mêmes règles que pour les symboles de fonction des rayons.

w = a.
x = +a; -a b.
z = { -f(X) }.

Lorsque l'on se réfère à un identifiant de constellation, on utilise le préfixe #:

y = #x.

Comme pour l'application en programmation fonctionnelle, l'union de constellations est notée avec un espacement :

union1 = #x #y #z.

On peut aussi ajouter des parenthèses autour des expressions pour plus de lisibilité ou pour éviter des ambiguïtés syntaxiques :

union1 = (#x #y) #z.

Mais il faut noter que contrairement à la programmation fonctionnelle, il n'y a pas d'ordre défini.

Les définitions statiques correspondent à la notion "d'objet-preuve" dans la correspondance de Curry-Howard.

Focus

On peut mettre le focus sur toutes les étoiles d'une constellation en la préfixant aussi avec @ et en l'entourant de parenthèses :

x = +a; -a b.
z = -f(X).
union1 = @#x #z.

Contraintes d'inégalité

Il est possible d'ajouter une séquence de contraintes d'inégalités entre des termes :

ineq = +f(a); +f(b); @-f(X) -f(Y) r(X Y) | X!=Y.

Cela rend invalide toute interaction où X et Y sont totalement définies (absence de variables) et instanciées avec la même valeur.

Ces inégalités peuvent être séparées par des espaces ou des virgules :

X!=Y X!=Z

X!=Y, X!=Z

Pre-execution

L'exécution d'une constellation dans un bloc exec ... end définit aussi une constellation :

exec +f(X); -f(a) end

Commandes

Commentaires

Les commentaires commencent par ' et sont écrits entre ''' pour les commentaires multi-lignes. Ils sont ignorés pendant l'exécution.

'this is a comment

'''
this is a
multiline comment
'''

Affichage

Pour afficher des constellations, vous pouvez utiliser la commande show suivit d'une constellation :

show +a; -a b.

La commande show n'exécute pas les constellations. Si vous voulez vraiment exécuter la constellation et afficher son résultat, utilisez la commande show-exec :

show-exec +a; -a b.

Trace d'exécution

Il est possible de suivre pas à pas l'exécution d'une constellation :

ineq = +f(a); +f(b); @-f(X) -f(Y) r(X Y) | X!=Y.
'trace ineq.

Effets réactifs

Stellogen utilise des "effets réactifs" qui sont déclenchés lors de l'interaction entre des rayons utilisant des symboles de têtes spéciaux.

Print

Pour l'affichage, il faut une interaction entre deux rayons %print. L'interaction génère une substitution définissant le rayon à afficher :

+%print(X); -%print("hello world\n").

La commande ci-dessus affiche hello world puis un saut à la ligne.

Lancement de constellation

Lorsque les constellations produisent des effets, une commande run est disponible pour les exécuter :

run +%print(X); -%print("hello world\n").

Substitutions

Les substitutions sont des expressions de la forme [... => ...] remplaçant une entité par une autre.

Variables

On peut remplacer des variables par n'importe quel rayon :

show-exec (+f(X))[X=>Y].
show-exec (+f(X))[X=>+a(X)].

Symboles de fonction

On peut remplacer les symboles de fonctions par d'autres symboles de fonction :

show-exec (+f(X))[+f=>+g].
show-exec (+f(X))[+f=>f].

On peut aussi omettre la partie gauche ou droite de => pour ajouter ou retirer un symbole de tête :

show-exec (+f(X); f(X))[=>+a].
show-exec (+f(X); f(X))[=>a].
show-exec (+f(X); f(X))[+f=>].

Identificateurs de constellations

show-exec (#1 #2)[#1=>+f(X) X][#2=>-f(a)].

Programmation logique

Les constellations sont des sortes de programmes logiques comme dans Prolog. C'est la matière élémentaire à tout faire.

En programmation logique, on voit les rayons comme des prédicats, des propriétés ou des relations :

'a is the child of b
childOf(a b).

Les rayons positifs sont des sorties/conclusions et les rayons négatifs sont des entrées/hypothèses. Avec les rayons, on peut créer des faits (vérités d'une base de connaissance) :

'knowledge base
+childOf(a b).
+childOf(a c).
+childOf(c d).

mais aussi des règles d'inférence :

-childOf(X Y) -childOf(Y Z) +grandParentOf(Z X).

Les faits et règles d'inférence vont former des étoiles d'actions qui vont interagir avec une étoile de requête qui permet de poser des questions comme on ferait une requête à une base de donnée :

-childOf(X b) res(X).

On renvoie un résultat qui nous dira qui sont les enfants de b.

Contrairement à des langages dédiés à ce genre d'opération comme Prolog, dans Stellogen, il faudra organiser et déclencher des interactions :

knowledge =
  +childOf(a b);
  +childOf(a c);
  +childOf(c d);
  -childOf(X Y) -childOf(Y Z) +grandParentOf(Z X).

query = -childOf(X b) res(X).

show-exec #knowledge @#query.

Galaxies

Les constellations peuvent être représentées en donnant un nom à des sous-constellation les composant. On appelle cela des galaxies.

On définit les galaxies avec des blocs galaxy ... end contenant une série d'étiquettes label = suivit de la galaxie associée :

g = galaxy
  test1 = +f(a) ok.
  test2 = +f(b) ok.
end

On accède ensuite aux champs d'une galaxie avec -> :

show #g->test1.
show #g->test2.

Cela ressemble au concept de record (enregistrement) en programmation sauf que lorsque les galaxies sont utilisées, elles sont représentées par leur constellation sous-jacente (par oubli d'étiquettes).

Interfaces

Il est possible de vérifier si une galaxie est formé d'une certaine manière avec des champs possédant un certain nom et étant d'un certain type :

interface nat_pair
  n :: nat.
  m :: nat.
end

g_pair :: nat_pair.
g_pair = galaxy
  n = +nat(0).
  m = +nat(0).
end

Typage

Le typage dans Stellogen illustre des principes majeurs de syntaxe transcendantale où les types sont définis comme des ensembles de tests eux-mêmes définis avec des constellations. La vérification de type implique le passage de tous les tests associés à un type.

Les types sont donnés par une galaxie où chaque champ représentent un test à faire passer :

t = galaxy
  test1 = @-f(X) ok; -g(X).
  test2 = @-g(X) ok; -f(X).
end

On peut aussi faire précéder la définition par spec pour indiquer qu'il s'agit d'une spécification :

spec t = galaxy
  test1 = @-f(X) ok; -g(X).
  test2 = @-g(X) ok; -f(X).
end

Une galaxie/constellation testée doit donc être confrontée à tous les tests définis par la galaxie ci-dessous pour être de type t.

Un type avec un unique test peut être défini par une simple constellation.

Il nous reste cependant à définir ce que signifient :

être confronté à un test;
passer un test avec succès.

Conformément à la correspondance de Curry-Howard, les types peuvent être vus comme des formules ou spécifications. On pourrait aussi étendre cela à la proposition de Thomas Seiller de voir les algorithmes comme des spécifications plus sophistiquées.

Checkers

Il faut définir des checkers qui sont des galaxies "juges" définissant :

un champ interaction contenant un identificateur #tested et #tested. Ce champ explique comment faire interagir un testé et un test;
un champ expect indiquant quel est le résultat attendu par l'interaction.

Par exemple :

checker = galaxy
  interaction = #tested #test.
  expect = ok.
end

Typage par test

On peut ensuite faire précéder les définitions par une déclaration de type :

c :: t [checker].
c = +f(0) +g(0).

La constellation c passe bel et bien les tests test1 et test2 de t. Il n'y a donc aucun problème. On dit donc que c est de type t ou que c est une preuve de la formule t.

Cependant, si nous avions une constellation qui ne passait pas les tests, comme :

c :: t [checker].
c = +f(0).

Nous aurions eu un message d'erreur nous indiquant qu'un test n'est pas passé.

Voici un type avec un unique test pour une représentation naïve des entiers naturels :

spec nat =
  -nat(0) ok;
  -nat(s(N)) +nat(N).

0 :: nat [checker].
0 = +nat(0).

1 :: nat [checker].
1 = +nat(s(0)).

On peut aussi omettre de préciser le checker. Dans ce cas, le checker par défaut est :

checker = galaxy
  interaction = #tested #test.
  expect = ok.
end

Cela nous permet d'écrire :

0 :: nat.
0 = +nat(0).

1 :: nat.
1 = +nat(s(0)).

Pluralité des types

Il est possible d'associer plusieurs types à une constellation:

soit en définissant plusieurs déclaration de types;
soit en écrivant des séquences de types (séparés par des virgules) si le même checker est utilisé.

Par exemple:

nat2 = -nat(X) ok.
2 :: nat [checker].
2 :: nat2.
2 = +nat(s(s(0))).

3 :: nat, nat2.
3 = +nat(s(s(s(0)))).
```

## Interfaces

Il est possible de définir des interfaces décrivant une liste d'identifiants
devant être d'un certain type.

```
nat_pair = interface
  n :: nat [checker].
  m :: nat [checker].
end
```

On peut ensuite demander à ce qu'une galaxie respecte cette interface.

```
g_pair :: nat_pair.
g_pair = galaxy
  n = +nat(0).
  m = +nat(0).
end
```

Attentes

Il est possible de vérifier si une constellation est exactement égale à une autre constellation avec un test d'attente :

x :=: +f(X).

En particulier, le passage des tests d'une spécification comme :

spec t = galaxy
  test1 = +f(X).
  test2 = +g(X).
end

g :: t.

peut être reformulé de façon équivalente ainsi :

t1 :=: ok.
t1 = #g #t->test1.
t2 :=: ok.
t2 = #g #t->test2.

Processus de construction

On peut enchaîner des constellations avec l'expression process ... end :

c = process
  +n0(0).
  -n0(X) +n1(s(X)).
  -n1(X) +n2(s(X)).
end

Cet enchaînement part de la première constellation +n0(0) considérée comme initiale. Chaque constellation suivante interagit ensuite avec le résultat précédent.

C'est comme si nous faisions le calcul suivant :

c = +n0(0).
c = @#c {-n0(X) +n1(s(X))}.
c = @#c {-n1(X) +n2(s(X))}.

C'est ce qui correspond aux tactiques dans des assistants de preuve comme Coq et que l'on pourrait assimiler aux programmes impératifs qui altèrent des représentation d'état (mémoire par exemple).

Les constructions dynamiques correspondent à la notion de "processus-preuve" chez Boris Eng ou de "proof-trace" chez Pablo Donato. Les processus-preuves construisent des objet-preuves (constellations).

Arrêt de processus

Dans le résultat d'une exécution, si l'on représente les résultats par des rayons à polarité nulle, alors les étoiles contenant des rayons polarisés peuvent être interprétés comme des calculs non terminés qui pourraient être effacés.

Pour cela, dans les processus de constructions, nous pouvons utiliser l'expression spéciale #kill :

c = process
  +n0(0).
  -n0(X) +n1(s(X)).
  -n1(X) +n2(s(X)).
  -n2(X) result(X); -n2(X) +n3(X).
  #kill.
end

show-exec c.

Nous avons utilisé un rayon +n3(X) pour poursuivre des calculs si nous souhaitons. Le résultat est stocké dans result(X). Mais si nous souhaitons seulement conserver le résultat et retirer toute autre possibilité de calcul alors on peut utiliser #kill.

Nettoyage de processus

Il arrive parfois que l'on se retrouve avec des étoiles vides [] dans les processus. Il est possible de s'en débarrasser avec la commande #clean :

show-exec process
  +f(0).
  -f(X).
  #clean.
end

tsguide