Les fondements de la logique et des mathématiques se trouvent dans l'informatique, car une démonstration correspond à l'exécution d'un programme informatique qui se termine. C'est pourquoi notre approche des fondements s'accompagne d'un développement informatique.
L'informatique ainsi que la logique classique utilise les booléens comme valeurs logiques et comme données élémentaires d'information. Néanmoins Turing et Godel nous dévoilent l'existence inévitable de propositions indémontrables, qui sont donc ni vrais ni fausses. Cela introduit une logique ternaire (voir Logique-ternaire ) qui ouvre un nouveau paradigme. Ce nouveau paradigme nous permet plus facilement de nous affranchir de nos présupposés et préjugées d'autant difficile à se défaire qu'ils nous sont inconscients.
Avant la logique, la contradiction n'existe pas, et plus précisément la négation n'existe pas. Néanmoins le raisonnement existe. Et il peut être décrit de la façon la plus générale possible comme étant un procédé calculatoire. On définit le raisonnement par la calculabilité. On considère le langage des propositions. Le système de déduction est un processus énumératif de proposition. Il énumère l'ensemble des propositions déductibles qui forme un sous-langage, et il se peut dans certain cas que le complémentaire de ce sous-langage ne soit pas énumérable. Un tel sous-langage est dit semi-décidable.
Les linguistes considèrent que tout langage se ramène nécessairement à un langage de caractères. Les éléments de ce langage sont appelés des mots. Dans un tel langage, un sous-langage semi-décidable se définit par son énumérateur, un moteur de production de mots qui l'engendre. Les travaux de Noam Chomsky montre que tout sous-langage semi-décidable peut être énuméré par un moteur de production de mot d'un type particulier, qui consiste à exécuter toutes les substitutions d'occurences possibles décrites par une grammaire formelle.
Une autre approche peut être faite en considérant que tout langage se ramène nécessairement à un langage d'opérateurs d'arité fixe. Les éléments de ce langage son appelés des termes. Dans un tel langage, un sous-langage semi-décidable se définit par un moteur de production de termes qui l'engendre. Le moteur en question exécute toutes les unifications possibles décrites par une grammaire formelle. Et il existe un parallèle entre les deux procédés de production, par substitution d'occurence, ou par unification.
Dans un point de vue simplifié, on ne retient pas la syntaxe des propositions. Nul syntaxe nécessaire pour formuler une proposition. On ne retient la syntaxe que dans les démonstrations. Autrement dit, tout mot est une proposition, et toute démonstration obéït à une syntaxe, qui est définie par une grammaire formelle.
La grammaire formelle utilise deux sortes de caractères, les caractères terminaux et les caractères non-terminaux. Ces derniers sont ajoutés à l'alphabet du langage pour former un langage étendu. Il y a alors deux sortes de mot ; les mots terminaux qui ne comprennent que des caractères terminaux, et les mots non-terminaux qui comprennent des caractères non-terminaux. Ces deux sortes de mot correspondent respectivevement à deux sortes de proposition ; les proposition concrètes, et les proposition abstraites.
Puis la grammaire formelle utilise des règles définies par un couple de mots terminaux ou non-terminaux et que l'on représente séparés par le meta-opérateur binaire `->`. La règle indique une substitution autorisée : Toute occurrence du premier mot apparaissant dans une proposition affirmée peut être susbstituée par le second mot pour produire une proposition déduite. Il apparait donc un troisième type de proposition que sont les couples de mots et constitue les règles de substitution.
La grammaire regroupe les règles de substitution autorisée. La notion de théorie est juste un petit peu plus générale. Elle ne fait pas de distinction entre proposition concrète, proposition abstraite, et règle de substitution. Dans un langage de caractère, une théorie est un ensemble fini de propositions pouvant couvrir les trois types de proposition : proposition concrète, proposition abstraite, et règle de substitution. Par exemple, considérons la théorie suivante où les caractères non-terminaux sont notés en majuscules :
`{aab, A"→"A A, ab"→"Aa, aA"→"bAb, bA"→"a}`
L'ensemble des déductions est :
`{aab,aAa,aA Aa,bAb,ab,Aa,bAbAa,abAa,aaa,... }`
La distinction entre proposition concrète et proposition abstraite traduit une préoccupation de concrétisation. N'est considéré comme concret que les seuls propositions concrètes. Ainsi l'ajout d'une proposition abstraite qui n'entrainerait aucune déduction concrète sera jugée comme une hypothèse abstraite dénuée de conclusion concrète.
On définit un langage d'opérateurs en présentant des opérateurs générateurs tel que par exemple `a,b,f"(.)",g"(.,.)",h"(.,.)"`. Les termes du langage sont les termes clos qu'il est possibles de construire par compostition tel que par exemple le terme `g(h(a,f(b)),g(a,a))`. Puis on ajoute dans ce langage des variables `A,B,C,...` dites libres, et que l'on note en majuscule. Notez alors que les éléments `a,b` sont des constantes, et qu'il y a donc deux types d'opérateurs nullaires, les contantes et les variables. Une proposition ne comprenant que des opérateurs constants est appelée une proposition constante. Une proposition comprenant une ou des variables est appelées une proposition universelle. Une proposition réduite à une variable tel que `A` désigne toutes les propositions, puisqu'elle est unifiable avec toutes les propositions. Ainsi on donne une interprétation ensembliste à chaque proposition universelle. Chacune d'elles désigne l'ensemble des propositions constantes unifiables à elle. Et chaque proposition constante désigne l'ensemble singleton le contenant.
Le moteur de production va comparer deux propositions en tentant de les unifier. Le processus d'unification va affecter les variables de la façon la plus générale possible. Et un premier choix de moteur devra être fait à ce stade. À savoir, s'il faut accepter les termes récurcifs ou non. Si l'unification réussit, elle produit une proposition représentant l'intersection des deux ensembles représentés par les deux propositions.
La grammaire formelle comprend des propositions universelles c'est à dire contenant des variables, et des règles de production binaire, ternaire, ou quaternaire..., `"(.→.)"`, `"(.,.→.)"`, `"(.,.,.→.)"` dont la signification est la suivante. Si les premiers arguments s'unifient à des propositions affirmées alors l'opérateur de production produit une nouvelle proposition de déduction qui est son dernier argument dans lequel les variables libres sont remplacées par leurs valeurs d'affectation obtenues lors de l'unification des autres arguments.
La notion de théorie est juste un petit peu plus générale. Elle ne fait pas de distinction entre proposition constante, proposition universelle, et règle de production par unification. Dans un langage d'opérateurs, une théorie est un ensemble fini de propositions pouvant couvrir les trois types de proposition : proposition constante, proposition universelle, et règle de production par unification. Par exemple, considérons la théorie suivante où les opérateurs nullaires variables sont notés en majuscules :
`{f(a), f(A)"→"f(f(A))}`
L'ensemble des déductions est :
`{f(a), f(f(a)), f(f(f(a))),...}`
Mais n'allons pas trop vite. Commençons par le langage le plus rudimentaire possibles, c'est à dire ne contenant que des opérateurs nullaires `a,b,c,d...` que l'on peut numéroter de `1` à `n`. Dans un tel langage `Omega`, il y a exactement `n` propositions possibles `Omega"="{1,2,3,...,n}`. Les règles de raisonnement sont des couples d'éléments, que l'on note à l'aide du méta-opérateur de production `"→(.,.)"`. La règle `x"→y"` signifie que si la proposition `x` est affirmée alors on en déduit la proposition `y`. Cette règle syntaxique de production est une règle de raisonnement. Et on est encore dans le raisonnement hypothético-déductif, même sans définition ni de la négation ni de la contradiction, ni d'aucun autre connecteur logique. La proposition qui sert d'hypothèse est affirmée. Mais, de par l'absence de négation, elle ne peut pas être négativée, et de par l'absence d'autre connecteur logique elle ne peut pas être présentée comme une alternative ou une conjonction avec une autre.
Le méta-langage des règles se définit donc comme étant `Omega^2`. Chaque règle désigne un arc entre deux sommets éléments de `Omega`. Dans ce langage simple, une grammaire est un graphe (ensemble d'arcs). Une théorie est juste un petit peu plus générale qu'une grammaire, en regroupant des propositions appartenant à `Omega` et des règles appartenant à `Omega^2`. Une théorie est un graphe (ensemble d'arcs) avec un sous-ensemble de sommets.
Un premier principe réflexif stipule qu'une hypothèse se démontre à partir d'elle-même. Autrement dit, si on affirme une proposition `p` alors on déduit la proposition `p`. Ce principe est nécessaire pour réunir les hypothèses avec les propositions déduites en un seul ensemble de propositions dites affirmées. Cet ensemble fini qui s'apparente à une conjonction représente l'état de connaissance du moteur de déduction. Et cet état évolue par accroissement, jamais par réduction car une proposition affirmée l'est toujours, de par le principe réflexif. Ce principe se traduit dans un autre méta-langage par la règle de production suivante :
`P |-- P`
où `P` désigne une variable universelle unifiable à toute proposition du langage.
Dans notre exemple générale, nous considérons `n` propositions possibles `1,2,3,...,n`, et donc `n^2` règles possibles. Une théorie consistera en un ensemble de propositions et de règles. Il convient de les implémenter, c'est à dire d'en trouver une représentation informatique pertinente. Et on ne va pas se restreindre aux seuls entiers pour désigner ces `n` atomes, on utilisera n'importe quel mot lisible par un humain.
La première forme qu'il convient d'établir est le dump-texte (en anglais "text dump"), c'est à dire une sauvegarde lisible par un humain, un texte, et qui doit pouvoir s'incorporé dans une ligne de commande linux comme paramètre. On choisira naturellement le texte le plus proche de l'écriture théorique. Ainsi la chaine de caractères `a"→"b,c,b"→"d` désignera un dump-texte d'une théorie. Néanmoins il ne doit pas y avoir de caractère d'espace ni de caractère réservé au shell Bash dans l'expression. Si on souhaite réduire cette contrainte, il convient de mettre des guillement doubles ou simples autour de l'expression. Mais là encore, quelques règles propres au shell perduront. Aussi, afin de complètement se libérer de ces restrictions tout en restant à un bas niveau de programmation système, il nous faut permettre de pouvoir choisir les caractères opérateurs "`"→"`" et séparateur "`","`" et de les remplacer par n'importe quel caractère distincts si nécessaire, de prévoir une traduction des autres caractères, et aussi une traduction des mots, constituant ainsi un premier niveau de traduction. Car on ne veut pas être contraint par la forme du texte.
La seconde forme est celle compilée, prête à être utilisée de manière rapide. Lorsque `n` n'est pas trop grand, c'est la mémorisation sous forme d'une matrice, la matrice d'adjacence. Lorsque `n` devient grand, c'est la mémorisation sous forme d'une liste de listes, et lorsque `n` devient trés grand devant le nombre d'arcs, on établit à l'aide d'un hachage une liste plus petite de sommets comprenant les sommets ayant au moins un arc.
Le but est de donner une valeur de vérité pour chaque sommet, valant `1` s'il fait partie de l'hypothèse ou s'il est accessible à partir de l'hypothèse en empruntant des arcs, et valant `0` sinon. On utilise pour cela la matrice d'adjacence booléenne. On calcul la propagation d'un flux à travers un graphe. On peut enrichir le résultat pour donner une valeur de complexité à chaque sommet, valant zéro s'il fait partie de l'hypothèse, valant `1` si on y accède en appliquant au moins une règle (un arc), valant `n` si on y accède en appliquant au moins `n` règles (`n` arcs se succédant), et valant `oo` si le sommet n'est pas accessible. On peut en plus enrichir le résultat pour donner à chaque sommet, un tel exemple de chemin le plus court y accédant en partant des hypothèses.
Le but peut se limiter à évaluer un sommet en particulier. L'algorithme utilisé part alors du sommet en question et calcul la propagation inverse d'un flux partant de ce sommet à travers le graphe, jusqu'à atteindre un sommet faisant partie de l'hypothèse.
Le problème s'enrichie en attribuant une complexité spécifique toujours positive à chaque arc. Et la résolution s'obtient alors à l'aide d'un algorithme un peu plus sophistiqué de recherche du plus court chemin qu'est l'algorithme de Dijkstra. Cet algorithme est de complexité en `O(aln(n))` où `n` est le nombre de sommets et ou `a` est le nombre d'arrètes.
Le problème s'enrichie en attribuant un poids spécifique positif à chaque arc. Il faut de plus poser des arcs réflexifs sur tous les sommets. Pour chaque sommet, on attribue une probabilité d'emprunter un arc égale au rapport du poid de l'arc divisé par la sommes des poids des autres arcs partant du même sommet. Et on considère une évolution au hasard, une succession de transition d'état au hasard selon des probabilités fixes ainsi calculées.
Chaque règle `x"→"y` est ainsi munie d'une probabilité réel, et la somme des probabilités des différentes règles partant d'un même sommet `x` est égale à `1`. Cela modélise un système qui raisonne au hasard selon des probabilités de transition qui sont fixe. Le but consiste à calculer les probabilités d'état, à l'état d'équilibre, ou autrement dit, à la fin des temps. On utilise pour cela la matrice de transition.
La maxime qui affirme que le caractère véridique d'une proposition est renforcé si elle est démontrée par des voix différentes et indépendantes (principe de la redondance permettant de détecter les erreurs), doit pouvoir se traduire par une valuation des sommets dans notre graphe, et aussi par une valuation des liens entre sommets.
Commençons donc le raisonnement dans le cas le plus simple, en valuant les sommets, et où les arcs sont considérés comme sûre. S'il existe `n` sommets distincts qui ont un arc allant sur `x`, et que les `n` sommets et le sommet `x` n'ont pas d'autres arcs, alors la valuation de `x`, notée `frV(x)` est égale à `n`. En effet, les sommets en dehors de `x` sont indépendants, et apportent donc chacun une contribution entière. On dira que le sommet est confirmé `n` fois, et cela définira l'indice de redondance du sommet `x` notée `frV(x)`.
Mais un calcul plus précis de probabilité peut être opéré en considérant une distribution équiprobable d'évènements élémentaires indépendants, où un évènement élémentaire, tel un état microscopique, est défini par un `n`-uplet de booléens désignant la valeur de vérité booléenne de chacun des `n` sommets.
Il y a alors `2^n -1` micro-états sur les `2^n` micro-états possibles, qui entrainent `x`. La probabilité de déduire `x` est donc égale à `1-2^-n`.
Par contre si parmi ces `n` sommets, certains sont liés de façon symétrique, c'est à dire sont reliés par un arc dans les deux sens, ils ne comptent alors que pour un. Et ce principe reste valable si les sommets sont liés de façon symétrique non pas par deux arcs mais par deux chemins de taille quelconque, car cela indique que les sommets en question sont équivalents. Et s'ils sont équivalents, ils sont complètement dépendants et ne compte donc que pour un.
Un calcul plus précis de probabilité peut être opéré, en prenant comme hypothèse une distribution équiprobable et indépendante des `n`-uplets (valeurs de vérité des `n` sommets) dans laquelle on enlève toutes les configurations non compatibles avec les arcs du graphe. Si une relation d'équivalence subdivise ces `n` sommets en `k` classes alors la propabilité de déduire `x` devient égale à `1-2^-k`. Et l'indice de redondance du sommet `x` tombe à `k`.
Dans le cas plus générale, le dénombrement se fait de la façon suivante : Considérons un graphe s'appuyant sur `n` sommets. Le nombre de micro-état est ` 2^n`. Pour chacun des micro-états, on vérifit s'il est compatible avec le graphe, et on ne retient que ceux compatibles avec le graphe. Puis pour chaque sommet, on calcul sa probabilité `p` qui est égale au rapport entre le nombre de micro-état compatible où le sommet est vrai, et le nombre de micro-état compatible où le sommet est faux. Puis on passe de la probabilité `p` à l'indice de redondance par la formule `-log(1-p)` avec un logatithme en base `2`.
Maintenant valuons les liens entre sommets à partir des chemins existant. La valuation sera minimale positive et se définira récursivement. S'il existe `n` chemins disjoints qui partent de `x` pour aller sur `y`, et qu'il n'y a pas d'autre arc, alors la valuation du lien de `x` à `y`, noté `frV(x,y)`, est égale à `n`. En effet, les chemin en dehors de `x` et `y`, sont disjoints et indépendants, et apportent donc chacun une contribution entière. On dira que le lien est confirmé `n` fois, et cela définira l'indice de redondance du lien `(x,y)`.
Si on compose bout à bout et dans le bon sens deux liens ayant comme valuation `a` et `b`. Le lien résultant aura une valuation nécessairement supérieur ou égale à `"min"(a,b)`. En effet si chaque partie d'un chemin est confirmée `k` fois alors le chemin complet est nécessairement confirmé au moins `k` fois, et il peut l'être davantage s'il existe d'autres chemins parallèles au chemin complet. Par contre s'il existe un arc entre deux de ces chemins parallèles, on ne peut pas faire la valuation du fait que les chemins ne sont pas indépendants. Et dans ce cas, on considérera un chemin plus court afin que cette situation ne se produise pas. L'ensemble de ces règles permet de définir une valuation à minima des liens.
Un calcul un peu différent basé sur les probabilité peut être opéré. On considèrer une probabilité forte `tau` de non-erreur de calcul propre à chaque arc. On considère de plus que ces probabilités sont indépendantes entre-elles. Délors la probabilités de non-erreur d'un chemin de taille `k` vaut `tau^k`. Et il est alors possible de définir de façon exacte la probalitité d'un lien. C'est la probabilité que tous les chemins parallèles au lien soient en erreur.
---- 21 février 2021 ----
d'évènements élémentaires indépendants, où un évènement élémentaire, tel un état microscopique, est défini par un `n`-uplet de booléens désignant la valeur de vérité booléenne de chacun des `n` sommets.
distribution équiprobable d'évènements élémentaires indépendants, où un évènement élémentaire, tel un état microscopique, est défini par un `n`-uplet de booléens désignant la valeur de vérité booléenne de chacun des `n` sommets.
Une première interprétation consiste à poser une probabilité faible `epsilon` d'erreur de calcul inhérente à chaque arc. Si l'arc en question à un indice de redondance égale à `k`, c'est que l'arc est confirmé
c'est à dire de l'indice de redondance des liens `k=frV(x,y)`, qui se traduit par une probabilité des liens d'implication `(x,y)` par la formule inverse `1-2^-k`.
On peut alors perfectionner notre valuation des sommets en tenant compte de la valuation des chemins.
tel que décrit dans l'approche calculatoire Logique-ternaire .
Une règle syntaxique de déduction peut se définir de la manière la plus générale possible comme étant un opérateur binaire `"→(.,.)"` qui prend comme premier argument une proposition jouant le rôle d'hypothèse et qui indique dans son second argument ce que produit la règle si l'hypothèse est affirmé. Cette règle syntaxique de production est une règle de raisonnement. Et on est encore dans le raisonnement hypothético-déductif, même sans définition de la négation ni de la contradiction. La proposition qui sert d'hypothèse est affirmée, mais, de par l'absence de négation, elle ne peut pas être négativée.
Un premier principe réflexif stipule qu'une hypothèse se démontre à partir d'elle-même. Aautremant dit, si on affirme une proposition `p` alors on déduit la proposition `p`. Ce principe est nécessaire pour réunir les hypothèses avec les propositions déduites en un seul ensemble de propositions dites affirmées. Cet ensemble fini représente l'état de connaissance du moteur de déduction. Et cet état évolue par accroissement, jamais par réduction car une proposition affirmée l'est toujours, de par le principe réflexif. Ce principe se traduit dans le langage par la règle de production suivante :
`p -> p`
où `p` désigne une variable universelle unifiable à toute proposition du langage. Dans l'exemple nous considérons 4 constantes prélogiques `a,b,c,d`, mais nous pouvons avoir `n` contantes prélogiques. Dans ce langage d'opérateurs `(a,b,c,d,"→(.,.)")`, les propositions sont des éléments du `"Magma"("→(.,.)",a,b,c,d)` qu'il convient d'implémenter, c'est à dire d'en trouver une représentation informatique pertinente.
Un élément du magma à `n` générateurs est un arbre binaire stricte (où chaque noeud a exactement `0` ou `2` fils) et dont les feuilles sont des éléments appartenant à un ensemble de `n` atomes tel que par exemple `{1,2,3,...n}` et qui représenteront `n` constantes prélogiques, c'est à dire dans un univers sans négation. Néanmoins on ne va pas se restreindre aux seuls entiers pour désigner les atomes, on utilisera n'importe quelle mot lisible par un humain.
La première forme qu'il convient d'établir est le « dump texte » , c'est à dire une sauvegarde lisible par un humain, un texte, et qui doit pouvoir s'incorporé dans une ligne de commande linux comme paramètre. On choisira naturellement le texte le plus proche de l'écriture théorique. Ainsi la chaine de caractères `a"⊢"(b"⊢"c)` désignera un dump texte. Néanmoins il ne doit pas y avoir de caractère d'espace ni de caractère réservé au shell Bash dans l'expression. Or les parenthèses sont des caractères réservés. Si on souhaite outre-passer cette condition, il convient de mettre des guillement double ou simple autour de l'expression. Mais là encore, quelques règles propres au shell doivent être respectées. Puis, afin de se libérer de toutes ces contraintes tout en restant à un bas niveau de programmation système, il nous faut pouvoir spécifier les caractères opérateurs `"⊢"` et `"("` et `")"` afin de pouvoir les remplacer par n'importe quel caractère distincts, et prévoir une transcription éventuelle d'autres caractères voir de mots, constituant un premier niveau de traduction.
La seconde forme est celle dite compilée, prête à être utilisé de manière rapide. C'est la mémorisation sous forme d'arbre binaire.
Etant donné `n` atomes qui représentent `n` inconnus prélogiques. Une proposition prélogique est un élément du magma engendré par ces `n` atomes. Etant donné une liste de propositions appelées hypothèses, il existe un procédé exhaustif qui énumère toutes les déductions possibles avec leur niveau de complexité démonstrative c'est à dire le nombre minimum d'application de règles de déduction nécessaire pour produire le résultat.
L'algorithme consiste à explorer toutes les productions possibles par application de la règles de transitivité :
`(a"⊢"b", " b "⊢"c) -> a"⊢"c`
L'unification qui est utilisé est très rudimentaire. Elle utilise l'accès au premiers fils, l'accès au second fils, ainsi que l'opération inverse la construction d'une proposition à partir de deux propositions jouant le rôle des fils. Et elle utilise l'égalité d'expression entre proposition.
---- 17 février 2021 ----
7) Résolution prélogique en partant du but.
Un terme est une règle de production si et seulement il possède comme racine un opérateur de production. Et alors sont aspect dynamique consiste à unifier ses arguments d'entrés avec d'autre terme (ou lui-même), ce qui entraine la production d'un nouveau terme résultat.
On considère un ensemble de termes comme un mélange chimique. Les termes sont considérés comme des molécules et intéragissent suite à des collisions. Un terme productif peut unifier ses arguments d'entrée avec d'autres termes (ou lui-même) présent dans le mélange et produire un nouveau terme qui s'ajoute au mélange. Par exemple :
`g(A,B),h(A,B)→g(B,f(B))`
`g(a,a)`
`h(A,A)`
Le terme `g(a,a)` et le terme `h(A,A)` que l'on renomme en `h(C,C)` afin que ses variables soient différentes de celles déjà existantes, peuvent s'unifier avec les entrées du terme productif et ainsi produire le résultat suivant : `g(a,f(a))`
Notez que dans d'autres cas, le résultat peut être également un terme productif.
On utilise une structure de données mettant en oeuvre le partage de données afin que là où un seul traitement est nécessaire cela ne nécesssite pas plusieurs traitements. Pour faire cela, on utilse des pointeurs qui peuvent pointer les sous-termes d'un terme. Chaque pointeur pointe soit une constante, soit une variable, ou soit un terme.
Un terme est mémorisé sous forme d'un graphe orienté acyclique composé de noeuds comprenant 2, 3 ou plus de pointeurs selon l'arité maximum utilisée, et de feuilles que sont les variables et les constantes. Par exemple le terme `g(a,g(X,a))` est mémorisé comme suit :
Les variables et les constantes sont des composants symétriques ici respectivement en vert et en orange tandis que les noeuds sont en blanc. Les variables et les constantes sont mémorisés de façon unique, autrement dit il ne peut y avoir deux cases contenant une même variable ou une même constante. Le noeud représente le terme dont il est la racine.
On programme quelques opérations de base :
L'itérateur Lister(A,B) prend en argument deux pointeurs A, B pointant sur des noeuds de même taille et retourne la liste des couples (A[0],B[0]), (A[1],B[1]), (A[2],B[2]),... où A[n] représente le pointeur présent dans la case numéro n du noeud A.
La fonction VariableLibre(P) prend en argument un pointeur et retourne vrai s'il pointe sur une variable libre.
La fonction Taille(P) prend en argument un pointeur pointant sur un noeud et retourne sa taille.
La condition a=b retourne vrai si les pointeurs a et b sont égaux c'est à dire s'ils pointent sur un même endroit.
L'affectation a:=b modifie le contenue de la variable libre pointée par a, en lui attribuant la valeur pointée par b. Une fois affectée, la variable n'est plus libre et à chaque solicitation, elle retourne ce quelle contient, en créant d'éventuels raccourcis au cas où plusieurs variables sont mémorisés en cascades, cette création de raccourcis étant nécessaire pour assurer pleinement la complexité linéaire de l'algorithme.
Unifie(a,b) {
if a=b then return true
if VariableLibre(a) then {a:=b; return true}
if VariableLibre(b) then {b:=a; return true}
if Constante(a) or Constante(b) then return false
if Taille(a) ≠ Taille(b) then return false
Lister(a,b){(u,v) | if not Unifit(u,v) then return false}
return true
}
La fonction Unifie prend en argument deux pointeurs pointant deux termes et les unifie. Elle retourne vrai si l'unification réussie. Après une unification réussie, les variables contiennent le réultat de l'unification. Il faut donc préalablement garder en mémoire ces variables, ceci afin de pouvoir récupérer leur valeur après unification. (L'unification peut aussi s'effectuer à n termes de façons très efficaces par un algorithme analogue).
L'epression du genre f(a){x|g(x)} correspond à une forme de programmation Ruby appellée "bloc de code", où le bloc de code en question est {x|g(x)}. Cela signifie que f(a) produit une listes de valeurs résultats, et pour chaque valeur x ainsi produite on exécute la commande g(x).
On se place dans un langage `ccL` d'opérateurs d'arités fixes. Les mots de ce langage sont appelés des termes est correspondent à des propositions.
On procède à une extension élémentaire, par exemple de trois éléments, notée `ccL[x,y,z]`, en ajoutant trois variables `x,y,z` qui représentent n'importe quelle proposition du langage. Ces variables sont initialement libres et servent d'arguments. Ainsi un élément de `ccL[x,y,z]` constitue une application de `ccL^3->ccL`.
On programme l'unification de deux termes du langage comme suit : Les termes sont mémorisé sous forme d'arbre (ou de graphe).
unifit(x,y)
if x=y then return 1
if