Keywords:Equational Reasoning, Anti-unification, Generalization, Computational Verification, Interactive Theorem Proving, PVS.

1 Introduction↩︎

Motivation and Contextualization↩︎

Generalization is the scientific principle of drawing broad conclusions from specific observations, aiming to identify patterns or laws that hold beyond the original cases studied. In logic, this idea of generalization is formalized by a concept called anti-unification. It consists of finding the common structure and uniformly abstracting over differences when comparing two objects of a certain type, and it was first investigated and developed independently in the 1970s by Plotkin [1] and Reynolds [2].

Given terms \(s\) and \(t\), one says that \(s\) is more general than \(t\) (or that \(t\) is more specific than \(s\)) and writes \(s\preceq t\) iff there exists a substitution \(\sigma\) such that \(s\sigma=t\). The relation \(\mathord{\preceq}\) is known as instantiation preorder [3]. A generalizer for two terms \(s\) and \(t\) is a term \(r\) such that \(r\preceq s\) and \(r\preceq t\). The \(\mathord{\preceq}\)-minimal generalizers for \(s\) and \(t\) are called least general generalizers for \(s\) and \(t\). Thus, the syntactic anti-unification problem can be formally stated as: For terms \(s\) and \(t\), construct their least general generalizers. It is known that syntactic anti-unification is of type unitary [4], [5], i.e., any instance of the problem has a unique solution (up to renaming). For instance, the terms \(X\), \(f(X,Y)\), \(f(g(X,Y),Z)\), and \(f(g(X,Y),X)\) are generalizers for \(f(g(c,d),c)\) and \(f(g(g(u,v),v),g(u,v))\), but only \(f(g(X,Y),X)\) is their least general generalizer.

The first procedural algorithms for solving the syntactic anti-unification problem were presented independently by Plotkin [1] and Reynolds [2] in the 1970s. Their algorithm essentially reads the pair of input expressions, identifies the smallest positions where conflicts occur, and uniformly assigns fresh variables to those positions [2]. That allows the construction of the least general generalizer as being the join in a certain complete non-modular lattice whose order is \(\succeq\) [2]. Huet presented an algorithm in 1976 in [6] by means of a recursive function \(\lambda\) that acts in the form \(\lambda(s,t)=f(\lambda(s_1,t_1),\ldots,\lambda(s_m,t_m))\) if \(s=f(s_1,\ldots,s_m)\) and \(t=f(t_1,\ldots,t_m)\) and \(\lambda(s,t)=\phi(s,t)\) otherwise, where \(\phi\) is a bijection between pairs of terms and variables (ensuring that \(\lambda\) solves conflicts uniformly). A good exposition of that algorithm is presented by Lassez et al. in [4].

Rule-based procedures for anti-unification were presented by Pfenning [7] for the Calculus of Constructions, by Alpuente et al. [8] for order-sorted generalization, by the same authors for anti-unification modulo associativity and commutativity [9], and by Baumgartner et al. [10] for simply-typed lambda-terms in \(\eta\)-long \(\beta\)-normal forms, among others. Alpuente et al.’s proofs of completeness were non-constructive and relied on the anti-unification type; in the syntactic case, for instance, on the fact that syntactic anti-unification is unitary. A more preferred proof of completeness for rule-based algorithms would be constructive, as the one presented in this paper.

Real-world applications of anti-unification are, for instance, the identification of regularities in sequential code to transform it into efficient parallel code [11]; preventing failures and detecting errors in software [12]; repairing software bugs [13]–[15]; detecting code cloning and plagiarism [16], [17]; maintaining mathematical or software libraries [18], [19]; detecting similarities among chemical compounds to infer their carcinogenicity [20]. An open-source library of anti-unification algorithms (implemented in Java) for first- and second-order unranked terms, higher-order patterns, and nominal terms was presented in [21]. The paper [5] surveys the state-of-the-art in theory and applications of anti-unification.

Surprisingly, the current interest in the practical applications of anti-unification techniques has not yet been followed by the development of formal, mechanically verified certificates in proof assistants. That situation contrasts with the case for unification, where one aims to identify two expressions. For instance, successful work related to the formalization of unification and matching in interactive theorem provers are the ones developed in [22] for AC-matching (in Coq), in [23] for nominal C-matching through unification with protected variables (also in Coq), in [24] for nominal unification, in [25] for nominal C-unification, in [26] for nominal AC-matching, and in [27] for AC-unification (all in PVS). Advancing this line of research to provide formal certificates for proof assistants for anti-unification techniques and to strike a balance between theoretical development and practical application is of utmost importance. The only formalization of an anti-unification algorithm known to date is due to [28] for syntactic anti-unification. In that work, an algorithm for syntactic anti-unification is specified in PVS, and its termination and soundness are mechanically verified. Only the formal certificate for completeness remained to be constructed, and providing such a construction is the goal of the current work. Completing that work is of utmost importance, for it will allow the extraction of certified executable code of a sound and complete algorithm for syntactic anti-unification.

This paper formally studies the additional requirements that are essential for proving the completeness of algorithms based on the standard anti-unification inference rules (see Figure 1) that appear in [28]. The main motivation of this study is to understand in detail the greater complexity of proofs required for anti-unification compared to those for formalizations of unification algorithms (e.g., [29]–[31]). In [28], for formalizing soundness, important differences were highlighted, particularly in the cases of detection of solved and syntactically equal problems. In anti-unification, two crucial aspects concern the treatment of such problems. The former corresponds to equational questions between terms headed by different (function) symbols. In contrast, the latter corresponds to trivial (i.e., syntactically equal atomic) problems in which the terms are either the same constant or the same variable. Surprisingly, most of the formalization work (more than 90%, as quantified in [28]) for verifying the anti-unification algorithm was devoted to these two kinds of apparently straightforward cases. For obtaining a formal proof, the rigorous analysis of these cases requires more elaboration than the one usually devoted to the completeness of anti-unification in pen-and-paper proofs (e.g., [1], [2], [6], [32]).

In unification, if a problem is what we call a solved problem above in the context of anti-unification, one has a failure because terms with different head function symbols can not be unified; and syntactically equal problems are trivially resolved using the identity substitution. In anti-unification, the situation is completely different. A solved equation does not mean a failure, but the detection of a difference in the structure of the terms being compared. That difference is recorded in the computed substitution of the current configuration. In fact, unlike unification, anti-unification never fails. To solve the general case of anti-unification, one should proceed by further checking for other occurrences of the same difference, thereby detecting all possible regularities.

