unification是什么意思_unification的常见用法_近义词

词典释义

n.f.
统一;划一
unification d'un pays一个国家

统一

近义、反义、派生词

近义词：

fusion, intégration, normalisation, alignement, homogénéisation, standardisation, uniformisation, jonction, rassemblement, regroupement, réunion, union, fusionnement

反义词：

démembrement, diversification, fédéralisme, schisme, séparation

联想词

réunification 重新统一; harmonisation 协调，调和; unifier 统一，划一，使一致; intégration 结合，一体化，融合; standardisation 标准化; convergence 聚合，会聚，集中，汇合，辐合; centralisation 集中; réorganisation 重新组织，改组; consolidation 加固，加强，巩固; internationalisation 国际化; hégémonie 霸权，盟主权;

当代法汉科技词典

unification f. 兼并[作用]；统一[化]；统一

短语搭配

unification d'un pays一个国家的统一

原声例句

Plusieurs empereurs ont régné sur son territoire depuis son unification il y a plus de 2220 ans!

自2220多年前统一以来，好几位皇帝统治了它的领土!

[Vraiment Top]

En fait, cette unification fait écho à la paix qui existait durant l'hégémonie de la dynastie des Zhou Occidentaux et le début des Zhou Orientaux, entre 1100 et 700 avant notre ère environ.

实际上，这种统一呼应了西周霸权和东周初期的和平，大约在公元前1100年到公元前700年之间。

[硬核历史冷知识]

En mai 1943, enfin, REX accomplit la mission que DE GAULLE lui avait donnée, l'unification de la résistance, étape essentielle pour que la France participe à sa libération et relève le défi de son avenir.

最后，在1943年5月，雷克斯完成了戴高乐赋予他的使命，统一了抵抗运动，这是法国参与其解放和迎接其未来挑战的重要一步。

[法国总统马克龙演讲]

Sa mère a confirmé aujourd'hui être une adepte de l'Église de l'Unification, également connue sous le nom de « secte Moon » .

他的母亲今天证实，她是统一教会的信徒，也被称为“月亮教”。

[RFI简易法语听力 2022年7月合集]

Il l'a confirmé, en effet, la mère de Tetsuya Yamagami est bien une adepte de l'Église de l'Unification, qui revendique 600 000 fidèles au Japon.

他证实了，确实，山神哲也的母亲确实是统一教会的信徒，在日本有60万信徒。

[RFI简易法语听力 2022年7月合集]

Le Figaro montre ce collage, il me dit l'unification de la crème de l'espèce via les réseaux sociaux et le bistouri , et il dit les tortures.

《费加罗报》展示了这幅拼贴画，它通过社交网络和手术刀告诉我物种奶油的统一，并说了折磨。

[La revue de presse 2020年2月合集]

Les combats vont se poursuivre mais avec cette unification il y aura une meilleure coordination une meilleure efficacité.

战斗将继续下去，但随着这种统一，将会有更好的协调和更好的效率。

[RFI简易法语听力 2013年11月合集]

Autre facteur de division en Europe, il existe des États à l'unification ancienne comme la France, le Royaume-Uni, la Russie et d'autres qui sont des constructions politiques beaucoup plus récentes.

欧洲的另一个分裂因素是，有些国家有着旧的统一，如法国、英国、俄罗斯和其他更近的政治结构。

[TV5每周精选 2014年10月合集]

" La séance plénière de clôture du 4e cycle de pourparlers s'est terminée à 17h23 heure locale" , a confirmé l'agence de presse Yonhap, citant un responsable du ministère sud-coréen de l'Unification.

" “第四轮会谈的闭幕全体会议于当地时间下午5点23分结束.m，”韩联社证实，援引韩国统一部官员的话说。

[CRI法语听力 2013年7月合集]

L'histoire de la Chine est extrêmement ancienne : avant même son unification, de nombreuses dynasties se succèdent et des royaumes naissent, s'affrontent, fusionnent ou disparaissent.

