# A Sufficient Condition for the Existence of a Minimal Complete Set of Equational Generalizations

David M. Cerna

► To cite this version:

David M. Cerna. A Sufficient Condition for the Existence of a Minimal Complete Set of Equational Generalizations. UNIF 2025 - 39th International Workshop on Unification, Jul 2025, Birmingham, United Kingdom. hal-05148831

HAL Id: hal-05148831

https://hal.science/hal-05148831v1

Submitted on 7 Jul 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# A Sufficient Condition for the Existence of a Minimal Complete Set of Equational Generalizations

David M. Cerna*

Dynatrace Research, Linz, Austria

Czech Academy of Sciences, Institute of Computer Science, Prague, Czechia

## Abstract

Anti-unification, also known as generalization, is the process of extracting commonalities shared between a set of symbolic expressions. In the syntactic case, a unique minimal solution exists commonly referred to as the least general generalization. However, we are often interested in finding generalizations modulo an equational theory. For equational generalization, a unique minimal solution is no longer guaranteed, and in many cases, such expressions do not even exist. We can mitigate issues concerning the construction of a minimal complete set of generalization by focusing on minimal linear solutions, i.e., variables occur at most once. However, even this restriction does not guarantee the existence of minimal solutions. This paper describes ongoing work to classify theories where well-behaved linear generalization implies well-behaved generalization. Surprisingly, this correspondence holds for ground theories even though many known theories in this class have anti-unification type nullary; a minimal complete set of generalizations does not exist.

# 1 Introduction

Surprisingly, even if we restrict ourselves to ground equational theories, there exist theories with two axioms whose anti-unification type is nullary, for example, {$f(a) = a, f(b) = b$}. Furthermore, this theory is nullary even if we restrict ourselves to linear generalizations. This can be illustrated by considering the anti-unification problem $a \triangleq b$. A complete set of solutions for these two terms is {$f^n(x) | n \ge 0$}. If we consider the categorization of theories presented in [6], we can easily find such poorly-behaved theories in every category except the simplest of categories (from the anti-unification perspective), finite theories.

For example, {$f(a, g(x)) = f(a, x), f(b, g(x)) = f(b, x)$} is a simple theory whose anti-unification type is nullary even if we restrict ourselves to linear generalizations. Consider the anti-unification problem $f(a, c) \triangleq f(b, d)$. A complete set of solutions for these two terms is {$f(x, g^n(y)) | n \ge 0$}.

Furthermore, distinctions made in [6] seem to have less meaning for anti-unification than unification. Consider a canonical example of the idiosyncracies of anti-unification type, the theory {$f(x, \epsilon_f) = x, f(\epsilon_f, x) = x, g(x, \epsilon_g) = x, g(\epsilon_g, x) = x$}, i.e. the 2-unital theory [4]. This theory is categorized as a collapse theory. From it, one can easily obtain a collapse-free theory with similar properties, in particular, preserving the anti-unification type<fnref n="1" />:

$$ \left\{ \begin{array}{l} h(f(e_f, y)) = h(f(y, e_f)) = h(y), \quad h(g(e_g, y)) = h(g(y, e_g)) = h(y), \\ h(f(x, y)) = f(h(x), y), \quad h(f(x, y)) = f(x, h(y)), \quad h(g(x, y)) = g(h(x), y), \quad h(g(x, y)) = g(x, h(y)) \end{array} \right\} $$

Essentially, $h(\cdot)$ points to the position in the term where the equational theory may be applied.

What we want to illustrate by the above examples is that a different categorization of equational theories is needed for anti-unification. While generalization of finite theories exists for constructing a minimal complete set of generalizations [5], well-studied, more general classes of theories tend to poorly distinguish well-behaved theories from nullary theories.

Observe that for finite theories, a minimal complete set of generalizations always exists for both the set of linear and non-linear minimal solutions. We ask whether there exist classes of equational theories extending this property:

<footnote>*Joint work with Temur Kutsia and Daniel Nantes</footnote>

<footnote n="1">¹Similar to the procedure outlined in [3]. However, we extend the signature rather than restrict it.</footnote>
Linear Correspondence

Given a theory E, does the existence of a minimal complete set of linear E-generalizations imply the existence of a minimal complete set of E-generalizations?

While not trivial to show, there are simple (i.e., subterm-collapse-free) theories that violate this property (See Appendix A):

$$ \{h(x, b) = g(x), h(x, a) = g(x), f(x, g(y)) = f(x, y)\} $$

To provide some understanding as to why this theory violates the property, consider the anti-unification problem $f(a, c) \triangleq f(b, d)$. There is a single linear minimal generalization $f(x, y)$. However, one can construct an infinite chain in the non-linear case: $\{f(x, y), f(x, h(y, x)), f(x, h(h(y, x), x)), \dots\}$.

While there are many ground theories with nullary anti-unification type, linear correspondence holds. Furthermore, there are non-trivial extensions of ground theories which we conjecture to have linear correspondence, so-called semi-ground theories. A well-known example of such theories is the class of absorptive theories, Theories containing distinct instances of the following axioms: $\{f(x, \epsilon_f) = \epsilon_f, f(\epsilon_f, x) = \epsilon_f\}$ [1]. Both ground and semi-ground theories are instances of a framework we propose, so-called local theories. We conjecture that several classes of local theories generalizing semi-ground have the linear correspondence property.

## 2 Preliminaries

