Un mécanisme algorithmique qui calcule la plus petite relation de congruence contenant un ensemble donné d'égalités entre termes, généralement en fusionnant des classes d'équivalence et en propageant la congruence des fonctions pour permettre un raisonnement égalitaire efficace, en particulier pour les fonctions non interprétées.

Principe

Maintenir des classes d'équivalence de termes sous les égalités affirmées, fusionner les classes lorsque des égalités apparaissent, et assurer que si f(a1,...,an) et f(b1,...,bn) sont présentes et que ai ≡ bi pour tout i alors les termes composés sont fusionnés, répéter jusqu'à atteindre la clôture.

Démonstration

Étant données les égalités a = b et f(a) = c, la fermeture fusionne a et b en une classe, reconnaît ensuite que f(a) et f(b) sont équivalents et fusionne leurs classes, permettant au solveur de déduire efficacement d'autres égalités ou contradictions.

Mauvaise application

Appliquer la fermeture de congruence naïvement sur de très grands graphes de termes sans hash-consing ni union-by-rank peut conduire à des surcoûts massifs en temps et mémoire ; une gestion incorrecte des arités des symboles de fonction ou des tris peut entraîner des fusions non valides.

Conséquence

Une fermeture de congruence correcte fournit un raisonnement égalitaire rapide et canonique utilisé dans les moteurs SMT et les démonstrateurs, permettant des vérifications de représentants en temps constant et des mises à jour incrémentales à mesure que des égalités sont ajoutées.

Inversion

L'inverse consiste à traiter les égalités uniquement par appariement syntaxique sans propagation de clôture : cela conserve les égalités initiales mais manque de nombreuses égalités impliquées et donne un pouvoir de raisonnement plus faible.

Limite

Cible le raisonnement d'égalité pour fonctions non interprétées sur termes du premier ordre et égalités ground ; elle ne traite pas en elle-même des théories interprétées (arithmétique, tableaux) sans combinaison avec d'autres solveurs de théorie ou axiomes.

Tension sémantique

Tension entre la fermeture de congruence et le traitement des égalités par résolution : la fermeture de congruence offre une maintenance incrémentale pilotée par structures de données, tandis que la résolution traite les égalités via manipulation et inférence de clauses.

Synthèse

La fermeture de congruence fusionne incrémentalement des classes d'équivalence de termes et propage la congruence des fonctions pour former la plus petite congruence contenant les égalités données, fournissant un raisonnement égalitaire compact et efficace qui s'intègre naturellement aux procédures de décision SMT.