Generalization of terms via universal algebra

TL;DR

The paper develops a universal-algebraic framework for generalizing terms up to equational theories (e-generalization) by translating problems into homomorphisms from the 1-generated free algebra and studying their kernels via projective and exact algebras. It proves that for broad classes of varieties, notably 1EP and 1ESP, the e-generalization type can be analyzed using the congruence lattice of the 1-generated free algebra, and in 1ESP varieties the solution poset is dual to the lattice of projective congruences below ker(h). The authors illustrate unitary e-generalization type for several key varieties, including abelian groups, commutative monoids and semigroups, lattices/semilattices, Boolean algebras, Kleene algebras, and Gödel algebras, and apply the theory to algebraizable logics such as classical, Gödel-Dummett, and Kleene logics. The framework provides invariant-based classifications of generalization problems, yields practical methods to obtain least general solutions through congruence data, and suggests directions for extending the approach to Heyting and MV-algebras and for applications to refutation systems and inductive logic programming.

Abstract

We provide a new foundational approach to the generalization of terms up to equational theories. We interpret generalization problems in a universal-algebraic setting making a key use of projective and exact algebras in the variety associated to the considered equational theory. We prove that the generality poset of a problem and its type (i.e., the cardinality of a complete set of least general solutions) can be studied in this algebraic setting. Moreover, we identify a class of varieties where the study of the generality poset can be fully reduced to the study of the congruence lattice of the 1-generated free algebra. We apply our results to varieties of algebras and to (algebraizable) logics. In particular we obtain several examples of unitary type: abelian groups; commutative monoids and commutative semigroups; all varieties whose 1-generated free algebra is trivial, e.g., lattices, semilattices, varieties without constants whose operations are idempotent; Boolean algebras, Kleene algebras, and Gödel algebras, which are the equivalent algebraic semantics of, respectively, classical, 3-valued Kleene, and Gödel-Dummett logic.

Figures (5)

• Figure 1:
• Figure 2: ${\bf F}_{\mathsf{BA}}(z)$ and its congruence lattice, where $\langle z, 1 \rangle$ and $\langle\neg z, 1 \rangle$ represent, respectively, the congruences generated by $(z,1)$ and $(\neg z,1)$.
• Figure 3: On the left-most, the free 1-generated Kleene algebra ${\bf F}_{\mathsf{KA}}(z)$; then from left-to-right its quotients ${\bf 4}_{\mathsf{KA}}$ (generated by the congruence $\langle(z\vee \neg z), 1\rangle$), ${\bf K}_{4}$ (given by $\langle z, (z\vee \neg z)\rangle$ or $\langle z, (z\wedge \neg z)\rangle$), ${\bf K}_{3}$ (obtained by $\langle z, \neg z\rangle$), ${\bf 2}_{\mathsf{KA}}$ (from $\langle z,1\rangle$$\langle \neg z,1\rangle$), and the trivial algebra (by $\langle 0,1\rangle$).
• Figure 4: The involutive posets dual of the 1-generated exact Kleene algebras ${\bf F}_{\mathsf{KA}}(1)$, ${\bf K}_{4}$ and ${\bf 2}_{\mathsf{KA}}$ respectively.
• Figure 5: The lattice of congruences of ${\bf F}_{\mathsf{KA}}(z)$, with highlighted the projective congruences.

Theorems & Definitions (70)

• Definition 2.1
• Theorem 2.2
• Definition 2.3
• Definition 2.4
• Theorem 2.5
• Definition 2.6
• Proposition 2.7
• proof
• Remark 2.8
• Definition 3.1