Let $\mathcal{V}$ be a countable set of variables and $\Sigma$ a finite set of function symbols with a fixed arity. The set of terms derived from $\Sigma$ and $\mathcal{V}$ is denoted by $\mathcal{T}(\Sigma, \mathcal{V})$, whose members are constructed using the grammar $t ::= x | f(t_1, \dots, t_n)$, where $x \in \mathcal{V}$ and $f \in \Sigma$ with arity $n \ge 0$. When $n = 0$, $f$ is called a constant. The set of variables occurring in $t$ is denoted by $\text{vars}(t)$. The size of a term is defined inductively as: $\text{size}(x) = 1$, and $\text{size}(f(t_1, \dots, t_n)) = 1 + \sum_{i=1}^n \text{size}(t_i)$. The depth of a term $t$ is defined inductively as $\text{dep}(x) = 1$ for variables and $\text{dep}(f(t_1, \dots, t_n)) = \max\{0, \text{dep}(t_1), \dots, \text{dep}(t_n)\} + 1$ otherwise. By symbols($t$) we denote the multi-set constructed inductively from $t \in \mathcal{T}(\Sigma, \mathcal{V})$: (i) if $t \in \mathcal{V}$, then symbols($t$) = $\{\{x\}\}$, and (ii) if $t = f(t_1, \dots, t_n)$ where $n \ge 0$, then symbols($t$) = $\{\{f\}\} \cup \bigcup_{i=1}^n \text{symbols}(t_i)$ where $\cup$ is the multiset union. By $\text{occ}(s, t)$, we denote the number of occurrences of $s$ in $t$, which we define inductive as follows: (i) if $s = t$, then $\text{occ}(s, t) = 1$, (ii) if $s \neq t$ and $\text{dep}(t) \le \text{dep}(s)$, then $\text{occ}(s, t) = 0$, (iii) otherwise, if $t = f(t_1, \dots, t_n)$, then $\text{occ}(s, t) = \sum_{i=1}^n \text{occ}(s, t_i)$.

We refer to a term $t$ as linear if for all $x \in \mathcal{V}$, $\text{occ}(x, t) \le 1$. By $\text{lin}(t)$, we denote the linearization of $t$; that is, we replace each variable in $t$ with a distinct fresh variable.

The set of positions of a term $t$, denoted by $\text{pos}(t)$, is a set of strings of positive integers, defined as $\text{pos}(f(t_1, \dots, t_n)) = \{\epsilon\} \cup \bigcup_{i=1}^n \{i.p \mid p \in \text{pos}(t_i)\}$, where $f \in \Sigma$, $t_1, \dots, t_n$ are terms, and $\epsilon$ denotes the empty string. For example, the term at position 1.2 of $g(f(x, a))$ is a. Given terms $t, t'$ and $p \in \text{pos}(t)$, then $t|_p$ denotes the subterm of $t$ at position $p$ and $t[t'|_p$ denotes the term that results from replacing the term at position $p$ of $t$ by $t'$. Given a term $t$ and $p, q \in \text{pos}(t)$, we write $p \sqsubseteq q$ if $q = p.q'$ and $p \sqsubseteq q$ if $p \sqsubseteq q$ and $p \neq q$. The set of subterms of a term $t$ is defined as $\text{sub}(t) = \{t|_p \mid p \in \text{pos}(t)\}$. The head of a term $t$ is defined as $\text{head}(x) = x$ and $\text{head}(f(t_1, \dots, t_n)) = f$, for $n \ge 0$. A context $C$ is a term with a single hole • where, syntactically, the hole is treated like a distinguished constant from the signature. When necessary, we explicitly mark the position $p$ of the hole by writing $C[\bullet]_p$. Otherwise, $\text{hp}(C)$ denotes the position of the hole of C. When the hole is replaced by a given term $t$, we represent it as $C[t]$ (or $C[t]_p$ when it is necessary to make the position explicit).

A substitution is a function $\sigma: \mathcal{V} \to \mathcal{T}(\Sigma, \mathcal{V})$ such that $\sigma(x) \neq x$ for only finitely many variables. The set of the variables that are not mapped to themselves is called the domain of $\sigma$, denoted as $\text{dom}(\sigma)$. The range of $\sigma$, denoted $\text{ran}(\sigma)$, is the set of terms $\{\sigma(x) \mid x \in \text{dom}(\sigma)\}$. We refer to a ground term $t$ if $\text{vars}(t) = \emptyset$ and a ground substitution $\sigma$ if for all $t \in \text{ran}(\sigma)$, $t$ is ground. Substitutions are extended to terms as usual. We use the postfix notation for substitution application to terms and write $t\sigma$ instead of $\sigma(t)$.

Substitutions can be described as sets of bindings of variables in their domains into terms in their ranges, e.g., we represent a substitution $\sigma$ as the set $\{x \mapsto x\sigma \mid x \in \text{dom}(\sigma)\}$. Lowercase Greek letters denote substitutions except for the identity substitution that we denote by $\text{id}$. The composition of substitutions $\sigma$ and $\rho$ is written $\sigma\rho$ and is defined by $(\sigma\rho)(x) = (x\sigma)\rho$ for each $x \in \mathcal{V}$.

Given $s, t \in \mathcal{T}(\Sigma, \mathcal{V})$, we refer to $s \approx t$ as an equational identity.
**Definition 1** (Equational theory [2]). Let $E$ be a set of equational identities (referred to as axioms).
The relation $\approx_E := \{(s,t) \in \mathcal{T}(\Sigma, \mathcal{V}) \times \mathcal{T}(\Sigma, \mathcal{V}) \mid E \models s \approx t\}$ is called the equational theory induced by $E$. We refer to $E$ as an axiomisation of $\approx_E$.

By $s \approx_E t$ we denote that $(s,t)$ belongs to $\approx_E$. In this work, we only consider equational theories which have a finite axiomisation and are consistent, that is, for all $x, y \in \mathcal{V}$, if $x \approx_E y$, then $x = y$. Given a term $t$ and an equational theory $E$, we define $[t]_E = \{t' \mid t' \in \mathcal{T}(\Sigma, \mathcal{V}) \wedge t' \approx_E t\}$, i.e., the equivalence class of $t$ over $E$. Using equivalence classes, we can define the size minimal representation of a term $t$ modulo an equational theory $E$, $size_E(t) = \min\{size(t') \mid t' \in [t]_E\}$. Furthermore, the representatives of a term $t$ modulo an equational theory $E$ are the size minimal members of $[t]_E$, that is
$$Rep_E(t) = \{t' \mid t' \in [t]_E \wedge size_E(t') = size(t')\}.$$