中国的历史非常悠久：甚至在统一之前，许多朝代相继相继，王国诞生、冲突、合并或消失。

[硬核历史冷知识]

例句库

Une grande unification de la gamme de produits, de l'eau à l'épreuve, ultra-haute luminosité, de basse tension de sécurité, est une tradition durable des tubes néon et les meilleures alternatives.

产品结构标准化程高，防水，超高亮度，低压安全，经久耐用是传统灯管及霓虹灯的最佳替代品。

La raison majeure de ce décalage résidait dans l'unification allemande, qui a engendré un choc réel asymétrique pour toute l'Europe.

这种脱节现象主要是德意志统一造成的，该事件的确对整个欧洲形成了一种非对称的冲击。

L’unification de la péninsule avec la création, en 1861, du royaume d’Italie, aboutira le 2 octobre 1870 à l’annexion de l’Etat pontifical.

意大利半岛的统一，以及1861年建立的意大利王国，导致了1870年10月2日罗马*教*皇*国的加入。

L'actuel laboratoire de haute pureté, une grande pureté des matériaux atelier de production, avec l'unification de l'art atelier de production.

现有高纯实验室、高纯材料生产车间，其中具有一流标准化生产车间。

Cette unification s'accompagna d'une réglementation quant à leur nombre.

对于执达官的数量来说，这种统一伴随着一项规章。

Les questions de droit matériel relatives aux sûretés et aux autres droits sur des valeurs mobilières détenues auprès d'un intermédiaire sont abordées dans un projet de convention que prépare actuellement l'Institut international pour l'unification du droit privé (Unidroit).

国际统一私法协会（统法会）正在编写的一项公约草案述及与担保相关和与中间人所持证券上设定的其他权利相关的实体法问题。

De ce fait, bien que le régime envisagé par le Guide vise à s'appliquer à de nombreuses formes d'opérations de consommateurs, il n'est pas censé avoir préséance sur les lois relatives à la protection de ces derniers ni examiner les politiques de protection des consommateurs, car cette question ne se prête pas à unification.

因此，虽然本指南设想的制度将适用于多种形式的消费者交易，但其本意并不是取代保护消费者的法律，也不是要讨论消费者保护政策，因为这一事项不易求得统一。

Dans le même temps, pour qu'il y ait des progrès sur le terrain, toutes les tentatives sécessionnistes visant Chypre doivent immédiatement cesser, conformément aux résolutions pertinentes du Conseil de sécurité, et une vision unique reposant sur l'unification de l'île doit prévaloir.

与此同时，若要在实地取得进展，就必须根据安全理事会有关决议，立即终止一切分离塞浦路斯的企图，并使基于该岛统一的单一愿景获得胜利。

Ce processus d'unification a deux ramifications.

这一统一进程有两个分支。

La Conférence a en vertu de son statut pour mission d'œuvrer à l'unification progressive des règles du droit international privé.

海牙会议的法定任务是，致力于逐步统一国际司法的法规。

La Conférence coopère avec le système des Nations Unies dans tous ses domaines d'activité : c'est ainsi qu'elle collabore avec la Commission des Nations Unies pour le droit commercial international et l'Institut international pour l'unification du droit privé sur une base tripartite.

该会议与联合国系统在所有其工作领域中密切合作：例如，它与联合国国际贸易法委员会和国际统一司法学会在三方的基础上共同合作。

Une coopération étroite s'est instaurée entre la Commission des Nations Unies pour le droit commercial international (CNUDCI), l'Institut international pour l'unification du droit privé (UNIDROIT) et la Conférence.

海牙国际私法会议已经与联合国贸易法委员会（贸易法委员会）和国际统一私法协会（私法协）建立了密切的合作。

Recommande en outre que tous les pays continuent d'assurer l'intégration et la diffusion de données gravimétriques et altimétriques afin de contribuer à l'unification du système de référence pour les hauteurs.

