{'fraction_non_alphanumeric': 0.056057731651973364, 'fraction_numerical': 0.008667187441877767, 'mean_word_length': 3.980363097443498, 'pattern_counts': {'":': 0, '<': 4, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 9, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Exact Unification and Admissibility

A new hierarchy of"exact"unification types is introduced, motivated by the study of admissible rules for equational classes and non-classical logics. In this setting, unifiers of identities in an equational class are preordered, not by instantiation, but rather by inclusion over the corresponding sets of unified identities. Minimal complete sets of unifiers under this new preordering always have a smaller or equal cardinality than those provided by the standard instantiation preordering, and in significant cases a dramatic reduction may be observed. In particular, the classes of distributive lattices, idempotent semigroups, and MV-algebras, which all have nullary unification type, have unitary or finitary exact type. These results are obtained via an algebraic interpretation of exact unification, inspired by Ghilardi's algebraic approach to equational unification.


Introduction
It has long been recognized that the study of admissible rules is inextricably related to the theory of equational unification (see, e.g., [34,16,17]). Indeed, from an algebraic perspective, admissibility of clauses in an equational class of algebras may be understood as a generalization of unifiability of finite sets of identities in the class, and conversely, checking admissibility may be reduced to comparing certain sets of unifiers. This paper provides a new classification of equational unification problems that simplifies these reductions for certain classes, including distributive lattices, idempotent semigroups, and MV-algebras.
Let us fix an equational class of algebras V for a finite algebraic language L. 1 We denote the formula algebra of L over a set of variables X by Fm L (X) and write Var(Σ) to denote the set of variables occurring in a set of L-identities Σ. A substitution (homomorphism) σ : Fm L (X) → Fm L (ω) is called a V-unifier (over X) of a set of L-identities Σ with Var(Σ) ⊆ X if for all ϕ ≈ ψ in Σ, V |= σ(ϕ) ≈ σ(ψ).
In this case, Σ is also said to be V-unifiable.
In particular, Σ is V-unifiable if and only if (henceforth iff) Σ ⇒ ∅ is not V-admissible.
Suppose now that the unification type of V is at most finitary: that is, every V-unifier of a set of L-identities Σ over a finite set X ⊇ Var(Σ) is equivalent in V to one of a finite set S of V-unifiers of Σ over X composed with a further substitution. Then any clause Σ ⇒ ∆ satisfying Var(∆) ⊆ X is V-admissible iff each member of S is a V-unifier of a member of ∆. If there is an algorithm for determining such a finite basis set S for Σ and the equational theory of V is decidable, then checking V-admissibility is also decidable. This observation, together with the pioneering work of Ghilardi on equational unification for classes of Heyting and modal algebras [16,17], has led to a wealth of decidability, complexity, and axiomatization results for admissibility in these classes and corresponding intermediate and modal logics [21,22,24,13,5,4,32,19].
The success of this approach to admissibility appears to rely on considering varieties with at most finitary unification type. That this is not a necessary condition, however, is illustrated by the case of MV-algebras, the algebraic semantics of Lukasiewicz infinitevalued logic (see [12] for details). Decidability, complexity, and axiomatization results for admissibility in MV-algebras have been established by Jeřábek [25,26,27] via a similar reduction of finite sets of identities to finite approximating sets of identities. On the other hand, it has been shown by Marra and Spada that the class of MV-algebras has nullary unification type [29]. This means that there are finite sets of identities for which no finite basis of unifiers exists. Further examples of this discrepancy may be found in [11,31], including the simple example of the class of distributive lattices where admissibility and validity of clauses coincide but unification is nullary.
As mentioned above, it is possible to check the V-admissibility of a clause Σ ⇒ ∆ by checking that every V-unifier of Σ in a certain basis set V-unifies some member of ∆. Such a basis set S typically has the property that every other V-unifier of Σ is obtained, modulo equivalence in V, by applying a further substitution to a member of S. The starting point for this paper is the observation that a weaker condition on S suffices, leading potentially to smaller basis sets of V-unifiers. For checking V-admissibility, it is enough that any V-unifier of Σ over a finite set X ⊇ Var(Σ) is a V-unifier of all identities with variables in X that are V-unified by some particular member of S. Then Σ ⇒ ∆ with Var(∆) ⊆ X is V-admissible iff each member of S is a V-unifier of a member of ∆. This observation leads to a new preordering of V-unifiers and hierarchy of "exact" unification types.
We also provide here an algebraic characterization of exact unification, where finite sets of identities are represented by finitely presented algebras. In Ghilardi's algebraic account of (standard) unification, unifiers are homomorphisms from finitely presented algebras into projective algebras of the class, preordered by composition of homomorphisms [15]. Coexact unifiers are defined here as homomorphisms from finitely presented algebras onto algebras that embed into the ω-generated free algebra of the class; the preordering remains the same. This contrasts with the syntactic account of exact unification where the unifiers are unchanged but a new preorder is introduced. Nevertheless, the syntactic and algebraic exact unification types coincide as in the standard unification setting.
Although certain equational classes have the same exact type as unification type (e.g., any equational class of unitary unification type will have unitary exact type), we also obtain examples where the exact type is strictly smaller. In particular, the classes of distributive lattices and Stone algebras have nullary unification type but unitary exact type, while the classes of idempotent semigroups, pseudo-complemented distributive lattices, Kleene algebras, De Morgan algebras, and MV-algebras all have nullary unification type but finitary exact type. We also provide an example (due to R. Willard) of an equational class that has infinitary unification type but finitary exact type. 2 We proceed as follows. In Section 2, we recall some standard notions of equational unification and admissibility, and describe Ghilardi's algebraic account of unification types. In Section 3, we introduce the new exact unification preordering and exact types, providing also an algebraic interpretation and applications. Several cases studies are considered in Section 4 and some ideas for further research are presented in Section 5.

Equational Unification and Admissibility
In this section, we describe briefly some key notions from the theory of equational unification (referring to [3] for further details) and their relevance to the study of admissible rules. In particular, we recall the unification type of a finite set of identities in an equational class and the algebraic account of unification provided by Ghilardi in [15]. These notions and also those to appear in subsequent sections are most elegantly presented in the general setting of preordered sets.
Let P = P, ≤ be a preordered set (i.e., ≤ is a reflexive and transitive binary relation on P ). A complete set for P is a subset M ⊆ P such that for every x ∈ P , there exists y ∈ M satisfying x ≤ y. A complete set M for P is called a µ-set for P if x ≤ y and y ≤ x for all distinct x, y ∈ M . It is easily seen that if P has a µ-set, then every µ-set of P has the same cardinality. Hence P may be said to be nullary if it has no µ-sets (type(P) = 0), infinitary if it has a µ-set of infinite cardinality (type(P) = ∞), finitary if it has a finite µ-set of cardinality greater than 1 (type(P) = ω), and unitary if it has a µ-set of cardinality 1 (type(P) = 1). These types are ordered as follows: 1 < ω < ∞ < 0.
The following trivial but helpful observation confirms that the type of a preordered set depends only on its corresponding quotient poset. . Suppose that two preordered sets P, ≤ and Q, ≤ are equivalent: i.e., there exists a map e : P → Q such that (1) for each q ∈ Q, there is a p ∈ P such that e(p) ≤ q and q ≤ e(p), and (2) ] for all p 1 , p 2 ∈ P , p 1 ≤ p 2 iff e(p 1 ) ≤ e(p 2 ). Then P, ≤ and Q, ≤ have the same type.
2 Another alternative hierarchy of unification types is obtained by considering left and right substitutions and so-called essential unifiers [20]. Although some of the advantages of this hierarchy are shared by our approach (e.g., the type of idempotent semigroups is in both cases finitary, contrasting with the fact that the unification type is nullary), the preordering for essential unification is different to the preordering presented here and not suited to reasoning about admissibility.
We turn our attention now to the syntactic account of equational unification. Let us fix a finite algebraic language L and an equational class V of L-algebras (equivalently, a variety: a class of L-algebras closed under taking products, subalgebras, and homomorphic images). 3 Consider a finite set X ⊆ ω and substitutions σ i : Fm L (X) → Fm L (ω) for i = 1, 2. We say that σ 1 is more general than σ 2 in V, written σ 2 V σ 1 , if there exists a substitution τ : Let Σ be a finite set of L-identities and let X ⊇ Var(Σ) be a finite set of variables. Then U V (Σ, X) is defined as the set of V-unifiers of Σ over X preordered by V , and we let U V (Σ) = U V (Σ, Var(Σ)). Note also that, trivially, For U V (Σ) = ∅, the V-unification type of Σ is defined as type(U V (Σ)). The unification type of V is then the maximal type of a V-unifiable finite set Σ of L-identities.
Let us now recall Ghilardi's algebraic account of equational unification [15]. We denote the free L-algebra of V over a set of variables X by F V (X) and let h V : Fm L (X) → F V (X) be the canonical homomorphism acting as the identity on X. Given a finite set of Lidentities Σ and a finite set of variables X ⊇ Var(Σ), we denote by Fp V (Σ, X), the algebra in V finitely presented by Σ and X: that is, the quotient algebra We also let FP(V) denote the class of finitely presented algebras of V. type U V (Σ, X) = type U V (Fp V (Σ, X)) . 3 The results of this paper also hold for quasi-equational classes and, more generally, any class of algebras that contains finitely presented algebras for all finite presentations (equivalently, prevarieties: classes closed under taking products, subalgebras, and isomorphic images [18]). However, as the vast majority of cases considered in the literature are equational classes, we restrict our account to this slightly simpler setting.

EXACT UNIFICATION AND ADMISSIBILITY 5
Hence the algebraic unification type of V coincides with the unification type of V.
Let us see now how these ideas relate to the notion of admissibility defined in the introduction. Recall that the kernel of a homomorphism h : A → B is defined as In what follows, we will freely identify L-identities with pairs of L-formulas. We will also say that an L-clause Σ ⇒ ∆ is valid in a class of L-algebras K, written K |= Σ ⇒ ∆, if the universal sentence (∀x)( Σ ⇒ ∆) is valid in each algebra in K. The admissibility of an L-clause can then be reformulated as follows: Then the following are equivalent: Proof. We give a proof here of this well known equivalence (see, e.g., [34,31]) for the sake of completeness.
Corollary II.11.6]) that, for each L-identity ϕ ≈ ψ: Hence a substitution σ : be a homomorphism such that Σ ⊆ ker g. Let σ be a map sending each variable x to a member of the equivalence class g(x). By the universal mapping property for Fm L (ω), this extends to a homomorphism σ : If ∆ = {ϕ ≈ ψ}, then (ii) is clearly equivalent to (iv).
Suppose now that V is any equational class of L-algebras and that Σ and ∆ are finite sets of L-identities. Given any complete set S for U V (Σ, Var(Σ ∪ ∆)), it follows directly that Moreover, if V is unitary or finitary and there exists an algorithm for finding finite complete sets of unifiers, then checking admissibility in V is decidable whenever the equational theory of V is decidable. There are, however, important equational classes having infinitary or nullary unification type for which such a method is unavailable. The starting point for the new approach described below is the observation that the above equivalence can hold even for a set S that is not complete for the V -preordered set of V-unifiers. It suffices rather that each σ ∈ U V (Σ, Var(Σ ∪ ∆)) is a V-unifier of all the identities V-unified by some particular member of S.