In anti-unification, the decomposition of the problem is guided by mutually distinct labels associated with subproblems of the input problem and by a substitution that records the problem’s structure. As soon as a solved subproblem is detected, it is stored separately. The essential elements for addressing solved and syntactic equations for formalizing soundness in [28] include preservation properties for the sets of labels of the unsolved and solved subproblems, and for the variables in the domain and the image of the computed substitution.

Main Contribution↩︎

• For the formalization of completeness, we discuss why the preservation properties developed for soundness together with the adjustments of generalizer notions (Subsection 3.2) are enough to address the inference rules for decomposition.

• Although the required notions for dealing with the cases of solved and syntactic rules in the soundness proof were much more elaborate than those required for unification, these notions were not enough for formalizing anti-unification completeness. We introduce the required additional elements in notions such as arbitrary generalizers so that a series of invariance and preservation properties are guaranteed; among them, properties that assure that the steps of the algorithm do not change anti-unification problems, and that the partially computed solutions can always be refined into generalizers that are less general than any arbitrary generalizer (Subsection 3.1). Based on these properties, a restricted notion of generalizer is introduced (Subsection 3.2).

• Finally, using the restricted notion of generalizer, we formalize (Subsection 3.3) the completeness theorem (stated as Theorem 1) and obtain as a corollary the main result that states the completeness of the algorithm regarding arbitrary generalizers (Corollary 1).

Organization↩︎

Section 2 presents the required background following standard nomenclature on anti-unification, which is the one used in the formalization [28]. Section 3 is the kernel of the paper. Subsection 3.1 presents the additional notions required to record preservation and invariance properties that compile the history of the algorithm’s computation. Subsection 3.2 presents the adjustments required to address completeness; then, Subsection 3.3 discusses how solved and syntactic subproblems are treated. Subsection 3.4 discusses the analysis of decomposition rules. Finally, Section 4 concludes and briefly discusses future work. Several points in the paper include links to the specification (). An extended version of this paper  presents quantitative information on a direct approach for dealing with the decomposition inference rules.

2 Background↩︎

The background related to terms, substitutions, and configurations is present in [28] and will be restated here to provide the proper vocabulary. The set of terms is generated by the standard nominal grammar \(s, t \Coloneqq c | X | () | \left(s,t\right) | f\,s\) adapted from [33], where \(c\) stands for constants, \(X\) stands for variables, \(s\) and \(t\) stand for terms, \(\left(s,t\right)\) stands for pairs of terms, \(()\) stands for the unit,¹ \(f\) stands for function symbols, and \(fs\) stands for functional applications. It is specified in PVS by means of the abstract data type (ADT) first_order_term , requiring types for constants, function symbols, and variables as parameters. A basic substitution is a binding \(\left(X\mapsto t\right)\), where \(X\) is a variable and \(t\) is a term. A substitution is a finite list of basic substitutions (the identity substitution is the empty list \(\iota\)). Those are specified in PVS in the theory first_order_substitution  using pairs and lists of these pairs. The action of a substitution on a term  is standard. The domain of a substitution \(\sigma\) is denoted by \(\mathtt{dom}(\sigma)\) . The set of variables in its range is denoted by \(\mathtt{rvars}(\sigma)\). The substitutions recognized by the predicate nice?  defined in the previous theory are the most important and widely employed in the specification.

An anti-unification problem is encoded by an anti-unification triple (AUT), which is an expression of the form \(s\mathrel{{\triangleq}_{{\scriptstyle X}}} t\), where \(s\) and \(t\) are terms, called its left- and right-hand sides, respectively, and \(X\) is a fresh variable for \(s\) and \(t\) called its label. That structure is specified in PVS by means of a record type AUT , where record accessors for label and left- and right-hand sides are present. The expression \(\mathord{eq}_{X}\) will be used to denote an AUT whose label is the variable \(X\). Its left- and right-hand sides will be denoted by \(\tt lhs(\mathord{eq}_{X})\) and \(\tt rhs(\mathord{eq}_{X})\), respectively. To solve an anti-unification problem, one must compare two terms and decompose their common structure. That motivates an AUT classification that allows no superposition: An AUT \(\mathord{eq}_{X}\) is decomposable iff \(\tt lhs(\mathord{eq}_{X})\) and \(\tt rhs(\mathord{eq}_{X})\) are either both pairs or both functional applications headed by the same function symbol;it is trivial iff \(\tt lhs(\mathord{eq}_{X})=\tt rhs(\mathord{eq}_{X})\) is the unit, a constant or a variable; and it is solved in any other case. That AUT classification guides the design of the inference rules presented in Figure 1 and, in PVS, it is specified by means of unary predicates match_DecF? , match_DecP? , match_Synt? , and match_Sol?  that checks whether or not an AUT matches the application of a rule.

During the decomposition, the labels are the most general solutions to anti-unification (sub)problems. Since those subproblems occur in different positions in the common structure of terms, it makes sense to label new subproblems with fresh labels to distinguish them. The decomposition produces a finite number of AUTs that are described as a finite collection. In PVS, that collection is specified as a list of AUTs . To a finite collection of AUTs \(A\), one associates two sets whose members are variables that play completely distinct roles in the anti-unification algorithm. The first one is its set of labels \(\mathtt{lbls}(A)\) , which collects all the labels of the members of \(A\). The second one is its set of variables \(\mathtt{vars}(A)\) , which collects all the variables that occur in the left- and right-hand sides of its members. To refer to a collection of subproblems obtained from a problem consistently, it is necessary to define a valid set of AUTs as being a finite set \(A\) of AUTs such that \(\mathtt{lbls}(A)=\left|A\right|\) and \(\mathtt{vars}(A)\cap\mathtt{lbls}(A)=\emptyset\). In PVS, valid sets of AUTs were specified by means of valid lists of AUTs, which are recognized by the unary predicate valid_AUTs? .

