Politeness for the Theory of Algebraic Datatypes (Extended Abstract)

1 Introduction

Algebraic datatypes are extremely common in many programming languages. Reasoning about them is therefore crucial for modeling and verifying programs. Various decision procedures for algebraic datatypes have been and continue to be developed and employed by formal reasoning tools such as theorem provers and Satisfiability Modulo Theories (SMT) solvers [Barrett et al., 2007; Reynolds et al., 2018; Reynolds and Blanchette, 2017; Kov´acs et al., 2017; Guti´errez and Meseguer, 2017; Meseguer, 2018; Hojjat and R¨ummer, 2017; Bonacina and Echenim, 2007; Armando et al., 2009]. SMT solvers employ a combination framework that derives a decision procedure for combined theories by using the decision procedure for each theory as a black box. This is useful, as many applications require reasoning about combined theories. For example, the verification of a simple programmay require reasoning about arithmetic, bit-vectors, datatypes, etc. To integrate a new theory into such a framework, it suffices to focus on the decision procedure of the new theory, and its interface to the generic combination framework. The interface is what we focus on in this paper.

∗Originally published as Politeness for the Theory of Algebraic Datatypes at the 10th edition of the International Joint Conference on Automated Reasoning (IJCAR) in Paris, France.

The traditional combination method of Nelson and Oppen [Nelson and Oppen, 1979] is applicable for the combination of the theory of datatypes with other theories, as long as the other theories are stably infinite. Some theories of interest, however, are not stably infinite, the most notable one being the theory of fixed-width bit-vectors, which is commonly used for modeling and verifying both hardware and software. To be able to perform combinations with such theories, a more general combination method was designed [Ranise et al., 2005], which relies on polite theories. This notion was later strengthened to strongly polite theories [Jovanovic and Barrett, 2010], which are needed to properly handle variable arrangements in the theory combination mechanism. Strongly polite theories can be combined with any other disjoint decidable theories. While strong politeness was already proven for several useful theories (such as equality, arrays, sets, multisets [Ranise et al., 2005]), strong politeness of algebraic datatypes remained an unanswered question.

The main contribution of this paper is an affirmative answer to this question. The main challenge in proving politeness is producing a witness function that preserves equivalence but allows for minimal satisfying models. We introduce a witness function that essentially "guesses" the right constructors of variables without an explicit constructor in the formula. We show how to "shrink" any model of a formula that is the output of this function to obtain a minimal model. The witness function, as well as the model construction, can be used by any SMT solver that includes the theory of datatypes and implements polite theory combination. We introduce and use the notion of additive witnesses, which allows us to prove politeness and conclude strong politeness. We further study the theory of datatypes beyond politeness and extend a decision procedure for a subset of this theory presented in [Chocron et al., 2020] to support the full theory.

2 Datatypes and Politeness

2.1 The Theory of Datatypes

We use the definition of the theory of algebraic datatypes as it appears in the SMT-LIB 2 standard [Barrett et al., 2010]. Our formalization is based on [Barrett et al., 2007], but adjusted to suit our investigation of politeness. For formal definitions, we refer the reader to [Sheng et al., 2020]. Here we provide only a summary of the definitions.

A signature Σ consists of sort, function and predicate symbols. We use varsσ(ϕ) to denote the set of variables with sort σ in formula ϕ. FΣ denotes the set of function symbols of Σ and SΣ denotes the set of sorts in Σ. A datatypes signature further splits the set of sorts into a set of element sorts denoted Elem, and a set of struct sorts denoted Struct, with finitely many constructors (used in formulas like y = c(w1, ...,wk)) and selectors (used in formulas like y = sc,i(x)) as function symbols, and testers (used in formulas like isc(x)) as predicate symbols. In what follows, CO stands for the constructors in Σ and SE for its selectors.

Interpretations and satisfaction are defined as usual. For a Σ-interpretation A, γA denotes the interpretation of γ in A, where γ can be a sort, a variable, or a function/predicate symbol, or a set of these. A Σ-theory is a class of Σinterpretations.