There are a few well-known classes of equation theories we describe below: **Ground**, For all $s \approx t$ in any finite axiomisation of $E$, $s, t \in \mathcal{T}(\Sigma, \emptyset)$, **Finite**, For all $t \in \mathcal{T}(\Sigma, \mathcal{V})$, $[t]_E$ is finite. **Permutative**, For all $s \approx t$ in any finite axiomatisation of $E$, $symbols(s) = symbols(t)$, **Regular**, For all $s \approx t$ in any finite axiomisation of $E$, $\mathcal{V}(s) = \mathcal{V}(t)$. **Simple**, For all $s \approx_E t$, if $s \neq t$, then $s \notin \text{sub}(t)$ and $t \notin \text{sub}(s)$. **Collapse-free**, For all $s \approx_E t$, if $s \neq t$, then $s, t \notin \mathcal{V}$.

**Definition 2 (E-generalization, $\leq_E$).** The generalization relation of the theory induced by $E$ holds for terms $r, s \in \mathcal{T}(\Sigma, \mathcal{V})$, written $r \leq_E s$, if there exists a substitution $\sigma$ such that $r\sigma \approx_E s$. In this case, we say that $r$ is more general than $s$ modulo $E$. If $r \leq_E s$ and $r \leq_E t$, we say that $r$ is an E-generalization of $s$ and $t$. The set of all (linear) E-generalizations of $s, t \in \mathcal{T}(\Sigma, \emptyset)$ is denoted as $\mathcal{G}_E(s, t)$ ($\mathcal{G}_E^{\text{lin}}(s, t)$). By $\prec_E$ and $\simeq_E$, we denote the strict and equivalence relations induced by $\leq_E$, respectively.

**Assumption 1.** We only consider generalizations of ground terms, that is, terms in $\mathcal{T}(\Sigma, \emptyset)$.

**Definition 3 (Minimal Linear Generalization).** Let $E$ be an equational theory, $s, t \in \mathcal{T}(\Sigma, \emptyset)$, and $g \in \mathcal{G}_E(s, t)$. We refer to $g$ as a minimal (linear) generalization if there does not exist $g' \in \mathcal{G}_E(s, t)$ ($g' \in \mathcal{G}_E^{\text{lin}}(s, t)$) such that $g \prec_E g'$.

**Definition 4 (Generalizing Substitutions).** Let $E$ be an equational theory, $s, t \in \mathcal{T}(\Sigma, \emptyset)$, and $g \in \mathcal{G}_E(s, t)$. We define the set genSub($g, s, t$) as follows: For all substitutions $\theta_s$ and $\theta_t$, $(\theta_s, \theta_t) \in \text{genSub}(g, s, t)$ if (i) $\text{dom}(\theta_s) \subseteq \text{vars}(g)$ and $\text{dom}(\theta_t) \subseteq \text{vars}(g)$, (ii) $\text{vars}(\text{ran}(\theta_s)) = \text{vars}(\text{ran}(\theta_t)) = \emptyset$, and (iii) $g\theta_s \approx_E s$ and $g\theta_t \approx_E t$.

**Definition 5 (variable minimal).** Let $E$ be an equational theory. Then a term $t$ is $E$-variable-minimal if $t \approx_E t'$, then $\text{vars}(t) \subseteq \text{vars}(t')$. We refer to $E$ as variable-minimizing if for all terms $s \in \mathcal{T}(\Sigma, \mathcal{V})$, there exists $s' \in [s]_E$ such that $s'$ is $E$-variable-minimal.

**Definition 6 (Minimal (linear) complete set of E-generalizations).** The minimal (linear) complete set of E-generalizations of the terms $s$ and $t$, denoted as $mcsg_E(s, t)$ ($mcslg_E(s, t)$), is a subset of $\mathcal{G}_E(s, t)$ ($\mathcal{G}_E^{\text{lin}}(s, t)$) satisfying:

1. For each $r \in \mathcal{G}_E(s, t)$ ($r \in \mathcal{G}_E^{\text{lin}}(s, t)$) there exists $r' \in mcsg_E(s, t)$ ($r' \in mcslg_E(s, t)$) such that $r \leq_E r'$.

2. If $r, r' \in mcsg_E(s, t)$ ($r, r' \in mcslg_E(s, t)$) and $r \leq_E r'$, then $r = r'$ (minimality).

**Assumption 2.** All equational theories considered in the rest of this paper are variable-minimizing. Thus, we assume that the minimal (linear) complete sets only contain $E$-variable-minimal terms.

**Definition 7 ((Linear) Anti-unification type).** The anti-unification type of an equational theory $E$ may have one of the following forms:

* Unitary: $mcsg_E(s, t)$ ($mcslg_E(s, t)$) exists for all $s, t \in \mathcal{T}(\Sigma, \mathcal{V})$ and is always singleton.

* Finitary: $mcsg_E(s, t)$ ($mcslg_E(s, t)$) exists and is finite for all $s, t \in \mathcal{T}(\Sigma, \mathcal{V})$, and there exist $s', t' \in \mathcal{T}(\Sigma, \mathcal{V})$ for which $1 < |mcsg_E(s, t)| < \infty$ ($1 < |mcslg_E(s, t)| < \infty$).

* Infinitary: $mcsg_E(s, t)$ ($mcslg_E(s, t)$) exists for all $s, t \in \mathcal{T}(\Sigma, \mathcal{V})$, and there exist $s', t' \in \mathcal{T}(\Sigma, \mathcal{V})$ such that $mcsg_E(s', t')$ ($mcslg_E(s', t')$) is infinite.