As decomposition proceeds, it may be necessary to address an anti-unification problem that was previously handled but at a distinct position in the common structure. Such problems are essentially the same but encoded by AUTs that differ only in their labels. Those are called repeated AUTs. That can be extended to sets of AUTs:An AUT \(\mathord{eq}_{X}\) is repeated in a set \(A\) of AUTs iff there exists an AUT \(\mathord{eq}_{Y}\) in \(A\) such that \(\mathord{eq}_{X}\) and \(\mathord{eq}_{Y}\) are repeated. The binary predicates repeated_AUT?  and AUT_repeated_in?  are specified to recognize such repetitions.

During the decomposition of the common term structure, one must understand the current state and the states visited to reach it. In that way, the problems already computed and those remaining to be computed will be identified. That is encoded by means of a valid configuration, which is an expression of the form \(\langle\mathcal{C}_{\mathtt{Uns}}\,\,\vert\,\,\mathcal{C}_{\mathtt{Sol}}\,\,\vert\,\,\mathcal{C}_{\mathtt{Sub}}\rangle\), where \(\mathcal{C}_{\mathtt{Sub}}\) is a substitution, \(\mathcal{C}_{\mathtt{Uns}}\) and \(\mathcal{C}_{\mathtt{Sol}}\) are valid sets of AUTs called its computed substitution and unsolved and solved parts, respectively, and each of those three components satisfy the following constraints:

1. The sets \(\mathcal{C}_{\mathtt{Uns}}\) and \(\mathcal{C}_{\mathtt{Sol}}\) are disjoint and \(\mathcal{C}_{\mathtt{Uns}}\cup\mathcal{C}_{\mathtt{Sol}}\) is a valid set of AUTs;

2. The set \(\mathcal{C}_{\mathtt{Sol}}\) contains only solved AUTs that are not repeated in \(\mathcal{C}_{\mathtt{Sol}}\);

3. The sets \(\mathtt{lbls}(\mathcal{C}_{\mathtt{Uns}})\), \(\mathtt{lbls}(\mathcal{C}_{\mathtt{Sol}})\), and \(\mathtt{dom}(\mathcal{C}_{\mathtt{Sub}})\) are pairwise disjoint. The sets \(\mathtt{dom}(\mathcal{C}_{\mathtt{Sub}})\) and \(\mathtt{rvars}(\mathcal{C}_{\mathtt{Sub}})\) are also disjoint.

The inference rules in Figure 1 induce a reduction relation over valid configurations, which is denoted as \(\Rightarrow\) using standard rewriting notation [34]; thus, \(\Rightarrow^*\), \(\Rightarrow^+\), and \(\Rightarrow^n\) denote the reflexive transitive closure, transitive closure, and the \(n\)-reduction steps derivation relations obtained from \(\Rightarrow\), respectively. In specific derivations, superscripts with the names of the applied rules are added to the relation symbol \(\Rightarrow\). For the example in the introduction, we have the following derivation:

\[\begin{array}{rl} \langlef\,\left(g\,\left(c,d\right),c\right)\mathrel{{\triangleq}_{{\scriptstyle X}}} f\,\left(g\,\left(g\,\left(u,v\right),v\right),g\,\left(u,v\right)\right)\,\,\vert\,\,\emptyset\,\,\vert\,\,\iota\rangle & \xRightarrow{\mathtt{DecF},\,\mathtt{DecP}} \\ \langle g\,\left(c,d\right)\mathrel{{\triangleq}_{{\scriptstyle Y}}} g\,\left(g\,\left(u,v\right),v\right), c\mathrel{{\triangleq}_{{\scriptstyle Z}}} g\,\left(u,v\right)\,\,\vert\,\,\emptyset\,\,\vert\,\,X\mapsto f\,\left(Y,Z\right)\rangle & \xRightarrow{\mathtt{DecF},\,\mathtt{DecP}} \\ \langle c\mathrel{{\triangleq}_{{\scriptstyle Y_1}}} g\,\left(u,v\right), d\mathrel{{\triangleq}_{{\scriptstyle Y_2}}} v, c\mathrel{{\triangleq}_{{\scriptstyle Z}}} g\,\left(u,v\right) \,\,\vert\,\,\emptyset\,\,\vert\,\,X\mapsto f\,\left(g\,\left(Y_1,Y_2\right),Z\right)\rangle & \xRightarrow{\mathtt{SolNR},\,\mathtt{SolNR}} \\ \langle c\mathrel{{\triangleq}_{{\scriptstyle Z}}} g\,\left(u,v\right) \,\,\vert\,\,c\mathrel{{\triangleq}_{{\scriptstyle Y_1}}} g\,\left(u,v\right), d\mathrel{{\triangleq}_{{\scriptstyle Y_2}}} v \,\,\vert\,\,X\mapsto f\,\left(g\,\left(Y_1,Y_2\right),Z\right)\rangle & \xRightarrow{\mathtt{SolR}} \\ \langle\emptyset \,\,\vert\,\,c\mathrel{{\triangleq}_{{\scriptstyle Y_1}}} g\,\left(u,v\right), d\mathrel{{\triangleq}_{{\scriptstyle Y_2}}} v \,\,\vert\,\,X\mapsto f\,\left(g\,\left(Y_1,Y_2\right),Y_1\right)\rangle \end{array}\]

A configuration is specified in PVS by means of Configuration , which is a record type with record accessors for unsolved, solved, and computed substitution (always a nice one). Among configurations, the valid ones are recognized by the unary predicate validConfiguration? . The intuition for each component of a valid configuration is as follows. Its unsolved part encodes the problems to be computed, its solved part encodes the problems where the common term structure differs and which were detected for the first time, and its computed substitution encodes the common term structure already decomposed. Thus, a valid configuration encodes the entire history of the decomposition up to that point.

The decomposition of the term structure is carried out by the inference rules presented in Figure 1. The algorithm Antiunify  is specified in [28] as a recursive unary function that maps valid configurations into valid configurations, and it consists of the exhaustive application of the rules to a valid input configuration. Since the unsolved part of a valid configuration is specified by a list of AUTs, the rules are always applied to the first member of that list. The size of the unsolved part of a configuration, which is the sum of the sizes  of its members, was the chosen metric for ensuring termination in [28].