Exact Unification
We begin by defining a new preorder on substitutions relative to a fixed equational class of L-algebras V. Let X be a finite set of variables and let σ i : More precisely: Clearly, ⊑ V is a preorder on substitutions of the form σ : Fm L (X) → Fm L (ω).
Now let Σ be a finite set of L-identities and let X ⊇ Var(Σ) be a finite set of variables. E V (Σ, X) is defined as the set of V-unifiers of Σ over X preordered by ⊑ V , and we denote E V (Σ, Var(Σ)) by E V (Σ). If E V (Σ) = ∅, then the exact type of Σ in V is defined as type(E V (Σ)). We also define the exact type of V to be the maximal exact type of a V-unifiable finite set Σ of L-identities in V.
The following relationship between exact unification and admissibility in V is an immediate consequence of Lemma 2.4.
Corollary 3.2. Let Σ ∪ ∆ be a finite set of L-identities and let X ⊇ Var(Σ ∪ ∆) be a finite set of variables. If S is a complete set for E V (Σ, X), then the following are equivalent: Note (again) that if V has unitary or finitary exact type and there exists an algorithm for finding finite complete sets of unifiers, then checking admissibility in V is decidable whenever the equational theory of V is decidable. We also observe that the cardinality of a finite complete set of unifiers for the premises of a clause provides a bound for the number of consequences relevant for determining its admissibility.
We turn our attention now to the algebraic interpretation of exact unification. Note that while the syntactic accounts of exact unification and standard unification use the same sets of unifiers but consider different preorders, the algebraic interpretations of exact unification and standard unification share the same preorder but differ in the sets of (algebraic) unifiers considered (see also the comments after Theorem 3.6).
Following [14], a finite set of L-identities Σ will be called exact in V if there exists a substitution σ : Fm L (Var(Σ)) → Fm L (ω) such that for all ϕ, ψ ∈ Fm L (Var(Σ)), Note that, by definition, every finite set of L-identities that is exact in V is V-unifiable.
Let Σ be a finite set of L-identities and let X ⊇ Var(Σ) be a finite set of variables. We define ρ (Σ,X,V) : F V (X) → Fp V (Σ, X) as the canonical quotient homomorphism from the free algebra F V (X) to the finitely presented algebra Fp V (Σ, X).
An algebra A ∈ V is called exact in V if it is isomorphic to a finitely generated subalgebra of F V (ω). By Lemma 3.5 (see also [14]), a finite set of L-identities Σ is exact in V iff the finitely presented algebra Fp V (Σ, Var(Σ)) is exact in V.
Given A ∈ FP(V), an onto homomorphism u : A → E is called a coexact unifier for A in V if E is exact in V. Coexact unifiers are preordered in the same way as algebraic unifiers; that is, if u i : A → E i for i = 1, 2 are coexact unifiers for A in V, then u 1 ≤ u 2 iff there exists a homomorphism f : Let C V (A) be the set of coexact unifiers for A ∈ FP(V) preordered by ≤. If C V (A) = ∅, then the exact type of A is defined as the type of C V (A). The algebraic exact type of V is the maximal exact type of A in V such that C V (A) = ∅. Theorem 3.6. Let V be an equational class and let Σ be a finite V-unifiable set of Lidentities. Then for any finite set of variables X ⊇ Var(Σ): Hence the exact type and the algebraic exact type of V coincide.
Then Σ ⊆ ker(σ•h V ), and there exists a homomorphism u σ : Note that the map u σ is onto h V (σ(Fm L (X))). Because h V (σ(Fm L (X))) is a finitely generated subalgebra of F V (ω), also u σ ∈ C V (Fp V (Σ, X)). It suffices now, by Lemma 2.1, to show that the assignment σ → u σ determines an equivalence between the preordered sets E V (Σ, X) and C V (Fp V (Σ, X)).
(2) Using (3.1), for all σ 1 , σ 2 ∈ E V (Σ, X): Let us denote the codomains of u σ 1 and u σ 2 by E 1 and E 2 , respectively. Because u σ 1 is onto E 1 , also ker(u σ 1 ) ⊆ ker(u σ 2 ) iff there exists h : In passing from Ghilardi's algebraic account of unification to algebraic coexact unifiers, we have modified the definition of unifiers but preserved the preorder. An alternative approach, perhaps closer to the syntactic approach to exact unification, would be to preserve the unifiers as maps from a finitely presented algebra into a projective algebra, modifying the preorder. However, the characterization provided here highlights the connection between coexact unifiers and certain congruences of the relevant finitely presented algebra.
Given an algebra A in V, recall that Con(A) denotes the set of congruences on A. We let Con e (A) denote the set of congruences θ ∈ Con(A) of A such that the quotient A/θ is exact in V; i.e., Con e (A) = {θ ∈ Con(A) | A/θ ∈ IS(F V (ω))}.
Theorem 3.7. Let V be an equational class and A ∈ FP(V).
(a) For any onto homomorphism u : A → B: Hence Proof. For (a), observe that, by the homomorphism theorem: .
Corollary 3.8. Let V be a locally finite equational class. Then type(C V (A)) ∈ {1, ω} for each A ∈ FP(V). Hence V has unitary or finitary exact type.
Proof. As V is locally finite, each finitely generated algebra in V is finite. In particular, any given A ∈ FP(V) is finite. But then also Con e (A) is finite. Hence, using Theorem 3.7, type(C V (A)) = type(Con e (A)) ∈ {1, ω}.
Corollary 3.9. Let V be an equational class and consider A ∈ FP(V) such that Con(A) is totally ordered by inclusion. If C V (A) = ∅, then it is totally ordered and type(C V (A)) ∈ {1, 0}. In particular, if A is simple, then either C V (A) = ∅ or type(C V (A)) = 1.