还建议所有国家继续努力综合和传播重力和水平面数据，以支持高度系统的统一。

Il restera également en contact avec le secrétariat de l'Institut international pour l'unification du droit privé.

欧洲空间法中心还将与国际统一私法协会（统法会）秘书处保持联系。

Les autres difficultés sont la porosité des frontières, le manque de soutien matériel et financier, le manque d'une volonté politique réelle d'intégration et d'unification dans le chef de certains responsables avec impact négatif tant sur le plan sécuritaire que politique, administratif, économique, social et humanitaire.

边界防守不严密；物资和财政支助不足；有些领导人缺少真正的融合与统一政治意愿，对安全、政治、行政、经济社会和人道主义各方面造成不利影响。

L'absence d'intégration et d'unification des services de douane, d'immigration, de l'aviation civile et de sécurité pourrait être comptée parmi les conséquences de ces situations.

这些情况造成，海关、移民、民航和安全各部门缺乏整体统一性。

Dans la même résolution, l'Assemblée générale a souligné l'importance, pour la poursuite de l'unification et de l'harmonisation progressives du droit privé, de l'entrée en vigueur des conventions issues des travaux de la Commission et, à cette fin, a invité instamment les États qui ne l'avaient pas encore fait à envisager de signer et de ratifier ces conventions ou d'y adhérer.

大会在同一项决议中强调使委员会的工作所产生的各项公约生效的重要性，以推进私法的逐步协调和统一，为此促请尚未签署、批准或加入这些公约的国家考虑签署、批准或加入这些公约。

Le Gouvernement de la République de Corée se réjouit de continuer à participer au processus d'harmonisation et d'unification du droit commercial international.

他的政府期待继续参与协调和统一国际贸易法的工作。

L'Assemblée générale voudra peut-être prendre note de l'importance de ces activités pour la coordination et la promotion de la modernisation, de l'harmonisation et de l'unification du droit commercial international.

大会愿意承认，这些活动对于协调和促进国际贸易法的进一步现代化、协调和统一具有重要意义。

Comme un certain nombre d'autres organisations travaillent sur des projets connexes ou sont, de par leurs compétences, intéressées par ce domaine, le Groupe de travail coordonne ses travaux avec elles, notamment la Conférence de La Haye de droit international privé, l'Institut international pour l'unification du droit privé et l'Organisation mondiale de la propriété intellectuelle.

由于许多其他组织正在讨论相关的项目或在该领域存在的机构利益，工作组正在与这些组织合作，包括海牙国际私法会议、国际统一私法协会和世界知识产权组织。

法语百科

En informatique et en logique, un problème d'unification est un système d'équations qui portent sur des termes. Par exemple, est un problème d'unification (avec une seule équation). L'unification a des applications en programmation logique, en système de réécriture. Souvent, on s'intéresse à l'unification syntaxique où il faut que les membres gauche et droit des équations sont syntaxiquement égaux. Par exemple, la solution de est car on lit de part et d'autre de l'équation. Par contre, le problème d'unification syntaxique n'a pas de solution ː attention, n'est pas une solution car les termes et sont syntaxiquement différents.

Histoire

Le premier chercheur à évoquer un algorithme d'unification est Jacques Herbrand dans sa thèse, mais en fait l'unification a été redécouverte par John Alan Robinson dans le cadre de sa méthode de résolution en démonstration automatique. C'est lui qui lui donna son nom actuel. Une étape importante est ensuite la découverte d'algorithmes linéaires par Martelli et Montanari, Paterson et Wegman et Huet. Prolog a aussi beaucoup contribué à sa popularisation. Des algorithmes spécifiques pour les termes de certaines théories, appelés aussi unification équationnelle (en particulier associative et commutative par Stickel) ont été proposés (voir ci-dessus).

Quelques exemples

