Combining Generalization Algorithms
in Regular Collapse-Free Theories

We consider a first-order alphabet consisting of a signature $\mathrm{\Sigma }$ (set of fixed arity function symbols) and a set of variables $𝒱$. The set of terms $𝒯(\mathrm{\Sigma },𝒱)$ over $\mathrm{\Sigma }$ and $𝒱$ is defined in the standard way: $t\in 𝒯(\mathrm{\Sigma },𝒱)$ iff $t$ is defined by the grammar $t:=x\mid f(t_1,\mathrm{\dots },t_n)$, where $x\in 𝒱$ and $f\in \mathrm{\Sigma }$ is an $n$-ary symbol with $n\ge 0$.

We denote arbitrary function symbols by $f,g,h$, constants by $a,b,c$, variables by $x,y,z,v$, and terms by $s,t,r,u$. The notions of term depth, term size, and a position in a term are defined in the standard way, see, e.g., [6]. By ${t|}_p$, we denote the subterm of $t$ at position $p$, and by $t{[s]}_p$, a term obtained from $t$ by replacing the subterm at position $p$ with the term $s$. For any position $p$ in a term $t$ (including the root position $ϵ$), $t(p)$ is the symbol at position $p$. The set of all variables in $t$ is denoted by $\mathrm{𝑉𝑎𝑟}(t)$. A term is called linear if no variable occurs in it more than once, and ground if $\mathrm{𝑉𝑎𝑟}(t)=\mathrm{\varnothing }$.

A sequence of terms $t_1,\mathrm{\dots },t_n$ may be written $\overline{t}$ when $n$ is clear from the context.

Given any signature $\mathrm{\Sigma }$ and any finite set of constants $C$ such that $\mathrm{\Sigma }\cap C=\mathrm{\varnothing }$, the signature $\mathrm{\Sigma }\cup C$ is denoted by ${\mathrm{\Sigma }}^C$.

A substitution is a mapping from $𝒱$ to $𝒯(\mathrm{\Sigma },𝒱)$, which is the identity almost everywhere. We use the Greek letters $\sigma ,\vartheta ,\phi$ to denote substitutions, except for the identity substitution, which is written as $\mathrm{𝐼𝑑}$. We represent substitutions using the usual set notation, e.g., $\sigma =\{x_1\mapsto t_1,\mathrm{\dots },x_n\mapsto t_n\}$ where $\{x_1,\mathrm{\dots },x_n\}$ is the domain of $\sigma$, denoted by $\mathrm{𝐷𝑜𝑚}(\sigma )$. Application of a substitution $\sigma$ to a term $t$, denoted by $t\sigma$, is defined as $x\sigma =\sigma (x)$ and $f(t_1,\mathrm{\dots },t_n)\sigma =f(t_1\sigma ,\mathrm{\dots },t_n\sigma )$. Substitution composition is defined as a composition of mappings. It is associative but not commutative, with $\mathrm{𝐼𝑑}$ playing the role of the unit element. We write $\sigma \vartheta$ for the composition of $\sigma$ with $\vartheta$.

Let $E$ be a set of term pairs, i.e., elements of $𝒯(\mathrm{\Sigma },𝒱)\times 𝒯(\mathrm{\Sigma },𝒱)$. An equational $\mathrm{\Sigma }$-theory generated by $E$, denoted by ${=}_E$, is the least congruence relation on $𝒯(\mathrm{\Sigma },𝒱)$ that is closed under substitution application and contains $E$. We call $E$ a presentation of ${=}_E$, and the elements of $E$ are called the axioms of ${=}_E$, written as $l=r$. If $t{=}_{E}u$, we say that $u$ is equal modulo $E$ to $t$. When $E=\mathrm{\varnothing }$, every term is equal only to itself, and the theory is called the empty or free theory.

It is common to slightly abuse the terminology in the literature by calling both $E$ and ${=}_E$ an equational theory. For a given $E$, we denote by $\mathrm{𝗌𝗂𝗀}(E)$ the set of all function symbols occurring in $E$.

A sequence of $E$-equalities $t_1{=}_E{u}_1,\mathrm{\dots },t_n{=}_E{u}_n$ may be written $\overline{t}{=}_E\overline{u}$ when $n$ is clear from the context.