The rules presented in Figure 1 are specified in [28] by means of unary functions DecF , DecP , Synt , and Solve  that require an input valid configuration that matches the application of the rule and returns an output configuration according to their (dependent) type. That type encodes, among other properties, that the output configuration is a valid configuration with a smaller size than the input configuration. PVS generated a type correctness condition (TCC) for each function, and each one of those TCCs required a manual proof. The advantage of this approach is that PVS generates a termination TCC for the specification of Antiunify, and the prover can automatically prove it using the information encoded in the (dependent) types of the input-output configurations of the inference rules. Thus, an exhaustive application of the rules terminates in a configuration with an empty unsolved part. Those are called normal configurations (or final configurations) and are recognized in PVS by means of the predicate normal_configuration? .

The background was enough to prove antiunif_is_sound  in [28]. The argument was constructed by induction on the size of the unsolved part of a valid configuration together with a case analysis concerning the employed rule in the inductive step, which is presented in Figure 2. The effort required was measured in [28] by the number of proof commands (for the proof and also its dependencies) and the amounts are \(2.09\)% for \(\mathtt{DecF}\), \(4.56\)% for \(\mathtt{DecP}\), \(61.70\)% for \(\mathtt{Synt}\), \(29.60\)% for \(\mathtt{SolR}\), and \(2.05\)% for \(\mathtt{SolNR}\). Surprisingly, the rules \(\mathtt{Synt}\)and \(\mathtt{SolR}\)together make up \(91.10\)% of the entire effort and algorithmically, going from \(\mathcal{C}\) to \(\mathcal{C}'\), they only add to \(\mathcal{C}_{\mathtt{Sub}}\) a new basic substitution \(\left(X\mapsto a\right)\), where \(X\) is a label in \(\mathcal{C}_{\mathtt{Uns}}\) and \(a\) is an atomic term. While that transformation seems trivial in a pen-and-paper proof, a considerable amount of work is required to analyze its effects in a mechanized and formally verified proof for the case where \(a\) is a variable. In that case, the branches for those two rules relied on dependencies (lemmas) that stated the invariance and preservation properties concerning the action of \(\theta_f\) on the variable \(a\). These properties explained why all that effort was required.

3 Dissection Towards a Mechanized Completeness Proof↩︎

Using the formalization elements developed for the proof of soundness in [28], one can try to address the completeness proofs for the decomposition rules (\(\mathtt{DecF}\)and \(\mathtt{DecP}\)). Indeed, for an inductive proof like the one presented in Figure 2 using a notion r_generalizer  of arbitrary generalizer that restrict its domain and range avoiding occurrences of the variables used by the algorithm, the completeness case analysis of these two rules will amount more than 2500 and 3500 PVS proof commands for the \(\mathtt{DecF}\)and \(\mathtt{DecP}\)rules, respectively (see the extended version of this paper ). Such an approach is sufficient to guarantee the completeness of the algorithm for the subclass of anti-unification problems that do not require applications of the rules \(\mathtt{SolR}\)and \(\mathtt{Synt}\), but not for arbitrary problems. An important class of such problems comprises those that do not repeat variables or constants. For those problems, the decomposition rules will only lead to solved AUTs that cannot appear more than once. Since no variable nor constant appears repeatedly, no application of the rules \(\mathtt{SolR}\)or \(\mathtt{Synt}\)is possible.

Surprisingly, following the same inductive schema with the same notion of generalizer did not work for the \(\mathtt{SolR}\), \(\mathtt{SolNR}\), and \(\mathtt{Synt}\)rules, as this section explains. The problem arises in the inductive step: given an arbitrary generalizer \(\gamma\) for the problem encoded by a configuration \(\cal C\), to apply the inductive hypothesis, one needs to build an associated generalizer \(\gamma'\) for the configuration \({\cal C}'\); and using the hypothesis that it is more general than the computed solution given by \(\theta_f\), in the final configuration \(\mathcal{C}_f\), prove that \(\gamma\) is also more general than \(\theta_f\) (see Figure 3).

Initially, Subsection 3.1 explains new notions that are required to compile configuration preservation properties for the analysis of the \(\mathtt{Synt}\), \(\mathtt{SolR}\), and \(\mathtt{SolNR}\)rules. These notions are used to record invariance properties throughout the history of computations. Afterward, Subsection 3.2 presents crucial adjustments required to address completeness for those rules; finally, Subsection 3.3 discusses how these adjusted notions are used in the formalization of the inductive proof. Although the branches of the decomposition rules can be derived from the elements developed in [28], for insertion into the case analysis of this new inductive schema, they require straightforward adaptations, as explained in Subsection 3.4.

3.1 New Notions Required for the Completeness Analysis↩︎

An initial configuration is a valid configuration with an empty solved part and identity computed substitution, and it is recognized in PVS by means of the unary predicate initial_configuration? . In PVS, a single application of any of the rules is recognized by the binary predicate Antiunify?  specified from the binary predicates DecF? , DecP? , Synt? , and Solve? . These predicates check whether a configuration is derived from another configuration by applying the respective inference rule. The binary predicate RTC(Antiunify?), constructed using the reflexive-transitive closure of abstract reduction relations, RTC(R) , from the NASAlib theory of rewriting (see, e.g., [35], [36]). For brevity, in this section, we will also use standard rewriting notation for the specified predicate Antiunify?; thus, \(\mathord{\Rightarrow}\) and \(\mathbin{\Rightarrow^{\ast}}\) will denote Antiunify? and RTC(Antiunify?), respectively.

All information pertaining to the derivation of a valid configuration from an initial configuration is stored in the former. All labels that were used during its derivation encode positions in the common term structure where subproblems were detected. Labels are transformed at each step taken:New labels are generated, labels are moved from the unsolved part to the solved part, to the domain of the computed substitution, or to its range. That motivates the following definition:

The information encoded by labels is essential if one aims for completeness, as labels encode positions. One important preservation property is stated in the next lemma and proved by induction on the number of steps in a derivation. Intuitively, all information encoded by the labels of a valid configuration is inherited by every valid configuration derived from it. In particular, if \(\mathcal{C}\Rightarrow\mathcal{C}'\) by means of \(\mathtt{SolR}\), \(\mathtt{SolNR}\), or \(\mathtt{Synt}\), then \(\mathtt{lbls}(\mathcal{C}')=\mathtt{lbls}(\mathcal{C})\).

Another important class of variables in a valid configuration derived from an initial configuration are those which appear on the left- and right-hand sides of the AUTs of the latter. In the decomposition of the common term structure, one can detect a trivial AUT whose both sides are the same variable, and the rule \(\mathtt{Synt}\)transforms that AUT accordingly, storing the following information at the computed substitution:The label that encodes the position where the problem was encountered must be mapped to that variable that occurs at that position. That is the only possible transformation regarding those types of variables, and it motivates the following definition:

A variable that occurs in the left- or right-hand side of an AUT of \(\mathcal{C}_0\) can occur in a subsequent derived configuration \(\mathcal{C}\) in \(\mathtt{vars}(\mathcal{C}_{\mathtt{Uns}}\cup\mathcal{C}_{\mathtt{Sol}})\cup\mathtt{rvars}(\mathcal{C}_{\mathtt{Sub}})\). How they appear in those sets is understood by the action of the inference rules employed in the derivation. One important invariance property is presented in the following lemma, which is proved by induction on the number of steps of a derivation. A crucial step in that proof is understanding how the set of variables of the computed substitution of a valid configuration changes after applications of the standard inference rules.

An important consequence of the previous lemma is the following: the set of protected variables of any configuration derived from an initial configuration is exactly the set of variables of the unsolved part of the latter. Also, it is important to notice that \(\mathtt{lbls}(\mathcal{C})\cap\operatorname{\mathtt{prtd}}{\left(\mathcal{C}\right)}=\emptyset\) for any valid configuration \(\mathcal{C}\). Another type of invariant present throughout the computation is the problem being solved. To discuss that, one requires the proper vocabulary:

By definition, one can see that \(\mathtt{rvars}(\rho_{L}^{\mathcal{C}})\cup\mathtt{rvars}(\rho_{R}^{\mathcal{C}})\subseteq\operatorname{\mathtt{prtd}}{\left(\mathcal{C}\right)}\), thus the lateral substitutions associated with \(\mathcal{C}\) are idempotent. Also, their restriction to any part of \(\mathcal{C}\) is the corresponding lateral substitution associated with that part. Lateral substitutions play an important role in reconstructing AUTs that encode anti-unification problems. The invariance result hinted at before can be stated as the next lemma. It is proved by induction on the length of the derivation, paying attention to how each inference rule modifies the lateral  and computed substitutions associated with a configuration, as well as to the role of the label of the AUT transformed by the inference rule.

Since all information is preserved in a derivation, one can think intuitively about Lemma 3 by employing a jigsaw puzzle: One breaks the entire picture (an AUT of the unsolved part of a valid configuration) into small pieces (AUTs obtained from that AUT by applications of inference rules to configurations) in a way that, if all of them are put together (the compositions of the computed and lateral substitutions), then one obtains the original picture again. That is the problem invariance:No matter how one breaks a problem into subproblems, the problem remains the same throughout the computation.

All the preservation properties presented so far can be used to completely describe the history of computation in the derivation of a valid configuration from an initial one. For instance, an argument by induction is sufficient for proving the following lemma:

Another important description of the history of computation during a derivation concerns the domain of the computed substitution. That history is presented in the next lemma, which can be proved by induction using Lemma 3:

3.2 Adjustment of Generalizer Notions↩︎

At this point, one has sufficient grounds to provide the building blocks of a definition that encodes what a generalizer for a valid configuration is. Lemma 3 guarantees the consistency of the following definition:

A close inspection of the previous definition and the definition of lateral substitutions ensures that the set just introduced is a valid set of AUTs. Suppose \(\mathcal{C}\Rightarrow\mathcal{C}'\). If \(\mathtt{SolNR}\)is the employed rule, then \(\mathcal{C}_{\mathtt{Ext}}'=\mathcal{C}_{\mathtt{Ext}}\). If any other rule is the employed one, then \(\mathcal{C}_{\mathtt{Ext}}'=\mathcal{C}_{\mathtt{Ext}}\cup\left\{\,\mathord{eq}_{X}\,\right\}\), where \(\mathord{eq}_{X}\) is the AUT in \(\mathcal{C}_{\mathtt{Uns}}\) that is transformed by the rule. Thus, an inductive argument together with Lemma 3 provides the following natural result:

Notice that in the set of labels of a valid configuration, the labels of the unsolved and solved parts are obtained directly from the AUTs that are already present in the configuration. The labels in the domain of the substitution refer to AUTs that were already transformed, and the extended set of AUTs is a very natural way to recover them. Thus, one can define:

A close inspection of the previous definition ensures that the set just introduced is a valid set of AUTs. Moreover, the identity \(\mathtt{lbls}(\mathcal{C}_{\mathtt{Tot}})=\mathtt{lbls}(\mathcal{C})\) holds. Suppose \(\mathcal{C}\Rightarrow\mathcal{C}'\). If \(\mathtt{SolNR}\), \(\mathtt{SolR}\), or \(\mathtt{Synt}\)is the employed rule, then \(\mathcal{C}_{\mathtt{Tot}}'=\mathcal{C}_{\mathtt{Tot}}\). If any decomposition rule is the employed one, then \(\mathcal{C}_{\mathtt{Ext}}'=\mathcal{C}_{\mathtt{Ext}}\cup A\), where \(A\) is the set of new AUTs introduced by the employed rule. Thus, an inductive argument provides the following natural result:

Given two terms \(s\) and \(t\), a term \(g\) is a generalizer for \(s\) and \(t\) iff there exist substitutions \(\sigma\) and \(\tau\) such that \(g\sigma=s\) and \(g\tau=t\). Thus, a generalizer for an AUT is a generalizer for both its sides. In the case of a valid configuration, one requires a notion of a generalizer that uniformly generalizes all the AUTs associated with that configuration. Thus, a generalizer for a valid configuration must be a substitution, and any comparison between generalizers must rely on the instantiation preorder restricted to the set of labels of the configuration. A natural definition is the following one:

That is the notion of a generalizer for a valid configuration required for proving completeness. The identity \(\iota\) is a total generalizer for every valid configuration \(\mathcal{C}\) and the lateral substitutions of \(\mathcal{C}_{\mathtt{Tot}}\) are its cohesion substitutions. That mirrors the fact that a variable generalizes any term. As a bonus, the new notions presented so far are already enough to prove soundness in a way that is different from the ones presented in [28] or in [9]. The new proof of soundness relies on the preservation properties stated in Lemmas 3 and 7, and it is done by induction on the number of steps of the derivation.

The pen-and-paper proof of completeness that is going to be presented here is constructive and completely different from the one presented in [9], because no results on confluence or the type of syntactic anti-unification will be assumed. On the contrary, that type will be a consequence of termination, soundness, and completeness. Before presenting the proof, certain properties of generalizers for valid configurations must be proved. The first one is a natural definitional corollary:

A particularly important preservation result concerning total generalizers for valid configurations is the following one. Despite being a natural definitional corollary, it essentially informs that a total generalizer cannot associate the same solution to problems encoded by AUTs of distinct classes:

The key step in the proof of the previous lemma is the existence of cohesion substitutions associated with the total generalizer \(\gamma\). Under the hypothesis \(X\gamma=Y\gamma\), they force the left and right-hand sides of the AUTs \(\mathord{eq}_{X}\) and \(\mathord{eq}_{Y}\) to be respectively the same terms. A particularly important consequence of the previous lemma is the following lemma, which deals with syntactic and solved AUTs:

An important application of Lemmas 8 and 10 is the following.If \(\mathcal{C}\) is a valid configuration, then the members of \(\mathcal{C}_{\mathtt{Sol}}\) are not repeated in it. Thus, a total generalizer for \(\mathcal{C}\) maps distinct labels in \(\mathtt{lbls}(\mathcal{C}_{\mathtt{Sol}})\) to distinct variables. In other words, a total generalizer for a valid configuration is able to separate non-repeated solved (resp.non-repeated trivial) AUTs that appear in a derivation ending in that same configuration. This property will play an important role in a step of the proof of completeness. Another important property of total generalizers for valid configurations is presented in the following lemma:

To prove the previous lemma, one needs to enumerate all the variables in \(\mathtt{rvars}(\gamma)\cap\mathbb{A}\) (if there are any) and rename all of them into distinct fresh variables using a renaming \(\alpha\). New cohesion substitutions are constructed using \(\alpha\) and the old ones. Lemma 11 serves as inspiration for providing the following definition:

The specification of that type of total generalizer is crucial in the proof of completeness. Lemma 11 shows that if a valid configuration admits a total generalizer, then it admits a restricted total generalizer that is equivalent to the original one on the labels of that configuration. That means that one can restrict their attention to that class of more well-behaved total generalizers for valid configurations. Also, since equivalence holds, completeness is not lost by such a restriction. That is the path followed in the PVS specification. We are ready to state completeness. All the preservation properties, invariants, and (restricted) total generalizer properties presented so far will naturally guide the construction of the proof. It will be dismembered into parts. \(\mathtt{Synt}\), \(\mathtt{SolNR}\), and \(\mathtt{SolR}\)rules are presented in Subsection 3.3, while \(\mathtt{DecF}\)and \(\mathtt{DecP}\)are presented in Subsection 3.4.

The proof of Theorem 1 is done by induction on the number of steps taken in \(\mathcal{C}\mathbin{\Rightarrow^{\ast}}\mathcal{C}_f\). In the base case, one has \(\mathcal{C}=\mathcal{C}_f\). Let \(S_f\) be the solved part of \(\mathcal{C}_f\). By the definition of total generalizer for \(\mathcal{C}_f\), one can always assume that \(\mathtt{dom}(\gamma)\cap\operatorname{\mathtt{prtd}}{\left(\mathcal{C}_f\right)}=\emptyset\). Since \(\mathtt{rvars}(\theta_f)\subseteq\mathtt{lbls}(S_f)\cup\operatorname{\mathtt{prtd}}{\left(\mathcal{C}_f\right)}\), one employs the definition of restricted total generalizer and Lemmas 4, 5, 8, and 10 to conclude that \(\gamma\preceq_{\mathtt{lbls}(\mathcal{C}_f)}\theta_f\).

For the inductive step, one assumes the result for derivations of length \(m\) and supposes that \(\mathcal{C}_0\mathbin{\Rightarrow^{\ast}}\mathcal{C}\Rightarrow^{m+1}\mathcal{C}_f\). Thus, there exists a valid configuration \(\mathcal{C}'\) such that \(\mathcal{C}_0\mathbin{\Rightarrow^{\ast}}\mathcal{C}\Rightarrow\mathcal{C}'\Rightarrow^{m}\mathcal{C}_f\). The analysis now proceeds by considering the rule employed in the step \(\mathcal{C}\Rightarrow\mathcal{C}'\). One must start with an arbitrary restricted total generalizer \(\gamma\) for \(\mathcal{C}\) relative to \(\mathcal{C}_f\) and use it to construct a restricted total generalizer \(\gamma'\) for \(\mathcal{C}'\) relative to \(\mathcal{C}_f\) to use the induction hypothesis (i.h.). That construction must be so that one can push the comparison using the instantiation preorder back to \(\gamma\). The situation is presented in Figure 4. Once the proof is finished, one can employ Lemma 11 to derive the following corollary from which one concludes that the type of syntactic anti-unification is unitary:

3.3 Completeness Analysis for Syntactic and Solve Rules↩︎

This subsection is concerned with the branches of the proof of completeness where the step \(\mathcal{C}\Rightarrow\mathcal{C}'\) is achieved by means of the rules \(\mathtt{Synt}\), \(\mathtt{SolNR}\), or \(\mathtt{SolR}\). Let \(\gamma\) be an arbitrary restricted total generalizer for \(\mathcal{C}\) relative to \(\mathcal{C}_f\). The information concerning both \(\gamma\) and the history of the computation is required for constructing a restricted total generalizer \(\gamma'\) for \(\mathcal{C}'\) relative to \(\mathcal{C}_f\) that allows the use of the reasoning illustrated in Figure 4.

1. If \(\mathtt{Synt}\)is the employed rule, then there exists a trivial AUT \(\mathord{eq}_{X}\) in \(\mathcal{C}_{\mathtt{Uns}}\) such that \(\mathcal{C}_{\mathtt{Uns}}'=\mathcal{C}_{\mathtt{Uns}}\setminus\left\{\,\mathord{eq}_{X}\,\right\}\), \(\mathcal{C}_{\mathtt{Sol}}'=\mathcal{C}_{\mathtt{Sol}}\), and \(\mathcal{C}_{\mathtt{Sub}}'=\mathcal{C}_{\mathtt{Sub}}\left(X\mapsto\tt lhs(\mathord{eq}_{X})\right)\). By Lemma 9, one knows that \(X\gamma\) is different from every variable that is assigned by \(\gamma\) to the labels of non-trivial AUTs. The problem encoded by the trivial AUT \(\mathord{eq}_{X}\) may appear in different positions in the common term structure. The information about it may be already stored in \(\mathcal{C}_{\mathtt{Uns}}\setminus\left\{\,\mathord{eq}_{X}\,\right\}\) or in \(\mathcal{C}_{\mathtt{Sub}}\).

2. If \(\mathtt{SolNR}\)is the employed rule, then there exists a solved AUT \(\mathord{eq}_{X}\) in \(\mathcal{C}_{\mathtt{Uns}}\) such that \(\mathcal{C}_{\mathtt{Uns}}'=\mathcal{C}_{\mathtt{Uns}}\setminus\left\{\,\mathord{eq}_{X}\,\right\}\), \(\mathcal{C}_{\mathtt{Sol}}'=\mathcal{C}_{\mathtt{Sol}}\cup\left\{\,\mathord{eq}_{X}\,\right\}\), and \(\mathcal{C}_{\mathtt{Sub}}'=\mathcal{C}_{\mathtt{Sub}}\). In other words, this is the first time that the problem encoded by the solved AUT \(\mathord{eq}_{X}\) is encountered. From Lemma 10, it follows that \(X\gamma\) is different from \(Y\gamma\) for every \(Y\) in \(\mathtt{lbls}(\mathcal{C}_{\mathtt{Sol}})\). By Lemma 9, one knows that \(X\gamma\) is different from every variable that is assigned by \(\gamma\) to the labels of non-solved AUTs. Notice that no information about the problem is already stored in \(\mathcal{C}_{\mathtt{Sub}}\). Nonetheless, information about it may already be stored in \(\mathcal{C}_{\mathtt{Uns}}\setminus\left\{\,\mathord{eq}_{X}\,\right\}\).

3. If \(\mathtt{SolR}\)is the employed rule, then there exist solved AUTs \(\mathord{eq}_{X}\) in \(\mathcal{C}_{\mathtt{Uns}}\) and \(\mathord{eq}_{X^{\prime}}\) in \(\mathcal{C}_{\mathtt{Sol}}\) such that \(\mathcal{C}_{\mathtt{Uns}}'=\mathcal{C}_{\mathtt{Uns}}\setminus\left\{\,\mathord{eq}_{X}\,\right\}\), \(\mathcal{C}_{\mathtt{Sol}}'=\mathcal{C}_{\mathtt{Sol}}\), and \(\mathcal{C}_{\mathtt{Sub}}'=\mathcal{C}_{\mathtt{Sub}}\left(X\mapsto X^{\prime}\right)\). In other words, the problem encoded by the solved AUT \(\mathord{eq}_{X^{\prime}}\) is encountered again. From Lemma 10, it follows that \(X\gamma\) and \(X^{\prime}\gamma\) are different from \(Y\gamma\) for every \(Y\) in \(\mathtt{lbls}(\mathcal{C}_{\mathtt{Sol}})\setminus\left\{\,X^{\prime}\,\right\}\). Since \(\mathord{eq}_{X}\) and \(\mathord{eq}_{X^{\prime}}\) are repeated AUTs, it is not necessarily the case that \(X\gamma=X^{\prime}\gamma\). By Lemma 9, one knows that \(X\gamma\) is different from every variable that is assigned by \(\gamma\) to the labels of non-solved AUTs. The problem encoded by the solved AUT \(\mathord{eq}_{X}\) may appear in different positions in the common term structure, and the information about it is already stored in \(\mathcal{C}_{\mathtt{Sol}}\).

That explains why the elements provided by [28] are not sufficient for addressing those rules and why it is crucial to require in the specification of a total generalizer for a valid configuration that it must also generalize both its solved part and the domain of its computed substitution together with its unsolved part. Only requiring that for the latter does not necessarily provide all the needed information regarding the history of the computation to compare the restricted total generalizer and the final computed substitution in those branches of the proof. Now, both the definition of total generalizer and the preservation properties previously discussed come to the rescue. Since the employed rule is \(\mathtt{Synt}\), \(\mathtt{SolNR}\), or \(\mathtt{SolR}\), one knows by Lemma 7 that \(\mathcal{C}_{\mathtt{Tot}}'=\mathcal{C}_{\mathtt{Tot}}\) and \(\mathtt{lbls}(\mathcal{C}')=\mathtt{lbls}(\mathcal{C})\). In other words, all the information required for the comparison is already present in \(\mathcal{C}\) and is preserved from \(\mathcal{C}\) to \(\mathcal{C}'\). Thus, one concludes that \(\gamma\) is already a restricted total generalizer for \(\mathcal{C}'\) relative to \(\mathcal{C}_f\) and \(\gamma\preceq_{\mathtt{lbls}(\mathcal{C})}\theta_f\) follows immediately from the induction hypothesis. Although the pen-and-paper proof seems straightforward, much of the effort in the verification will be related to its dependencies.

3.4 Completeness Analysis for Decomposition Rules↩︎

This subsection is concerned with the branches of the proof of completeness where the step \(\mathcal{C}\Rightarrow\mathcal{C}'\) is achieved by means of either \(\mathtt{DecF}\)or \(\mathtt{DecP}\). Let \(\gamma\) be an arbitrary restricted total generalizer for \(\mathcal{C}\) relative to \(\mathcal{C}_f\).

1. If \(\mathtt{DecF}\)is the employed rule, then there exist a decomposable AUT \(\mathord{eq}_{X}=ft_L\mathrel{{\triangleq}_{{\scriptstyle X}}} ft_R\) in \(\mathcal{C}_{\mathtt{Uns}}\) and a variable \(Y\) fresh for \(\mathcal{C}\) such that \(\mathcal{C}_{\mathtt{Uns}}'=\mathcal{C}_{\mathtt{Uns}}\cup\left\{\,\mathord{eq}_{Y}\,\right\}\setminus\left\{\,\mathord{eq}_{X}\,\right\}\), \(\mathcal{C}_{\mathtt{Sol}}'=\mathcal{C}_{\mathtt{Sol}}\), \(\mathcal{C}_{\mathtt{Sub}}'=\mathcal{C}_{\mathtt{Sub}}\left(X\mapsto fY\right)\), and \(\mathord{eq}_{Y}=t_L\mathrel{{\triangleq}_{{\scriptstyle Y}}} t_R\). By Lemma 8, the term \(X\gamma\) is either a variable or \(ft\) for some term \(t\).

   1. Suppose \(X\gamma=ft\) for some term \(t\).Define: \[\gamma'\mathrel{\vcenter{:}}=\left.\gamma\right\vert_{\mathtt{dom}(\gamma)\setminus\left\{\,Y\,\right\}}\left(Y\mapsto t\right).\] That is a restricted total generalizer for \(\mathcal{C}'\) relative to \(\mathcal{C}_f\). By the i.h., \(\gamma'\preceq_{\mathtt{lbls}(\mathcal{C}')}\theta_f\). There exists a substitution \(\delta'\) such that \(\gamma'\delta'=_{\mathtt{lbls}(\mathcal{C}')}\theta_f\). Letting \[\delta\mathrel{\vcenter{:}}=\left(Y\mapsto t\right)\delta',\] one concludes that \(\gamma\delta=_{\mathtt{lbls}(\mathcal{C})}\theta_f\). Indeed, \[\begin{align} X\gamma\delta&=ft\delta'=fY\gamma'\delta'=fY\theta_f=X\theta_f, \end{align}\] and \(Z\gamma\delta=Z\gamma'\delta'\) for \(Z\) in \(\mathtt{lbls}(\mathcal{C})\setminus\left\{\,X\,\right\}\). Thus, \(\gamma\preceq_{\mathtt{lbls}(\mathcal{C})}\theta_f\);

   2. Suppose \(X\gamma=U\) is a variable. There exist cohesion substitutions \(\tau_{L}^{\mathcal{C}}\) and \(\tau_{R}^{\mathcal{C}}\) of \(\gamma\). There exists a substitution \(\delta''\) such that \(\gamma\delta''=_{\mathtt{lbls}(\mathcal{C})}\theta_f\gamma\). Let \(W\) be fresh for \(\mathcal{C}_f\), \(\gamma\), \(\tau_{L}^{\mathcal{C}}\), \(\tau_{R}^{\mathcal{C}}\), and \(\delta'\). Define: \[\gamma'\mathrel{\vcenter{:}}=\left.\gamma\right\vert_{\mathtt{dom}(\gamma)\setminus\left\{\,Y\,\right\}}\left(U\mapsto fW\right)\left(Y\mapsto W\right).\] That is a restricted total generalizer for \(\mathcal{C}'\) relative to \(\mathcal{C}_f\). By the i.h., \(\gamma'\preceq_{\mathtt{lbls}(\mathcal{C}')}\theta_f\). There exists a substitution \(\delta'\) such that \(\gamma'\delta'=_{\mathtt{lbls}(\mathcal{C}')}\theta_f\). Letting \[\delta\mathrel{\vcenter{:}}=\left(U\mapsto fW\right)\left(Y\mapsto W\right)\delta',\] one concludes that \(\gamma\delta=_{\mathtt{lbls}(\mathcal{C})}\theta_f\). Indeed, \[\begin{align} X\gamma\delta&=fW\delta'=fY\gamma'\delta'=fY\theta_f=X\theta_f, \end{align}\] and \(Z\gamma\delta=Z\gamma'\delta'\) for \(Z\) in \(\mathtt{lbls}(\mathcal{C})\setminus\left\{\,X\,\right\}\). Thus, \(\gamma\preceq_{\mathtt{lbls}(\mathcal{C})}\theta_f\);

2. The analysis for \(\mathtt{DecP}\)is similar and will be omitted.

Crucial steps in verifying the previous arguments rely on the constraints imposed by the definition of restricted total generalizers. For instance, the constraint \(\mathtt{rvars}(\gamma)\cap\left(\mathtt{lbls}(\mathcal{C}_f)\cup\operatorname{\mathtt{prtd}}{\left(\mathcal{C}_f\right)}\right)=\emptyset\) is vital for the construction of the substitution \(\gamma'\). Moreover, the fact that a total generalizer for a valid configuration generalizes the unsolved part of that configuration is crucial for applying the induction step in verifying these branches of the proof.

4 Conclusion↩︎

This paper presented a rigorous pen-and-paper proof of the completeness theorem for syntactic anti-unification and the discussion clarified the formal elements required to mechanically verify the theorem inductively in PVS (and other proof assistants as well). In particular, the paper highlighted important differences that make that mechanization exercise much more complex than verifying the algorithmic solutions to unification, for which the cases of solved and syntactically equal subproblems are resolved immediately, leading to failures and trivial solutions. For formalizing the proof of the completeness theorem in PVS, we addressed these problems with the necessary theoretical rigor. The greater complexity of mechanizing verification for anti-unification algorithms lies in how to record the history of decomposing problems into solved and syntactic subproblems, whose regularities (repetitions) are further encoded by storing repeated solved and syntactic subproblems via the substitution solution under construction. The precise notions that guarantee the construction of a solution more specific than any arbitrary generalizer involve elaborate invariant properties related to the preservation of the problem (Lemma 3), history of the computed solution (Lemma [lemma::History-Computed-Substitution]), preservation of the extended problem and coherence of the partial solution generated during the computation (Lemmas 7, and 8). In addition, by definition of a restricted notion of arbitrary generalizers (Definition 7), the main completeness result is obtained as a corollary (Corollary 1) of the completeness for such a class of generalizers (Theorem 1). All results presented in Subsection 3.1 are already completely specified and formally verified in PVS.

Future work↩︎

Work in progress includes the formalization in PVS of the definitions and lemmas presented in Section 3.2 to obtain a mechanically and formally verified proof of completeness for the functional rule-based algorithm Antiunify, from which certified executable code can be extracted. Additional work includes the extension of the formalization for verifying algorithms to anti-unification modulo various algebraic properties widely used in mathematics, such as commutativity, associativity [32], [37], absorption [38], [39], and their combinations.

Acknowledgments↩︎

This work was partially supported by the Austrian Science Fund (FWF) project P 35530, the Rustaveli National Science Foundation of Georgia under project FR-25-5957, the Brazilian Research Council CNPq Universal grant 407461/2025-6, and Research productivity grants 313290/2021-0 and 6/2026-7, and a PDSE scholarship of the Brazilian Higher Education Council (CAPES) Finance Code 001 to the last author.

References↩︎