Le problème d'unification $f(x,y) = f(a,g(x))$ a une solution $x = a, y = g(a)$ car substituer (i.e. remplacer) le terme $a$ à la variable $x$ et le terme $g(a)$ à la variable $y$ , dans les deux termes $f(x,y)$ et $f(a,g(x))$ donne le même terme $f(a,g(a))$ .

Le problème d'unification $f(a,x) = f(a,g(y))$ a une infinité de solutions ː

x = g(f(a,a)), y = f(a,a)

x = g(f(a,w)), y = f(a,w)

x = g(z), y = z

etc.

En revanche, le problème d'unification $f(x,y) = h(a,x)$ n'a pas de solution et le problème d'unification $x = g(x)$ non plus.

Solution principale

Une solution $\sigma_2$ d'un problème d'unification est dite plus générale qu'une solution $\sigma_1$ , si $\sigma_1$ est obtenue en substituant des termes à des variables dans $\sigma_2$ .

Par exemple, si on considère le problème d'unification

f(a,x) = f(a,g(y))

alors la solution

\sigma_2 = (x = g(f(a,w)), y = f(a,w))

est plus générale que la solution

\sigma_1 = (x = g(f(a,a)), y = f(a,a))

qui est obtenue en substituant le terme $a$ à la variable $w$ dans $\sigma_2$ . De même, la solution

\sigma_3 = (x = g(z), y = z)

est plus générale que la solution $\sigma_2$ , qui est obtenue en substituant le terme $f(a,w)$ à la variable $z$ dans la solution $\sigma_3$ .

Une solution $\sigma$ d'un problème d'unification est dite principale si elle est plus générale que toutes les solutions de ce problème, c'est-à-dire si toute solution est obtenue en substituant des termes à des variables dans $\sigma$ .

Dans cet exemple, la solution $\sigma_3$ est une solution principale du problème

f(a,x) = f(a,g(y))

Le théorème de la solution principale exprime que si un problème d'unification a une solution, alors il a une solution principale.

Algorithme de Robinson pour l'unification syntaxique

L'algorithme de Robinson permet de décider si un problème d'unification a des solutions ou non et, quand il en a, de calculer une solution principale.

On choisit une équation dans le système.

Si cette équation a la forme

f(t_1,\ldots,t_n) = f(u_1,\ldots,u_n)

on la remplace par les équations $t_1 = u_1$ , ..., $t_n = u_n$ et on résout le système obtenu.

Si cette équation a la forme

f(t_1,\ldots,t_n) = g(u_1,\ldots,u_m)

où $f$ et $g$ sont des symboles différents, on échoue.

Si cette équation a la forme

x = x

on la supprime du système et on résout le système obtenu.

Si cette équation a la forme

x = t

t = x

où $x$ apparaît dans $t$ et est distinct de $t$ , on échoue.

Si cette équation a la forme

x = t

t = x

et que $x$ n'apparaît pas dans $t$ , on substitue le terme $t$ à la variable $x$ dans le reste du système, on résout le système obtenu, ce qui donne une solution $\sigma$ et on retourne la solution $\sigma, x = \sigma t$ .

Filtrage

Un problème de filtrage est un problème d'unification dans lequel, dans chaque équation, les variables n'apparaissent que dans le terme de gauche. Par exemple, le problème

f(a,x) = f(a,g(b))

est un problème de filtrage, car le terme $f(a,g(b))$ ne contient pas de variables.

Dans le cas du filtrage, l'algorithme de Robinson se simplifie.

On choisit une équation dans le système.

Si cette équation a la forme

f(t_1,\ldots,t_n) = f(u_1,\ldots,u_n)

on la remplace par les équations $t_1 = u_1$ , ..., $t_n = u_n$ et on résout le système obtenu.

Si cette équation a la forme

f(t_1,\ldots,t_n) = g(u_1,\ldots,u_m)

où $f$ et $g$ sont des symboles différents, on échoue.

Si cette équation a la forme

x = t