An axiom $l=r$ is regular if $\mathrm{𝑉𝑎𝑟}(l)=\mathrm{𝑉𝑎𝑟}(r)$. An axiom $l=r$ is collapse-free if $l$ and $r$ are non-variable terms. An axiom $l=r$ is shallow if variables can only occur at a position at depth at most $1$ in both $l$ and $r$. An equational theory is regular (resp., collapse-free/shallow) if all its axioms are regular (resp., collapse-free/shallow). An equational theory $E$ is finite if, for each term $t$, there are only finitely many terms $u$ such that $t{=}_{E}u$. An equational theory $E$ is subterm collapse-free if there are no terms $t,u$ such that $t{=}_{E}u$ and $u$ is a strict subterm of $t$. A subterm collapse-free theory is necessarily collapse-free, and a finite theory is necessarily regular and subterm collapse-free.

A theory $E$ is syntactic if it has a finite resolvent presentation $RP$, defined as a finite set of axioms $RP$ such that each equality $t{=}_{E}u$ has an equational proof $t{\leftrightarrow }_{RP}^{\ast }u$ with at most one equational step ${\leftrightarrow }_{RP}$ applied at the root position. Note that any axiom in $RP$ can be applied in both directions: from the left to the right and from the right to the left. Any shallow theory is syntactic [17], and any collapse-free theory with finitary unification is syntactic [29].

One can easily check that $A=\{x\ast (y\ast z)=(x\ast y)\ast z\}$ (Associativity), $C=\{x\ast y=y\ast x\}$ (Commutativity), and $AC=A\cup C$ (Associativity-Commutativity) are regular and collapse-free. Moreover, $A$, $C$ and $AC$ are finite and syntactic [34, 29], but only $C$ is shallow. Since $A$, $C$, and $AC$ are finite theories, they are also subterm collapse-free.

The rest of the paper assumes that $E_i$ is a regular collapse-free ${\mathrm{\Sigma }}_i$-theory for $i=1,2$, where ${\mathrm{\Sigma }}_1$ and ${\mathrm{\Sigma }}_2$ are disjoint signatures. For the sake of brevity, the combined signature ${\mathrm{\Sigma }}_1\cup {\mathrm{\Sigma }}_2$ is abbreviated to ${\mathrm{\Sigma }}_{1,2}$, and the combined theory $E_1\cup E_2$ is also denoted by $E_{1,2}$.

A $\mathrm{\Sigma }$-rooted term $t$ is a term whose root symbol is in $\mathrm{\Sigma }$. Given any ${\mathrm{\Sigma }}_{1,2}^C$-term $t$ where $t$ is ${\mathrm{\Sigma }}_i$-rooted, an alien subterm of $t$ is any subterm $s$ of $t$ which is not ${\mathrm{\Sigma }}_i$-rooted and such that any proper superterm of $s$ in $t$ is ${\mathrm{\Sigma }}_i$-rooted. The set of alien subterms of $t$ is denoted by $Alien(t)$. Given any term $t$, its height of theory is formally defined as follows: $ht(t)=1+\max \{ht(t^{\prime })|t^{\prime }\in Alien(t)\}$. Given a finite set $T$ of ground ${\mathrm{\Sigma }}_{1,2}^C$-terms, we consider $Aliens={\bigcup }_{t\in T}\mathrm{𝐴𝑙𝑖𝑒𝑛}(t)$ and a mapping $\pi :Aliens\to FC$ such that $FC$ is a set of fresh free constants ($FC\cap C=\mathrm{\varnothing }$) and for any $a,a^{\prime }\in Aliens$, $\pi (a)=\pi (a^{\prime })$ iff $a{=}_{E_1\cup E_2}{a}^{\prime }$. Conversely, we define ${\pi }^{-1}:FC\to Aliens$ as a mapping such that for any $a\in Aliens$, ${\pi }^{-1}(\pi (a)){=}_{E_1\cup E_2}a$. The $i$-abstraction of any term $t\in T$ is denoted by $t^{{\pi }_i}$ and is inductively defined as follows:

• $\mathrm{■}$

  $c^{{\pi }_i}=c$ if $c\in C$,

• $\mathrm{■}$

  ${(f(t_1,\mathrm{\dots },t_n))}^{{\pi }_i}=f(t_1^{{\pi }_i},\mathrm{\dots },t_n^{{\pi }_i})$ if $f\in {\mathrm{\Sigma }}_i$,

• $\mathrm{■}$

  ${(f(t_1,\mathrm{\dots },t_n))}^{{\pi }_i}=\pi (f(t_1,\mathrm{\dots },t_n))$ if $f\in {\mathrm{\Sigma }}_j$ for $j\ne i$.

