L'open source nous permet d'obtenir les sources, de les modifier ou simplement de les paramétrer, et de les recompiler. Seulement ces moyens sont complexes et nécessite des compétences avancées en matière de programmation de la part de l'utilisateur : une perte de l'information haute se produisant toujours du fait de l'absence de norme et de la non unification des méthodes de développement, seuls amènent de garantir où trouver cette information haute dans un code source.
Pour démocratiser d'avantage et transmettre aux utilisateurs finaux, la tâche fondamentale de vérification ainsi que la responssabilités des choix importants de développement, on souhaite lui donner les moyens de démonter le programme par le haut en plusieurs modules exécutable et de pouvoir les réassembler, en parties ou avec d'autres, en un autre programme pour faire autre chose. Il s'agit de donner aux éxecutables binaires les qualitées de la programmation modulaire (de Bertrand Meyer) à quelques modifications près, à savoir :
La décomposabilité : La division du
logiciel en plusieurs modules éxécutables, une division par le haut.
La composabilité : L'assemblage des différents modules
éxécutables, par le biais d'un langage et d'un interpreteur.
La compréhensibilité : Chaque module décrit de manière
compréhensible ce qu'il fait.
L'auto-preuve statistique : Chaque modules possède un
mecanisme d'auto-preuve.
L'assemblage des modules exécutables se faisant au travers un interpreteur et selon un langage intermédiaire, cela revient à créer une structure possèdant ce langage, mais à la différence de la construction des structures mathématique, faite par le bas en présentant des générateurs, celle-ci est faite par le haut en subdivisant un logiciel existant en plusieurs modules exécutables jouant le rôle d'opérateurs élémentaires, créant ainsi un langage dont la théorie regroupe l'ensemble de leurs propriétés, et servira pour établir les procédures de tests.
Les modules en C/C++, une fois compilés, sont presque des éxécutables. Le linkage, qui a lieu après la compilaton, construit les liens entre chaque module qui correspondent à leurs variables communes et à leurs appelles de méthodes appartenant à d'autre module.
Nous ne souhaitons pas donner l'ensemble de la charge du linkage à l'utilisateur, mais seulement lui donner les moyens d'agir sur des entités exécutables plus larges que les modules initiaux, appelées modules exécutables, que l'on classifie selon le comportement de leurs entrés-sorties. L'utilisateur final pourra combiner les modules exécutables à sa guise en aiguillant leurs entrés-sorties.
Le premier type d'entrés-sorties le plus simple que l'on puissent rencontrer, consiste en la transmission d'une donnée finie, c'est à dire en la transmition d'un objet que l'on représente par un point symbolisant une variable universelle libre. Une entrés de n objets est similaire à n entrés d'un objet ou bien à une entré d'un objet composé de n sous-objets.
Le deuxième type d'entré-sortie, lorsque l'on ne précise pas de typage d'objet, est l'énumération ou la semie-énumération (l'énumération se distingue de la semie-énumération par l'assurence d'énumérer une suite infini, c'est à dire tel que quelque soit n, on soit sûre que le calcul du nième élément se fera en un temps fini). D'un point de vue informatique ce deuxième type d'entré-sortie correspond à un tube (tuyaux) entre deux processus UNIX, un flux de donnée.
L'étude des stuctures définie par le haut est faite au chapitre des Categories. Pour l'instant, continuons à développer une méthode de développement sans se préoccuper de la décomposition en modules exécutables.
Le premier ordre est un langage possèdant une grande interopérabilité. Car il n'y a qu'un seul type de variable universelle et aucune restriction d'unification n'est faite. Une structure se compose d'une présentation qui est un ensemble fini d'opérateurs d'arité fixé agissant sur un seul type de variable dite universelle, définissant ainsi un langage du premier ordre, et d'une théorie écrite dans ce langage sous forme d'une conjonction de skolems n'utilisant que des variables universelles sans aucune variable existancielle, et n'utilisant pas la négation. La théorie est dite d'égalité du premier ordre, et s'inscrit dans une logique constructive.
Si on ajoute aux langage la négation, les théories se décomposent toujours en des conjonctions de skolems, et le langage est seulement appelé langage du premier ordre. Une théorie qui nécessite la négation reste du premier ordre mais perd sa qualité constructive.
Pour définir une présentation de structure on énumère entre accolades les prédicats en majuscule avec leurs arités entre parenthèse puis les fonctions en minuscule avec leurs arités entre parenthèse. Les constantes, fontions ou prédicat d'arité zero, n'ont pas de parenthèse. Par exemple la structure de présentation :
{A(1), B(2), s(1), f(2), c}
comprend un sous-ensemble A de W, un sous-ensemble B deWxW, une fonction unaire s, une fonction binaire f et une constante c. L'univers de Herbrand de cette structure est :
{c, s(c), f(c,c), s(f(c,c)), f(s(c),c), f(c,s(c)), f(f(c,c),c), ...}
La présentation permet d'écrire les constantes de l'univers de Herbrand, puis en ajoutant les variables universelles, permet d'écrire des fonctions simple de la structure, puis en ajoutant le prédicats "=" et l'opérateurs logique "ou" , et la négation des littéraux, permet d'écrire des skolems c'est à dire des disjonctions de littéraux.
Par exemple voici une théorie composé de 2 skolems :
f(x,x)=x ou ¬A(x) ou B(c,s(x))
f(x,y)=f(y,x) ou ¬B(x,y)
Il n'y a pas de différence fondamentale entre le prédicat et la fonction. Une fonction y=f(x) peut être définie sous la forme d'un prédicat A(x,f(x)), et un prédicat B(x) peut être défini par une fonction f(x) d'image {0,1}. Il y a donc possibilité d'unifier d'avantage le langage.
La théorie est une conjonction de skolems, c'est à dire un ensemble de disjonctions de littéraux. S'il est necéssaire de recourire à une variable existencielle, alors on la skolemise en une fonction existencielle première que l'on intègre dans la présentation c'est à dire dans le langage. Une axiomatique est un sous-ensemble minimale de skolems qui engendre la théorie. La théorie possède plusieurs axiomatiques équivalentes qui forme autant de facette logique de la structure.
La représentation d'une théorie comme un ensemble de skolems est évidement à l'ordre prés des skolems, et pour chaque skolem à l'ordre prés des littéraux de la skolem et à une permutation près des variables de la skolem.
Le principe de la structuration mathématique, de première abord, consiste à extraire, dans un langage du premier ordre, des petites structure suffisament générale pour pouvoir être réutiliser dans de nombreux cas similaires en effectuant une simple traduction, une substitution des opérateurs avec permutation des arguments. On extrait d'une structure quelconque, une sous-structure qui servira de model et que nous appelons catégorie. Afin qu'elle soit la plus générale possible, on fait abstraction de ses méthodes de constructions particulières pour ne retenir que les méthodes propres à la sous-structure choisie. La catégorie est en cela une forme d'abstraction. Nous dirons qu'une structure appartient à la catégorie s'il existe une traduction transportant la théorie de la structure dans le langage de la categorie et qui permet de valider une axiomatique de la categorie. L'appartenance d'une structure à une catégorie est validé par un moteur de recherche, et une fois validé, les apports de la categorie sont compilée dans la structure.
L'arité est un entier positif ou nul. On y ajoute l'arité µ, correspondant à l'arités d'une suite finie. Et on y ajoute par extension n*µ correspondant à n suites finies et µ*n correpondant à une suite fini de n-uplets. Et on y ajoute µ*µ correspondant à une suite finie de suites finies, et ainsi de suite. Nous avons également µ+3 qui correspond à une suite finie d'élément de W suivi de 3 éléments de W. On évalue les arités entières quand cela est possible et on ordonne dans l'addition les arités les plus importantes en premier de tel sorte que l'arité µ*2*µ + µ*(µ+2) ne peut s'écrire autrement.
Une serie infinie, d'un point de vue constructif, est une fonction calculable f tel que la serie est égale à (f(0),f(1),f(2),f(3),f(4),...). Aussi, désigner une serie infinie comme argument d'une fonction ou d'un prédicat revient à désigner une fonction calculable f d'arité 1 comme argument. On note une tel arité par la lettre F. De même l'arité 2*F désigne 2 séries infinies et l'arité F*2 désigne une suite infinie de couples. Et l'arité F*F désigne une suite infinie de suite infinie, le tout calculable c'est à dire une fonction calculable d'arité 2. Et ainsi de suite.
Noter que "Quelque soit une fonction d'arité 1" est une assertion du second ordre alors que l'expression "Quelque soit une fonction calculable d'arité 1" reste du premier ordre car les fonctions calculables sont énumérables. Ce sont des programmes qui peuvent être énumérés. Il existe une fonction calculable qui appliquer à un entier retourne une fonction calculable de la structure, et qui couvre l'ensemble des fonctions calculables de la structure.
Une structure peut hériter d'une categorie, de ses fonctions calculables, de ses propositions calculables et de ses démonstrations, de ses prédicats et fonctions qui s'ils sont calculables constituent des algorithmes. Pour cela, un branchement doit être opéré au niveau du langage c'est à dire au niveau d'une partie de la présentation de la structure et de la présentation de la categorie, opérant ainsi une simple traduction, une substitution des opérateurs avec permutation des arguments. Et une axiomatique de la categorie doit être vérifiée à partir de la théorie de la structure qui peut être traduite en partie, dans le langage de la categories du fait du branchement choisi. Une fois le branchement opéré et la théorie de la catégorie validées, toutes les axiomatiques de la catégories sont traduites dans la structure en des sous-axiomatiques de la structures, et toute les skolems de la catégorie sont traduites dans la structure en des skolems de la structures, et toute les constructions de la categorie sont transcrite dans la structure.