on substitue le terme $t$ à la variable $x$ dans le reste du système, on résout le système obtenu, ce qui donne une solution $\sigma$ et on retourne la solution $\sigma, x = t$ .

Utilisation de l'unification et du filtrage dans les langages de programmation

L'unification est ce qui distingue le plus le langage de programmation Prolog des autres langages de programmation.

En Prolog, l’unification est associée au symbole « = » et ses règles sont les suivantes :

une variable X non-instanciée (c'est-à-dire ne possédant pas encore de valeur) peut être unifiée avec une autre variable (instanciée ou pas); les deux variables deviennent alors simplement des synonymes l'une de l'autre et représenteront dorénavant le même objet (ou la même structure) ;

une variable X non-instanciée peut être unifiée avec un terme ou un atome et représentera dorénavant ce terme ou atome ;

un atome peut être unifié seulement avec lui-même ;

un terme peut être unifié avec un autre terme : si leurs noms sont identiques, si leur nombres d'arguments sont identiques et si chacun des arguments du premier terme est unifiable avec l'argument correspondant du second terme.

En raison de sa nature déclarative, l'ordre dans une suite d'unifications ne joue aucun rôle.

Exemples d'exécution de l'unification en Prolog

On suppose que toutes les variables (en majuscules) sont non-instanciées.

A = A

réussit (réflexivité)

A = B, B = abc

A et B représentent alors l'atome 'abc'

xyz = C, C = D

réussit: l'unification est symétrique

abc = abc

réussit: les atomes sont les mêmes.

abc = xyz

échoue: des atomes distincts ne s'unifient pas

f(A) = f(B)

réussit: A est unifié avec B

f(A) = g(B)

échoue: les termes ont des noms différents

f(A) = f(B, C)

échoue: les termes ont un nombre d'arguments différent

f(g(A)) = f(B)

réussit: B est unifié au terme g(A)

f(g(A), A) = f(B, xyz)

réussit: A est unifié à l'atome 'xyz' et B est unifié au terme g(xyz)

A = f(A)

l'unification est infinie: A est unifié au terme f(f(f(f(f(...)))). Suivant le système logique utilisé, l'unification échoue ou réussit; pour la plupart des systèmes, l'unification échoue.

A = abc, xyz = X, A = X

échoue: car abc=xyz échoue

Autres algorithmes pour l'unification syntaxique

Algorithme de Herbrand (redécouvert par Martelli et Montanari)

L'algorithme de Herbrand est redécouvert par Martelli et Montanari (1982). On se donne un ensemble fini d'équations G = { s₁ ≐ t₁, ..., s_n ≐ t_n } où les s_i et t_i sont des termes du premier ordre. L'objectif est de calculer une substitution la plus générale. On applique les règles suivantes à l'ensemble G jusqu'à épuisement :

G ∪ { t ≐ t }	⇒	G		supprimer
G ∪ { f(s₁,...,s_k) ≐ f(t₁,...,t_k) }	⇒	G ∪ { s₁ ≐ t₁, ..., s_k ≐ t_k }		décomposer
G ∪ { f(t⃗) ≐ x }	⇒	G ∪ { x ≐ f(t⃗) }		échanger
G ∪ { x ≐ t }	⇒	G{x↦t} ∪ { x ≐ t }	si x ∉ vars(t) et x ∈ vars(G)	éliminer

Les règles suivantes sont également ajoutées en guise d'optimisation :

G ∪ { f(s⃗) ≐ g(t⃗) }	⇒	⊥	si f ≠ g or k ≠ m	conflit
G ∪ { x ≐ f(s⃗) }	⇒	⊥	si x ∈ vars(f(s⃗))	vérifier (occurs-check)

L'algorithme est en temps exponentiel et demande un espace mémoire au plus exponentiel si l'on représente les termes par leurs arbres syntaxiques. Néanmoins, on peut n'utiliser qu'un espace mémoire si on représente les termes par des graphes.

Implémentation avec des graphes

L'algorithme d'unification prend en entrée deux termes représentés par des graphes, ici f(x, g(x, x)) et f(h(y), g(z, h(1))). En sortie, une substitution la plus générale est représentée par des pointeurs (en bleu).

En implémentant l'algorithme avec des graphes, l'espace mémoire est linéaire en la taille de l'entrée même si le temps reste exponentiel dans le pire des cas. L'algorithme prend en entrée deux termes sous la forme de graphes, c'est à dire un graphe acyclique où les nœuds sont les sous-termes. En particulier, il y a un unique nœud par variables (cf. figure à droite). L'algorithme retourne en sortie une substitution la plus générale ː elle est écrite en place dans le graphe représentant les termes à l'aide de pointeurs (en bleu dans la figure à droite). C'est à dire, en plus du graphe décrivant la structure des termes (qui sont des pointeurs aussi), nous avons des pointeurs particuliers pour représenter la substitution. Par si x ː= h(1) est la substitution courante, x pointe vers le nœud correspondant au terme h(1).

Pseudo-code de l'implémentation avec des graphes

entrée ː deux termes t1, t2
sortie ː vrai si les termes sont unifiables, non sinon
fonction unifier(t1, t2)
      t1 = find(t1);
      t2 = find(t2);
      si t1 = t2
              retourner vrai;
      sinon etude de cas sur (t1, t2)
                (x, y):
                        faire pointer x vers y
                        retourner vrai;
                (x, t) ou (t, x):
                        si x apparaît dans t
                               retourner faux
                        sinon
                               faire pointer x vers t
                               retourner vrai;
               (f(L), g(M)):
                          si f = g
                                       retourner unifierlistes(L, M)
                          sinon
                                       retourner faux

où unifierListes unifient les termes de deux listes ː

entrée ː deux listes de termes L, M
sortie ː vrai si les termes des listes sont deux à deux sont unifiables, non sinon
fonction unifierlistes(L, M)
            etude de cas sur (L, M)
                       ([], [])ː retourner vrai;
                       ([], t::t') ou (t::t', [])ː retourner faux;
                       (s::L', t::M'):
                                   si unifier(s, t)
                                             retourner unifierlistes(L', M')
                                   sinon
                                             retourner faux

où find trouve la fin d'une chaîne ː

entrée ː un terme t
sortie ː le terme en bout de chaîne de t
fonction find(t)
         si t n'est pas une variable
                    retourner t
         sinon
                    si t est déjà assigné à un terme u
                           retourner find(u)
                    sinon
                           retourner t

et où une implémentation naïve de "x apparaît dans t" est donné par ː

entrée ː une variable x et un terme t
sortie ː vrai si la variable x apparaît dans le terme t, non sinon
fonction apparaîtdans(x, t)
          etude de cas sur t
                    y: retourner x = y
                    f(L): retourner apparaîtdansliste(x, L)

entrée ː une variable x et une liste de termes L
sortie ː vrai si la variable x apparaît dans l'un des termes de L, non sinon
fonction apparaîtdansliste(x, L)
         etude de cas sur L
                   []: retourner faux
                   t::L':
                            si apparaîtdans(x, find(t))
                                         retourner vrai
                            sinon
                                         retourner apparaîtdansliste(x, L')

Algorithme quadratique

L'algorithme présenté dans cette sous-section est du à Corbin et Bidoit (1983). Pour avoir une complexité quadratique, il y a deux améliorations de l'algorithme précédent.

Tester qu'une variable apparaît dans un sous-terme

Le graphe des deux termes avec les pointeurs en bleu.

L'implémentation pour tester si une variable x apparaît dans un sous-terme t est a priori en temps exponentiel. L'idée est d'éviter de parcourir plusieurs fois les même nœuds. On marque les nœuds visités comme dans un parcours en profondeur de graphe. Une fois un test d'appartenance effectué, il faut a priori démarquer les nœuds. Au lieu de cela, on les marque avec le "temps actuel". On ajoute alors un champ aux nœuds du graphe que l'on appelle poinçon qui contient le "temps actuel". Nous disposons d'une variable globale "temps actuel" qui est incrémenté à chaque test d'appartenance.

Pseudo-code de l'implémentation du test d'appartenance entrée ː une variable x et un terme t sortie ː vrai si la variable x apparaît dans le terme t, non sinon fonction apparaîtdans(x, t) temps actuel ː= temps actuel + 1 retourner apparaîtdans'(x, t) entrée ː une variable x et un terme t sortie ː vrai si la variable x apparaît dans le terme t, non sinon (ne change pas le temps) fonction apparaîtdans'(x, t) etude de cas sur t y: retourner x = y f(s): si f(s) est poinçonné au temps actuel retourner faux sinon poinçonner f(s) au temps actuel retourner apparaîtdansliste(x, s) entrée ː une variable x et une liste de termes L sortie ː vrai si la variable x apparaît dans l'un des termes de t, non sinon fonction apparaîtdansliste(x, L) etude de cas sur t []: retourner faux t::L': si apparaîtdans'(x, find(t)) retourner vrai sinon retourner apparaîtdansliste(x, L') Éviter des appels inutiles à unifier Pour éviter des appels inutiles à la procédure qui cherche à unifier deux termes, on utilise des pointeurs pour tous les nœuds et pas seulement les variables. On peut montrer que le nombre d'appels à la procédure qui unifie est O(|A|) où |A|`est le nombre d'arcs dans le graphe. Le traitement interne utilise un parcours de pointeurs "find" en O(|S|) où |S| est le nombre de sommets et un test d'appartenance d'une variable dans un terme qui est en O(|S|̹̹̹̹̹̹̹̹̹̹̹̝+|A|) = O(|A|) car le graphe est connexe. Donc l'algorithme est bien quadratique.+ Pseudo-code de l'adaptation de la procédure d'unification entrée ː un terme t sortie ː le terme en bout de chaîne de t fonction find(t) si t pointe vers un terme u retourner find(u) sinon retourner t et entrée ː deux termes t1, t2 sortie ː vrai si les termes sont unifiables, non sinon fonction unifier(t1, t2) t1 = find(t1); t2 = find(t2); si t1 = t2 retourner vrai; sinon etude de cas sur (t1, t2) (x, y): faire pointer x vers y retourner vrai; (x, t) ou (t, x): si x apparaît dans t retourner faux sinon faire pointer x vers t retourner vrai; (f(L), g(M)): si f = g faire pointer f(L) vers g(M) retourner unifierlistes(L, M) sinon retourner faux Algorithme quasi-linéaire L'algorithme est inspiré de l'algorithme quadratique de la section précédente. Le test de savoir si x apparaît dans t n'est plus effectué au cours de l'algorithme mais uniquement à la fin ː à la fin, on vérifie que le graphe est acyclique. Enfin, les pointeurs de la substitution et "find" sont implémentés à l'aide d'une structure de données Union-find. Plus précisément, on conserve les pointeurs dans la structure mais on dispose en plus une structure annexe Union-find. Dans la structure de données Union-find, les classes d'équivalence ne contiennent soit que des variables soit que des termes complexes. Pour passer d'une variable à un terme complexe, on utilise les pointeurs éventuels qui sont dans le graphe. Pseudo-code de la procédure d'unification qui utilise Union-find entrée ː deux termes t1, t2 sortie ː vrai si les termes sont unifiables ou que le graphe final est acyclique, non sinon fonction unifier(t1, t2) t1 = find(t1); t2 = find(t2); si t1 = t2 retourner vrai; sinon etude de cas sur (t1, t2) (x, y): Union(x, y) retourner vrai; (x, t) ou (t, x): si x apparaît dans t retourner faux sinon faire pointer x vers t retourner vrai; (f(L), g(M)): si f = g Union(f(L), g(M)) retourner unifierlistes(L, M) sinon retourner faux Construction de graphes à partir d'arbres Pour construire un graphe à partir d'un arbre, on parcourt l'arbre et on utilise une table de symboles (implémenté avec une table de hachage ou un arbre binaire de recherche) pour les variables car il faut garantir l'unicité du nœud x pour une variable x.

Unification équationnelle

Unification et logique d'ordre supérieur Lorsqu'on raisonne en logique du premier ordre, où les variables ne peuvent être unifiées qu'à des constantes, les choses se passent bien: savoir si deux termes et sont unifiables est décidable (grâce par exemple à l'algorithme ci-dessus). De plus, s'ils le sont, il existe un unificateur le plus général (most general unifier ou mgu en anglais), c'est-à-dire un terme tel que tous les autres unificateurs de et soient dérivables par instantiation de variables de . Cette situation idéale ne se retrouve hélas pas dans tous les systèmes logiques. En particulier, si on se place en logique d'ordre supérieur, c'est-à-dire qu'on s'autorise à utiliser des variables comme symboles de fonction ou comme prédicats, on perd la décidabilité et l'unicité de l'unificateur quand il existe. Au pire, deux termes peuvent même avoir une infinité d'unificateurs tous différents.

