Exemple : X = f(b), Z = g(A, A), R = h(Z, Y)
Exemple : {A ↦ f(X, X)} * {Y ↦ f(b), X ↦ f(b)}
Exemple : {X ↦ f(X, g(X))}
Exemple : f(a, b, c, d, f(X, h(h(X))))
Dans le champ de saisie du haut de la page ont peut inscrire des expressions conformes à la grammaire suivante :
Soit :
- une série de clauses à unifier, séparées par des virgules.
- un produit de substitutions
- une substitution
- ou un terme
Une clause est :
- un terme gauche le signe « = » un terme droit.
Un terme est soit :
- un prédicat
- une constante
- une variable
Une constante est un identificateur commençant par une minuscule.
Les identificateurs commencent par une lettre et sont éventuellement suivis par des lettres et chiffres ou le blanc souligné « _ ».
Une variable est un identificateur commençant par une majuscule.
Un prédicat est un identificateur formé comme une constante, mais suivit par une liste d’arguments entre parenthèses et séparés par des virgules.
Les arguments sont des termes.
Une substitution est délimitée par des accolades : « { » et « } ». Dans les accolades, on place une liste de couples séparés par des virgules.
Chaque couple est une variable suivie d’une flèche et d’un terme.
La flèche est le caractère unicode « ↦ ». (cf. caractères Unicode)
un produit de substitutions est soit :
- une substitution « * » un produit de substitutions
- une substitution « * » une substitution
- une substitution « * » un terme.
Exemples :
constante : a
variable : X
prédicat : f(h(X), g(b))
terme : f(h(X), g(b))
substitution : { X ↦ h(Y), Z ↦ b }
clause : X = g(b)
clauses : A = f(X, X), Y = f(b), X = f(b), Z = g(A, A), R = h(Z, Y)
produit de substitution : {A ↦ f(X, X)} * {Y ↦ f(b), X ↦ f(b)} * {Z ↦ g(A, A)} * h(Z, Y)
ou encore : {A ↦ f(X, X)} * {Y ↦ f(b), X ↦ f(b)}
ou {Z ↦ g(A, A)} * h(Z, Y)
Les éléments peuvent être séparés par des espaces et des retours à la ligne.
Note : les exemples de Wikipédia comme f(g(X),X) = f(Y,a) peuvent être copier-collés directement.
Le parseur est écrit avec la bibliothèque PEG.js Parser Generator for JavaScript acessible à l'adresse : https://pegjs.org