Intuitively, the interpretations in the theory of datatypes correspond to term models generated by the constructors. The interpretation of testers is as expected, and the interpretation of selectors is also as expected for terms that were built with the corresponding constructor (otherwise, selectors are freely interpreted). We use TΣ to denote the theory of datatypes based on the datatypes signature Σ.

Example 1. The signature Σlist has sorts elemand list. Its function symbols are cons of arity (elem × list) → list, nil of arity list, car of arity list → elem and cdr of arity list → list. Its predicate symbols are isnil and iscons , both of arity list. It is a datatypes signature, with Elem = {elem}, Struct = {list}, CO = {nil , cons} and SE = {car, cdr}. car represents the head of the list and cdr represents its tail. nil represents the empty list.

In the theory of datatypes, a sort σ is inductive if for any natural number k, there is a term with sort σ that applies k nested constructors. We call such a term a struct term with depth k. For example, cons(a, cons(a, cons(a, nil))) has depth 3. A non-inductive sort is called finite.

2.2 Politeness

Given two theories T1 and T2, polite theory combination requires that T1 and T2 agree on the cardinality of their respective models, and also there must be an agreement between T1 and T2 on the interpretation of formulas built over the equality symbol. The following definition will be useful.

Definition 1 (Arrangement). Let V be a finite set of variables whose sorts are in S and {Vσ | σ ∈ S} a partition of V such that Vσ is the set of variables of sort σ in V . We say that a formula δ is an arrangement of V if δ = ∧σ∈S (∧(x,y)∈Eσ (x = y) ∧ ∧(x,y)/∈Eσ (x ̸= y)), where Eσ is some equivalence relation over Vσ for each σ ∈ S.

Definition 2 (Smoothness). Let Σ be a signature, S a subset of sorts in Σ, and T a Σ-theory. T is smooth w.r.t. S if for every quantifier-free formula φ, T -interpretation A |= φ, and function κ from S to the class of cardinals such that κ(σ) ≥

∣∣σA∣∣ for every σ ∈ S, there exists a Σ-interpretation A′ that satisfies φ with ∣∣∣σA′ ∣∣∣ = κ(σ) for every σ ∈ S.

Let φ be a quantifier-free (QF) Σ-formula. We say that a function wtn : QF(Σ) → QF(Σ) is a strong witness for T w.r.t. S if for every φ ∈ QF(Σ) we have that:

1. φ and ∃ -→w. wtn(φ) are T-equivalent for -→w = vars (wtn(φ)) \ vars (φ); and
2. if wtn(φ) ∧ δV is T-satisfiable, for an arrangement δV , where V is a set of variables whose sorts are in S, then there exists a T -interpretation A satisfying wtn(φ) ∧ δV such that σA = varsσ(wtn(φ) ∧ δV )A, for all σ ∈ S. We also say Γ = wtn(φ) ∧ δV is finitely witnessed for T w.r.t. S and A is a finite witness of Γ for T w.r.t. S.

Correspondingly, the definition of a witness for T w.r.t. S is obtained by dismissing V and δV , and then replacing every occurrence of wtn(φ) ∧ δV with wtn(φ).

Definition 3 (Finitely Witnessable). The theory T is (strongly) finitely witnessable w.r.t. S if there exists a (strong) witness for T w.r.t. S which is computable.

Definition 4 (Polite). T is called (strongly) polite w.r.t. S if it is smooth and (strongly) finitely witnessable w.r.t. S.

3 AdditiveWitnesses

It was shown in [Jovanovic and Barrett, 2010] that politeness is not sufficient for the proof of the polite combination method from [Ranise et al., 2005]. Strong politeness was introduced to fix the problem. In this section we offer a simple (yet useful) criterion for the equivalence of the two notions. Let Σ and S denote an arbitrary signature and a subset of its sorts, and let T denote an arbitrary Σ-theory.

Definition 5 (Additivity). Let f : QF(Σ) → QF(Σ). We say that f is S-additive for T if f(f(φ) ∧ ϕ) and f(φ) ∧ ϕ are T -equivalent and have the same set of S-sorted variables for every φ, ϕ ∈ QF(Σ), provided that ϕ is a conjunction of flat literals such that every term in ϕ is a variable whose sort is in S. When T is clear from the context, we say that f is S-additive.

We show that additive witnesses are strong:

Proposition 1. Let wtn be a witness for T w.r.t. S. If wtn is S-additive then it is a strong witness for T w.r.t. S.

The concept of additive witnesses will be useful in the following section, where we define a witness and instead of proving that it is a strong witness, we only need to prove that it is additive.

4 Politeness for the SMT-LIB 2 Theory of Datatypes

Let Σ be a datatypes signature with SΣ = Elem ⊎ Struct and FΣ = CO ⊎ SE. In this section, we prove that TΣ is strongly polite with respect to Elem. In Section 4.1, we consider theories with only inductive sorts; we consider theories with only finite sorts in Section 4.2. We combine them in Section 4.3, where arbitrary theories of datatypes are considered. For smoothness, however, it is straightforward to show that the Elem domain of a given interpretation can always be augmented without changing satisfiability of quantifier-free formulas, for both finite and inductive sorts.

Lemma 1. TΣ is smooth w.r.t. Elem.

4.1 Inductive Datatypes

In this section, we assume that all sorts in Struct are inductive. To prove finite witnessability, we now introduce an additive witness function. Following arguments from [Ranise et al., 2005], it suffices to define the witness only for conjunctions of flat literals. Similarly, it suffices to show a function wtni(φ) that is finitely witnessed for φ which is a conjunction of flat literals. Essentially, our witness guesses possible constructors for variables whose constructors are not explicit in the input formula.

Definition 6 (A Witness for TΣ). Let φ be a quantifier-free conjunction of flat Σ-literals. wtni (φ) is obtained from φ by performing the following steps:

1. For any literal of the form y = sc,i(x) such that x = c(-→ u1, y, -→ u2) does not occur in φ and x = d(-→ ud) does not occur in φ for any -→ u1, -→ u2, -→ ud, we conjunctively add x = c(-→ u1, y, -→ u2) ∨ (∨d̸=c x = d(-→ ud)) with fresh -→ u1, -→ u2, -→ ud, where c and d range over CO.
2. For any literal of the form isc(x) such that x = c(-→u ) does not occur in φ for any -→u , we conjunctively add x = c(-→u ) with fresh -→u .
3. For any literal of the form ¬isc(x) such that x = d(-→ ud) does not occur in φ for any d ̸= c and -→ ud, we conjunctively add ∨d̸=c x = d(-→ ud), with fresh -→ ud.
4. For any sort σ ∈ Elem such that φ does not include a variable of sort σ we conjunctively add a literal x = x for a fresh variable x of sort σ.

The requirement for absence of literals before adding literals or disjunctions to φ is used to ensure additivity of wtni . And indeed:

Lemma 2. wtni is Elem-additive.

Further, it can be verified that:

Lemma 3. Let φ be a conjunction of flat literals. φ and ∃-→w .Γ are TΣ-equivalent, where Γ = wtni (φ) and -→w = vars (Γ) \ vars (φ).

The remainder of this section is dedicated to the proof of the following lemma:

Lemma 4 (Finite Witnessability). Let φ be a conjunction of flat literals. Then, Γ = wtni(φ) is finitely witnessed for TΣ with respect to Elem.

Suppose that Γ is TΣ-satisfiable, and let A be a satisfying TΣ-interpretation. We define a TΣ-interpretation B as follows, and then show that B is a finite witness of Γ for TΣ w.r.t. Elem. First, for every σ ∈ Elem, we set σB = varsσ(Γ)A, and for every variable e ∈ varsσ(Γ), we set eB = eA. The interpretations of Struct-sorts, testers, and constructors are uniquely determined by the theory. It is left to define the interpretation of Struct-variables in B, as well as the interpretation of the selectors (the interpretation of selectors is fixed by the theory only when applied to the "right" constructor). We do this in several steps:

Step 1 - Simplifying Γ: since φ is a conjunction of flat literals, Γ is a conjunction whose conjuncts are either flat literals or disjunctions of flat literals (introduced in Items 1 and 3 of Definition 6). Since A |= Γ, A satisfies exactly one disjunct of each such disjunction. We can thus obtain a formula Γ1 from Γ by replacing every disjunction with the disjunct that is satisfied by A. Notice that A |= Γ1 and that it is a conjunction of flat literals. Let Γ2 be obtained from Γ1 by removing any literal of the form isc(x) and any literal of the form ¬isc(x). Let Γ3 be obtained from Γ2 by removing any literal of the form x = sc,i(y). For convenience, we denote Γ3 by Γ′ . Obviously, A |= Γ′ , and Γ′ is a conjunction of flat literals without selectors and testers.