Case Studies
Any unitary equational class (e.g., the class of Boolean algebras or the class of all algebras for some language) also has unitary exact type. Similarly, any finitary equational class will have unitary or finitary exact type. In particular, the class of Heyting algebras is finitary [16] and also has finitary exact type: the identity x ∨ y ≈ ⊤ has two most general exact unifiers as described in Example 2.2. Minor changes to the original proofs that the classes of groups (see [1]) have infinitary unification type and modal algebras for the logic K (see [23]) have nullary unification type establish that the same holds also for the exact types. The class of semigroups has infinitary unification type [33] and, by considering again the set {x · y ≈ y · x}, infinitary or nullary exact type; we have been unable so far to determine which of these holds, however. Below we consider some more interesting cases where the type is known to change, collecting these results in Table 1.
In such cases, we may be able to obtain characterizations and algorithms for most exact unifiers of finite sets of identities. Consider again the class D of distributive lattices, where L is the language of lattices and 2 = ({0, 1}, ∧, ∨) is the two-element distributive lattice with 0 < 1. For each set of variables X and each map g : X → {0, 1}, let us denote byḡ : Fm L (X) → 2, the unique homomorphism extending g. Recall that 2 generates the variety D. Hence for α, β ∈ Fm L (X), h D (α) = h D (β) iffḡ(α) =ḡ(β) for all maps g : X → {0, 1}. So for a substitution σ : We define a substitution σ : To see that σ is a D-unifier of Σ, we claim thatḡ • σ ∈ S for each g : Y → {0, 1}. Note first that if g is the constant map 0, then clearlyḡ(σ(α)) = 0 =ḡ(σ(β)) for each α ≈ β ∈ Σ, that is,ḡ • σ ∈ S. If there exists k ∈ {1, . . . , m} such that g(y i ) = 1 iff i = k, then for i ∈ {1, . . . , n}, that is,ḡ • σ =f k ∈ S. Finally, if g(y i ) = g(y j ) = 1 for some i = j, thenḡ(ϕ) = 1, and g • σ(α) =ḡ • σ(β) = 1 for each α ≈ β ∈ Σ. Hence σ is a D-unifier of Σ and, by (4.1), To see that σ is the most exact D-unifier of Σ, let σ ′ : Fm L (X) → Fm L (ω) be a D-unifier of Σ and let Z be a finite subset of ω such that σ ′ (Fm L (X)) ⊆ Fm L (Z). Then, given a map g : Hence σ ′ ⊑ D σ. For each n ∈ N, let B n = (B n , ∧, ∨, * , ⊥, ⊤) denote the finite Boolean algebra with n atoms and let B ′ n be the algebra obtained by adding a new top ⊤ ′ to the underlying lattice of B n and endowing it with the unique operation * making it into a pseudocomplemented distributive lattice. Let B n denote the subvariety of B ω generated by B ′ n . It was proved by Lee in [28] that the subvariety lattice of B ω is where B 0 and B 1 are the varieties of Boolean algebras and Stone algebras, respectively. We have already observed that the variety B 0 of Boolean algebras has unitary exact type. The case B 1 of Stone algebras is similar to distributive lattices: B 1 has nullary unification type [15], but all finitely presented Stone algebras are exact (see [11,Lemma 20]), so B 1 has unitary exact type.
In [15] it was proved that B ω has nullary unification type, and the same result was proved in [10] for B n for each n ≥ 2. However, all these varieties are locally finite, so an application of Corollary 3.8 proves that they have at most finitary exact type. It is easy to prove that {x ∨ ¬x ≈ ⊤} ⇒ {x ≈ ⊤, ¬x ≈ ⊤} is B ω -admissible and B n -admissible for each n ≥ 2 and that neither {x ∨ ¬x ≈ ⊤} ⇒ x ≈ ⊤ nor {x ∨ ¬x ≈ ⊤} ⇒ ¬x ≈ ⊤ is B ω -admissible or B n -admissible with n ≥ 2. So, using Proposition 3.4, the classes B ω and B n with n ≥ 2 have finitary exact type. Then up to equivalence in V, formulas have a normal form (again associating to the left) 0, 1, or xy 1 y 2 . . . y n where x is any variable, y 1 , . . . , y n are variables or 1, and y i = y j = 1 implies i = j. It is immediate that finitely generated free algebras are finite and hence that V is locally finite. Note also that {xy ≈ 0} has three most general exact unifiers σ 1 (x) = 1, σ 1 (y) = y; σ 2 (x) = 0, σ 2 (y) = y; σ 3 (x) = x, σ 3 (y) = yz.
So the exact type of V is finitary. However, the following set of identities has infinitary unification type: Observe that σ(x) = x, σ(y) = 1 is a V-unifier of Σ, as are, for each n ∈ N and distinct variables z 1 , . . . , z n different from y, σ n (x) = xyz 1 . . . z n , σ n (y) = y.
Moreover, the set {σ n | n ∈ N} ∪ {σ} is a µ-set for U V (Σ). Finally, no finite set of identities has nullary unification type. To see this, it suffices to show that the set of substitutions over some finite set of variables X preordered by V contains no infinite strictly increasing chains. Intuitively, this is because applying a substitution to a formula in normal form either produces a formula of greater or equal length or a formula equivalent to 0. More formally, consider some substitution σ over X = {x 1 , . . . , x n }. We prove that σ does not form part of an infinite strictly increasing chain by induction on the number k of variables x in X such that σ(x) is equivalent to 0. For the base case k = 0, if σ V σ ′ , then the length of the normal form of σ ′ (x i ) must be smaller than or equal to the length of the normal form of σ(x i ). As there are finitely many non-equivalent (up to the names of the variables) such strings of characters, there are finitely many non-equivalent possible σ ′ more general than σ. For the inductive step, we suppose that σ(x i ) is equivalent to 0 and assume for a contradiction that σ forms part of an infinite strictly increasing chain of substitutions. Observe that σ ′ (x i ) must be equivalent to 0 for every σ ′ above σ in the chain; otherwise, by the induction hypothesis applied to σ ′ , the chain is finite, contradicting our assumption. But then we can construct another strictly increasing infinite chain of substitutions extending σ by setting σ ′ (x i ) = z for a fresh variable z, for each σ ′ in the original chain, contradicting the induction hypothesis.
Example 4.4 (MV-Algebras). It was proved in [29] that the equational class MV of MValgebras, the algebraic semantics of Lukasiewicz infinite-valued logic (see [12] for details), has nullary unification type. This class is not locally finite, so Corollary 3.8 does not apply, but combining results from [26] and [9], we can still prove that it has finitary exact type.
Let L be the language of MV-algebras and let Σ be a finite set of L-identities. Finitely presented MV-algebras admit a presentation {α ≈ ⊤}, so there is no loss of generality in assuming that Σ = {α ≈ ⊤}. Let us fix X = Var(Σ) and A = Fp MV ({α ≈ ⊤}, X).