* Nullary: for some $s, t \in \mathcal{T}(\Sigma, \mathcal{V})$, $mcsg_E(s, t)$ ($mcslg_E(s, t)$) does not exist.

**Definition 8.** An equational theory $E$ is referred to as linearly-minimal if for all $s, t \in \mathcal{T}(\Sigma, \emptyset)$, $mcslg_E(s, t)$ exists.
**Definition 9 (Merged).** Let $E$ be an equational theory, $s, t$ ground terms, and $g \in \mathcal{G}_E(s,t)$. Then we refer to $g$ as merged if for all $x, y \in \text{vars}(g)$ there does not exist substitutions $\theta_s$ and $\theta_t$ such that $g\theta_s \approx_E s$, $g\theta_t \approx_E t$, $x\theta_s \approx_E y\theta_s$, and $x\theta_t \approx_E y\theta_t$.

**Definition 10 (Merger).** Let $E$ be an equational theory, $s, t$ ground terms, and $g \in \mathcal{G}_E(s,t)$. Then a substitution $\sigma$ is referred to as a merger of $g$ if $g\sigma$ is merged.

## 3 Local Theories

In this section, we provide a general definition for defining classes of equational theories based on local application of the theory. Essentially, given an equational theory $E$ and an equation $C[r] \approx_E C[r']$, where $C$ is a context and $r$ and $r'$ are terms chosen from particular subsets of $\mathcal{T}(\Sigma, \mathcal{V})$. Furthermore, the choice of $r'$ is dependent on the choice of $r$. This dependence is formally described through an $\mathcal{R}$-selection operator, that is a function $f^{\mathcal{R}}: \mathcal{R} \to \mathcal{P}(\mathcal{T}(\Sigma, \mathcal{V}))$ where $\mathcal{R} \subseteq \mathcal{T}(\Sigma, \mathcal{V})$. We define a few useful selection functions below:

* **Ground:** for all $\mathcal{R} \subseteq \mathcal{T}(\Sigma, \mathcal{V})$ and $t \in \mathcal{R}$, $\text{gnd}(t) = \mathcal{T}(\Sigma, \emptyset)$.

* **Permutative:** for all $\mathcal{R} \subseteq \mathcal{T}(\Sigma, \mathcal{V})$ and $t \in \mathcal{R}$, $\text{perm}(t) = \{t' \mid \text{symbols}(t) = \text{symbols}(t') \wedge t' \in \mathcal{R}\}$.

**Definition 11 (($\mathcal{R}, f^{\mathcal{R}}$)-local).** Let $\mathcal{R} \subseteq \mathcal{T}(\Sigma, \mathcal{V})$, $f^{\mathcal{R}}$ a selection operator, and $E$ a variable-minimizing, equational theory. Then $E$ is ($\mathcal{R}, f^{\mathcal{R}}$)-local if for all $t_0, t_1 \in \mathcal{T}(\Sigma, \mathcal{V})$, $t_0 \approx_E t_1$ if and only if $t_0 = t_1$ or there exists $i \in \{0, 1\}$, a context $C$, $r \in \mathcal{R}$, and $r' \in f^{\mathcal{R}}(r)$ such that $r \approx_E r'$, and $t_i = C[r]$ and $C[r'] \approx_E t_{i+1}(\text{mod } 2)$.

Many classes of equational theories are ($\mathcal{R}, f^{\mathcal{R}}$)-local given the appropriate choice of $\mathcal{R}$ and $f^{\mathcal{R}}$. For example, ground equational theories are ($\mathcal{T}(\Sigma, \emptyset)$, $\text{gnd}$)-local and permutative theories are ($\mathcal{R}$, $\text{perm}$)-local where $\mathcal{R} = \mathcal{T}(\Sigma, \mathcal{V}) \setminus \mathcal{V}$. A simple generalization of ($\mathcal{T}(\Sigma, \emptyset)$, $\text{gnd}$)-local results in a novel class of theories generalizing ground equational theories:

**Definition 12 (Semi-ground).** Let $\mathcal{R} = \mathcal{T}(\Sigma, \mathcal{V}) \setminus \mathcal{V}$, $E$ be an equational theory. Then $E$ is semi-ground if it is ($\mathcal{R}, \text{gnd}$)-local.

A natural example of a semi-ground theory is $\{f(x, \epsilon_f) \approx_E \epsilon_f, f(\epsilon_f, x) \approx_E \epsilon_f\}$. In the subsequent section, we provide a framework for proving linear correspondence. We conjecture that semi-ground theories fit into this framework and thus have linear correspondence.

## 4 Frozen-minimal Theories

We introduce the notion of a frozen variable. It provides a slightly weaker notion than minimal generalization as it only considers more specific terms resulting from linear substitutions, i.e., the range only contains linear terms. Essentially, frozen is minimality with respect to linear terms.

**Definition 13 (Frozen).** Let $E$ equational theory, $s, t \in \mathcal{T}(\Sigma, \emptyset)$, $g \in \mathcal{G}_E(s, t)$ such that $g$ is variable-minimal, and $x \in \text{vars}(g)$. Then we refer to $x$ as frozen in $g$ if for all $r_1, r_2 \in \mathcal{T}(\Sigma, \emptyset)$ where $g\{x \mapsto r_1\} \prec_E s$ and $g\{x \mapsto r_2\} \prec_E t$, $\text{mcslg}_E(r_1, r_2)$ exists and $\text{mcslg}_E(r_1, r_2) = \{y\}$ *In this sense, it is not that the position is for some $y \in \mathcal{V}$.* The set of frozen variables in $g$ is denoted $\ast_g$ and the set of non-frozen variables is denoted $\overline{\ast}_g = \{x \mid x \in \text{vars}(g) \wedge x \notin \ast_g\}$. When $\ast_g = \text{vars}(g)$, we refer to $g$ as frozen.

Observe that frozen is dependent upon the existence of the minimal complete set of linear generalizations. We extend the concept to theories as follows:

**Definition 14 (Frozen Theory).** Let $E$ be a linear-minimal, variable-minimizing equational theory. Then we refer to $E$ as frozen if for all $s, t \in \mathcal{T}(\Sigma, \emptyset)$ and $g \in \text{mcslg}_E(s, t)$, $g$ is frozen.

Furthermore, certain frozen theories produce minimal generalizations through iterative substitution of linear generalizations followed by mergers.

**Definition 15 (Minimal-producing).** Let $E$ be a frozen equational theory. Then $E$ is minimal-producing if for all $s, t \in \mathcal{T}(\Sigma, \emptyset)$ and frozen, merged $g \in \mathcal{G}_E(s, t)$, $g$ is a minimal generalization.

The most important property concerning minimal-producing equational theories is that there minimal complete set of generalizations always exists.
**Theorem 1.** Every minimal-producing equational theory is, at most, type infinitary.

Now, we address the existence of minimal-producing equational theories as such theories have the linear correspondence property.

# 5 Ground Theories

To understand why ground theories are minimal-producing and thus exhibit the linear correspondence property, we need to consider the paths from variable occurrences in a term to the root of the term.

**Definition 16 (Symbol Path).** Let $t \in \mathcal{T}$ and $p \in \text{pos}(t)$. Then p-path of t, denoted by $\text{path}(t, p)$ is defined as follows:

* If $p = \epsilon$, then $\text{path}(t, p) = [\text{head}(p)]$

* If $p = q.i$ where $1 \le i \le \text{arity}(\text{head}(t|_q))$, then $\text{path}(t, p) = \text{path}(t, q) \circ [\text{head}(p)]$

**Example 1.** Consider the following terms and positions: If $t = f(g(a, s(b)), x)$ and $p = 1.2.1$, then $\text{path}(t, p) = [f, g, s, b]$. If $t = f(g(a, s(b)), x)$ and $p = 2$, then $\text{path}(t, p) = [f, x]$. If $t = f(g(a, s(b)), x)$ and $p = 1.2$, then $\text{path}(t, p) = [f, g, s]$. If $t = x$ and $p = \epsilon$, then $\text{path}(t, p) = [x]$.

An Important observation concerning ground theories is that variable occurrence blocks the application of the theory at any position above the variable. This essentially freezes a part of the term.

**Lemma 1.** Let E be a ground equational theory, $s, t \in \mathcal{T}$, and $p \in \text{pos}(s)$ such that $s|_p \in \mathcal{V}$. Then if $s \approx_E t$, then $p \in \text{pos}(t)$ and $\text{path}(s, p) = \text{path}(t, p)$.

A simple corollary of this observation is the equivalence of two terms, which is invariant to the number of occurrences per variable.

**Corollary 1.** Let E be a ground equational theory, $s, t \in \mathcal{T}(\Sigma, \mathcal{V})$. Then $\text{lin}(s) \approx_E \text{lin}(t)$ if and only if $s \approx_E t$

*Proof.* Lemma 1 implies that for all $s, t \in \mathcal{T}(\Sigma, \mathcal{V})$, $s \approx_E t$ iff for all $p \in \text{pos}(s)$ where $s|_p \in \mathcal{V}$, $s|_p = t|_p$. Thus, it does not matter how many times each variable occurs. $\square$

Corollary 1 Tells us that if we assume the minimal complete set of linear generalizations always exists for a given ground theory E (linearly-minimal), then we can produce minimal generalization by merging variables. To show linear correspondence, we still have to show that we do not miss any minimal generalizations in this process.

**Lemma 2.** Linearly minimal, ground equational theories are frozen.

**Lemma 3.** Linearly-minimal ground equational theories are minimal-producing.

Observe that linearly-minimal is essential to the result as there exist ground equational theories that are not linearly-minimal and for which the correspondence fails:

**Theorem 2.** There exists a ground equational theory E and $s, t \in \mathcal{T}(\Sigma, \emptyset)$ such that $\text{mcslg}_E(s, t)$ exists and $\text{mcsg}_E(s, t)$ does not exists.

*Proof.* Consider the equational theory:

$$E = \{ g(c) = c, g(d) = d, f(a, c, d) = e, f(b, c, d) = h, f(a, c, c) = e, f(b, d, d) = h \}$$

See Appendix F. $\square$

# References

[1] Mauricio Ayala-Rincón, David M. Cerna, Andres Felipe Gonzalez Barragan, and Temur Kutsia. Equational anti-unification over absorption theories. In Christoph Benzmüller, Marijn J. H. Heule, and Renate A. Schmidt, editors, *Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings, Part II*, volume 14740 of Lecture Notes in Computer Science, pages 317-337. Springer, 2024.
[2] Franz Baader and Tobias Nipkow. Term rewriting and all that. Cambridge University Press, 1998.

[3] Hans-Jürgen Bürckert. Some relationships between unification, restricted unification, and matching. In Jörg H. Siekmann, editor, 8th International Conference on Automated Deduction, Oxford, England, July 27 - August 1, 1986, Proceedings, volume 230 of Lecture Notes in Computer Science, pages 514–524. Springer, 1986.

[4] David M. Cerna and Temur Kutsia. Unital anti-unification: Type and algorithms. In FSCD, LIPIcs, 2020.

[5] Temur Kutsia Mauricio Ayala-Rincón, David Cerna and Christophe Ringeissen. Combining generalization algorithms in regular collapse-free theories. In FSCD, LIPIcs, 2025.

[6] Jörg H. Siekmann. Unification theory. J. Symb. Comput., 7(3/4):207–274, 1989.

# A Proof of Simple Theory Introduction

**Theorem 3.** There exists a linearly-minimal, simple equational theory E and s, t ∈ T(Σ, ∅) such that $mcsg_E(s, t)$ does not exist.

*Proof.* Consider the equational theory:

$$E = \{h(x, b) \approx_E g(x), h(x, a) \approx_E g(x), f(x, g(y)) \approx_E f(x, y)\}$$

Let $s, t \in T(\Sigma, \emptyset)$ such that $size(s) = size_E(s)$ and $size(t) = size_E(t)$, i.e. subterms of the form $f(r_1, g(r_2))$, $h(r, a)$, or $h(r, b)$ do not occur in $s$ or $t$. We show that the theory is linearly-minimal by induction on $n = size(s) + size(t)$.

* **Basecase:** let $n = 2$. Observe that $s$ and $t$ are constants, and thus, their E-equivalence classes are singleton. Thus, $G_E^{lin}(s, t)$ only contains syntactic solution implying $mcslg_E(s, t)$ exists and is singleton.

* **Stepcase:** We assume $mcslg_E(s, t)$ exists when $size(s) + size(t) \le n$ and show it exists when $size(s) + size(t) \le n + 1$. We now consider a few cases:

- $head(s) \ne head(t)$ and without loss of generality that $s = h(r_1, r_2)$ and $t = g(r_3)$. We know, by our assumption that $size(s) = size_E(s)$, that $r_2 \notin \{a, b\}$. Furthermore, $t \approx_E h(r_3, a)$ and $t \approx_E h(r_3, b)$. By the induction hypothesis, we know that $mcslg_E(r_1, r_3)$, $mcslg_E(r_2, a)$, and $mcslg_E(r_2, b)$ exist. Thus, w.l.o.g $mcslg_E(s, t) \approx_E \{h(u', u''\sigma) | u' \in mcslg_E(r_1, r_3) \wedge u'' \in mcslg_E(r_2, a) \wedge u'' \approx_E u''\sigma \wedge vars(u') \cap vars(u''\sigma) = \emptyset\}$. Observe that constructing $mcslg_E(s, t)$ as above results in incomparable terms. Thus, $mcslg_E(s, t)$ exists.

- $head(s) \ne head(t)$ and without loss of generality $head(s) \notin \{h, g\}$. This, case is similar to the basecase as the solution is the syntactic generalization, that is a variable. Furthermore, the theory is not collapse, and thus, the E-equivalence class of a variable is singleton.

- $head(s) = head(t)$ and $s = h(r_1, r_2)$ and $t = h(r_3, r_4)$. We know, by our assumption that $size(s) = size_E(s)$ and $size(t) = size_E(t)$, that $r_2, r_4 \notin \{a, b\}$. By the induction hypothesis, we know that $mcslg_E(r_1, r_3)$ and $mcslg_E(r_2, r_4)$ exist. Let $u' \in mcslg_E(r_2, r_4)$. If $u' \in \{a, b\}$, then $g(u) \in mcslg_E(s, t)$ where $u \in mcslg_E(r_1, r_3)$. Otherwise, $h(u, u'\sigma) \in mcslg_E(s, t)$ where $u \in mcslg_E(r_1, r_3)$, $u' \in mcslg_E(r_2, r_4)$, and $\sigma$ a linear variable renaming such that $vars(u) \cap vars(u'\sigma) = \emptyset$. In either case, there are only finitely many incomparable terms constructed. Thus, $mcslg_E(s, t)$ exists.

- $head(s) = head(t)$ and $s = f(r_1, r_2)$ and $t = f(r_3, r_4)$. By the induction hypothesis, we know that $mcslg_E(r_1, r_3)$ and $mcslg_E(r_2, r_4)$ exists. Observe that $f(u_1, u_2) \preceq_E f(u_1, g(u_2))$, but, due to the axiom $f(x, g(y)) \approx_E f(x, y)$, $f(u_1, g(u_2)) \preceq_E f(u_1, u_2)$ where $u_1 \in mcslg_E(r_1, r_3)$ and $u_2 \in mcslg_E(r_2, r_4)$, implying there are finitely many incomparable terms of the form $f(u_1, u_2)$. Thus, $mcslg_E(s, t)$ exists.

- $head(s) = head(t)$ and $s = g(r_1)$ and $t = g(r_2)$. By the induction hypothesis, we know that $mcslg_E(r_1, r_2)$ exists. Observe that $s \approx_E h(r_1, a)$ and $t \approx_E h(r_1, b)$. Thus, for any $u \in mcslg_E(r_1, r_2)$, $h(u, y) \in G_E^{lin}(s, t)$ where $y \in V$. However, $h(u, y) \preceq_E g(u)$ due to the linearity of the terms. Thus, there are finitely many incomparable terms of the form $g(u)$ implying $mcslg_E(s, t)$ exists.
Now that we proved $E$ is linearly-minimal we show that for the terms $s = f(a, c)$ and $t = f(b, d)$, the $mcsg_E(s, t)$ does not exists. Observe that every complete set must contain a generalization more specific than $f(x, y)$. Furthermore, every $g \in \mathcal{G}_E(s, t)$, has the form $f(x, r)$ where $r \in \mathcal{T}(\Sigma, \mathcal{V})$. We will assume, towards contradiction, that $C \subset \mathcal{G}_E(s, t)$ is minimal and complete. Let $f(x, r) \in C$. Observe that $r \in \mathcal{G}_E(s', t')$ where $s' \approx_E g^n(c)$ and $t' \approx_E g^m(d)$ for $n, m \ge 0$. This observation implies that there exists $y \in \text{vars}(r)$ such that $r\{y \mapsto c\} \prec_E g^n(c)$ and $r\{y \mapsto d\} \prec_E g^m(d)$ for some $n, m \ge 0$. Furthermore, this properties holds for $r' = r\{y \mapsto h(y, x)\}$ as $h(y, x) \preceq_E g(y)$. From these observations we can deduce that $f(x, r) \prec_E f(x, r')$ because $f(x, r')\{x \mapsto a\}, f(x, r')\{x \mapsto b\} \notin \mathcal{G}_E(s, t)$. This contradicts our assumption that $C$ is minimal and complete.

Thus, we have shown that there is a linearly-minimal simple theory $E$ that is nullary. $\square$

## B Proof Theorem 1

*Proof.* Let $E$ be a frozen equational theory and $s, t \in \mathcal{T}(\Sigma, \emptyset)$. We now show that the $mcsg_E(s, t)$ exists. By the assumption that $E$ is frozen we know that $E$ is linear-minimal and thus for all $s', t' \in \mathcal{T}(\Sigma, \emptyset)$, $mcslg_E(s', t')$ exists. We prove the theorem by showing that from any generalization, we can reach a minimal generalization. We continue by induction over $|\mathcal{g}|$ where $g \in \mathcal{G}_E(s, t)$.

* **Base case:** Assume $\text{vars}(g) = \mathcal{g}$, i.e. $\mathcal{g} = \emptyset$. This case follows from Definition 15.

* **Step case:** We assume that for all generalizations $g \in \mathcal{G}_E(s, t)$ such that $|\mathcal{g}| \le n$ there exists $g' \in \mathcal{G}_E(s, t)$ such that $g \preceq_E g'$, $\text{vars}(g') = \mathcal{g}'$; and thus, given a merger $\sigma'$ of $g'$, $g'\sigma'$ is frozen and merged. Thus, by Definition 15, $g'\sigma'$ is a minimal generalization. We show that for all generalizations $g \in \mathcal{G}_E(s, t)$ such that $|\mathcal{g}| = n+1$ there exists $g' \in \mathcal{G}_E(s, t)$ such that $g \preceq_E g'$, $\text{vars}(g') = \mathcal{g}'$; and thus given a merger $\sigma'$ of $g'$, $g'\sigma'$ is frozen and merged. Thus, by Definition 15, $g'\sigma'$ is a minimal generalization.

Let $g \in \mathcal{G}_E(s, t)$ be a generalization such that $|\mathcal{g}| = n+1$ and $x \in \mathcal{g}$. By the definition of (non-) frozen, there exist ground terms $r_1$ and $r_2$ such that $g\{x \mapsto r_1\} \prec_E s$, $g\{x \mapsto r_2\} \prec_E t$, and for all $g'' \in mcslg_E(r_1, r_2)$, $g'' \notin \mathcal{V}$. Let $r_1, r_2 \in \mathcal{T}(\Sigma, \emptyset)$ be such terms. Now, let $g^* \in mcslg_E(r_1, r_2)$ and $\nu$ a variable renaming such that $\text{vars}(g^*\nu) \cap \text{vars}(g) = \emptyset$. Because pur theory is frozen (Definition 14) we know that $\text{vars}(g^*\nu) = \mathcal{g}^*\nu$. Let $g'' = g\{x \mapsto g^*\nu\}$. Observe the $|\mathcal{g}''| = n$ and thus by the induction hypothesis there exists $g' \in \mathcal{G}_E(s, t)$ such that $g \preceq_E g'$, $\text{vars}(g') = \mathcal{g}'$, and furthermore, there exists a merger $\sigma'$ of $g'$, such that $g'\sigma$ is a minimal generalization.

Observe that, by induction, we have shown that from any $g \in \mathcal{G}_E(s, t)$, we can reach a minimal generalization. Thus, the set of all the reachable minimal generalizations is the $mcsg_E(s, t)$. $\square$

## C Proof Lemma 1

*Proof.* We prove the lemma by induction on the length of $p$.

* **Base case:** If $p = \epsilon$ then $s \in \mathcal{V}$. Given that our theory is consistent, it must hold that $t = s$. Thus, $p \in \text{pos}(t)$ and $\text{path}(s, p) = [s] = \text{path}(t, p)$.

* **Step case:** We assume the lemma holds for all $s \in \mathcal{T}(\Sigma, \mathcal{V})$ and $p \in \text{pos}(s)$ where $|p| \le n$, and $s|_p \in \mathcal{V}$. We show the lemma holds for all $s \in \mathcal{T}(\Sigma, \mathcal{V})$ and $p \in \text{pos}(s)$ where $|p| = n+1$ and $s|_p \in \mathcal{V}$.

Let us assume for contradiction, that there exists $t \in \mathcal{T}(\Sigma, \mathcal{V})$ such that $s \approx_E t$, and $p \notin \text{pos}(t)$ or $\text{path}(s, p) \ne \text{path}(t, p)$. Furthermore, let $p = q_1, q_2$ such that $q_1 \ne \epsilon$, $r, r' \in \mathcal{T}(\Sigma, \mathcal{V})$ be terms, $C$ and $C'$ be contexts such that $C|_{q_1} = C'|_{q_1} = \bullet$, $C \approx_E C'$, $s = C[r]$, and $t = C'[r']$. Observe that, by the induction hypothesis, $\text{path}(C[x], q_1) = \text{path}(C'[x], q_1)$ for any $x \in \mathcal{V}$. It follows from the above construction that either

(a) $q_2 \notin \text{pos}(r')$, or

(b) $\text{path}(r, q_2) \ne \text{path}(r', q_2)$.
However, from the induction hypothesis, we know that both (a) and (b) do not hold. Thus, we have reached a contradiction. This implies that the only position at which the equational theory can apply is at $\epsilon$; however, this is not possible as we know that $s$ contains at least one variable and $E$ cannot apply on terms that contain variables. Thus, we have proven the induction step.

□

## D Proof Lemma 2

*Proof.* Let $E$ be a linearly-minimal ground equational theory, $s, t \in \mathcal{T}(\Sigma, \emptyset)$ and $g \in \mathrm{mcslg}_E(s, t)$. Furthermore, ground theories are variable-minimizing. We prove the lemma by case distinction on $\mathrm{vars}(g)$.

* Case 1: $\mathrm{vars}(g) = \emptyset$, Then $s \approx_E t$ and the theorem trivially holds.

* Case 2: $\mathrm{vars}(g) \neq \emptyset$. We prove the statement by contradiction by assuming that there exists $g \in \mathrm{mcslg}_E(s, t)$ and $x \in \mathrm{vars}(g)$ such that $x \notin \mathcal{G}_g$. This, implies that there exists $r_1, r_2 \in \mathcal{T}(\Sigma, \emptyset)$ such that $g\{x \mapsto r_1\} \prec_E s, g\{x \mapsto r_2\} \prec_E t$ and for all $g' \in \mathrm{mcslg}_E(r_1, r_2)$, $g' \notin \mathcal{V}$. Let $r_1, r_2 \in \mathcal{T}(\Sigma, \emptyset)$ be such terms, $g' \in \mathrm{mcslg}_E(r_1, r_2)$, $\sigma$ a variable renaming such that $\mathrm{vars}(g) \cap \mathrm{vars}(g'\sigma) = \emptyset$, and $g^* = g\{x \mapsto g'\sigma\} \in \mathcal{G}_E(s, t)$. Observe that (i) $\mathrm{vars}(g') \neq \emptyset$ and (ii) $g \preceq_E g^*$. By contraposition of Lemma 1, $g \not\preceq_E g^*$ because for any position $p \in \mathrm{pos}(g)$ such that $g|_p = x, \mathrm{path}(g, p) \neq \mathrm{path}(g^*, p)$. Furthermore, there does not exists a substitution $\nu$ with $\mathrm{dom}(\nu) \subseteq \mathrm{vars}(g^*)$ such that $g^*\nu \approx_E g$ as this would imply that $g' \notin \mathrm{mcslg}_E(r_1, r_2)$. Thus, $g \prec_E g^*$ and we have arrived at a contradiction.

□

## E Proof Lemma 3

*Proof.* Let $E$ be a linearly-minimal ground equational theory. By Lemma 2, We know that $E$ is frozen. We now show that $E$ is minimal-producing, that is, for all $s, t \in \mathcal{T}(\Sigma, \emptyset)$ and frozen, merged $g \in \mathcal{G}_E(s, t)$, $g$ is a minimal generalization. Observe that if there exists $g' \in \mathcal{G}_E(s, t)$ such that $g \prec_E g'$, then there would have to exist $x \in \mathrm{vars}(g)$ and $r_1, r_2 \in \mathcal{T}(\Sigma, \emptyset)$ such that $g\{x \mapsto r_1\} \prec_E s, g\{x \mapsto r_2\} \prec_E t$, and $g'' \in \mathcal{G}_E(r_1, r_2)$, $g'' \notin \mathcal{V}$. Observe that $g''$ cannot be ground as this would imply that $g$ is not frozen. By Corollary 1, we can replace $g''$ by $\mathrm{lin}(g'')$ and by linear-minimality we know that there exists $g^* \in \mathrm{mcslg}_E(r_1, r_2)$ such that $\mathrm{lin}(g'') \preceq_E g^*$. Thus, we can substitute $x$ by $g^*$ instead of $g'$. However, if $g^*$ is not a variable, this construction contradicts our assumption that $\mathrm{vars}(g) = \mathcal{G}_g$. Thus, $g$ must be minimal.

□

## F Proof Theorem 2

*Proof.* Consider the equational theory:

$$E = \left\{ \begin{array}{l} g(c) = c, g(d) = d, \\ f(a, c, d) = e, f(b, c, d) = h, \\ f(a, c, c) = e, f(b, d, d) = h \end{array} \right\}$$

Let $s = e$ and $t = h$. We now show that $\mathrm{mcslg}_E(s, t)$ exists. Observe that $f(x, y, z) \in \mathcal{G}_E^{\mathrm{lin}}(s, t)$. The only term $r$ more specific than $f(x, y, z)$ such that $r \in \mathcal{G}_E^{\mathrm{lin}}(s, t)$ is $f(x, c, d)$. Observe that all other terms constructable from $E$ are either equivalent to $f(x, c, d)$ or more general.

Now that we proved for terms $s = e$ and $t = h$ that $\mathrm{mcslg}_E(s, t)$ exists, we show that for the terms $s = e$ and $t = h$, the $\mathrm{mcsg}_E(s, t)$ does not exist. Observe that every complete set must contain a generalization more specific than $f(x, y, y)$. Furthermore, every $g \in \mathcal{G}_E(s, t)$, such that $f(x, y, y) \prec_E g$ has the form $f(x, r, r)$ where $r \in \mathcal{T}(\Sigma, \mathcal{V})$. We will assume, towards contradiction, that $C \subset \mathcal{G}_E(s, t)$ is minimal and complete. Let $f(x, r, r) \in C$. Observe that $r \in \mathcal{G}_E(s', t')$ where $s' \approx_E g^n(c)$ and $t' \approx_E g^n(d)$ for $n \ge 0$. This observation implies that there exists $y \in \mathrm{vars}(r)$ such that $r\{y \mapsto c\} \prec_E c$ and $r\{y \mapsto d\} \prec_E d$. Furthermore, this properties holds for $r' = r\{y \mapsto g(y)\}$ by axioms $g(c) = c$ and $g(d) = d$. From these observations we can deduce that $f(x, r, r) \prec_E f(x, r', r')$ because $f(x, r', r')\{y \mapsto c\}, f(x, r', r')\{y \mapsto d\} \notin \mathcal{G}_E(s, t)$. This contradicts our assumption that $C$ is minimal and complete.

Thus, we have shown that there is a linearly-minimal simple theory $E$ that is nullary.

□