中文百科

本文有关计算机科学主题。其他学科的条目参见合一 (消歧义)。

在数理逻辑中，特别是应用于计算机科学中，两个项的同一是就特殊化次序而言的并(格的最小上界), 就是说，我们在项的集合上假定一个预序，其中 t* ≤ t 意味着 t* 是通过代换(substitute)在 t 中某些项的一个或多个自由变量而从 t 获得的。s 和 t 的同一 u，如果存在的话，是 s 和 t 二者的代换实例的一个项。s 和 t 的任何公共的代换实例也是 u 的实例。

例如，对于多项式 X 和 Y 可以通过采纳 X = Z 和 Y = Z 而同一到 Z。

Prolog 中的合一

在传统 Prolog 中，未实例化的变量 X — 就是说在它上面以前没有进行合一，可以合一于一个原子、一个项、或另一个未实例化的变量，因此在效果上变成了它的别名。在很多现代 Prolog 方言和一阶逻辑演算中，变量不能合一于包含它的项；这叫做出现检查。

Prolog 原子只能合一于同一个原子。

类似的，项只能合一于另一个项，如果顶部函数符号和项的元数(arity)和这个项是一样的，并且参数可以同时合一。注意这是递归行为。

合一的例子

A = A : 成功(重言式)

A = B, B = abc : A 和 B 二者合一于原子 abc

xyz = C, C = D : 合一是对称的

abc = abc : 合一成功

abc = xyz : 合一失败，因为原子是不同的

f(A) = f(B) : A 合一于 B

f(A) = g(B) : 失败，因为项的头部是不同的

f(A) = f(B, C) : 合一失败，因为项有不同的元数

f(g(A)) = f(B) : B 合一于项 g(A)

f(g(A), A) = f(B, xyz) : A 合一于原子 xyz 而 B 合一于项 g(xyz)

A = f(A) : 无限合一， A 合一于 f(f(f(f(...))))。在严格的一阶逻辑和很多现代 Prolog 方言中，这是禁止的(并由出现检查来强制)

A = abc, xyz = X, A = X : 合一失败；效果上 abc = xyz

引用

F. Baader and T. Nipkow, Term Rewriting and All That. Cambridge University Press, 1998.

F. Baader and W. Snyder, Unification Theory. In J.A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, volume I, pages 447–533. Elsevier Science Publishers, 2001.

法法词典

unification nom commun - féminin ( unifications )

1. regroupement en un tout (d'éléments jusque-là séparés) Synonyme: réunion

l'unification de la gauche
2. homogénéisation (d'éléments disparates) Synonyme: uniformisation

l'unification des systèmes de mesure