On construit un langage d'opérateurs comme un jeu de légos, d'une façon la plus libre possible afin d'obtenir une syntaxe simple possèdant une trés grande capacité d'expression. Et nous procédons étape par étape de tel sorte que chaque choix découle de source.
Puis on construit un modèle qui donne à ces opérateurs un sens plus profond, une sémantique.
Puis on construit un langage logique où chaque propositions est décidable dans ce modèle, c'est à dire tel qu'à chaque proposition exprimable par le langage, il existe un algorithme de calcul donnant toujours une réponse affirmative ou négative en un temps fini.
La construction s'appuit sur la programmation qui est le véritable fondement de la logique. Selon les préceptes élémentariens, la garanti de cohérence du système logique est reportée dans le processus constructif auquel nous nous soumettons.
Syntaxe et sémantique constituent deux niveaux de langages, l'un étant complètement formalisé, l'autre pas toujours, mais ayant l'avantage d'être à la base de l'intuition. L'intuition ne participe pas d'un langage de démonstration exacte. Elle s'appuit sur l'empirisme et le rêve qui sont l'antithèse de la science hypothético-déductive. L'intuition est ce par quoi on construit l'hypothèse. La démonstration exacte est peut être écartée de ce processus, mais le principe constructif est toujours là, et l'intuition peut aussi être formalisée telle une heuristique.
On définie un langage d'opérateurs en présentant un ensemble d'opérateurs générateurs d'arité fixe formant un jeu de légos parfairtement libre, tel que :
`L = {a, b, f"(.)", g"(.,.)"}`
Syntaxiquement ces opérateurs sont enfichables les uns dans les autres pour former, par composition close, des termes tels que `b`, `f(a)`, `g(a,f(a))`, etc..
Le typage exprime les règles d'emboitement :
`a` et `b` sont des éléments de type `E`.
`f"(.)"` est un élément de type `E->E`.
`g"(.,.)"` est un élément de type `(E,E)->E`.
Le point "`.`" désigne un élément attendu de type `E`.
Sémantiquement, ces opérateurs représentent des fonctions opérant sur un ensemble sous-jacent noté `E` (et pour certains d'entre eux, `a` et `b`, directement des éléments de `E` considérés comme des opérateurs d'arité zéro). Les arités sont mentionnées par les suffixes `"(.)"` pour unaire, `"(.,.)"` pour binaire, etc., et le point "`.`" désigne un élément attendu appartenant à l'ensemble `E`.
Peut-on choisire l'ensemble `E` , les éléments `a, b` et les fonctions `f, g`, pour que le jeu de légos associé soit parfaitement libre ?. Oui, en unifiant la syntaxe à la sémantique, il suffit de choisire comme ensemble `E` l'ensemble des termes engendrés. C'est le modèle de Herbrand.
L'ensemble des termes est obtenue par composition close des opérateurs générateurs, et forme l'univers de Herbrand noté `L° = "<"a,b,f,g">"`. Cela regroupe tous les éléments constructibles d'arité nulle, et cela forme une structure libre.
`L° = "<"a,b,f,g">" = {a,b,f(a),f(b),g(a,a),g(a,b),..., f(f(a)),...}`
La structure `L°` , noté aussi `"<"a,b,f,g">"` est libre. Cela signifie que la méthode de construction est libre, telle un assemblage de légos. Chaque terme distinct ainsi construit désigne nécessairement un élément distinct de la structure.
Par exemple le terme `g(a,f(b))` est un élément de la structure libre `"<"a,b,f,g">"`. Syntaxiquement, il est de type `E`. Sémantiquement, il appartient à `E`. Et lorsque `E` est identifié à l'univers de Herbrand, cela revient strictement au même. On identifie donc l'ensemble sous-jacent à la structure libre. On se place donc dans le modèle de Herbrand :
`E = L° = "<"a,b,f,g">"`
Ainsi, la première méthode de construction que propose de langage d'opérateurs est la composition close d'opérateurs. Puis le langage va s'enrichir, se complexifier, et d'autres méthodes de construction seront mises en oeuvre.
Il y a deux sortes d'extensions possibles, les extensions intérieurs et les extensions extérieurs. Les extensions extérieurs consistent à compléter le langage (et donc le modèle) selon la même logique de construction, en ajoutant de nouveaux éléments et opérateurs générateurs. Par contre les extensions intérieurs réalisent une cloture de construction avec les moyens existant. Elles apparaissent sous forme de variables internes ou externes.
Une variable interne `x` désigne un élément inconnu mais qui est constructible par le langage c'est à dire un terme appartenant à `E`.
`x in E`
Une variable externe `x` désigne un nouvel opérateur générateur, qui va agrandire `E` et qui correspond à une extension du langage (et donc du modèle).
`x !in E`
Les variables complètent le langage selon la même logique de construction et possède une arité et un type.
Les variables internes d'arité nulle sont dites de type `E` et sont des éléments de `E` . Les variables internes unaires sont dites de type `E->E` est sont des fonctions de `E` vers `E`. Les variables internes binaires sont dites de type `(E,E)->E` et sont des fonctions de `E×E` vers `E`, etc.. Mais à ce stade, on ne considère que des variables internes de type `E`, et la logique ainsi développée s'appelle la logique du premier ordre.
La seconde méthode est la création de séquences. Ainsi on peut définir une séquence tel que `(a, f(b), g(a,f(a)), a)` qui sera de type `(E,E,E,E)` que l'on note aussi `E×E×E×E` ou de façon condensé `E^4`. On peut aussi créer des séquences de type varié telle que `(a, g, f)` qui sera de type `(E,(E×E->E),(E->E))` noté également `E×(E×E->E)×(E->E)`.
Nos connaissances en programmation nous permettent de voir une simplification utile des types listes, en les considérant comme des listes aplaties sur un seul niveau appelé séquence. Cela consiste à considérer l'opération × dans le langage des types comme étant une opération associative, `(A×B)×C = A×(B×C) = A×B×C` ou autrement dit `((A,B),C) = (A,(B,C)) = (A,B,C)`.
La troisième méthode est la construction de fonction unaire. Cela consiste à utiliser une variable d'entré puis à composer un terme en utilisant cette variable d'entré. La construction se fait en utilisant le méta-opérateur binaire `|->` et en l'appliquant à une variable et à un terme dans le langage augmenté de cette variable. La variable constitue la tête de la fonction. Le terme constitue le corps de la fonction. Par exemples, en utilisant la variable `x` de type `E`, voici un exemple de fonction :
`x |-> g(g(x,x),a)`
Le terme ainsi construit désigne un opérateur de type `E->E`.
La tête est une variable libre, c'est à dire soit non encore utilisée, ou soit considéré comme un double non encore utilisée et qui ne sera utilisé que dans le corps de la fonction. Le corps est un terme dans le langage augmenté de la variable de tête.
Les constructions d'opérateurs peuvent être emboitées. Par exemple :
`x |-> ( y |-> g(x,f(y)))`
Après chaque opérateur `|->`, le corps se situe dans un environnement augmenté de la variable de tête, de tel sorte qu'une succession d'opérateurs `|->` dans ce sens abouti à un coprs situé dans un environnement augmenté de plusieurs variables de tête. Et il y a une représentation pratique consistant à regrouper les têtes en une seul tête-liste comme suit :
`(x,y) |-> g(x,f(y))`
Syntaxiquement l'ordre d'évaluation par defaut du méta-opérateur `|->` est choisie de droite à gauche. Ainsi l'exemple précédent devient :
`x |-> y |-> g(x,f(y)))`
et son type est `E->E->E` ou bien encore `(E,E)->E` ce qui est synonyme.
Nos connaissances en programmation nous permettent de voir une simplification utile des types de fonctions. On définie les types de fonction modulo la currification. Ainsi, étant donné trois types quelconques `A,B,C`, le type `(A,B)->C` est identique au type `A->(B->C)` que l'on note `A->B->C` en adoptant un ordre d'évaluation par defaut du méta-opérateur `->` de droite à gauche.
Ainsi `A->B->C` est appellé la représentation série tandis que `(A,B)->C` est appellé la représentation parallèle. Mais les deux expressions représentent le même type. Par contre le type `(A->B)->C` ne se simplife pas.
La construction d'opérateurs unaires emboités les uns dans les autres permet de construire des opérateurs d'arité supérieurs.
La currification à une autre conséquence sur la composition d'opérateurs, elle permet à tout opérateur de pouvoir s'appliquer sur une liste d'arguments partielle mais toujours en commençant par les premiers arguments. Ainsi `g(a)` est de type `E->E` et `g(a)(b)` est égale à `g(a,b)` qui est de type `E`.
Puis il convient de donner également un sens à l'application d'un opérateur sur une liste d'arguments plus grande. Considérons le langage :
`L° = "<"a,b,c,f"(.)",h"(.)",g"(.,.)",k"(.,.)>"`
Trois possibilités s'offrent à nous :
Mode tronqué : `f(a,b,c) = f(a)`
Mode série : `f(a,b,c) = (f(a),b,c)`
Mode harmonique `f(a,b,c) = (f(a),f(b),f(c))`
Le mode tronqué ne convient pas car il occasionne une perte d'information et le mode série est pauvre par rapport au mode harmonique. C'est pourquoi on choisie le mode harmonique qui constitue un mécanisme de factorisation rudimentaire, `f(a,b,c) = (f(a),f(b),f(c))`. Noter que le type de `a` et de `b` et de `c` doit être celui attendu par `f`. Pour un opérateur binaire, nous avons :
`g(a,b,c,d) = (g(a,b),g(c,d))`
`g(a,b,c) = (g(a,b),g(c))`
Réciproquement il convient de donner également un sens à l'application d'une liste d'opérateurs sur une liste d'arguments. Trois possibilités s'offrent à nous :
Mode tronqué : `(f,h)(a) = f(a)`
Mode série : `(f,h)(a) = (f(a),h)`
Mode harmonique `(f,h)(a) = (f(a),h(a))`
Le mode harmonique complète le mécanisme de factorisation. Noter qu'un opérateur d'arité nulle ne peut pas être appliqué à des arguments ni faire partie d'une liste appliquée à des arguments. Pour deux opérateurs binaires, nous avons :
`(g,k)(a,b) = (g(a,b),k(a,b))`
C'est ce que l'on appelle la composition parallèle. Cette méthode de construction permet d'exprimer des calculs complexes avec peu de mots, et constitue une factorisation programmative essentielle du langage.
Pour des opérateurs unaires et binaires, nous avons :
`(f,g)(a,b,c,d) = (f(a),f(b),g(a,b),f(c),f(d),g(c,d))`
`(f,g)(a,b,c) = (f(a),f(b),g(a,b),f(c),g(c))`
La période est donnée par le ppcm (plus petit commun diviseur) des arités en présence.
Notez que l'ensemble des fonctions constructibles par ce procédé est loin d'épuiser l'ensemble des fonctions existantes opérant sur `E`.
Comme on peut le voir, il se constitue déjà un langage de types. Et il est possible d'utiliser des variables de type complexe trés différents. Par exemple, en utilisant une variables `x` de type `E`, une variable `φ` de type `E->E` et une variables `ψ` de type `(E->E)->E`, nous pouvons construire les termes suivants :
Notation série |
Notation parallèle |
||
Terme |
Type |
Terme |
Type |
`x |-> y |-> g(x,f(y)))` |
`E -> E -> E`
|
`(x,y) |-> g(x,f(y)))` |
`(E,E) -> E` |
`x |-> φ |-> g(φ(x),φ(f(x)))` |
`E -> (E->E) -> E`
|
`(x,φ) |-> g(φ(x),φ(f(x)))` |
`(E,(E->E)) -> E` |
`ψ |-> φ |-> φ(ψ(φ))` |
`((E ->E)->E) -> (E->E) ->E`
|
`(ψ,φ) |-> φ(ψ(φ))` |
`((E->E)->E, E->E)) -> E` |
Chaque terme ainsi construit possède un type qui caractérise sont comportement syntaxique que sont les types de ses arguments et le type de son résultat.
Le type d'un terme peut se déduire à partir de sa construction qui le définie et des types des variables qui le composent. Grâce à ce procédé, il se crée au dessus du langage d'opérateurs, un langage des types.
On définie le type des éléments sous-jacents, noté `"E"`, et on définie tous les types dérivables à partir de ce seul type. Ce sont tous les types constructibles à l'aide de l'opérateur binaire `->`.
On constate alors que le langage des types est une langage d'opérateurs `{E, ->}` où `E` désigne un élément de `bbbE` et `->` désigne un opérateur binaire de `bbbE` vers `bbbE`. L'ensemble sous-jacent `bbbE` représente l'ensemble de tous les types constructible à l'aide de `E` et `->`.
`bbbE = "<" E,-> ">"`
Puis on ajoute la construction des listes aplaties, appellées séquences. Par exemple étant donné les types `A`, `B` et `C` on peut définir la séquence `(A,B,C)`. On note `ccL(bbbE)` l'ensemble `bbbE` augmenté de ses séquences.
Puis on étend le domaine de définition de `->` qui est `bbbE ×bbbE`, à l'ensemble `ccL(bbbE)`×`bbbE`.
Puis on introduit une règle d'égalité, à savoir :
Et pour obtenir une règle s'appliquant à des séquences de taille quelconque, on utiliser des variable appartenent à `ccL(bbbE)` ainsi que l'opération de concaténation de séquences notée par une virgule`AA(A,B,C)inbbbE^3, A->(B->C) = (A,B)->C`
`AA(A,B)inccL(bbbE)^2, AACinbbbE, A->(B->C) = (A,B)->C`
Néanmoins une règle plus simple suffit et n'utilise qu'une seul variable appartenant à `ccL(bbbE)` et l'opération de concaténation d'un élément à une séquence notée par un point virgule.
`AABinccL(bbbE), AA(A,C)inbbbE^2, A->(B->C) = (A;B)->C`
On évite ainsi d'utiliser l'opérateur de concaténation de séquences car celui-ci ne permet pas de garantire l'existence d'un algorithme d'unification de complexité linéaire.
--- 1 septembre 2015 ---
Et il n'est pas nécessaire de préciser le type des termes, car la définition du terme est suffisante pour préciser son type dans un modèle d'inférence de type. A partir de variables `x, y,...` de type inconnue notées `a, b, ...` on précise le type des termes comme par exemples :
`L = {a, b, f"(.)", g"(.,.)", h"(...)"}`
Puis on manipule des tuples de termes, mais on n'en fait pas des termes. On parlera donc de tuple de termes, et de type de tuple de termes. La portée de la variable d'une fontcion ne porte que sur son corps, ainsi le tuple `(x->f(x), x->g(x,x))` est identique au tuple `(x->f(x), y->g(y,y))` :
Le terme `g(a)` est identique à la fonction `x|->g(a,x)`.
Les types `a` et `b` sont des variables libres dans le langage des types.
On définie le langage d'opérateurs avec des types plus complexe, des types exprimables dans le langage des types. Dans notre exemple, le langage d'opérateurs est définie comme suit :
`L = {`
`a in E`
`b in E`
`f in E->E`
`g in (E,E)->E`
`h in E"*"->E`
`}`
Il est possible de définir des opérateurs de type plus complexe tel que par exemple `r in` `(E->E)->(E->E)`. De même, une variable interne ou externe possède un type qu'il convient de définir avant de pouvoir l'utiliser. On complète le langage en déclarant un ensemble de variables internes pareillement :
`{`
`x in E`
`y in E`
`z in E`
`w in E->E`
`φ in (E->E)->(E->E)`
`}`
On peut utiliser des variables de type complexe telles que `φ` et `w` pour définir le terme suivant :
`(φ,w,x) -> g(φ(f)(x), w(x))`
Le type de ce terme se calcule par inférence de type :
`((E->E)->(E->E)) × (E->E) × E -> E`
On peut également utiliser des types inconnues `a` et `b`. On peut définir le type suivant :
`(a->b) -> (b->a)`
Puis définir une variable `alpha` de ce type.
`alpha in (a->b) -> (b->a)`
Cette variable peut alors s'appliquer à l'élément `f`. Le terme `alpha(f)` est alors de type `E->E`
On construit les ensembles, les relations, les fonctions et les propositions d'égalités, en utilisant des variables internes.
Un terme possèdant des variables, détermine un ensemble, l'ensemble de tous les termes que l'on peut obtenir en remplaçant les variables par n'importe quel terme possible. Par exemple :
`{f(a)}` `{f(a),f(b),f(f(a)), f(f(b)), f(g(a,a),...}` `{g(a,f(a)), g(b,f(b)), g(f(a),f(f(a))), ...}`
La construction se fait en utilisant le méta-opérateur unaire "union" s'appliquant à un terme possèdant des variables. Par exemples en utilisant deux variables `x` et `y` de type `E` :
`uu_(x,y){g(x,y)} = {g(a,a),g(a,b),g(b,a),g(b,b),g(f(a),a),...}`
Et cet ensemble sera un élément de type `"set"(E)`.
Puis il faut considérer les tuples. On construit les tuples en utilisant le méta-opérateur associatif "virgule" sur des éléments de type quelconque. Par exemple voici un tuple `(a,a,f(a),f(b))` de type `E^4`.
Un tuple possèdant des variables, détermine un ensemble, l'ensemble de tous les tuples que l'on peut obtenir en remplaçant les variables par n'importe quel terme possible. Par exemple :
`{(a,a),(a,b),(b,a),(b,b),(f(a),a),f(f(a),a)...}` `{(a,a),(b,b),(f(a),f(a)),(f(b),f(b)),(g(a,a),g(a,a)),(f(f(a),f(f(a))),...}`
Le méta-opérateur unaire union s'applique également à un tuple possèdant des variables. Par exemples en utilisant la variable `x` de type `E` :
`uu_x{(x,f(x))} = {(a,f(a)),(b,f(b)), (f(a),f(f(a))), (f(b),f(f(b))), (g(a,a),f(g(a,a)))...}`
Le méta-opérateur union peut s'appliquer plusieurs fois de suites, mais il faut préciser qu'elles sont les variables qui varient. Il faut définir précisément le langage utilisé c'est à dire les opérateurs constants, les opérateurs variables qui servent de paramètre c'est à dire qui se comportent comme des constantes, et les opérateurs variables servant à l' union. Par exemple voici une telle construction avec sa définition classique qui s'obtient par une traduction simple :
`uu_x{(uu_y {g(x,y)}, f(x))} = {({g(x,y) "/" y in E},f(x)) "/" x in E}` de type `"set"("set"(E),E)`
Nous pouvons pareillement définir une relation. Une relation binaire est un ensemble de couples. Par exemple le couple de termes `(g(x,x), f(x))` peut définir un ensemble de couples, c'est à dire une relation reliant entre autre :
`g(a,a)` avec `f(a)`,
`g(b,b)` avec `f(b)`,
`g(f(a),f(a))` avec `f(f(a))`,
etc..
Les ensembles construit à l'aide du méta-opérateur union et du méta-opérateur virgule, sont dit premiers. L'intersection de deux ensembles premiers est encore un ensemble premier. Et il existe un algorithme d'unification de complexité linéaire capable de calculer l'intersection de deux ensembles premiers. Cet algorithme constitue la première règle de déduction.
Elle permet de calculer par exemple la valeur logique de la proposition suivante :
`g(f(a),f(a)) in uu_(x,y){g(x,f(y))}`
Cette proposition est identique à la proposition suivante :
`EExEEy : g(f(a),f(a)) = g(x,f(y))`
L'égalité mentionnée désigne l'égalité des termes dans le modèle standart, c'est à dire dans la structure libre du langage, en remplaçant les variables par leur valeur.
Un ensemble est un prédicat unaire. L'appartenance d'un élément à un tel ensemble définie le prédicat `in`. Par exemple :
`g(a,b) in uu_x{g(x,x)} = faux`
`g(f(a),f(a)) in uu_x {g(x,x)} = vrai`
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 cela on utilse des pointeurs qui peuvent pointer sur 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. Chaque variable possède un attribut dont la valeur initiale est le mot clé "libre". Le noeud représente le terme dont il est la racine.
On programme quelques opérations de base :
L'itérateur Distribue prend en argument deux pointeurs `A`, `B` pointant sur des noeuds de même taille et retourne sous forme d'itération les 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 prend en argument un pointeur et retourne vrai si cela pointe sur une variable libre.
La fonction Taille 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é 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 effectuant au cas ou plusieurs variables sont mémorisés en cascades la transitivité de cette cascade en créant les raccourcis correspondants (peut être nécessaire pour assurer stricto-sens-us la complexité linéaire de l'algorithme).
Unifit(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
Distribue(a,b){(u,v) | if no Unifit(u,v) then return false}
return true
}
La fonction Unifit prend en argument deux pointeurs pointant deux termes et les unifie. Elle retourne vrai si l'unification réussie. Pour récupérer la solution présente dans la liste des variables, il faut préalablement avoir mémorisé cette liste de variables, ceci afin de pouvoir récupérer leur valeur après unification.
Un terme est dit indépendant de la variable `x` ssi il ne contient pas la variable `x`. Avec cette notion on définie une quantification des variables respecteuse de l'indépendance. Les variables quantifiées universellement ne dépende de rien puisqu'elle parcours toutes les valeurs possibles. Parcontre les variables quantifiées existentiellement peuvent ne pas dépendre de certaines variables universelles, et on énumèrera pour chacune d'elle les variables universelles dont elle peut dépendre.
Considérons la proposition d'égalité entre deux termes où toutes les variables présentes sont quantifiées avec respect de l'indépendance, c'est à dire en spécifiant pour chaque variable existentielle les seuls variables universelles dont elle est suceptible de dépendre. Par exemple :
`AAxAAyAAzEEu(x)EEv(y,z) : g(u,v) = g(f(x),g(y,z))`
Dans cette proposition qui est vrai dans le modèle standard, toutes les variables présentes sont quantifiés ; trois variables `x`, `y` et `z` sont quantifiées universellement, la variable `u` est quantifiée existentiellement et est indépendante des variables universelles autres que `x`, et la variable `v` est quantifiée existentiellement et est indépendante des variables universelles autres que `y` et `z`.
Une telle proposition se résoud par l'algorithme d'unification qui a le double avantage d'être de complexité linéaire et de produire des solutions constructives. En l'occurrence l'algorithme démontre la proposition en produisant les solutions suivantes pour les deux variables existentielles :
`u = f(x)`
`v = g(y,z)`
La conjonction de propositions d'égalité forme une proposition d'égalité, car la conjonction de deux égalités entre termes se regroupe en une seul égalité entre deux couples de termes.
La négation d'une proposition s'obtient en intervertissant les quantifications avec respect de l'indépendance, et en prenant la négation de l'identité.
`¬ AAxAAyAAzEEu(x)EEv(y,z) : g(u,v) = g(f(x),g(y,z))`
`AAuAAvEEx(u)EEy(v)EEz(v) : g(u,v) != g(f(x),g(y,z))`
La démonstration de ce fondement ne pose pas trops de problèmes tant que le langage est engendré par un nombre fini d'opérateurs.
L'algorithme de résolution n'étant pas un demi-algorithme donnant une demi-réponse, il résoud les non identités avec autant de facilité que les identités. C'est pourquoi les non identités sont ajoutées aux propositions premières.
Comme la négation d'une conjonction est une disjonction, la disjonction de propositions premières est encore une proposition première.