Step 2 - Working with Equivalence Classes: We would like to preserve equalities between Struct-variables from A. To this end, we group all variables in vars(Γ) into equivalence classes according to their interpretation in A. Let ≡A denote an equivalence relation over vars(Γ) such that x ≡A y iff xA = yA. We denote by [x] the equivalence class of x. Let α be an equivalence class; then, αA = {xA | x ∈ α} is a singleton. Identifying this singleton with its only element, we have that αA denotes aA for an arbitrary element a of the equivalence class α.

Step 3 - Ordering Equivalence Classes: We would also like to preserve disequalities between Struct-variables from A. Thus, we introduce a relation ≺ over the equivalence classes, such that α ≺ β if y = c(w1, . . . ,wn) occurs as one of the conjuncts in Γ′ for some w1, . . . ,wn, y ∈ β, wk ∈ α and c ∈ CO. Call an equivalence class α nullary if A |= isc(x) for some x ∈ α and nullary constructor c. Call an equivalence class α minimal if β ̸≺ α for every β. Notice that each nullary equivalence class is minimal. The relation ≺ induces a directed acyclic graph (DAG), denoted G. The vertices are the equivalence classes. Whenever α ≺ β, we draw an edge from vertex α to β.

Step 4 - Interpretation of Equivalence Classes: We define αB for every equivalence class α. Then, xB is simply defined as [x]B , for every Struct-variable x. Let m be the number of equivalence classes, l the number of minimal equivalence classes, r the number of nullary equivalence classes, and α1, . . . , αm a topological sort of G, such that all minimal classes occur before all others, and the first r classes are nullary. Let d be the length of the longest path in G. We define αB i by induction on i.

1. If 0 < r and i ≤ r then αi is a nullary class and so we set αB i = αA i .
2. If r < i ≤ l then αi is minimal and not nullary. Let σ be the sort of variables in αi. If σ ∈ Elem, then all variables in the class have already been defined. Otherwise, σ ∈ Struct. In this case, we define αB i to be the interpretation of an arbitrary struct term with depth strictly greater than max {depth(αB j ) | 0 < j < i} + d (here max ∅ = 0).
3. If i > l then we set αB i = c(βB 1 , . . . , β B n ) for the unique equivalence classes β1, . . . , βn ⊆ {α1, . . . , αi-1} and

c such that y = c(x1, . . . , xn) occurs in Γ′ for some y ∈ αi and x1 ∈ β1, . . . , xn ∈ βn.

Since Σ is a datatypes signature in which all Struct-sorts are inductive, the second case of the definition is well-defined. Further, the topological sort ensures β1, . . . , βn exist, and the partition into equivalence classes ensures that they are unique.

Step 5 - Interpretation of Selectors: Let sc,i ∈ SE for c : σ1×. . .×σn → σ, 1 ≤ i ≤ n and a ∈ σB . If a ∈ isBc , we must have a = c(a1, . . . , an) for some a1 ∈ σB 1 , . . . , an ∈ σB n . We then set sBc,i (a) = ai. Otherwise, we consider two cases. If xB = a for some x ∈ vars (Γ) such that y = sc,i(x) occurs in Γ2 for some y, we set sBc,i (a) = yB . Otherwise, sBc,i (a) is set arbitrarily.

Now that B is defined, it is left to show that it is a finite witness of Γ for TΣ w.r.t. Elem. By construction, σB = varsσ(Γ)B for every σ ∈ Elem. B also preserves the equalities and disequalities in A, and by considering every shape of a literal in Γ′ we can prove that B |= Γ′ . Our interpretation of the selectors then ensures that:

Lemma 5. B |= Γ.

Lemma 5, together with the definition of the domains of B, gives us that B is a finite witness of Γ for TΣ w.r.t. Elem, and so Lemma 4 is proven. As a corollary of Lemmas 1, 2 and 4, strong politeness is obtained.