Lemma 1 holds when the component theories $E_1$ and $E_2$ are regular collapse-free. In the general case where the component theories are arbitrary, we need to assume that $t$ and $u$ are in layer-reduced form [23] to have the same correspondence with their $i$-abstractions.

Given an equational theory $E$, a term $t$ is more general than $u$ modulo $E$, or is an $E$-generalization of $u$, if there exists a substitution $\sigma$ such that $t\sigma {=}_{E}u$. In such a case, we write $t{⪯}_{E}u$ and also say the term $u$ is less general than $t$ modulo $E$ or that $u$ is an $E$-instance of $t$. The relation ${⪯}_E$ is a quasi-order and generates the equivalence relation, denoted by ${\simeq }_E$. The strict part of ${⪯}_E$ is denoted by ${\prec }_E$.

An equational generalization problem is formulated as follows:

Given:

an equational theory $E$ and two terms $t$ and $u$;

Find:

a term $r$ such that $r{⪯}_{E}t$ and $r{⪯}_{E}u$ ($r$ is said to be an $E$-generalization of $t$ and $u$).

Given an equational theory $E$ and two terms $t$ and $u$, a set of terms $𝒢$ is called a complete set of $E$-generalizations of $t$ and $u$ if it satisfies the following properties:

1. 1.

   Soundness: every element of $𝒢$ is an $E$-generalization of $t$ and $u$,

2. 2.

   Completeness: for every $E$-generalization $q$ of $t$ and $u$ there exists $r\in 𝒢$ such that $q{⪯}_{E}r$.

The set $𝒢$ is called a minimal complete set of $E$-generalizations of $t$ and $u$, denoted ${\mathrm{𝑚𝑐𝑠𝑔}}_E(t,u)$ if it, in addition, satisfies the following:

1. 3.

   Minimality: if there exist $r,q\in 𝒢$ such that $r{⪯}_{E}q$, then $r=q$.

The existence and cardinality of ${\mathrm{𝑚𝑐𝑠𝑔}}_E$ define what is called the generalization type of an equational theory $E$ as follows: $E$ has the generalization type 0 (or is nullary) if there are two terms $t$ and $u$ such that ${\mathrm{𝑚𝑐𝑠𝑔}}_E(t,u)$ does not exist. Otherwise, the generalization type of $E$ is

• $\mathrm{■}$

  unitary, if ${\mathrm{𝑚𝑐𝑠𝑔}}_E(t,u)$ is a singleton for all $t$ and $u$ (in this case, the sole element of ${\mathrm{𝑚𝑐𝑠𝑔}}_E(t,u)$ is called a least general $E$-generalization of $t$ and $u$ and is denoted by ${\mathrm{𝑙𝑔𝑔}}_E(t,u)$),

• $\mathrm{■}$

  finitary, if ${\mathrm{𝑚𝑐𝑠𝑔}}_E(t,u)$ is finite for all $t$ and $u$, and there exists at least one pair of terms for which this set is not a singleton,

• $\mathrm{■}$

  infinitary, if there exist $t$ and $u$ for which ${\mathrm{𝑚𝑐𝑠𝑔}}_E(t,u)$ is infinite.

In the rest of the paper, we consider generalization algorithms defined as terminating inference systems transforming anti-unification triples (AUTs, for short) written $x:t\triangleq u$ where $x$ is a variable, and $t$ and $u$ are the two ground terms to generalize. More precisely, we are focusing on rule-based systems working on configurations $𝒞$ of the form $A;S;\sigma$, where $A$ and $S$ are sets of AUTs, called the active set and store of $𝒞$, respectively, and $\sigma$ is a substitution, called the generalization component of $𝒞$. From now on, $𝒞$ is said to be a PSS-configuration; it consists of a problem together with a store and a substitution. Given a set of AUTs $P={\bigcup }_{i=1}^n\{x_i:t_i\triangleq u_i\}$, we associate two substitutions: $\{x_1\mapsto t_1,\mathrm{\dots },x_n\mapsto t_n\}$ is the left substitution of $P$ and $\{x_1\mapsto u_1,\mathrm{\dots },x_n\mapsto u_n\}$ is the right substitution of $P$. A set of AUTs may be written using the disjoint union symbol $\uplus$ to isolate a specific AUT from that set.