Concluding Remarks
In this paper, we have introduced a new hierarchy of exact types based on an inclusion preordering of unifiers, and shown, via an algebraic interpretation of unifiers, that certain classes have nullary or infinitary unification type, but unitary or finitary exact type. We do not know, however, if there exist equational classes of (i) finitary unification type that have unitary exact type, (ii) infinitary unification type that have unitary or nullary exact type, or (iii) nullary unification type that have infinitary exact type.
In [11], the current authors have presented axiomatizations for the admissible rules of several locally finite (and hence at most finitary exact type) equational classes with nullary unification type. In all these cases, a complete description of exact algebras, and the unitary or finitary exact type plays a central (if implicit) role. We expect that this approach will also be useful for addressing admissibility in other classes of algebras that have unitary or finitary exact type, but nullary or infinitary unification type: e.g., the locally finite equational classes of pseudocomplemented distributive lattices (see [10]) and Sugihara algebras, the algebraic semantics of the relevant logic R-Mingle (see [30]). Note, however, that the most significant open problems in this area concern the decidability and axiomatization of unifiability and admissibility in the modal logic K, where the exact type remains nullary.
Finally, although it is possible, as in the case of distributive lattices above, to obtain algorithms for building a (finite) set of most general exact unifiers for a finite set of identities, we do not yet have a general method, even for locally finite equational classes. Here the problem is that we may be able to construct the congruence lattice of the relevant algebra but we do not know how to decide if the quotient of the algebra by a particular congruence embeds into the free algebra on countably infinitely many generators of the class.