Theorem 1. If Σ is a datatypes signature and all sorts in StructΣ are inductive, then TΣ is strongly polite w.r.t. ElemΣ.

4.2 Finite Datatypes

In this section, we assume that all sorts in Struct are finite. For finite witnessability, we define the following witness, that guesses the construction of each Struct-variables until a fixpoint is reached. For every quantifier-free conjunction of flat Σ-literals φ, define the sequence φ0, φ1, . . ., such that φ0 = φ, and for every i ≥ 0, φi+1 is obtained from φi by conjoining it with a disjunction ∨c∈CO x = c(wc1 , . . . , wcnc ) for fresh wc1 , . . . ,wcnc , where x is some arbitrary Structvariable in φi such that there is no literal of the form x = c(y1, . . . , yn) in φi for any constructor c and variables y1, . . . , yn, if such x exists. Since Struct only has finite sorts, this sequence becomes constant at some φk.

Definition 7 (AWitness for TΣ). wtnf (φ) is φk for the minimal k such that φk = φk+1.

As in Section 4.1, we have that wtnf is a strong witness for TΣ w.r.t. Elem and hence:

Theorem 2. If Σ is a datatypes signature and all sorts in StructΣ are finite, then TΣ is strongly polite w.r.t. ElemΣ.

4.3 Combining Finite and Inductive Datatypes

For the general case, let Σ be a datatypes signature. We prove that TΣ is strongly polite w.r.t. Elem by showing that there are datatype signatures Σ1,Σ2 ⊆ Σ such that TΣ = TΣ1 ⊕ TΣ2 , and then using Theorem 1 from [Jovanovic and Barrett, 2010] about the preservation of politeness when combining polite theories.

Theorem 3. If Σ is a datatypes signature then TΣ is strongly polite w.r.t. ElemΣ.

5 Axiomatizations

In this section, we show how to reduce any TΣ-satisfiability problem to a satisfiability problem modulo an axiomatized theory of trees. The latter can be decided using syntactic unification [Baader et al., 2001].

Let Σ be a datatypes signature. The set TREE ∗Σ of axioms contains all the axioms as follows for c, d ∈ CO, c ̸= d: (where free variables are implicitly universally quantified, t is a non-variable term containing x that is selector-free, and σ ∈ Struct).

Let TREEΣ be the set obtained from TREE ∗Σ by dismissing Ext1 and Ext2. TREEΣ is a generalization of the theory of Absolutely Free Data Structures (AFDS) from [Chocron et al., 2020] to many-sorted signatures with selectors and testers. In what follows we identify TREEΣ (and TREE ∗Σ) with the class of structures that satisfy them when there is no ambiguity.

Proposition 2. Every TREE ∗Σ-unsatisfiable formula is TΣunsatisfiable.

The following result shows that any TΣ-satisfiability problem can be reduced to a TREEΣ-satisfiability problem. This leads to a TΣ-satisfiability procedure.

Proposition 3. Let Σbe a finite datatype signature and ϕ any conjunction of flat Σ-literals including an arrangement over the variables in ϕ. Then, there exists a Σ-formula ϕ′ such that:

1. ϕ and ∃-→w . ϕ′ are TΣ-equivalent, where -→w = vars (ϕ′ )\vars (ϕ).

1. ϕ′ is TΣ-satisfiable iff ϕ′ is TREEΣ-satisfiable.

Proposition 3 can be easily lifted to any conjunction of Σ-literals ϕ by flattening and then guessing all possible arrangements over the variables. Further, ∃-→w . ϕ′ and ϕ are not only TΣ-equivalent but also TREE ∗Σ-equivalent. As a consequence, Proposition 3 also holds when stated using TREE ∗Σ instead of TΣ.

6 Conclusion

In this paper, we have studied the theory of algebraic datatypes, as it is defined by the SMT-LIB 2 standard. Our investigation included both finite and inductive datatypes. We have proved that this theory is strongly polite, making it amenable for combination with other theories using the polite combination method. Our proofs used the notion of additive witnesses, also introduced in this paper. We concluded by extending existing axiomatizations to support this theory of datatypes.