Résolution stellaire

La résolution stellaire est le langage (théorique) utilisé dans la syntaxe transcendantale. Il s'agit d'un langage fonctionnant par interaction asynchrone d'agents indépendants. Cette interaction se base sur un algorithme d'unification (celui qui intervient dans le langage Prolog) servant de noyau minimal du calcul.

Il représente le calcul par un réseau de contraintes syntaxiques qui doivent être résolues pour propager de l'information. Le résultat du calcul correspond aux informations laissées par les réseaux qui sont restés cohérents jusqu'au bout sans rencontrer de conflits.

Ce sont des idées qui existent déjà en programmation logique mais qui sont reformulées et utilisées différemment. En particulier, on n'attache aucun sens logique aux objets (même si on peut les voir comme tel, ils ne sont pas censés représenter des relations ou des objets de systèmes logiques).

Ce calcul peut être compris de plusieurs manières. C'est :

• un calcul de processus;
• un langage de programmation par contraintes;
• une variante des clauses disjonctives avec règle de résolution de Robinson;
• une généralisation non planaire des tuiles de Wang ou des abstract tile assembly models (aTAM);
• une généralisation des tuiles flexibles de Jonoska utilisés en calcul ADN;
• une généralisation des briques LEGO;
• un langage de bas niveau exprimant le sens logique;
• une boîte à outils pour construire des types/formules;
• une généralisation des structures de preuves de Jean-Yves Girard;
• une forme de réseaux d'interaction de Lafont ne reposant sur aucune règle autre que les principes d'unification de termes.