**Algorithm 3.** OMT-REDUCE-ASSIGNMENT-GUIDED ($\varphi, \eta, \text{cost}$)

**Input:** Formula $\varphi$, $\mathcal{T}$-satisfiable total truth assignment $\eta$ satisfying $\varphi$, objective cost

**Output:** Reduced truth assignment $\mu \subseteq \eta$ satisfying $\varphi$

1: $\mu \leftarrow \eta$

2: $\mathcal{M} \leftarrow \text{T-Solver.MinimizeApprox}(\mu, \text{cost})$

3: $\ell \leftarrow \text{T-Solver.ProposeLiteralToDrop}()$

4: **while** $\ell \neq \perp$ **do**

5: &nbsp;&nbsp;&nbsp;&nbsp;**if** $\mu \setminus \{\ell\}$ satisfies all clauses in $\varphi$ **then**

6: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;$\mu \leftarrow \mu \setminus \{\ell\}$

7: &nbsp;&nbsp;&nbsp;&nbsp;$\mathcal{M} \leftarrow \text{T-Solver.MinimizeApprox}(\mu, \text{cost})$

8: &nbsp;&nbsp;&nbsp;&nbsp;$\ell \leftarrow \text{T-Solver.ProposeLiteralToDrop}()$

9: **return** $\mu$

## 4.2 Guided Assignment Reduction

We propose an ad-hoc assignment-reduction technique for OMT solving, which is outlined in Algorithm 3. Suppose that, after the $\mathcal{T}$-minimizer has found a minimum model within the current truth assignment $\mu$ (line 2), it returns also one (or more) literal(s) that limit the current minimum (line 3). These literals are part of some (possibly minimal) $\mu' \subseteq \mu$ such that $\mu' \cup \{\text{cost} < \mathcal{M}(\text{cost})\}$ is $\mathcal{T}$-unsatisfiable. Intuitively, the removal of any literal $\ell \in \mu'$ is very likely to lead to a better optimum model, provided that $\mu \setminus \{\ell\}$ still propositionally satisfies $\varphi$ (line 5).

We can then iteratively drop these literals and re-run the $\mathcal{T}$-minimizer, until no more literals can be dropped (lines 4–8). Notice that instead of **T-Solver.Minimize**, here we call **T-Solver.MinimizeApprox**, suggesting that also a relaxed optimization algorithm could be used. In the next paragraph, we describe how this can be exploited for *LIRA*.

Notice that, in Algorithm 3, we only drop one literal before every optimization call; nevertheless, in principle, more literals could be dropped. Experimentally, we found that dropping more than one literal was not beneficial. The reason is that, generally, when a literal is removed, most of the other literals in $\mu'$ do not limit the current minimum anymore. Hence, their removal not only does not lead to a better optimum model, but also can prevent the removal of other more-relevant literals.

*On Proposing Literals to Drop.* For an arbitrary theory $\mathcal{T}$, a generic implementation for **T-Solver.ProposeLiteralToDrop** (Algorithm 3, lines 3, 8) could be as follows. Once a minimum model $\mathcal{M}$ for $\mu$ is found, invoke the $\mathcal{T}$-solver on $\mu \land (\text{cost} < \mathcal{M}(\text{cost}))$ and return a (possibly-minimal) conflict set. For some theories, ad-hoc (possibly heuristic) procedures can be employed. We describe two such techniques for *LIRA* and *LIRA*.

As we recalled in Sect. 2.2, a *LIRA*-minimizer can be implemented as a variant of the Simplex method [11,31], by which an optimum model is always found on a vertex of the polytope defined by the conjunction of *LIRA*-constraints on which it is invoked. Thus, in this case, the candidate constraints to be dropped are those that form such a vertex. This information can be easily obtained from the Simplex tableau [11].

For *LIRA*, directly using a *LIRA*-minimizer and then identifying the limiting constraints presents some challenges: (a) a single call to the branch-and-bound-based
$\mathcal{LIRA}$-minimizer is worst-case exponential, hence calling it multiple times (as in Algorithm 3) is not feasible; (b) extracting the limiting constraints from a $\mathcal{LIRA}$-minimizer is not straightforward. We thus propose proceeding as follows. First, for the procedure T-Solver.MinimizeApprox a $\mathcal{LIRA}$-minimizer is invoked on the relaxation of $\mu$. Then, the procedure T-Solver.ProposeLiteralToDrop can be implemented as for $\mathcal{LIRA}$. The intuition here is that reasoning on the relaxation of $\mu$ is much easier and cheaper— especially if incremental calls are used—and still allows for enlarging the search area in a favourable direction for the $\mathcal{LIRA}$-minimizer. We remark that, after the assignment reduction, in Algorithm 2 (line 8), the complete $\mathcal{LIRA}$-minimizer is called.

As a last aspect, we suggest that, if the *T*-minimizer is able to find an optimum model $\mu$, then we can use these limiting literals $l_1, \dots, l_n$ also to learn a theory lemma ($\neg(\text{cost} < \text{ub}) \lor \neg l_1 \lor \dots \lor \neg l_n$) that blocks truth assignments that we know are not better than the current upper bound *ub*—thus preventing useless calls to the *T*-solver. The idea is that, in order to find a model with cost < *ub*, we need to assign at least one of these literals to false. This is the case of $\mathcal{LIRA}$, but not of $\mathcal{LIRA}$ if the truncated minimization method is used (see Sect. 2.2).

# 5 Experimental Evaluation

We implemented the above algorithms in the OMT solver OPTIMATHSAT [34], which is built on top of the MATHSAT5 SMT solver [9]. We evaluated the proposed strategies on a set of OMT($\mathcal{LIRA}$), OMT($\mathcal{LIRA}$), and OMT($\mathcal{LIRA} \cup AR$) benchmarks coming from different sources, evaluating both solving time for optimum solving, and the quality of the solutions found within the given timeout for anytime solving. All the experiments were run on an Intel Xeon Gold 6238R @ 2.20GHz 28 Core machine with 128 GB of RAM, running Ubuntu Linux 22.04. The timeout was set at 1200 s. The tool, benchmarks and results are available at https://optimathsat.disi.unitn.it/resources/optimathsat-partial-assignments.tar.gz.

## 5.1 Benchmarks

We evaluated the proposed strategies on two classes of OMT($\mathcal{LIRA}$) benchmarks: OMT-encoded optimal temporal planning [26,27] and strip-packing problems [31, 32]. We also modified the strip-packing benchmarks to use OMT($\mathcal{LIRA}$) and OMT($\mathcal{LIRA} \cup AR$) encodings, to evaluate the effectiveness of our strategies in these theories.

*Optimal Temporal Planning.* In [26,27], the authors proposed a way to encode optimal temporal planning problems into a sequence of OMT($\mathcal{LIRA}$) problems. Each problem encodes a bounded version of the problem up to a fixed horizon, with additional abstract actions representing an over-approximation of the plans beyond the bound, minimizing the makespan, i.e., the total time taken to reach the goal. If the optimal plan is found without using the abstract actions, then the plan is optimum for the original problem. Otherwise, the horizon is increased, and the process is repeated. We generated problems using the industrial problems Majsp (80 instances), MajspSimplified (80 instances), and Painter (30 instances) [27], with increasing horizon $h \in \{5, 10, 15, 20, 25, 30, 35, 40\}$, for a total of 1520 instances.
**Strip-Packing.** The strip-packing problem (SP) requires arranging *N* rectangles with widths $W_i$ and heights $H_i$ into a strip of fixed height *H* and unlimited length. The goal is to minimize the length of the used part of the strip, ensuring all rectangles are placed without overlap or rotation. An OMT($LRA$) encoding for SP was proposed in [32]. Following [32], we sampled $H_i$ uniformly in (0, 1], $W_i$ in (1, 2], and set $H = \sqrt{N}/2$.

We also generated OMT($LRA$) SP problems, by randomly choosing with equal probability whether encoding the coordinates of each rectangle with integer or rational variables. Finally, we generated OMT($LRA \cup AR$) encodings for SP, by simply replacing the variables $x_i$ in the OMT($LRA$) encoding with a $LRA \cup AR$ term $read(x, i + offset)$, where *x* is an array mapping from rationals to rationals, *i* is a constant indicating the index of the rectangle, and *offset* is a fresh rational variable.

For each of these encodings, we generated 25 random SP problems for each value of $N \in \{25, 50, 75, 100\}$, for a total of 100 instances per encoding.

## 5.2 Results

Figures 2, 3, 4 and 5 show the results on temporal planning and SP benchmarks for the different theories, respectively. For each benchmark set, we report a set of scatter plots.

On the rows, we have different metrics, namely the solving time in seconds (time(s)), the upper bound (u.b.)—i.e., the optimum value when the solver terminated within the time limit, or the value of the best solution found within the timeout otherwise—and the number of iterations (# iter) taken to reach the upper bound (see Algorithm 2).

On the columns, we compare the results obtained with the different truth-assignment-reduction strategies: in the left and center columns, we respectively compare the basic and the guided reductions with the plain algorithm without reductions. In the right column, we compare the two reduction strategies.

**OMT(LRA) Benchmarks.** The results are summarized in Figs. 2 and 3.

*Optimal Temporal Planning (Fig. 2).* In these benchmarks, with no truth-assignment reduction, OPTIMATHSAT reported 246 timeouts out of 1520 problems, 211 with the basic reduction, and 212 with the guided reduction.

From the plots (first row, left and center columns), we can see that applying either reduction almost uniformly improves the solving time with few exceptions, making optimal solving up to twice as fast as with no reduction.

Moreover, we observe that reducing truth assignments is very effective also for anytime solving (second row, left and center columns). Notice that when the solver terminated within the timeout with both strategies, then the corresponding points lie on the bisector, whereas when at least one strategy times out, the points are generally below the bisector. Indeed, this shows that, for anytime solving, both the basic and the guided reductions allow finding a much better upper bound than with no reduction.

Finally, we can see that both strategies are particularly effective in reducing the number of iterations needed to either find the optimum or to reach the best upper bound within the timeout (third row, left and center). Reducing the number of iterations is not
<figure><img src="image_28.png" /><figcaption>Fig. 2. Results on OMT(LRA)-encoded optimal temporal planning problems.</figcaption></figure>

an advantage in itself, but it is a good indicator of the effectiveness of truth-assignment reduction strategies in OMT.

Overall, in these benchmarks there is no clear winner between the two reduction strategies (right column), but it is evident that applying either form of truth-assignment reduction can be beneficial in OMT, both for optimal and anytime solving.

Strip-Packing (Fig. 3). Since no instance in this set of benchmarks terminated within the timeout, for these benchmarks we omit the time plots. We can see that here the basic reduction strategy is not really effective, since the value of the upper bound is not improved compared to the no-reduction strategy (first row, left column). Also, the number of iterations only slightly decreases (second row, left column), suggesting that here blindly removing atoms from the truth assignment does not help much in finding
<figure><img src="image_29.png" /><figcaption>Fig. 3. Results on OMT(LRA)-encoded strip-packing problems.</figcaption></figure>

<figure><img src="image_30.png" /><figcaption>Fig. 4. Results on OMT(LIRA)-encoded strip-packing problems.</figcaption></figure>
<figure><img src="image_31.png" /><figcaption>Fig. 5. Results on OMT($LRA \cup AR$)-encoded strip-packing problems.</figcaption></figure>

better solutions. On the other hand, the guided reduction strategy is much more effective, since it allows finding a much better upper bound within the timeout (first row, center and right columns), and the number of iterations is drastically reduced (second row, center and right columns).

**OMT($LIRA$) Benchmarks.** The results are summarized in Fig. 4.

*Strip-Packing* (Fig. 4). The plots show that also for $LIRA$, the trend is similar to the one for $LRA$. In fact, the basic reduction strategy is not very effective for improving the upper bound (first row, left column), and the number of iterations is only slightly reduced (second row, left column). On the other hand, the guided reduction allows finding a much better upper bound within the timeout (first row, center and right columns). Notice that, since these problems are much harder than the OMT($LRA$) ones, the number of iterations completed within the timeout is much smaller, so that the upper bounds found are also bigger.

**OMT($LRA \cup AR$) Benchmarks.** The results are summarized in Fig. 5.

*Strip-Packing* (Fig. 5). Similarly, here we can see that the technique works also for combination of theories, such as $LRA \cup AR$. The results are similar to the ones for $LRA$, and the advantage of the guided reduction is even more evident.

**Discussion.** The results show that applying either form of truth-assignment reduction can be beneficial in OMT, both for optimal and anytime solving, and that accurately
selecting which atoms to remove from the truth assignment can make a significant difference in finding better solutions in fewer iterations.

We observe, however, that a much smaller number of iterations, i.e. of truth assignments enumerated, not always correlates linearly with the solving time. This can be due to several reasons.

First, we remark that global efficiency of OMT depends on several factors, including the enumeration order of truth assignments, and different literal selections may alter this order. Also, the removal of some literals from the assignments can prevent the removal of others in subsequent iterations. The effects of these factors are quite unpredictable.

Second, we notice that in these problems, the number of truth assignments enumerated is typically contained to a few hundred. In fact, in OMT the bounds on the objective function already allow performing a very effective pruning of the search space.

Moreover, this pruning is typically done by theory reasoning, and most of it has to be done anyway, regardless of the number of truth assignments enumerated. Making it in a single iteration or in many iterations may not reflect as much on the solving time, because of the efficient incrementality of SMT solvers, which can reduce a lot the cost of consecutive iterations.

# 6 Conclusions and Future Work

In this paper, we have investigated the role of truth assignment enumeration in OMT solving, and proposed some ways for exploiting partial truth assignments for improving the efficiency and effectiveness of the search. In particular, we have proposed a truth assignment reduction strategy that takes advantage of the properties of the optimization problem to accurately choose the atoms to remove from the truth assignment.

We have implemented the proposed strategies in the OPTIMATHSAT solver, and evaluated them on a set of OMT(LRA), OMT(LIRA), and OMT(LRA ∪ AR) benchmarks. Our experimental results show that the proposed strategies can significantly improve the performance of the solver, uniformly reducing the overall solving time for optimal solving, and finding much better solutions for anytime solving for all the analyzed theories.

Other truth assignment reduction strategies, such as entailment-based methods [12], have shown significant benefits for SAT enumeration. Their extension to OMT problems could be a promising direction for future work.

**Acknowledgements.** RS was partially supported by the project "AI@TN" funded by the Autonomous Province of Trento. RS was partially supported by the MUR PNRR project FAIR - Future AI Research (PE00000013) funded by the NextGenerationEU. RS was partially funded under the NRRP, Mission 4 Component 2 Investment 1.4, by the European Union—NextGenerationEU (proj. nr. CN 00000013). RS was supported in part by the TANGO project funded by the EU Horizon Europe research and innovation program under GA No 101120763, funded by the European Union. Views and opinions expressed are however those of the author(s) only and do not necessarily reflect those of the European Union, the European Health and Digital Executive Agency (HaDEA) or The European Research Council. Neither the European Union nor the granting authority can be held responsible for them.
References

1. Albert, E., Correas, J., Gordillo, P., Román-Díez, G., Rubio, A.: GASOL: gas analysis and optimization for Ethereum smart contracts. In: TACAS 2020. LNCS, vol. 12079, pp. 118–125. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-45237-7_7

2. Barrett, C., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Handbook of Satisfiability, FAIA, vol. 336, pp. 1267–1329, 2 edn. IOS Press (2021). https://doi.org/10.3233/FAIA201017

3. Bian, Z., Chudak, F., Macready, W., Roy, A., Sebastiani, R., Varotti, S.: Solving SAT (and MaxSAT) with a quantum annealer: foundations, encodings, and preliminary results. Inf. Comput. 275, 104609 (2020). https://doi.org/10.1016/j.ic.2020.104609

4. Bigarella, F., et al.: Optimization modulo non-linear arithmetic via incremental linearization. In: Konev, B., Reger, G. (eds.) FroCoS 2021. LNCS (LNAI), vol. 12941, pp. 213–231. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-86205-3_12

5. Bjørner, N., Phan, A.D.: $\nu$Z - maximal satisfaction with Z3. In: Proceedings of the International Symposium on Symbolic Computation in Software Science, pp. 1–9 (2014). https://doi.org/10.29007/jmxj

6. Bjørner, N., Phan, A.-D., Fleckenstein, L.: $\nu$Z - an optimizing SMT solver. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 194–199. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46681-0_14

7. Bofill, M., Coll, J., Suy, J., Villaret, M.: An efficient SMT approach to solve MRCPSP/max instances with tight constraints on resources. In: Beck, J.C. (ed.) CP 2017. LNCS, vol. 10416, pp. 71–79. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66158-2_5

8. Bozzano, M., et al.: Efficient Theory Combination via Boolean Search. Inf. Comput. 204(10), 1493–1525 (2006). https://doi.org/10.1016/j.ic.2005.05.011

9. Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The MathSAT5 SMT solver. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 93–107. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-36742-7_7

10. Ding, J., Spallitta, G., Sebastiani, R.: Effective prime factorization via quantum annealing by modular locally-structured embedding. Sci. Rep. 14(1), 3518 (2024). https://doi.org/10.1038/s41598-024-53708-7

11. Dutertre, B., de Moura, L.: A fast linear-arithmetic solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 81–94. Springer, Heidelberg (2006). https://doi.org/10.1007/11817963_11

12. Fried, D., Nadel, A., Sebastiani, R., Shalmon, Y.: Entailing generalization boosts enumeration. In: SAT 2024. LIPIcs, vol. 305, pp. 13:1–13:14. LZI (2024). https://doi.org/10.4230/LIPIcs.SAT.2024.13

13. Fried, D., Nadel, A., Shalmon, Y.: AllSAT for combinational circuits. In: SAT 2023. LIPIcs, vol. 271, pp. 9:1–9:18. LZI (2023). https://doi.org/10.4230/LIPIcs.SAT.2023.9

14. Henry, J., Asavoae, M., Monniaux, D., Maïza, C.: How to compute worst-case execution time by optimization modulo theory and a clever encoding of program semantics. In: LCTES 2014, pp. 43–52. ACM (2014). https://doi.org/10.1145/2597809.2597817

15. Lahiri, S.K., Nieuwenhuis, R., Oliveras, A.: SMT techniques for fast predicate abstraction. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 424–437. Springer, Heidelberg (2006). https://doi.org/10.1007/11817963_39

16. Leofante, F., Giunchiglia, E., Ábrahám, E., Tacchella, A.: Optimal planning modulo theories. In: IJCAI 2020, vol. 4, pp. 4128–4134 (2020). https://doi.org/10.24963/ijcai.2020/571

17. Li, Y., Albarghouthi, A., Kincaid, Z., Gurfinkel, A., Chechik, M.: Symbolic optimization with SMT solvers. In: POPL 2014, pp. 607–618. ACM (2014). https://doi.org/10.1145/2535838.2535857
18. Ma, F., Yan, J., Zhang, J.: Solving generalized optimization problems subject to SMT constraints. In: Snoeyink, J., Lu, P., Su, K., Wang, L. (eds.) AAIM/FAW -2012. LNCS, vol. 7285, pp. 247–258. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-29700-7_23

19. Marques-Silva, J., Lynce, I., Malik, S.: Conflict-driven clause learning SAT solvers. In: Handbook of Satisfiability, FAIA, vol. 336. IOS Press (2021). https://doi.org/10.3233/FAIA200987

20. Masina, G., Spallitta, G., Sebastiani, R.: On CNF conversion for disjoint SAT enumeration. In: SAT 2023. LIPIcs, vol. 271, pp. 15:1–15:16. LZI (2023). https://doi.org/10.4230/LIPIcs.SAT.2023.15

21. Masina, G., Spallitta, G., Sebastiani, R.: On CNF conversion for SAT and SMT enumeration. J. Artif. Intell. Res. 83 (2025). https://doi.org/10.1613/jair.1.16870, to appear, preprint arXiv:2303.14971

22. Morgado, A., Marques-Silva, J.: Good learning and implicit model enumeration. In: ICTAI 2005, pp. 131–136. IEEE Computer Society (2005). https://doi.org/10.1109/ICTAI.2005.69

23. Nadel, A., Ryvchin, V.: Bit-vector optimization. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 851–867. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-49674-9_53

24. Nguyen, C.M., Sebastiani, R., Giorgini, P., Mylopoulos, J.: Multi-objective reasoning with constrained goal models. Requirements Eng. 23(2), 189–225 (2016). https://doi.org/10.1007/s00766-016-0263-5

25. Nieuwenhuis, R., Oliveras, A.: On SAT modulo theories and optimization problems. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 156–169. Springer, Heidelberg (2006). https://doi.org/10.1007/11814948_18

26. Panjkovic, S., Micheli, A.: Expressive optimal temporal planning via optimization modulo theory. In: AAAI 2023, vol. 37, no. 10, pp. 12095–12102 (2023). https://doi.org/10.1609/aaai.v37i10.26426

27. Panjkovic, S., Micheli, A.: Abstract action scheduling for optimal temporal planning via OMT. In: AAAI 2024, vol. 38, no. 18, pp. 20222–20229 (2024). https://doi.org/10.1609/aaai.v38i18.30002

28. Plaisted, D.A., Greenbaum, S.: A Structure-preserving clause form translation. J. Symb. Comput. 2(3), 293–304 (1986). https://doi.org/10.1016/S0747-7171(86)80028-1

29. Ravi, K., Somenzi, F.: Minimal assignments for bounded model checking. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 31–45. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24730-2_3

30. Sebastiani, R.: Lazy satisfiability modulo theories. JSAT 3(3–4), 141–224 (2007). https://doi.org/10.3233/SAT190034

31. Sebastiani, R., Tomasi, S.: Optimization in SMT with LA(Q) cost functions. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 484–498. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31365-3_38

32. Sebastiani, R., Tomasi, S.: Optimization modulo theories with linear rational costs. ACM Trans. Comput. Logic 16(2), 12:1–12:43 (2015). https://doi.org/10.1145/2699915

33. Sebastiani, R., Trentin, P.: Pushing the envelope of optimization modulo theories with linear- arithmetic cost functions. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 335–349. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46681-0_27

34. Sebastiani, R., Trentin, P.: OPTIMATHSAT: a tool for optimization modulo theories. J. Autom. Reason. 64(3), 423–460 (2018). https://doi.org/10.1007/s10817-018-09508-6

35. Spallitta, G., Sebastiani, R., Biere, A.: Disjoint partial enumeration without blocking clauses. In: AAAI 2024, vol. 38, pp. 8126–8135 (2024). https://doi.org/10.1609/aaai.v38i8.28652
36. Spallitta, G., Sebastiani, R., Biere, A.: Disjoint projected enumeration for SAT and SMT without blocking clauses. Artif. Intell. 345, 104346 (2025). https://doi.org/10.1016/j.artint.2025.104346

37. Teso, S., Sebastiani, R., Passerini, A.: Structured learning modulo theories. Artif. Intell. 244, 166–187 (2017). https://doi.org/10.1016/j.artint.2015.04.002

38. Toda, T., Soh, T.: Implementing efficient all solutions SAT solvers. ACM J. Exp. Algorithmics 21, 1–44 (2016). https://doi.org/10.1145/2975585

39. Trentin, P., Sebastiani, R.: Optimization modulo the theories of signed bit-vectors and floating-point numbers. J. Autom. Reason. 65(7), 1071–1096 (2021). https://doi.org/10.1007/s10817-021-09600-4

40. Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Siekmann, J.H., Wrightson, G. (eds.) Automation of Reasoning. Symbolic Computation, pp. 466–483. Springer, Heidelberg (1983). https://doi.org/10.1007/978-3-642-81955-1_28

41. Tsiskaridze, N., Barrett, C., Tinelli, C.: Generalized optimization modulo theories. In: Benzmüller, C., Heule, M.J., Schmidt, R.A. (eds.) IJCAR 2024. LNCS, vol. 14739, pp. 458–479. Springer, Cham (2024). https://doi.org/10.1007/978-3-031-63498-7_27

**Open Access** This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
# Shininess, Strong Politeness, and Unicorns

Benjamin Przybocki¹(✉), Guilherme V. Toledo², and Yoni Zohar²

1 University of Cambridge, Cambridge, UK
[benjamin.przybocki@gmail.com](mailto:benjamin.przybocki@gmail.com)

2 Bar-Ilan University, Ramat Gan, Israel

**Abstract.** Shininess and strong politeness are properties related to the theory combination procedures. In a paper titled "Many-sorted equivalence of shiny and strongly polite theories", Casal and Rasga proved that for decidable theories, these properties are equivalent. We refine their result by showing that: (i) shiny theories are always decidable, and therefore strongly polite; and (ii) there are (undecidable) strongly polite theories that are not shiny. This line of research is tightly related to a recent series of papers that have sought to classify all the relations between theory combination properties. We finally complete this project, resolving all of the remaining problems that were previously left open.

## 1 Introduction

In 2005, the shiny combination method was introduced [19], and was able to handle theories that were left out of the Nelson-Oppen method [11]. Unlike the Nelson-Oppen method, which requires both combined theories to be stably infinite, shiny combination requires a stronger property (*shininess*), but only from one of the theories. This allowed for theories that are not stably infinite, like the theory of bit-vectors [2], to be combined with other theories.

Shininess requires the ability to compute cardinalities of minimal models, which is computationally expensive. This was one of the reasons that led to the introduction of the polite combination method [15], replacing the computation of cardinalities by a computation of formulas called witnesses. The resulting property is called politeness. Later, in 2010, it was clarified that actually a stronger property is required for polite combination, called strong politeness [8]. While the definitions of shininess and strong politeness are different, in 2018, Casal and Rasga proved that they are equivalent for decidable theories [4].

In this paper, we investigate the equivalence between shininess and strong politeness, without assuming decidability. Our main result is that shiny theories are always strongly polite, while the converse does not hold. For the former, we show that shiny theories are always decidable, and then strong politeness follows. For the latter, we construct examples. Our examples are theories that are non-trivial, and build on a graph-theoretical interpretation of models.

We also study the relationship between strong politeness and additive politeness, a notion that was introduced in [16] to simplify strong politeness proofs,
and was shown to imply strong politeness. We prove that the converse does not hold in general, but it does hold in the absence of predicates (except equality).

Our results have several implications. First, they provide a deeper understanding of shininess and strong politeness. Second, since SMT solvers often deal with undecidable theories, combination methods for such theories can be useful for those cases in which the underlying solvers of both theories return a result. Third, our results entail that there are theories for which it is possible to compute witnesses but impossible to compute minimal models. This affirms the aforementioned motivation from [15] for the introduction of politeness, namely that the minimal model function is harder to compute in general than a witness.<fnref n="1" />

There is a completely different way to tell this story, leading to a fourth implication. The papers [21–23] analyzed connections between various properties, including (strong) politeness and shininess. For almost every combination of properties, they either found an example or proved that there are none. For three particular combinations, however, this was left open: Unicorn 1.0,<fnref n="2" /> Unicorn 2.0, and Unicorn 3.0 theories. In [14], it was proved that Unicorn 1.0 theories do not exist. Here, we prove that Unicorn 2.0 theories exist, while Unicorn 3.0 theories do not. We also resolve a related question from [14] regarding uncountable signatures. This closes all questions regarding unicorn theories, thus completing the project of analyzing the connections between theory combination properties.

The two narratives are inter-related: the nonexistence of Unicorn 3.0 theories directly follows from the implication from shininess to strong politeness; And every theory that is strongly polite but not shiny is a Unicorn 2.0 theory.

Figure 1a shows the connections between shininess, strong politeness and additive politeness. Blue connections are known, black are new. Figure 1b lists the results on unicorns, referring each problem to the section where it is solved.

To summarize: Sect. 3 proves that all shiny theories are decidable (and therefore strongly polite), and concludes that there are no Unicorn 3.0 theories. Section 4 constructs strongly polite theories that are not shiny. All of them are Unicorn 2.0 theories. Section 5 proves that strong politeness does not imply additive politeness, except over algebraic signatures. Section 6 solves a related problem from [14]. Section 7 concludes with directions for future work.<fnref n="3" />

# 2 Preliminaries

In what follows, $\mathbb{N}$ denotes the set of non-negative integers, $\mathbb{N}^+ = \mathbb{N} \setminus \{0\}$, $|X|$ is the cardinality of the set $X$, $\aleph_0 = |\mathbb{N}|$, and $\mathbb{N}_\omega = \mathbb{N} \cup \{\aleph_0\}$.

## 2.1 Many-Sorted Logic

A *signature* $\Sigma$ is a triple $(S_\Sigma, \mathcal{F}_\Sigma, \mathcal{P}_\Sigma)$ where $S_\Sigma$ is a non-empty set (of sorts), $\mathcal{F}_\Sigma$ is a set of function symbols, each equipped with an arity $\sigma_1 \times \dots \times \sigma_n \to \sigma$,

<footnote n="1">¹ The adoption of polite combination in cvc5 [1] provides an empirical affirmation.</footnote>

<footnote n="2">² In [14,21], these were simply called *Unicorn theories*. We rename them here to *Unicorn 1.0*, in order to be consistent with the other types of unicorns from [23].</footnote>

<footnote n="3">³ Some proofs are omitted and can be found in the arXiv version of this paper [13].</footnote>
<figure><img src="image_32.png" /><figcaption>Fig. 1. A summary of the contributions of this paper.</figcaption></figure>

for $\sigma_1, \dots, \sigma_n, \sigma \in S_\Sigma$, and $\mathcal{P}_\Sigma$ is a set of predicate symbols, each with an arity $\sigma_1 \times \dots \times \sigma_n$, for $\sigma_1, \dots, \sigma_n \in S_\Sigma$, that includes the equality symbol $=_{\sigma}$ of arity $\sigma \times \sigma$, for every $\sigma \in S_\Sigma$, usually denoted simply as $=$. A signature is called empty if it contains no function and predicate symbols other than the equalities. The cardinality of a signature is the cardinality of $S_\Sigma \cup \mathcal{F}_\Sigma \cup \mathcal{P}_\Sigma$.

We define terms, formulas, literals, clauses (disjunctions of literals), and sentences in the usual way; the set of free variables of sort $\sigma$ in $\varphi$ is denoted by $\text{vars}_\sigma(\varphi)$, the set of free variables whose sort $\sigma$ lies in $S \subseteq S_\Sigma$ is denoted by $\text{vars}_S(\varphi)$, and the set of all of its variables is simply $\text{vars}(\varphi)$. If $s$ is a function symbol of arity $\sigma \to \sigma$ and $x$ a variable of sort $\sigma$, we define recursively the terms $s^0(x) = x$ and $s^{n+1}(x) = s(s^n(x))$. A Horn clause is a formula of the form $\forall x_1, \dots, x_n. \varphi$ such that $\varphi$ is quantifier-free and has the form $\ell_1 \vee \dots \vee \ell_m$ for literals $\ell_1, \dots, \ell_m$, such that there is at most one $1 \le i \le m$ such that $\ell_i$ is an atomic formula (and all the other $\ell_i$s are negations of atomic formulas).

A $\Sigma$-structure $\mathcal{A}$ maps: each $\sigma \in \mathcal{A}$ to a non-empty set $\sigma^A$, called the domain of $\sigma$ in $\mathcal{A}$; each $f \in \mathcal{F}_\Sigma$ to a function $f^A: \sigma_1^A \times \dots \times \sigma_n^A \to \sigma^A$, where $\sigma_1 \times \dots \times \sigma_n \to \sigma$ is the arity of $f$; and each predicate $P \in \mathcal{P}_\Sigma$ to a subset $P^A$ of $\sigma_1^A \times \dots \times \sigma_n^A$, where $\sigma_1 \times \dots \times \sigma_n$ is the arity of $P$. A $\Sigma$-interpretation $\mathcal{A}$ is a $\Sigma$-structure further equipped with a mapping of variables $x$ to elements $x^A$, such that if $x$ has sort $\sigma$, then $x^A \in \sigma^A$. The value $\tau^A$ of a term $\tau$ is defined as usual. If $\Gamma$ is a set of terms, $\Gamma^A = \{\tau^A : \tau \in \Gamma\}$. Satisfaction is defined as usual, and denoted $\models$. Formulas we will make use of are given in Fig. 2, and an interpretation $\mathcal{A}$ that satisfies $\psi_{\ge n}^\sigma$ (or $\ne^\sigma$ $(x_1, \dots, x_n)$), $\psi_{\le n}^\sigma$ or $\psi_{=n}^\sigma$ has, respectively, at least, at most, or exactly $n$ elements in $\sigma^A$. When $S_\Sigma = \{\sigma\}$, we omit $\sigma$ from these formulas.

$$ \not\models^{\sigma} (x_1, \dots, x_n) = \bigwedge_{i=1}^{n-1} \bigwedge_{j=i+1}^{n} \neg(x_i = x_j) \qquad \psi_{\ge n}^{\sigma} = \exists x_1, \dots, x_n. \not\models^{\sigma} (x_1, \dots, x_n) $$

$$ \psi_{\le n}^{\sigma} = \exists x_1, \dots, x_n. \forall y. \bigvee_{i=1}^{n} y = x_i \qquad \psi_{=n}^{\sigma} = \psi_{\ge n}^{\sigma} \wedge \psi_{\le n}^{\sigma} $$

<caption>Fig. 2. Cardinality formulas, all variables are of sort $\sigma$.</caption>
A Σ-theory T is the class of all Σ-interpretations that satisfy a set of sentences Ax(T) called the axiomatization of T. We call them T-interpretations. A formula satisfied by a T-interpretation is said to be T-satisfiable (or simply satisfiable if T includes all Σ-interpretations), and if φ is satisfied by all T-interpretations it is said to be T-valid, and we write φ ⊨<T> φ. Two formulas are said to be T-equivalent if they are satisfied by precisely the same T-interpretations. A standard result that we will use is the Löwenheim–Skolem theorem.

**Theorem 1** ([10]). If Σ is countable and Γ is a satisfiable set of Σ-formulas, there is a Σ-interpretation B with B ⊨ Γ and |σ<sup>B</sup>| ≤ ℵ<sub>0</sub> for all σ ∈ S<sub>Σ</sub>.

## 2.2 Theory Combination Properties

In what follows, Σ is a signature and T is a Σ-theory. T is decidable if the set {φ ∈ QF(Σ) | φ is T-satisfiable} is decidable, where QF(Σ) is the set of quantifier-free formulas over Σ. T is convex [11] w.r.t. S if ⊨<T> φ → ⋀<i=1><sup>n</sup> x<sub>i</sub> = y<sub>i</sub> implies ⊨<T> φ → x<sub>i</sub> = y<sub>i</sub> for some 1 ≤ i ≤ n, where φ is a conjunction of literals and x<sub>i</sub> and y<sub>i</sub> have sorts in S.

T is stably infinite [12] (respectively, has the *finite model property*) w.r.t. S ⊆ S<sub>Σ</sub> if for every T-satisfiable φ ∈ QF(Σ), there is a T-interpretation A with A ⊨ φ such that for every σ ∈ S, |σ<sup>A</sup>| ≥ ℵ<sub>0</sub> (respectively, |σ<sup>A</sup>| < ℵ<sub>0</sub>). T is smooth [15] w.r.t. S if for every quantifier-free formula φ, T-interpretation A with A ⊨ φ, and function κ from S to the class of all cardinals such that κ(σ) ≥ |σ<sup>A</sup>| for every σ ∈ S, there is a T-interpretation B with B ⊨ φ and |σ<sup>B</sup>| = κ(σ) for all σ ∈ S. If we add the assumption that κ(σ) < ℵ<sub>0</sub> for every σ ∈ S<sub>Σ</sub>, the resulting property is called *finite smoothness* [14]. T is stably finite [15] if for every quantifier-free formula φ and T-interpretation A with A ⊨ φ there is a T-interpretation B with B ⊨ φ, and |σ<sup>B</sup>| < ℵ<sub>0</sub> and |σ<sup>B</sup>| ≤ |σ<sup>A</sup>| for all σ ∈ S.

Take a finite set of variables V and an equivalence relation E on V such that, if x and y are of different sorts, then xEy (where *E* is the complement of *E*). We define the *arrangement* induced by *E* on V, denoted by $\delta_V^E$ or $\delta_V$ if explicitly mentioning *E* is not necessary, as the conjunction of the literals x = y if xEy, and $\neg(x = y)$ if $x \not= E y$.

T is finitely witnessable [15] w.r.t. S if it has a witness wit : QF(Σ) → QF(Σ), which is a computable function such that for any quantifier-free formula φ: φ and ∃ x̄. wit(φ) are T-equivalent, where x̄ = vars(wit(φ)) \ vars(φ); and, if wit(φ) is T-satisfiable, there is a T-interpretation A with A ⊨ φ and σ<sup>A</sup> = vars<sub>σ</sub>(wit(φ))<sup>A</sup> for each σ ∈ S. T is strongly finitely witnessable [3] w.r.t. S if it has a strong witness, which is a witness that satisfies, for every quantifier-free formula φ, finite set of variables V whose sorts are in S, and arrangement δ<sub>V</sub> in V, if wit(φ) ∧ δ<sub>V</sub> is T-satisfiable, then there exists a T-interpretation A with A ⊨ wit(φ) ∧ δ<sub>V</sub> and σ<sup>A</sup> = vars<sub>σ</sub>(wit(φ) ∧ δ<sub>V</sub>)<sup>A</sup> for each σ ∈ S. T is polite, respectively strongly polite, w.r.t. S if it is smooth and finitely witnessable w.r.t. S, respectively smooth and strongly finitely witnessable.
A minimal model function [19,23] w.r.t. $S \subseteq S_\Sigma$ for $\mathcal{T}$ is a function that takes $\varphi \in QF(\Sigma)$ and returns a set $\mathbb{M}_{\mathcal{T}}(\varphi)$ of functions $\mathbf{n}$ from $S$ to the class of all cardinals such that, if $\varphi$ is $\mathcal{T}$-satisfiable: for every $\mathbf{n}$ in $\mathbb{M}_{\mathcal{T}}(\varphi)$, there exists a $\mathcal{T}$-interpretation $\mathcal{A}$ with $\mathcal{A} \models \varphi$ and $\mathbf{n}(\sigma) = |\sigma^A|$ for all $\sigma \in S$; if $\mathbf{m}, \mathbf{n} \in \mathbb{M}_{\mathcal{T}}(\varphi)$ and $\mathbf{m} \neq \mathbf{n}$, there exists $\sigma \in S$ such that $\mathbf{m}(\sigma) < \mathbf{n}(\sigma)$; and for every $\mathcal{T}$-interpretation $\mathcal{A}$ that satisfies $\varphi$, there exists $\mathbf{n} \in \mathbb{M}_{\mathcal{T}}(\varphi)$ such that $\mathbf{n}(\sigma) \le |\sigma^A|$ for all $\sigma \in S$. $\mathcal{T}$ is called *shiny w.r.t. S* if it is smooth, stably finite, and has a computable minimal model function, all w.r.t. S.

$\mathcal{T}$ is a *Unicorn 1.0 theory w.r.t. S* if it is stably infinite, strongly finitely witnessable but not smooth, all w.r.t. S. It is a *Unicorn 2.0 theory w.r.t. S* if it is strongly finitely witnessable but does not have a computable minimal model function, both w.r.t. S [23]. It is a *Unicorn 3.0 theory w.r.t. S* if it is polite and shiny, but is not strongly polite, all w.r.t. S [23].

We have the following theorem:

**Theorem 2** ([6,18]). If $Ax(\mathcal{T})$ consists solely of Horn clauses, then $\mathcal{T}$ is convex.

## 3 Shiny Theories Are Always Decidable (and Strongly Polite)

In [4], it was proven that for decidable theories, strong politeness and shininess are equivalent:

**Theorem 3** ([4, Theorem 3.10]). *A decidable theory is strongly polite w.r.t. a finite set $S$ of sorts if and only if it is shiny w.r.t. $S$.*

In this section, we show that the right-to-left direction holds without assuming decidability. Moreover, the reason for this is that shiny theories are in fact always decidable.

Now, it is important to clarify that the definition of shininess in [4] is slightly different from ours (which comes from [23]): in [4], the minimal model function of a $\Sigma$-theory $\mathcal{T}$ is only defined over $\mathcal{T}$-satisfiable $\Sigma$-formulas. With this definition, we cannot ask whether the minimal model function is computable for undecidable theories, since its domain is an undecidable set. In [23], a more general definition was found, that would apply also to undecidable theories. Thus, the domain of the minimal model function is all quantifier-free formulas, although the function can return anything for unsatisfiable formulas. This is natural: without knowing that a formula is $\mathcal{T}$-satisfiable, we may still be able to determine the size of its minimal model in case it is $\mathcal{T}$-satisfiable. However, this is not the only way one could have generalized the definition to undecidable theories; one could have instead allowed the minimal model function to be *partial*, so that the algorithm computing it may not terminate for unsatisfiable formulas. That said, we follow [23] in requiring the minimal model function to be total, an assumption we make essential use of.
With our definition, it makes sense to ask whether an undecidable theory is shiny. We show that the answer is always no: every shiny theory is decidable. In fact, we show something stronger, namely, that smoothness does not need to be assumed, but can be replaced by stable infiniteness.

**Theorem 4.** If a theory $T$ is stably infinite, stably finite, and has a computable minimal model function, all with respect to a non-empty set of sorts $S$, then $T$ is decidable.

Note that all the assumptions of the theorem are necessary: decidability does not follow from stable infiniteness and stable finiteness alone, and also not from either of them combined with the computability of the minimal model function. For more details on this, see Remark 1 of Sect. 4.4 below, where concrete examples are given.

Theorem 4 implies that shiny theories are decidable, since smoothness is a stronger property than stable infiniteness. As a corollary, we see that shininess implies strong politeness:

**Corollary 1.** If a theory is shiny with respect to a finite set of sorts $S$, then it is strongly polite with respect to $S$.

The fact that shininess implies politeness solves a problem that was left open in [23]. In that paper, it was left undetermined whether there exist Unicorn 3.0 theories, that is, theories that are polite and shiny, but not strongly polite. In particular, such theories, if exist, must be shiny without being strongly polite. But Corollary 1 tells us that such theories do not exist.

**Corollary 2.** There are no Unicorn 3.0 theories.

# 4 Some Strongly Polite Theories Are Not Shiny

In this section, we study the following question, which is the converse of the question from Sect. 3.

(*) Does strong politeness imply shininess?

By Theorems 3 and 4, this is equivalent to asking whether strong politeness implies decidability. Similarly to Sect. 3, this is also related to a question left open in [23]: the existence of strongly finitely witnessable theories that do not have a computable minimal model function, a.k.a. Unicorn 2.0 theories. If such theories do not exist, then the answer to (*) would be positive. In contrast, if such theories exist, this is still not enough to provide a negative answer: Unicorn 2.0 theories are definitely not shiny, since they do not have a computable minimal model function. But, they are only required to be strongly finitely witnessable, and not necessarily smooth. Thus, if a Unicorn 2.0 theory is found that is not smooth, this does not help us with determining the answer for (*). In fact, thanks to [14, Theorem 2], we know that every strongly finitely witnessable theory that is also
stably infinite is strongly polite (over countable signatures). Thus, a negative answer to (*) can be obtained by finding a Unicorn 2.0 theory that is also stably infinite.

As part of our strategy to resolve (*), we make a detour into the land of Unicorn 2.0 theories. One of the goals of [23] was to determine the feasibility of all Boolean combinations of model-theoretic properties studied there. After Sect. 3, we are closer to the end of that project, as it determined the feasibility of Unicorn 3.0 theories. To fully complete that project, we need to determine the feasibility of 10 different kinds of Unicorn 2.0 theories. Two of them, over empty signatures, will be shown to be impossible in Sect. 4.1. The remaining eight cases, all over non-empty signatures, are in fact possible, which we demonstrate in Sect. 4.2. Specifically, we prove that in non-empty signatures there are Unicorn 2.0 theories with all the possible combinations of the following properties: (1) being defined over a one-sorted (or many-sorted) signature; (2) being stably infinite (or not stably infinite); and (3) being convex (or not convex). In total, we present 8 Unicorn 2.0 theories. Since they include stably infinite ones, we obtain in Sect. 4.3 a positive answer to (*). We conclude this section by completing the picture of strong politeness, shininess, and decidability, by showing which combinations of these properties are possible in Sect. 4.4.

**4.1 Unicorns 2.0 over Empty Signatures**

We prove that there are no Unicorn 2.0 theories over empty signatures with finitely many sorts.

We start by proving that all theories that are based on empty signatures with finitely many sorts are decidable.

**Lemma 1.** If $\Sigma$ is an empty signature with finitely many sorts and $T$ is a $\Sigma$-theory, then $T$ is decidable.

*Proof Sketch.* Let $\{\sigma_1, \dots, \sigma_n\}$ be the sorts of $\Sigma$. Using a result very similar to Dickson's lemma [5], which states a subset of $\mathbb{N}^n$ has only finitely many minimal elements, we obtain $T$ has only finitely many interpretations $\mathcal{A}$ such that ($|\sigma_1^A|, \dots, |\sigma_n^A|$) is maximal. Because the signature is empty, to check whether $\varphi$ is $T$-satisfiable it is then enough to test whether $\varphi$ has an interpretation $\mathcal{B}$ in equational logic such that $|\sigma_i^\mathcal{B}| \le |\sigma_i^A|$ for all $1 \le i \le n$. $\square$

Now, let us go back to Theorem 3. The proof of the left-to-right direction assumes decidability, strong finite witnessability and smoothness, and proves stable finiteness and the computability of the minimal model function. A closer look at the proof reveals that when proving computability of the minimal model function, smoothness is not used. We can therefore obtain the following lemma, that was nevertheless not mentioned explicitly in [4]:

**Lemma 2.** If $T$ is decidable and strongly finitely witnessable with respect to $S$, then it has a computable minimal model function with respect to $S$.
Combining these two lemmas, we obtain that there are no Unicorn 2.0 theories over an empty signature with finitely many sorts.

**Corollary 3.** If $\Sigma$ is an empty signature with finitely many sorts, and $\mathcal{T}$ is a $\Sigma$-theory strongly finitely witnessable with respect to $S \subseteq S_\Sigma$, then it has a computable minimal model function with respect to $S$.

## 4.2 Unicorns 2.0 over Non-empty Signatures

<table><caption>**Table 1.** Signatures. All function symbols of $\Sigma_*$ and $f$ have arity $\sigma_1 \to \sigma_1$. $N, T$, and $P$ have arity $\sigma_1$. Each $P_i$ is a nullary predicate. $<$ has arity $\sigma_1 \times \sigma_1$.</caption><thead><tr><th>Section</th><th>Signature</th><th>Sorts</th><th>Function Symbols</th><th>Predicate Symbols</th></tr></thead><tbody><tr><td rowspan="2">Section 4.2</td><td>$\Sigma_f$</td><td>$\{\sigma_1\}$</td><td>$\{f\}$</td><td>$\emptyset$</td></tr><tr><td>$\Sigma_f^2$</td><td>$\{\sigma_1, \sigma_2\}$</td><td>$\{f\}$</td><td>$\emptyset$</td></tr><tr><td rowspan="2">Section 4.4</td><td>$\Sigma_1$</td><td>$\{\sigma_1\}$</td><td>$\emptyset$</td><td>$\emptyset$</td></tr><tr><td>$\Sigma_P^n$</td><td>$\{\sigma_1\}$</td><td>$\emptyset$</td><td>$\{P_1, P_2, \dots\}$</td></tr><tr><td>Section 5</td><td>$\Sigma_P$</td><td>$\{\sigma_1\}$</td><td>$\emptyset$</td><td>$\{P\}$</td></tr><tr><td>Section 6</td><td>$\Sigma_*$</td><td>$\{\sigma_1\}$</td><td>$\{f_\rho | \rho \in 2^\omega\}$</td><td>$\{N, T, <\}$</td></tr></tbody></table>

We now prove that there are Unicorn 2.0 theories over non-empty signatures. We start with the one-sorted case. The many-sorted case will be dealt with in the end of this section. We work within a single-sorted signature $\Sigma_f$ with only a unary function symbol $f$ and sort $\sigma_1$, as described in Table 1.

Our theories will make use of the following formula:

**Definition 1.** Given a number $n$ and a variable $x$, we denote by $cycle_n(x)$ the formula $f^n(x) = x \wedge \bigwedge_{m \neq n} f^m(x) \neq x$, where $m | n$ means that $m$ divides $n$.

In any $\Sigma_f$-interpretation $\mathcal{A}$, $f^A$ is, of course, a unary function. As such, it gives rise to a directed graph in which the vertices are the elements of $\sigma_1^A$, and each vertex has out-degree 1. For each $n \in \mathbb{N}^+$, and $\Sigma_f$-interpretation $\mathcal{A}$, $\mathcal{A} \models cycle_n(x)$ if $x^A$ is a part of a cycle of length $n$. Notice that this is stronger than just having $\mathcal{A} \models f^n(x) = x$, as in the latter case we might also have $\mathcal{A} \models f^m(x) = x$ for some $m$ that properly divides $n$.<fnref n="4" />

We define four Unicorn 2.0 $\Sigma_f$-theories: $\mathcal{T}_1, \mathcal{T}_2, \mathcal{T}_3, \mathcal{T}_4$. Their axiomatizations appear in Table 2. We will prove that $\mathcal{T}_1$, in addition to being Unicorn 2.0, is also stably infinite and convex; $\mathcal{T}_2$ is stably infinite but not convex; $\mathcal{T}_3$ is not stably infinite but convex; and $\mathcal{T}_4$ is neither stably infinite nor convex.

<footnote n="4">⁴ In $cycle_n(x)$, the requirements $m|n$ and $m \neq n$ can be replaced by the requirement $m < n$. However, we chose an encoding that skips redundant cases.</footnote>
<table><caption>**Table 2.** Theories. $cycle_n(x)$ is defined in Definition 1. $S$ is an undecidable set of prime numbers. In $T\langle h\rangle$, $h: N \to \{0, 1\}$ is a non-computable function. $\psi_n^P$ abbreviates the formula $(\exists x_1, \dots, x_n. \neq (x_1, \dots, x_n) \wedge \bigwedge_{i=1}^n P(x_i))$.</caption><thead><tr><th>Section</th><th>Theory</th><th>Signature</th><th>Axiomatization</th><th>Source</th></tr></thead><tbody><tr><td rowspan="4">Section 4.2</td><td>T<sub>1</sub></td><td>Σ<sub>f</sub></td><td>{(∃x. cycle<sub>n</sub>(x)) → ∀x. f<sup>2</sup>(x) ≠ x | n ∈ S}</td><td>new</td></tr><tr><td>T<sub>2</sub></td><td>Σ<sub>f</sub></td><td>Ax(T<sub>1</sub>) ∪ {¬∃x. cycle<sub>6</sub>(x)}</td><td>new</td></tr><tr><td>T<sub>3</sub></td><td>Σ<sub>f</sub></td><td>Ax(T<sub>1</sub>) ∪ {(∃x. f(x) = x) → ∀x. ∀y. x = y}</td><td>new</td></tr><tr><td>T<sub>4</sub></td><td>Σ<sub>f</sub></td><td>Ax(T<sub>2</sub>) ∪ Ax(T<sub>3</sub>)</td><td>new</td></tr><tr><td rowspan="3">Section 4.4</td><td>T<sub>EQ</sub></td><td>Σ<sub>1</sub></td><td>∅</td><td>everywhere</td></tr><tr><td>T<sub>=1</sub></td><td>Σ<sub>1</sub></td><td>{ψ<sub>=1</sub>}</td><td>[21]</td></tr><tr><td>T<sub>⟨h⟩</sub></td><td>Σ<sub>P</sub><sup>n</sup></td><td>{P<sub>n</sub>: h(n) = 1} ∪ {¬P<sub>n</sub>: h(n) = 0} ∪ {ψ<sub>=1</sub>}</td><td>new</td></tr><tr><td>Section 5</td><td>T<sub>2n</sub></td><td>Σ<sub>P</sub></td><td>{ψ<sub>n</sub><sup>P</sup> → ψ<sub>≥2n</sub> | n ∈ N<sup>+</sup>}</td><td>new</td></tr><tr><td>Section 6</td><td>T<sub>*</sub></td><td>Σ<sub>*</sub></td><td>See Definition 4</td><td>new</td></tr></tbody></table>

Let us provide some intuition for their definitions. We assume an arbitrary but fixed undecidable set $S$ of prime numbers that are greater than or equal to 7.<fnref n="5" /> Let $\mathcal{A}$ be a $\Sigma_f$-interpretation, and let $G_{\mathcal{A}}$ be the graph induced by $f^A$. Then: $\mathcal{A}$ is a $T_1$-interpretation if $G_{\mathcal{A}}$ either has no cycles whose lengths are in $S$, or it has no cycles of length 1 and 2. $\mathcal{A}$ is a $T_2$-interpretation if it is a $T_1$-interpretation, and, in addition, $G_{\mathcal{A}}$ has no cycles of length 6. $\mathcal{A}$ is a $T_3$-interpretation if it is a $T_1$-interpretation, and, in addition, if $G_{\mathcal{A}}$ has a loop (i.e., a cycle of length 1), then $\sigma_1^A$ has a single element. Finally, $\mathcal{A}$ is a $T_4$-interpretation if it is both a $T_2$-interpretation and a $T_3$-interpretation.

<figure><img src="image_33.png" /><figcaption>**Fig. 3.** The interpretations $\mathcal{A}_2$, $\mathcal{A}_3$ and $\mathcal{A}_6$, from left-to-right, all satisfy $f^6(x) = x$, but only $\mathcal{A}_6$ satisfies $cycle_6(x)$.</figcaption></figure>

We prove that all theories $T_1, \dots, T_4$ are Unicorn 2.0 theories; that is, they are strongly finitely witnessable (Lemma 3) but do not have a computable minimal

<footnote n="5">⁵ Such sets exist: consider any undecidable set $S_0$, and let $S_1$ be the image of the function $p$ that takes a natural number $i$ from $S_0$ and returns the $ith$ prime number. Then, $S_1$ is also undecidable. Finally, define $S := S_1 \setminus \{1, \dots, 6\}$. Then $S$ is an undecidable set of prime numbers greater than or equal to 7.</footnote>
model function (Lemma 4). For the latter, it can be shown that a computable
minimal model function can be used to decide $S$, contradicting its undecidability.

**Lemma 3.** For each $i \in [4]$, $\mathcal{T}_i$ is strongly finitely witnessable.

**Lemma 4.** For each $i \in [4]$, $\mathcal{T}_i$ has no computable minimal model function.

Now that we have found four Unicorn 2.0 theories, we prove which properties
each of them admit: the first two are stably infinite while the last two are not,
and $\mathcal{T}_1$ and $\mathcal{T}_3$ are convex while $\mathcal{T}_2$ and $\mathcal{T}_4$ are not.

For the first two theories, it is possible to add arbitrarily many elements to their interpretations without creating new cycles, and thus the resulting interpretations belong to the theories.

**Lemma 5.** For each $i \in \{1, 2\}$, the theory $\mathcal{T}_i$ is stably infinite.

In contrast, theories $\mathcal{T}_3$ and $\mathcal{T}_4$ are not stably infinite, as they restrict the size of the domain.

**Lemma 6.** For each $i \in \{3, 4\}$, the theory $\mathcal{T}_i$ is not stably infinite.

*Proof.* $f(x) = x$ is only $\mathcal{T}_3$- and $\mathcal{T}_4$-satisfiable by interpretations of size 1. $\square$

Next, we show that $\mathcal{T}_1$ and $\mathcal{T}_3$ can be re-axiomatized using Horn clauses, and then from Theorem 2 we get that they are convex.

**Lemma 7.** For each $i \in \{1, 3\}$, the theory $\mathcal{T}_i$ is convex.

*Proof.* If $n$ is prime, we have that $cycle_n(x)$ is equivalent to $f^n(x) = x \wedge f(x) \neq x$, and therefore $(\exists x. cycle_n(x)) \rightarrow \forall x. f^2(x) \neq x$ is equivalent to $\forall x. \forall y. f^n(x) \neq x \vee f(x) = x \vee f^2(y) \neq y$. Also, $(\exists x. f(x) = x) \rightarrow \forall x. \forall y. x = y$ is equivalent to $\forall x. \forall y. \forall z. f(x) \neq x \vee y = z$. Therefore, $\mathcal{T}_i$ can be axiomatized by Horn clauses, which implies that $\mathcal{T}_i$ is convex by Theorem 2. $\square$

Finally, we show that $\mathcal{T}_2$ and $\mathcal{T}_4$ are not convex.

**Lemma 8.** For each $i \in \{2, 4\}$, the theory $\mathcal{T}_i$ is not convex.

*Proof.* We have $\models_{\mathcal{T}_i} f^6(x) = x \rightarrow (f^2(x) = x \vee f^3(x) = x)$. Indeed, let $\mathcal{A}$ be a $\mathcal{T}_i$-interpretation. Then clearly, $\mathcal{A} \not\models cycle_6(x)$. Now suppose $\mathcal{A} \models f^6(x) = x$. Then $\mathcal{A} \models f(x) = x$, or $\mathcal{A} \models f^2(x) = x$, or $\mathcal{A} \models f^3(x) = x$. If the first case holds, then so do the second and the third. Hence we get $\mathcal{A} \models f^2(x) = x$, or $\mathcal{A} \models f^3(x) = x$.

However, $\not\models_{\mathcal{T}_i} f^6(x) = x \rightarrow f^2(x) = x$ and $\not\models_{\mathcal{T}_i} f^6(x) = x \rightarrow f^3(x) = x$. Indeed, consider a $\mathcal{T}_i$-interpretation $\mathcal{A}$ that satisfies $cycle_2(x) \wedge \neg cycle_3(x)$ (such as $\mathcal{A}_2$ from Fig. 3). Then $\mathcal{A} \models f^6(x) = x$ but $\mathcal{A} \not\models f^3(x) = x$. Similarly, Consider a $\mathcal{T}_i$-interpretation $\mathcal{B}$ that satisfies $cycle_3(x) \wedge \neg cycle_2(x)$ (see $\mathcal{A}_3$ in Fig. 3). Then $\mathcal{A} \models f^6(x) = x$ but $\mathcal{A} \not\models f^2(x) = x$. $\square$
With this, we have proven all necessary requirements for theories $\mathcal{T}_1, \dots, \mathcal{T}_4$.

Now, we turn to theories over a many-sorted signature. For that, we utilize the signature $\Sigma_f^2$ from Table 1, that simply adds a sort $(\sigma_2)$ to $\Sigma_f$. Rather than introducing completely new theories for this signature, we use the following result from [21], according to which a sort can be added while preserving all relevant properties.

**Definition 2** ([21], **Definition 4**). If $\mathcal{T}$ is a $\Sigma_f$-theory then $(\mathcal{T})^2$ is the $\Sigma_f^2$-theory axiomatized by $Ax(\mathcal{T})$.

**Lemma 9** ([21, 23]). Let $\mathcal{T}$ be a $\Sigma_f$-theory and $X$ be either strong finite witnessability, computability of the minimal model function, stable infiniteness or convexity. Then: $\mathcal{T}$ admits property $X$ with respect to $\{\sigma_1\}$ iff $(\mathcal{T})^2$ admits property $X$ with respect to $\{\sigma_1, \sigma_2\}$.

Thus, for the many-sorted case, we simply use the theories $(\mathcal{T}_1)^2$, $(\mathcal{T}_2)^2$, $(\mathcal{T}_3)^2$, and $(\mathcal{T}_4)^2$. For example, $(\mathcal{T}_1)^2$ has the exact same axiomatization as $\mathcal{T}_1$. It just has the additional sort $\sigma_2$ in its signature. Thus, every $\mathcal{T}_1$-interpretation can be turned into a $(\mathcal{T}_1)^2$-interpretation by simply assigning any non-empty domain to sort $\sigma_2$.

**Corollary 4.** For each $i \in [4]$, $(\mathcal{T}_i)^2$ is strongly finitely witnessable and does not have a computable minimal model function. Further, $(\mathcal{T}_i)^2$ is stably infinite iff $i \in \{1, 2\}$ and is convex iff $i \in \{1, 3\}$.

The results regarding Unicorn 2.0 theories over non-empty signatures are summarized in Table 3. For each theory, we list whether it is defined over a one-sorted signature, whether it is stably infinite, and whether it is convex.

<table><caption>**Table 3.** Unicorn 2.0 Theories in Non-empty Signatures.</caption><thead><tr><th>Theory</th><th>One Sorted</th><th>Stably Infinite</th><th>Convex</th></tr></thead><tbody><tr><td>T<sub>1</sub></td><td>✓</td><td>✓</td><td>✓</td></tr><tr><td>T<sub>2</sub></td><td>✓</td><td>✓</td><td>✗</td></tr><tr><td>T<sub>3</sub></td><td>✓</td><td>✗</td><td>✓</td></tr><tr><td>T<sub>4</sub></td><td>✓</td><td>✗</td><td>✗</td></tr><tr><td>(T<sub>1</sub>)<sup>2</sup></td><td>✗</td><td>✓</td><td>✓</td></tr><tr><td>(T<sub>2</sub>)<sup>2</sup></td><td>✗</td><td>✓</td><td>✗</td></tr><tr><td>(T<sub>3</sub>)<sup>2</sup></td><td>✗</td><td>✗</td><td>✓</td></tr><tr><td>(T<sub>4</sub>)<sup>2</sup></td><td>✗</td><td>✗</td><td>✗</td></tr></tbody></table>
## 4.3 Back to Theorem 3

We have now finished the detour to Unicorn 2.0 theories, and are able to come back to our original question (*) from the beginning of the section, and provide a negative answer: decidability is required for the second direction of Theorem 3, or in other words, the converse of Corollary 1 does not hold without further assuming decidability.

**Corollary 5.** *There are theories that are strongly polite but are not shiny.*

*Proof.* For example, stably infinite Unicorn 2.0 theories $T_1$ and $T_2$ are such. Indeed, no Unicorn 2.0 theory can be shiny. Further, every such theory that is stably infinite must be strongly polite, as [14] has shown that stable infiniteness and strong finite witnessability imply smoothness. □

By Theorem 3, this also means there are undecidable strongly polite theories.

**Corollary 6.** *There are theories that are strongly polite but are not decidable.*

## 4.4 Completing the Picture

From [4], we know that there are no decidable theories that are strongly polite but not shiny (or vice versa). From Theorem 4, we also know that there are no theories that are shiny but undecidable. From Corollary 5, we know that there are undecidable theories that are strongly polite but not shiny. What about the other possible combinations of decidability, shininess, and strong politeness?

We conclude this section by constructing theories for all the other combinations. The signatures for our theories are given in Table 1. The theories themselves are axiomatized in Table 2.

We start with a decidable, strongly polite and shiny theory. For that, we simply take the empty theory $T_{EQ}$ over the empty one-sorted signature $\Sigma_1$. This is the theory that is axiomatized by the empty set of axioms. The congruence closure algorithm (see, e.g., [9]) decides it; and it was proven to be strongly polite in [8,15]. From Theorem 3 it is also shiny.

To obtain a theory that is decidable but neither shiny nor strongly polite, consider $T_1$ (originally introduced in [21]), of structures with a single element. It is decidable, as it satisfies all equalities and no disequalities. It is clearly not smooth, and so it is neither strongly polite nor shiny.

Finally, for an undecidable theory that is neither shiny nor strongly polite, we use $T\langle h \rangle$, defined over signature $\Sigma_P^n$. It has nullary predicates $P_1, P_2, \dots$, such that $P_n$ holds iff $h(n) = 1$, for some non-computable function $h$, and all its models are singletons. $T\langle h \rangle$ is undecidable, otherwise we could compute $h$. Also, it is not smooth, so it is neither strongly polite nor shiny.

These results are summarized as a Venn diagram in Fig. 4. The left circle corresponds to strongly polite theories, the right circle to shiny theories, and the middle circle to decidable theories. Notice that the regions that correspond to decidable theories that are strongly polite but not shiny or vice versa are hatched,
marking that they are empty, citing [4]. Similarly, the region that corresponds to shiny theories that are not decidable is also hatched, citing Theorem 4. All other regions are feasible, and have a white background. Each such region lists the evidence for its inhabitance. Notice that $T\langle h\rangle$ is outside all the circles.

**Remark 1.** The examples of this section are useful in order to show that in Theorem 4 all three properties that are assumed are needed to ensure decidability. Indeed, The theory $T\langle h\rangle$ is stably finite and has a computable minimal model function (every model has size 1), but it is not decidable. Further, the theories $T_1$ and $T_2$ from Sect. 4.2 are stably infinite and stably finite but not decidable. Finally, Peano arithmetic is stably infinite and has a computable minimal model function (every model is infinite), but it is not decidable. These examples make Theorem 4 more surprising than it may at first seem.

<figure><img src="image_34.png" /><figcaption>**Fig. 4.** A Venn diagram summarizing the feasible combinations of strong politeness, shininess and decidability.</figcaption></figure>

# 5 Additive Politeness

In [16], the SMT-LIB theory of datatypes was proven to be strongly polite. It was observed there, however, that one of the challenges in proving strong politeness lies in the need to consider all possible arrangements, which is not needed when proving (weak) politeness. In order to make the proof of strong politeness more feasible, that paper introduced the notion of *additive witnesses*.

**Definition 3** ([16], **Definition 10**). Let $f : QF(\Sigma) \to QF(\Sigma)$. Let $S \subseteq S_\Sigma$. We say that $f$ is $S$-additive for $T$ if $f(f(\varphi) \wedge \psi)$ and $f(\varphi) \wedge \psi$ are $T$-equivalent and have the same set of $S$-sorted variables for every $\varphi, \psi \in QF(\Sigma)$, provided that $\psi$ is a conjunction of flat literals such that every term in $\psi$ is a variable whose sort is in $S$. When $T$ is clear from the context, we say that $f$ is $S$-additive. We say that $T$ is additively finitely witnessable w.r.t. $S$ if there exists a witness for $T$ w.r.t. $S$ which is $S$-additive. $T$ is said to be additively polite w.r.t. $S$ if it is smooth and additively finitely witnessable w.r.t. $S$.
It has been proven in [16] that additively polite theories are strongly polite. The converse, however, does not hold. To show this, we define a theory that is strongly polite but not additively polite, over signature $\Sigma_P$ from Table 1. It has a single sort $\sigma_1$, and one unary predicate symbol $P$. The theory, called $\mathcal{T}_{2n}$ and axiomatized in Table 2, admits those $\Sigma_P$-interpretations $\mathcal{A}$ where for each $n$, if there are at least $n$ elements in $P^A$, then there are at least $2n$ elements in $\sigma_1^A$.

We prove that $\mathcal{T}_{2n}$ is strongly polite but not additively polite. We do the former by proving shininess and then using Corollary 1, and the latter by reasoning about cardinalities of models of $\mathcal{T}_{2n}$ that satisfy formulas in which $P$ occurs.

**Lemma 10.** *The theory $\mathcal{T}_{2n}$ is strongly polite.*

**Lemma 11.** *The theory $\mathcal{T}_{2n}$ is not additively polite.*

Although strong politeness does not imply additive politeness in general, this implication holds for theories over *algebraic signatures*, which are signatures containing no predicate symbols (except equality) [7].

**Theorem 5.** *Let $\mathcal{T}$ be a theory over a countable algebraic signature, and let $S$ be a set of sorts. If $\mathcal{T}$ is strongly polite with respect to $S$, then it is additively polite with respect to $S$.*

Note that the strongly polite theories $\mathcal{T}_1$ and $\mathcal{T}_2$ from Sect. 4.2 are over algebraic signatures, so they are additively polite.

# 6 Finite Smoothness Versus Smoothness

As the current paper started with Unicorn 3.0 theories (Sect. 3) and continued with Unicorn 2.0 theories (Sect. 4), we end it with Unicorn 1.0 theories.

In [14], Unicorn 1.0 theories were proven not to exist. The main step in the proof was the following theorem:

**Theorem 6 ([14, Theorem 3]).** Let $\mathcal{T}$ be a theory over a countable signature. If $\mathcal{T}$ is stably finite and finitely smooth, both with respect to a set of sorts $S$, then $\mathcal{T}$ is smooth with respect to $S$.

Since stably infinite and strongly finitely witnessable theories are both stably finite and finitely smooth [14, Lemmas 3 and 4], Theorem 6 implies that, over countable signatures, such theories are smooth. This is equivalent to the claim that Unicorn 1.0 theories do not exist.

Notice that in Theorem 6 the signature is assumed to be countable. In [14], the necessity of this assumption was left open. We show that the assumption is necessary, by constructing a theory that is stably finite and finitely smooth, but not smooth, over an uncountable signature.

We define in Table 1 a single-sorted signature $\Sigma_*$ with unary predicates $N$ and $T$, and a binary predicate $<$ (written infix).$^6$ The signature $\Sigma_*$ also has

<footnote>$^6$Think of $N$ as being short for “number” and $T$ as being short for “tree”.</footnote>
function symbols {$f_\rho | \rho \in 2^\omega$}, where $2^\omega$ is the set of infinite binary sequences. Next, we define the theory $\mathcal{T}_*$, which we will use to show that Theorem 6 fails for uncountable signatures. We do so by first defining a class of interpretations, and then closing it to make it a theory.<fnref n="7" />

**Definition 4.** For each $n \in \mathbb{N}$, let $\{0, 1\}^{\le n}$ be the set of sequences over $\{0, 1\}$ of length at most $n$. A $\Sigma_*$-interpretation $\mathcal{A}$ is called $*$-interpretation if there is $n \ge 2$ and $S \subseteq \{0, 1\}^{n-1}$ such that: $\sigma_1^\mathcal{A} = [0, n-1] \cup \{0, 1\}^{\le n-2} \cup S$; $N^\mathcal{A} = [0, n-1]$; $T^\mathcal{A} = \{0, 1\}^{\le n-2} \cup S$; $a <^\mathcal{A} b$ if and only if $a, b \in N^\mathcal{A}$ and $a$ is less than $b$ as natural numbers; and for every $\rho \in 2^\omega$, we have that if $0 \le m \le n-2$ then $f_\rho^\mathcal{A}(m)$ is the sequence that consists of the first $m$ elements of $\rho$, if $m = n-1$ then $f_\rho^\mathcal{A}(m) \in T^\mathcal{A}$, and if $m \in T^\mathcal{A}$ then $f_\rho^\mathcal{A}(m) = m$.

Let $\mathcal{T}_*^-$ be the class of all $*$-interpretations, and let $Ax$ be the set of $\Sigma_*$-sentences that are satisfied by all $*$-interpretations. Then, $\mathcal{T}_*$ is the theory axiomatized by $Ax$, that is, $Ax(\mathcal{T}_*) = Ax$.

We give some intuition for the definition of a $*$-interpretation $\mathcal{A}$. Given $S \subseteq \{0, 1\}^{n-1}$, we can think of $T^\mathcal{A} = \{0, 1\}^{\le n-2} \cup S$ as representing a binary tree of height $n$ in which the first $n-1$ layers are full (each binary sequence of length $m$ is a node in the $(m+1)$th layer of the tree). We can think of $N^\mathcal{A} = [0, n-1]$ as representing numbers corresponding to each layer of the tree. Then, $\rho \in 2^\omega$ is a path through an infinite binary tree, and $f_\rho(m)$ picks out the $(m+1)$th element along that path, unless $m = n-1$, in which case $f_\rho(m)$ can be any element of the tree. See Fig. 5 for an illustrated example.

<figure><img src="image_35.png" /><figcaption>**Fig. 5.** Example of a $*$-interpretation $\mathcal{A}$, including values of the function $f_\rho$ on $N^\mathcal{A}$, where $\rho = 0000\dots$. Notice that $f_\rho(3)$ can be any element of the tree.</figcaption></figure>

Indeed, $\mathcal{T}_*$ admits the required properties in order to refute Theorem 6 over uncountable signatures:

**Theorem 7.** The theory $\mathcal{T}_*$ is stably finite and finitely smooth but not smooth.

<footnote n="7">⁷ The idea underlying the construction is inspired by [17, Exercise 2.3.1 (2)].</footnote>
## 6.1 The Existence of Unicorns?

Theorem 7 gives a counterexample to Theorem 6 for theories over uncountable signatures, but Theorem 7 was used in [14] as a stepping stone to the following, showing that Unicorn 1.0 theories do not exist:

**Theorem 8 ([14, Theorem 2]).** Let $\mathcal{T}$ be a theory over a countable signature. If $\mathcal{T}$ is stably infinite and strongly finitely witnessable, both with respect to a set of sorts $S$, then $\mathcal{T}$ is smooth with respect to $S$.

Does this theorem generalize to uncountable signatures? The question is actually ill-posed. A strong witness is a *computable* function. If the signature is uncountable, the domain of this (computable) function is uncountable, which is impossible in the standard notion of computability. The question becomes well-posed if we consider a weaker version of strong finite witnessability, where the strong witness may be non-computable: Define a *strong pre-witness* to be a strong witness without the computability requirement. We have the following:

**Theorem 9.** Let $\mathcal{T}$ be a theory and $S$ be a finite set of sorts. Then, the following are equivalent: (1) $\mathcal{T}$ is stably finite and finitely smooth with respect to $S$; and (2) $\mathcal{T}$ is stably infinite and has a strong pre-witness with respect to $S$.

In particular, this equivalence implies that $\mathcal{T}_*$ is stably infinite and has a strong pre-witness despite not being smooth. Thus, $\mathcal{T}_*$ is a Unicorn 1.0 theory, except for the requirement that its strong witness be computable. Unicorns may not exist, but $\mathcal{T}_*$ is pretty close to one.

## 7 Conclusion

We have refined the main result of [4], according to which strong politeness is the same as shininess for decidable theories, by showing that shininess implies strong politeness (since shiny theories are always decidable), while the converse does not hold in general. While doing so, we were able to close all open problems raised in a series of papers [14,21–23], by proving that Unicorn 2.0 theories exist, Unicorn 3.0 theories do not, and even though Unicorn 1.0 theories do not exist, there are theories that admit a similar property.

This completes the classification of which Boolean combinations of eight properties relevant to theory combination are possible (namely: stable infinite-ness and finiteness, smoothness, weak and strong finite witnessability, the finite model property, computability of the minimal model function, and convexity). The menagerie of theories we have constructed has already been useful for an ongoing research program that studies impossibility results in theory combination [20]. In the future, we hope to make further use of these theories to discover more about when theory combination is possible.

**Acknowledgments.** Toledo and Zohar were funded by the NSF-BSF grant 2020704, the ISF grant 619/21, and the Colman-Soref fellowship. Przybocki was supported by the NSF Graduate Research Fellowship Program under Grant No. DGE-2140739.
References

1. Barbosa, H., et al.: cvc5: a versatile and industrial-strength SMT solver. In: Fisman, D., Rosu, G. (eds) TACAS 2022. LNCS, vol. 13243, pp. 415–442. Springer, Cham (2022). https://doi.org/10.1007/978-3-030-99524-9_24

2. Barrett, C., Fontaine, P., Tinelli, C.: The satisfiability modulo theories library (SMT-LIB) (2016). www.SMT-LIB.org

3. Barrett, C.W., Dill, D.L., Stump, A.: A generalization of Shostak's method for combining decision procedures. In: Armando, A. (ed.) FroCoS 2002. LNCS (LNAI), vol. 2309, pp. 132–146. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45988-X_11

4. Casal, F., Rasga, J.: Many-sorted equivalence of shiny and strongly polite theories. J. Autom. Reason. **60**(2), 221–236 (2017). https://doi.org/10.1007/s10817-017-9411-y

5. Dickson, L.E.: Finiteness of the odd perfect and primitive abundant numbers with n distinct prime factors. Amer. J. Math. **35**(4), 413 (1913)

6. Harrison, J.: Handbook of Practical Logic and Automated Reasoning, pp. xx+681. Cambridge University Press, Cambridge (2009). https://doi.org/10.1017/CBO9780511576430. ISBN 978-0-521-89957-4

7. Hodges, W.: Model Theory. Encyclopedia of Mathematics and its Applications. Cambridge University Press (1993). https://doi.org/10.1017/CBO9780511551574

8. Jovanović, D., Barrett, C.: Polite theories revisited. In: Fermüller, C.G., Voronkov, A. (eds.) LPAR 2010. LNCS, vol. 6397, pp. 402–416. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-16242-8_29

9. Kroening, D., Strichman, O.: Decision Procedures - An Algorithmic Point of View. Texts in Theoretical Computer Science. An EATCS Series, 2nd edn. Springer (2016)

10. Monzano, M.: Introduction to many-sorted logic. In: Meinke, K., Tucker, J.V. (eds.) Many-sorted Logic and its Applications. Wiley Professional Computing. Wiley (1993)

11. Nelson, Greg, Oppen, Derek C.: Simplification by cooperating decision procedures. ACM Trans. Program. Lang. Syst. **1**(2), 245–257 (1979). https://doi.org/10.1145/357073.357079. ISSN 0164-0925

12. Oppen, D.C.: Complexity, convexity and combinations of theories. Theor. Comput. Sci. **12**(3), 291–302 (1980). https://doi.org/10.1016/0304-3975(80)90059-6. ISSN 0304-3975

13. Przybocki, B., Toledo, G.V., Zohar, Y.: Shininess, strong politeness, and unicorns. arXiv: 2507.04445 [cs.LO] (2025)

14. Przybocki, B., et al.: The nonexistence of unicorns and many-sorted Löwenheim-Skolem theorems. In: Platzer, A., et al. (eds.) FM 2024, Part I. LNCS, vol. 14933, pp. 658–675. Springer, Cham (2024). https://doi.org/10.1007/978-3-031-71162-6_34

15. Ranise, S., Ringeissen, C., Zarba, C.G.: Combining data structures with nonstably infinite theories using many-sorted logic. In: Gramlich, B. (ed.) FroCoS 2005. LNCS (LNAI), vol. 3717, pp. 48–64. Springer, Heidelberg (2005). https://doi.org/10.1007/11559306_3, https://hal.inria.fr/inria-00000570

16. Sheng, Y., et al.: Polite combination of algebraic datatypes. J. Autom. Reason. **66**(3), 331–355 (2022)

17. Tent, K., Ziegle, M.: A Course in Model Theory. Lecture Notes in Logic, vol. 40, pp. x+248. Association for Symbolic Logic/Cambridge University Press, La
Jolla/Cambridge (2012). https://doi.org/10.1017/CBO9781139015417. ISBN 978-0-521-76324-0

18. Tinelli, C.: Cooperation of background reasoners in theory reasoning by residue sharing. J. Autom. Reason. 30(1), 1–31 (2003)

19. Tinelli, C., Zarba, C.G.: Combining Nonstably Infinite Theories. J. Autom. Reason. 34(3), 209–238 (2005)

20. Toledo, G.V., Przybocki, B., Zohar, Y.: Being polite is not enough (and other limits of theory combination). Accepted to CADE- 30 (2025)

21. Toledo, G.V., Zohar, Y., Barrett, C.: Combining combination properties: an analysis of stable infiniteness, convexity, and politeness. In: Pientka, B., Tinelli, C. (eds.) CADE 2023. LNCS, vol. 14132, pp. 522–541. Springer, Cham (2023). https://doi.org/10.1007/978-3-031-38499-8_30

22. Toledo, G.V., Zohar, Y., Barrett, C.: Combining finite combination properties: finite models and busy beavers. In: Sattler, U., Suda, M. (eds.) FroCoS 2023. LNCS, vol. 14279, pp. 159–175. Springer, Cham (2023). https://doi.org/10.1007/978-3-031-43369-6_9

23. de Toledo, G.V., Zohar, Y.: Combining combination properties: minimal models. In: Proceedings of LPAR 2024 (2024)

**Open Access** This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

<figure><img src="image_36.png" /></figure>
# Polite Combination in Parametric Array Theories

Rodrigo Raya¹(✉) and Christophe Ringeissen²

¹ École Polytechnique Fédérale de Lausanne, Lausanne, Switzerland
rodrigo.raya@epfl.ch

² Université de Lorraine, CNRS, Inria, LORIA, 54000 Nancy, France
christophe.ringeissen@loria.fr

**Abstract.** Parametric array theories are extensions of the quantifier-free theory of arrays with relations that hold componentwise. We observe that decision procedures for the satisfiability of these theories rely on a kind of finite witnessability property. We use this insight to show the politeness of these theories with respect to the index and element sorts. Our results clarify the politeness of the theory of sets with the cardinality operator, which was left open in the literature.

## 1 Introduction

Satisfiability procedures form the core of SMT solvers. Their goal is to increase the automation of the theorem-proving process, reducing the interaction with the solver operators. Program verification particularly benefits from theories representing data structures; therefore, state-of-the-art SMT solvers include efficient decision procedures for them. Automatic combination methods, such as Nelson-Oppen's [12], derive decision procedures for formulas in the combination of data structure theories with specific theories of indices and contents. Unfortunately, Nelson-Oppen's method does not work for non-stably infinite theories, such as those referring to finite domains. Polite theory combination [7,14] addresses this problem.

This paper shows the politeness of data structure theories that generalise the extensionality axiom [20] to functions and relation symbols. This extension is useful in the verification of parametrised systems, where it is important to specify properties in subsets of system components. Supporting such generalisation incurs only a mild overhead with respect to the extensional fragment [10] and recent work shows that the theory combines with cardinality, regular, and aggregation constraints while preserving decidability [5,17]. Here, we develop the observation that the decision procedures in [5,17] reduce the satisfiability of the theory to satisfiability over a finite model, a small model property analogous to finite witnessability in the polite theory combination framework. We illustrate this observation in three paradigmatic examples with component-wise operations [10], cardinality constraints [22], and set interpretations [1]. These theories

<footnote>Research supported by the Swiss NSF Project P500PT_222338.</footnote>
extend the quantifier-free theory of power structures [4,9] with read and write operations.

**Related Work.** The literature on quantifier-free data structure theories is very broad. These include theories of sets [8], multisets [13], theories of sequences [18] and their combinations [5]. These combinations often include expressive theories such as theories with cardinality or aggregation constraints. These fragments can be used to encode further theories such as regular constraints [17,21]. The results regarding the modular combination of theories are comparatively underdeveloped. The main work, which also originated the research line on polite theory combination, is that of [14]. Logically, open problems in the area have arisen. In [2], it is left for future work to determine the politeness of a theory of sets with cardinality constraints. We solve this open problem and offer initial steps towards full modular combination of decision procedures for more modern data structure theories.

**Contributions.** We identify a family of data structure theories for which the polite theory combination method applies. In particular, we observe that the decision procedures for extensions of the theory of powers work by reducing satisfiability in the data structure to a finite number of satisfiability queries on witnesses on the indices or contents theory and show

- the politeness for theories of powers with component-wise operations (e.g. combinatory array logic) with respect to the index and element sorts,

- the politeness of theories of set abstractions with cardinality constraints (e.g. Zarba's theory of sets with cardinality constraints, which was left open in [2]) with respect to the index sort, and

- the politeness of theories with set interpretations (e.g. the simple flat array fragment with fixed set interpretations) with respect to the element sort and, when fixing formulas under set interpretations, also with respect to the index sort.

**Paper Organisation.** Section 2 introduces the polite combination framework. Section 3 introduces the data structure theories treated. Section 4 shows politeness of combinatory array logic. Section 5 shows the politeness of theories of sets with cardinality constraints. Section 6 shows the politeness of theories of interpreted sets with cardinalities. Section 7 concludes the paper.

## 2 Polite Combination

The polite combination method [7] provides a $T \cup T'$-satisfiability procedure when $T$ and $T'$ are signature-disjoint theories such that $T$ and $T'$ share only a set of sorts $S$, $T$ is **strongly** polite w.r.t $S$, $T'$ is an arbitrary theory, and satisfiability procedures are known for $T$ and $T'$. Let us start with the definition of politeness [14]. Let $\Sigma$ be a signature, let $S \subseteq \Sigma^S$ be a set of sorts, and let $T$ be a $\Sigma$-theory. We say that $T$ is *polite* with respect to $S$ if it is both smooth and finitely witnessable with respect to $S$.
**Definition 1 (Smoothness).** Let $\Sigma$ be a signature, let $S = \{\sigma_1, \dots, \sigma_n\}$ be a set of sorts in $\Sigma$, and let $T$ be a $\Sigma$-theory. We say that $T$ is smooth with respect to $S$ if:

- for every $T$-satisfiable quantifier-free $\Sigma$-formula $\varphi$,

- for every $T$-interpretation $\mathcal{A}$ satisfying $\varphi$,

- for every cardinal numbers $\kappa_1, \dots, \kappa_n$ such that $\kappa_i \ge |A_{\sigma_i}|$, for $i = 1, \dots, n$,

there exists a $T$-interpretation $\mathcal{B}$ satisfying $\varphi$ such that

$$|B_{\sigma_i}| = \kappa_i, \quad \text{for } i = 1, \dots, n$$

**Definition 2 (Finite witnessability).** Let $\Sigma$ be a signature, let $S$ be a set of sorts in $\Sigma$, and let $T$ be a $\Sigma$-theory. We say that $T$ is finitely witnessable with respect to $S$ if there exists a computable function witness that for every quantifier-free $\Sigma$-formula $\varphi$ returns a quantifier-free $\Sigma$-formula $\psi = \text{witness}(\varphi)$ such that (i) $\varphi$ and $(\exists \bar{v})\psi$ are $T$-equivalent, where $\bar{v} = \text{vars}(\psi)\setminus\text{vars}(\varphi)$; (ii) if $\psi$ is $T$-satisfiable then there exists a $T$-interpretation $\mathcal{A}$ satisfying $\psi$ such that $A_\sigma = [\text{vars}_\sigma(\psi)]^A$, for each $\sigma \in S$.

The next two propositions establish sufficient conditions to get smoothness and finite witnessability, considering only conjunctions of flat literals. A literal is flat if it is of the form, $x = f(y_1, \dots, y_n)$, $p(y_1, \dots, y_n)$, or $\neg p(y_1, \dots, y_n)$, where $x, y_1, \dots, y_n$ are variables, $f$ is a function symbol, and $p$ is a predicate symbol.

**Proposition 1 (Smoothness).** Let $\Sigma$ be a signature, let $S = \{\sigma_1, \dots, \sigma_n\}$ be a set of sorts in $\Sigma$, and let $T$ be a $\Sigma$-theory. Assume that for every conjunction $\Gamma$ of flat $\Sigma$-literals, for every $T$-interpretation $\mathcal{A}$ satisfying $\Gamma$, for every sort $\tau \in S$, and for every cardinal number $\kappa > |A_\tau|$, there exists a $T$-interpretation $\mathcal{B}$ satisfying $\Gamma$ such that $|B_\tau| = \kappa$, and $|B_\sigma| = |A_\sigma|$ for $\sigma \in S \setminus \{\tau\}$. Then $T$ is smooth with respect to $S$.

*Proof.* See [15, Proposition 11].

**Proposition 2 (Finite Witnessability).** Let $\Sigma$ be a signature, let $S$ be a set of sorts in $\Sigma$ and let $T$ be a $\Sigma$-theory. Assume that there exists a computable function witness that for every conjunction $\Gamma$ of flat $\Sigma$-literals such that $\text{vars}_\sigma(\Gamma) \ne \emptyset$, for each sort $\sigma \in S$, returns a quantifier-free $\Sigma$-formula $\psi = \text{witness}(\Gamma)$ such that (i) $\Gamma$ and $(\exists \bar{v})\psi$ are $T$-equivalent, where $\bar{v} = \text{vars}(\psi)\setminus\text{vars}(\Gamma)$; (ii) if $\psi$ is $T$-satisfiable then there exists a $T$-interpretation $\mathcal{A}$ satisfying $\psi$ such that $A_\sigma = [\text{vars}_\sigma(\psi)]^A$, for each $\sigma \in S$. Then $T$ is finitely witnessable w.r.t. to $S$.

*Proof.* See [15, Proposition 12].
Politeness implies strong politeness whenever the finite witness associated to $T$ is $S$-additive [19]. A mapping $w$ from conjunctions of literals to conjunctions of literals is said to be $S$-additive for $T$ if $w(w(\phi) \wedge \varphi)$ and $w(\phi) \wedge \varphi$ are $T$-equivalent and have the same set of $S$-sorted variables for every conjunctions of literals $\phi$ and $\varphi$ such that $\varphi$ is a conjunction of flat literals where every term is a variable whose sort is in $S$. It is important to notice that all the finite witnesses constructed in this paper are actually $S$-additive, and in this context politeness is sufficient to achieve strong politeness.

# 3 Extensions of the Theory of Powers

The first-order theory of powers [9] is the first-order theory of the structure $M^I$, where $M$ is a given structure and $I$ is a given set, whose carrier set is the set of all functions from $I$ to the carrier set of $M$, and the interpretation of functions and relations is defined component-wise in terms of the functions and relations in $M$. For instance, in linear algebra one often considers the structure $\langle\mathbb{R}^N, +\rangle$, where we have the definition $a + b = c \leftrightarrow \forall i.a[i] + b[i] = c[i]$, that is, the relation $a + b = c$ holds for vectors if and only if it holds homogeneously at every component. We study three theories that extend this construction. The first fragment is combinatory array logic [10] which extends the quantifier-free theory of arrays with functions and relations defined componentwise. The second fragment is the theory of sets with cardinalities of Zarba [22] (we view sets as functions from an index sort to Boole's algebra $\langle\{0,1\}, \wedge, \vee, \neg\rangle$). The last fragment is the simple flat array fragment [1, 16]. This fragment was also studied in [4,6] to extend the results of [9] to more general structures and substructures.

## 3.1 Combinatory Array Logic

$$ 
\begin{align*}
F &::= F_1 \wedge F_2 | F_1 \vee F_2 | \neg F | \mathrm{map}_R(\bar{A}) | A[i] = e \\
A &::= a | \mathrm{write}(A, i, E) | K(e) | \mathrm{map}_f(\bar{A}) \\
E &::= A[i] | e
\end{align*}
$$

<caption>Fig. 1. $T_{CAL}$'s syntax.</caption>

Combinatory array logic [10], $T_{CAL}$, uses a quantifier-free many-sorted language, comprising a sort index for indices, a sort element for elements, and a sort array for arrays. In Fig. 1, we use instances of letter $i$ to refer to variables of the index sort, letter $e$ to refer to variables of sort element and letter $a$ to refer to a variable of the array sort. Function symbol write takes as input an array, an index and an element and returns an array. Function read, $-[\cdot]$, takes an array and an index and returns an element. Function $K$ takes as input an element and returns an array which is constantly equal to that element. Function $\mathrm{map}_f(\bar{A})$
takes as input a tuple of arrays and returns an array where, for each index $i$, the $i$-th component is the result of applying the uninterpreted function $f$ to the $i$-th component of the input arrays. Relation $\text{map}_R(\bar{A})$ takes as input a tuple of arrays and returns true if and only if the uninterpreted relation $R$ holds for each tuple of elements in the $i$-th component. Formally, the introduced symbols satisfy the following axioms.

$$ \forall a, i, e. \text{ write}(a, i, e)[i] = e $$

$$ \forall a, i, j, e. i = j \lor \text{write}(a, i, e)[j] = a[j] $$

$$ \forall e, i. K(e)[i] = e $$

$$ \forall a_1, \dots, a_k, i. \text{map}_f(a_1, \dots, a_k)[i] = f(a_1[i], \dots, a_k[i]) $$

$$ \forall a_1, \dots, a_k. \text{map}_R(a_1, \dots, a_k) \leftrightarrow \forall i. R(a_1[i], \dots, a_k[i]) $$

We use $f$ for $\text{map}_f$ and $R$ for $\text{map}_R$ when no ambiguity occurs.

## 3.2 Theories of Sets

$$ F ::= A | F_1 \land F_2 | F_1 \lor F_2 | \neg F $$

$$ A ::= i_1 = i_2 | i \in B | B_1 = B_2 | B_1 \subseteq B_2 | T_1 = T_2 | T_1 < T_2 $$

$$ B ::= x | \emptyset | B_1 \cup B_2 | B_1 \cap B_2 | B_1 \setminus B_2 $$

$$ T ::= k | K | T_1 + T_2 | K \cdot T | |B| $$

$$ K ::= \dots | -2 | -1 | 0 | 1 | 2 | \dots $$

<caption>**Fig. 2.** $T_Z$'s syntax.</caption>

We will use Zarba's theory of sets [22] for technical reasons (see Sect. 5). Zarba's theory uses a quantifier-free many-sorted language, comprising a sort index for indices, a sort int for integers, and a sort set for sets of indices. In Fig. 2, we use (indexed) instances of letter $i$ to refer to variables of the index sort, letter $x$ to refer to variables of sort set and letter $k$ to refer to a variable of the integer sort. The language includes a first-order signature $\Sigma_{\text{index}}$ to express constraints over the indices. It also includes constants 0, 1, function $+$, and predicate $<$. Regarding sets, the language contains constant $\emptyset$, functions $\{\cdot\}$ (of sort index $\rightarrow$ set), $\cup$, $\cap$, $\setminus$ and predicates $\in$, $\subseteq$. Finally, there is the cardinality function $|\cdot|$ (of sort set $\rightarrow$ int). The semantics of these symbols is the standard.

Given a formula in $T_Z$ with set variables $S_1, \dots, S_n$, a Venn region is the semantics of a Boolean algebra expression on $S_1, \dots, S_n$. An elementary Venn region is the semantics of a Venn region of the form $S_1^{b_1} \cap \dots S_n^{b_n}$ where $b \in \{0, 1\}$ and $S^0 := S$ and $S^1 := S^c$ (i.e. the absolute complement of $S$). We usually abbreviate such elementary Venn regions as $E^\beta$ where $\beta = (b_1, \dots, b_n)$. We often decompose Venn regions $V$ into their elementary components as $V = \cup_{\{\beta|E^\beta \subseteq V\}} E^\beta$. This decomposition allows to transform a $T_Z$ formula into an equivalent Presburger arithmetic formula with an analogous procedure to that of [8].
## 3.3 Interpreted Theories

The simple flat array fragment [1, 5, 16], $T_F$, uses a quantifier-free many-sorted language, comprising a sort index for indices, a sort elem for elements, a sort int for integers, a sort set for sets of indices, and a sort array for arrays. In Fig. 3, we use (indexed) instances of letter $i$ to refer to variables of the index sort, letter $e$ to refer to variables of the element sort, letter $x$ to refer to variables of sort set, letter $k$ to refer to a variable of the integer sort and letter $a$ to refer to a variable of the array sort. The logic has as atoms set interpretations of the form $\{i | \varphi(\bar{a}[i], \bar{e})\}$ where $\bar{a}$ is a set of array variables, $\bar{a}[i]$ denotes the set of elements in the $i$-th component of the array variables, $\bar{e}$ is a set of constants of the element sort and $\varphi$ is an uninterpreted first-order formula over the element sort. These set interpretations are combined with Boolean algebra expressions and cardinality constraints. The semantics of these symbols is the standard.

$$ 
\begin{align*}
F ::= & A \mid F_1 \land F_2 \mid F_1 \lor F_2 \mid \neg F \\
A ::= & a[i] = e \mid i_1 = i_2 \mid i \in B \mid B_1 = B_2 \mid B_1 \subseteq B_2 \mid T_1 = T_2 \mid T_1 < T_2 \\
B ::= & x \mid \emptyset \mid B_1 \cup B_2 \mid B_1 \cap B_2 \mid B_1 \setminus B_2 \mid \{i \mid \varphi(\bar{a}[i], \bar{e})\} \\
T ::= & k \mid K \mid T_1 + T_2 \mid K \cdot T \mid |B| \\
K ::= & \dots \mid -2 \mid -1 \mid 0 \mid 1 \mid 2 \mid \dots
\end{align*}
$$

<caption>Fig. 3. $T_F$'s syntax</caption>

# 4 Politeness of Combinatory Array Logic

## 4.1 Smoothness

**Proposition 3.** Let $\mathcal{A}$ be a $T_{CAL}$-interpretation satisfying a conjunction $\Gamma$ of flat $\Sigma_{CAL}$-literals. Then there exists a $T_{CAL}$-interpretation $\mathcal{B}$ satisfying $\Gamma$ such that $|B_{elem}| = |A_{elem}|$ and $|B_{index}| = \kappa$, for each cardinal number $\kappa > |A_{index}|$.

*Proof.* Let $V_\sigma = \text{vars}_\sigma(\Gamma)$, for $\sigma \in \{\text{elem, index, array}\}$. We construct a $T_{CAL}$-interpretation $\mathcal{B}$ over $V_{elem} \cup V_{index} \cup V_{array}$ as follows. Fix a set $A'$ (disjoint from $A_{index}$) such that $|A_{index} \cup A'| = \kappa$, and let $B_{index} = A_{index} \cup A'$, $B_{elem} = A_{elem}$ and $i^\mathcal{B} = i^\mathcal{A}$ for each index-variable $i \in V_{index}$ and $e^\mathcal{B} = e^\mathcal{A}$ for each element variable $e \in V_{elem}$. In order to define $\mathcal{B}$ over the array-variables, observe that by definition of the semantics the index set is non-empty. Thus, we may fix some index $i_0 \in A_{index}$, and for each array-variable $a \in V_{array}$, we let

$$ a^{\mathcal{B}}(i) = \begin{cases} a^{\mathcal{A}}(i), & \text{if } i \in A_{\text{index}} \\ a^{\mathcal{A}}(i_0), & \text{otherwise} \end{cases} $$

By construction, $\mathcal{B}$ is a $T_{CAL}$-interpretation such that $|B_{elem}| = |A_{elem}|$ and $|B_{index}| = \kappa$. Next, we show that $\mathcal{B}$ satisfies all literals in $\Gamma$.
- Literals of the form $R(a_1, \dots, a_n)$: Let $i \in B_{\text{index}}$.

If $i \in A_{\text{index}}$ then $R(a_1^B(i), \dots, a_n^B(i)) = R(a_1^A(i), \dots, a_n^A(i))$.

If $i \notin A_{\text{index}}$ then $R(a_1^B(i), \dots, a_n^B(i)) = R(a_1^A(i_0), \dots, a_n^A(i_0))$.

Since we assume that $A \models R(a_1, \dots, a_n)$, it follows that $B \models R(a_1, \dots, a_n)$.

- Literals of the form $\neg R(a_1, \dots, a_n)$:

Since $\neg R(a_1^A, \dots, a_n^A)$, there exists $i \in A_{\text{index}}$ such that $\neg R(a_1^A(i), \dots, a_n^A(i))$.

It follows that $\neg R(a_1^B(i), \dots, a_n^B(i))$, which implies $\neg R(a_1^B, \dots, a_n^B)$.

- Literals of the form $e = a[i]$:

$$e^B = e^A = [a[i]]^A = a^A(i^A) = a^B(i^B) \quad \text{since } i^A \in A_{\text{index}}$$

- Literals of the form $a = \text{write}(b, i, e)$:

Let $j \in B_{\text{index}}$.

If $j = i^B$ then $a^B(i^B) = a^A(i^A) = e^A = e^B$.

If $j \in A_{\text{index}}$ then $a^B(j) = a^A(j) = b^A(j) = b^B(j)$.

If $j \notin A_{\text{index}}$ and $i_0 \neq i^B$ then $a^B(j) = a^A(i_0) = b^B(j)$.

If $j \notin A_{\text{index}}$ and $i_0 = i^B$ then $a^B(j) = a^A(i_0) = e^A = b^A(i_0) = b^B(j)$.

**Proposition 4.** Let $\mathcal{A}$ be a $T_{\text{CAL}}$-interpretation satisfying a conjunction $\Gamma$ of flat $\Sigma_{\text{CAL}}$-literals. Then there exists a $T_{\text{CAL}}$-interpretation $\mathcal{B}$ satisfying $\Gamma$ such that $|B_{\text{index}}| = |A_{\text{index}}|$ and $|B_{\text{elem}}| = \kappa$, for each $\kappa > |A_{\text{elem}}|$.

*Proof.* Similar to the proof of Proposition 3, we construct an interpretation on the variables by adding new points to the elements' carrier. In this case, the interpretation of the array variables is as in the original model. The new structure satisfies all the literals since the new values do not occur in the interpretation of the literals.

**Corollary 1 (Smoothness).** The theory $T_{\text{CAL}}$ is smooth w.r.t. $\{\text{elem}, \text{index}\}$.

## 4.2 Finite Witnessability

A witness function witness$_{CAL}$ for the theory $T_{\text{CAL}}$ can be defined as follows. Without loss of generality, let $\Gamma$ be a conjunction of flat $\Sigma_{\text{CAL}}$-literals such that $\text{vars}_{\text{index}}(\Gamma) \neq \emptyset$ and $\text{vars}_{\text{elem}}(\Gamma) \neq \emptyset$. We let witness$_{CAL}(\Gamma)$ be the result of applying to $\Gamma$ the following transformation:

1. Replace each literal of the form $\neg R(a_1, \dots, a_n)$ in $\Gamma$ with a literal of the form $\neg R(a_1[i], \dots, a_n[i])$, where $i$ is a fresh index-variable.

2. For each array index $i$ and each array variable $a$ used in the formula, add formulas $a[i] = e_i$ where $e_i$ is a fresh element variable.

3. Substitute other occurrences of the terms $a[i]$ by the element variable $e_i$ introduced in Step 2 (to ensure that the shape of the literals is as in Proposition 5).

*Remark 1.* Let $\Gamma$ be a conjunction of flat $\Sigma_{\text{CAL}}$-literals, let $\Delta = \text{witness}_{\text{CAL}}(\Gamma)$, and let $\bar{v} = \text{vars}(\Delta) \setminus \text{vars}(\Gamma)$. Then $\Gamma$ and $(\exists \bar{v})\Delta$ are $T_{\text{CAL}}$-equivalent.

**Proposition 5.** Let $\Gamma$ be a conjunction of flat $\Sigma_{\text{CAL}}$-literals such that
- vars<sub>index</sub>(Γ) ≠ ∅ and vars<sub>elem</sub>(Γ) ≠ ∅, and

- not containing any literal of the form ¬R(a₁, ..., aₙ).

- where each array read occurs in an equality with an element variable.

Then the following are equivalent:

1. Γ is T<sub>CAL</sub>-satisfiable.

2. There exists a T<sub>CAL</sub>-interpretation A satisfying Γ such that

$$
A_{\text{index}} = [\text{vars}_{\text{index}}(\Gamma)]^A \text{ and } A_{\text{elem}} = [\text{vars}_{\text{elem}}(\Gamma)]^A
$$

Proof. (2 ⇒ 1). Immediate.

(1 ⇒ 2). Let V<sub>σ</sub> = vars<sub>σ</sub>(Γ), for σ ∈ {elem, index, array}. Since Γ is T<sub>CAL</sub>-satisfiable, there exists a T<sub>CAL</sub>-interpretation B satisfying Γ. Let A be the T<sub>CAL</sub>-interpretation over V<sub>elem</sub> ∪ V<sub>index</sub> ∪ V<sub>array</sub> constructed as follows.

Let $A_{\text{index}} = V_{\text{index}}^{\mathcal{B}}$, $A_{\text{elem}} = V_{\text{elem}}^{\mathcal{B}}$, $i^{\mathcal{A}} = i^{\mathcal{B}}$, for each index-variable $i \in V_{\text{index}}$, $e^{\mathcal{A}} = e^{\mathcal{B}}$ for each element variable $e \in V_{\text{elem}}$ and $k^{\mathcal{A}} = k^{\mathcal{B}}$ for each integer variable $k \in V_{\text{int}}$. For each $a \in V_{\text{array}}$ and $i \in V_{\text{index}}$, let $a^{\mathcal{A}}(i^{\mathcal{A}}) = a^{\mathcal{B}}(i^{\mathcal{B}}) \in A_{\text{elem}}$.

Note that $\mathcal{A}$ is a well-defined $T_{\text{CAL}}$-interpretation, and that $A_{\sigma} = [\text{vars}_{\sigma}(\Gamma)]^{\mathcal{A}}$, for $\sigma \in \{\text{index, elem}\}$. Next, we show that $\mathcal{A}$ satisfies all literals in $\Gamma$.

- Literals of the form R(a₁, ..., aₙ): for i ∈ A<sub>index</sub>,

$$
R(a_1^A (i^A), \dots, a_n^A (i^A)) = R(a_1^B (i^B), \dots, a_n^B (i^B))
$$

- Literals of the form e = a[i]: e<sup>A</sup> = e<sup>B</sup> = [a[i]]<sup>B</sup> = a<sup>B</sup>(i<sup>B</sup>) = a<sup>A</sup>(i<sup>A</sup>)

- Literals of the form a = write(b, i, e):

- If j = i^A then a^A(i^A) = b^B(i^B) = e^B = e^A.

- If $j \in A_{\text{index}} \setminus \{i^A\}$ then $a^A(j^A) = a^B(j^B) = b^B(j^B) = b^A(j^A)$.

**Proposition 6 (Additivity).** *T<sub>CAL</sub> is additively finitely witnessable w.r.t. any nonempty set of sorts S ⊆ {elem, index}.*

*Proof.* It follows directly from the definition of additivity. We show that $f$ = witness<sub>CAL</sub>(Γ) is *S*-additive. To this end, let $\phi$, $\varphi$ be two quantifier-free formulas over CAL's signature such that $\varphi$ is a conjunction of flat literals where every term is a variable whose sort is in *S*. Then $f(f(\phi) \wedge \varphi)$ and $f(\phi) \wedge \varphi$

- are T<sub>CAL</sub>- equivalent: $f(f(\phi) \wedge \varphi) = f(f(\phi)) \wedge f(\varphi) = f(\phi) \wedge \varphi$.

- have the same set of *S*-sorted variables.

**Proposition 7 (Finite witnessability).** *The theory T<sub>CAL</sub> is additively finite witnessable with respect to {elem, index}.*

*Proof.* By Proposition 2, Remark 1, and the additivity of witness<sub>CAL</sub>.

By Corollary 1 and Proposition 7, we get:

**Theorem 1 (Politeness).** *The theory T<sub>CAL</sub> is strongly polite with respect to {elem, index}.*
# 5 Politeness of Sets with Cardinalities

We will now discuss the politeness of theories of sets that use cardinality constraints. Several such theories exist in the literature, including Zarba's fragment [22], Kunčak-Rinard's fragment [8] and Bansal et al.'s fragment [2, 3].

The fragment of [8] is not polite with respect to the index sort. This fragment includes syntax to denote the universe set $\mathcal{U}$, to denote the absolute complement of a set $S$, i.e. the set $\mathcal{U} \setminus S$ and an integer constant denoting the cardinality of $\mathcal{U}$. A formula of the form $|\mathcal{U}| = 3$ immediately shows that this theory is not smooth with respect to the index sort.

We will show that the theories [2,3,22] are polite with respect to the index sort. For smoothness, observe that the complement of the set variables in a formula cannot be used [2,3,22] (thus the definition of a “place” in [22] requiring at least one output equal to one). For finite witnessability, observe that one needs to introduce as many index variables as indicated by the minimal size of the universe. [2,3] left the politeness of this theory for future work.

## 5.1 Smoothness

**Proposition 8.** Let $\mathcal{A}$ be a $T_Z$-interpretation satisfying a conjunction $\Gamma$ of flat $\Sigma_Z$-literals. Then there exists a $T_Z$-interpretation $\mathcal{B}$ satisfying $\Gamma$ such that $|B_{\text{index}}| = \kappa$, for each $\kappa > |A_{\text{index}}|$.

*Proof*. Let $V_\sigma = \text{vars}_\sigma(\Gamma)$, for $\sigma \in \{\text{index, set, int}\}$. Construct a $T_Z$-interpretation $\mathcal{B}$ over $V_{\text{index}} \cup V_{\text{set}} \cup V_{\text{int}}$ as follows. Fix a set $A'$ such that $|A_{\text{index}} \cup A'| = \kappa$, let $B_{\text{index}} = A_{\text{index}} \cup A'$, $i^\mathcal{B} = i^\mathcal{A}$, for each index-variable $i \in V_{\text{index}}$, $x^\mathcal{B} = x^\mathcal{A}$, for each set-variable $x \in V_{\text{set}}$ and $s^\mathcal{B} = s^\mathcal{A}$, for each integer variable $s \in V_{\text{int}}$. By construction $\mathcal{B}$ is a $T_Z$-interpretation such that $|B_{\text{index}}| = \kappa$. Moreover, $\mathcal{B}$ satisfies all literals in $\Gamma$, since the newly introduced indices in $A'$ belong to the complement of the union of all the interpretations of the set variables of the formula, which is unconstrained as we are using the relative complement of sets.

**Corollary 2 (Smoothness).** The theory $T_Z$ is smooth with respect to index.

## 5.2 Finite Witnessability

**Witness Function.** A witness function $\text{witness}_Z$ for the theory $T_Z$ can be defined as follows. Without loss of generality, let $\Gamma$ be a conjunction of flat $\Sigma_Z$-literals such that $\text{vars}_{\text{index}}(\Gamma) \neq \emptyset$. $\text{witness}_Z(\Gamma)$ outputs the conjunction of $\Gamma$ and the result of the following transformation.

1. Replace index variables $i$ with singleton sets $\{i\}$ and impose $|\{i\}| = 1$.

2. Replace formulas $i \in x$ by $\{i\} \cap x = \{i\}$ and $i \notin x$ by $\{i\} \cap x = \emptyset$.

3. Replace $i_1 = i_2$ by $\{i_1\} = \{i_2\}$ and $i_1 \neq i_2$ by $\{i_1\} \neq \{i_2\}$.

4. Replace $x = y$ by $x \subseteq y \land y \subseteq x$ and $x \subseteq y$ by $|x \setminus y| = 0$.

5. Replace $x \neq y$ by $|x \setminus y \cup y \setminus x| > 0$ and $x \not\subseteq y$ by $|x \setminus y| > 0$.
6. We set up a linear integer programming problem obtained from applying the Venn region decomposition for each Boolean algebra expression $B_i$ appearing in an equation of the form $|B_i| = k$. Doing this for every such equation, we get a formula

$$G \wedge \bigwedge_{j=1}^{2^n} l_{\beta_j} \ge 0 \wedge \bigwedge_{i=0}^{p} \sum_{j=1}^{2^n} [[B_i]]_{\beta_j} \cdot l_{\beta_j} = k_i$$

where G is the quantifier-free Presburger arithmetic formula resulting from the original by substituting each occurrence of an expression $|B_i|$ by $k_i$, each bit-number $\beta_j$ viewed as a bit-string in $\{0, 1\}^n$ represents the elementary Venn region $E_{\beta_j} = S_1^{\beta_j(1)} \cap \dots \cap S_n^{\beta_j(n)}$ over the set variables $S_1, \dots, S_n$ occurring in the formula (where $S^0 := S^c$ and $S^1 := S$), $l_{\beta_j}$ represents the cardinality of $E_{\beta_j}$ and $[[B_i]]_{\beta_j}$ equals one when $E_{\beta_j} \subseteq B_i$ and zero otherwise.

7. The linear integer program minimises the linear function $\sum_{j=0}^{2^n-1} l_{\beta_j}$.

8. We solve the linear integer program. If there is no solution, we output the formula $\perp$. Otherwise, let $s$ be the minimal solution for the linear integer program. For each family of cardinalities $l_{\beta_j}$ of the elementary Venn regions such that $s = \sum_{j=0}^{2^n-1} l_{\beta_j}$, we check the system of cardinality constraints together with the requirement that the set $E_{\beta_j}$ has cardinality at least $l_{\beta_j}$ is satisfiable. For each such family, we build the following formula.

- We introduce for each elementary Venn region $E_{\beta_j}$, $l_{\beta_j}$ index variables $g$ and require that they are mutually distinct with atoms of the form $g_1 \neq g_2$ and that they belong to $E_{\beta_j}$, with atoms of the form $g \in E_{\beta_j}$.

- Rewrite the terms $g \in E_{(0,...,0)}$ into $g \notin S_1 \cup \dots \cup S_n$ and absolute complements $S^c$ as relative complements $(S_1 \cup \dots \cup S_n) \setminus S$, so that the resulting formula contains no absolute complements (not supported in the fragment of [22]).

9. We output the disjunction of the formulas constructed in the previous step.

**Proposition 9.** Let $\Gamma$ be a conjunction of flat $\Sigma$-literals, let $\Delta = witness_Z(\Gamma)$, and let $\bar{v} = vars(\Delta) \setminus vars(\Gamma)$. Then $\Gamma$ and $(\exists \bar{v})\Delta$ are $T_Z$-equivalent.

*Proof.* Indeed, if $\mathcal{A}$ is a model of $\Gamma$ then it contains at least $s$ elements. Moreover, any such collection of $s$ elements satisfies the disjunction introduced in Step 9. Thus, $\mathcal{A}$ satisfies $(\exists \bar{v})\Delta$. The converse direction is trivial since $\Gamma$ is part of $\Delta$.

**Proposition 10.** Let $\Gamma$ be a conjunction of flat $\Sigma$-literals with $vars_{index}(\Gamma) \neq \emptyset$. If $\Delta$ is $T_Z$-satisfiable then there exists a $T_Z$-interpretation $\mathcal{A}$ satisfying $\Delta$ such that $A_{index} = [vars_{index}(\Gamma)]^\mathcal{A}$.

*Proof.* If $\Delta$ is $T_Z$-satisfiable then it is also satisfied by a structure $\mathcal{A}$ of minimal index-set size $s$. Since $\Delta$ requires the existence of $s$ distinct indices, it follows that the interpretations of the indices of the formula yield the carrier set of the index sort in $\mathcal{A}$.

We next show that the witness function as given is not additive.
**Example 1.** On input $i_1 \in S \land i_2 \in S$, the witness procedure would output $i_1 \in S \land i_2 \in S \land g \in S$. Now, if we take $i_1 \neq i_2$ as a second formula in the definition of additivity. Then the output of the witness function applied to the formula $i_1 \in S \land i_2 \in S \land g \in S \land i_1 \neq i_2$ is $i_1 \in S \land i_2 \in S \land g_1 \in S \land g_2 \in S \land i_1 \neq i_2 \land g_1 \neq g_2$, which is not equivalent to $i_1 \in S \land i_2 \in S \land g \in S$.

We next give an additive modification of the witness function.

**Proposition 11 (Additivity).** $T_Z$ is additively finitely witnessable w.r.t. index.

*Proof.* Consider the function $f$ defined as follows for any input formula $\phi$:

- if $\phi$ is not arranged then output the disjunction of applying $f$ to $\text{arr} \land \phi$ for each arrangement $\text{arr}$ of the index variables in $\phi$.

- if $\phi$ is a $T_Z$-satisfiable formula of the form $\phi' \land \varphi$, where $\phi'$ is a witness formula of some arranged input and $\varphi$ is a conjunction of literals between index variables such that $\text{vars}_{\text{index}}(\varphi) \subseteq \text{vars}_{\text{index}}(\phi')$, then $f(\phi) = \phi$;

- if $\phi$ is a $T_Z$-satisfiable formula of the form $\phi' \land \varphi'$, where $\phi'$ is a conjunction of literals between index variables $x, y$ such that $x \notin \text{vars}_{\text{index}}(\phi')$ or $y \notin \text{vars}_{\text{index}}(\phi')$, then $f(\phi) = f(\phi') \land \varphi'$;

- otherwise, $f(\phi) = \text{witness}_Z(\phi)$.

According to this definition of $f$ and using $\varphi$ and $\varphi'$ as introduced above, we have

$$f(f(\phi) \land \varphi \land \varphi') = f(f(\phi) \land \varphi) \land \varphi' = f(\phi) \land \varphi \land \varphi'$$

Consequently, $f$ is index-additive.

**Proposition 12 (Finite witnessability).** The theory $T_Z$ is additively finitely witnessable with respect to the sort index.

*Proof.* By Propositions 2, 9, 10, and 11.

By Corollary 2 and Proposition 12, we get:

**Theorem 2 (Politeness).** The theory $T_Z$ is strongly polite with respect to the sort index.

# 6 Politeness for Theories with Set Interpretations

We will now discuss the politeness of theories of sets that use cardinality constraints and set interpretations. A technical condition is required in order to show smoothness with respect to the sort index. This condition allows us to enlarge theories' models in the Venn region determined by the complement of all set variables. We focus on the satisfiability problem of a subtheory of $T_F$ that fixes the formulas under set interpretations, is closed under propositional operations and satisfies the technical condition. The polite combination method is applicable to this subtheory.

**Definition 3.** If $\varphi_1, \dots, \varphi_n$ are the formulas under set interpretations in the $T_F$-formula $\varphi$, $\text{cl}(\varphi_1, \dots, \varphi_n)$ denotes the sentence $\exists \vec{v}. \bigwedge_{i=1}^n \neg \varphi_i(\vec{v}, \vec{c})$. Assuming that $\text{cl}(\varphi_1, \dots, \varphi_n)$ is $T_F$-satisfiable, the theory $T_F(\varphi_1, \dots, \varphi_n)$ is the set of $\Sigma_F$-sentences $\varphi$ such that the formulas under set interpretations in $\varphi$ are in $\varphi_1, \dots, \varphi_n$, and $T_F \cup \{\text{cl}(\varphi_1, \dots, \varphi_n)\} \models \varphi$.
## 6.1 Smoothness

**Proposition 13.** Let $\mathcal{A}$ be a $T_F$-interpretation satisfying a conjunction $\Gamma$ of flat $\Sigma_F$-literals in $T_F(\varphi_1, \dots, \varphi_n)$. Then there exists a $T_F$-interpretation $\mathcal{B}$ satisfying $\Gamma$ such that $|B_{elem}| = |A_{elem}|$ and $|B_{index}| = \kappa$, for each cardinal number $\kappa > |A_{index}|$.

*Proof.* Let $V_\sigma = \text{vars}_\sigma(\Gamma)$, for $\sigma \in \{\text{elem, index, array, set, int}\}$. We construct a $T_F$-interpretation $\mathcal{B}$ over $V_{elem} \cup V_{index} \cup V_{array} \cup V_{set} \cup V_{int}$ as follows. Fix a set $A'$ such that $|A_{index} \cup A'| = \kappa$, and let $B_{index} = A_{index} \cup A'$, $B_{elem} = A_{elem}$ and $i^B = i^A$ for each index-variable $i \in V_{index}$, $e^B = e^A$ for each elem-variable $e \in V_{elem}$, $s^B = s^A$ for each set-variable $s \in V_{set}$ and $k^B = k^A$ for each integer-variable $k \in V_{int}$.

In order to define $\mathcal{B}$ over the array-variables, observe that by Definition 3, if we list all the $m$ formulas $\varphi_j(\bar{a}[i], \bar{c})$ occurring in set interpretations in $\Gamma$, then the formula $\exists \bar{v}. \bigwedge_{j=1}^n \neg \varphi_j(\bar{v}, \bar{c})$ is true. This gives us a value $\bar{v}_0$ such that the formula $\bigwedge_{j=1}^n \neg \varphi_j(\bar{v}_0, \bar{c})$ is true. Observe that we may define as $\bar{v}_0$ the set of values at the newly introduced indices. This is because the formula only restricts indices values on the union of set interpretations. Thus, for each array-variable $a \in V_{array}$, we let

$$a^B(i) = \begin{cases} a^A(i) & \text{if } i \in A_{index} \\ (\bar{v}_0)_j & \text{where } a = (\bar{a})_j \end{cases}$$

By construction, $\mathcal{B}$ is a $T_F$-interpretation such that $|B_{elem}| = |A_{elem}|$ and $|B_{index}| = \kappa$. Next, we show that $\mathcal{B}$ satisfies all literals in $\Gamma$.

- Literals of the form $R(e_1, \dots, e_n)$, $R(i_1, \dots, i_n)$ or $R(k_1, \dots, k_n)$: immediate.

- Literals of the form $|S| = k$: immediate by definition of $\mathcal{B}$.

- Literals of the form $S = \{i | \varphi(\bar{a}[i], \bar{c})\}$: Let $i \in B_{index}$.

If $i \in A_{index}$ then $\varphi(a_1^B(i), \dots, a_n^B(i)) = \varphi(a_1^A(i), \dots, a_n^A(i))$.

If $i \notin A_{index}$ then $\varphi(a_1^B(i), \dots, a_n^B(i)) = \varphi((\bar{v}_0)_1(i), \dots, (\bar{v}_0)_n(i)) = \perp$.

Since $A \models S = \{i | \varphi(\bar{a}[i], \bar{c})\}$, $S^A = S^B$ and we have that $\{i | \varphi(\bar{a}[i], \bar{c})\}^A = \{i | \varphi(\bar{a}[i], \bar{c})\}^B$, it follows that $B \models S = \{i | \varphi(\bar{a}[i], \bar{c})\}$.

- Literals of the form $e = a[i]$:

$$e^B = e^A = [a[i]]^A = a^A(i^A) = a^B(i^B) \quad \text{since } i^A \in A_{index}$$

□

**Proposition 14.** Let $\mathcal{A}$ be a $T_F$-interpretation satisfying a conjunction $\Gamma$ of flat $\Sigma_F$-literals. Then there exists a $T_F$-interpretation $\mathcal{B}$ satisfying $\Gamma$ such that $|B_{index}| = |A_{index}|$ and $|B_{elem}| = \kappa$, for each $\kappa > |A_{elem}|$.

*Proof.* Similar to the proof of Proposition 4, we construct an interpretation on the variables by adding new points to the elements' carrier. The interpretation of the array variables is as in the original model. The new structure satisfies all the literals since the new values do not occur in the interpretation of the literals.
**Corollary 3 (Smoothness).**

- $T_F$ is smooth w.r.t. elem.

- $T_F(\varphi_1, \dots, \varphi_n)$ is smooth w.r.t. $\{\text{elem}, \text{index}\}$.

*Proof.* By Propositions 1, 13, and 14.

## 6.2 Finite Witnessability

**Witness Function.** A witness function $\text{witness}_F$ for the theory $T_F$ can be defined as follows. Without loss of generality, let $\Gamma$ be a conjunction of flat $\Sigma_F$-literals such that $\text{vars}_{\text{elem}}(\Gamma) \neq \emptyset$ and $\text{vars}_{\text{index}}(\Gamma) \neq \emptyset$. $\text{witness}_F(\Gamma)$ outputs the conjunction of $\Gamma$ and the result of the following transformation.

1-7. These steps are analogous to the ones for the theory of sets with cardinalities.

8. Each set variable $S$ in $\Gamma$ may be interpreted, i.e. $\Gamma$ contains an equation of the form $S = \{i \mid \varphi(\bar{a}[i], \bar{c})\}$, or uninterpreted, if no such equation exists. To each elementary Venn region $E_{\beta_j}$ we associate a formula $\varphi^{\beta_j} := \exists \bar{v}. \bigwedge_{i=1}^n \varphi^{\beta_j(i)}(\bar{v}, \bar{c})$, where $\varphi^{\beta_j(i)}$ is the formula in the set interpretation of $S_i$ if $\beta_j(i) = 1$, its negation if $\beta_j(i) = 0$ or $\top$ if $S_i$ is uninterpreted. For each $\beta_j \in \{0, 1\}^n$, we add the constraint $l_{\beta_j} = 0$ if $\varphi^{\beta_j}$ is unsatisfiable.

9. We solve the linear integer program. If there is no solution, we output the formula $\perp$. Otherwise, let $s$ be the minimal solution for the linear integer program. For each family of cardinalities $l_{\beta_j}$ of the elementary Venn regions such that $s = \sum_{j=0}^{2^n-1} l_{\beta_j}$, we check the system of cardinality constraints together with the requirement that the set $E_{\beta_j}$ has cardinality at least $l_{\beta_j}$ is satisfiable. For each such family, we build the following formula.

- We introduce for each elementary Venn region $E_{\beta_j}$, $l_{\beta_j}$ index variables $i$ and require that they are mutually distinct with atoms of the form $i_1 \neq i_2$ and that they belong to $E_{\beta_j}$, with atoms of the form $i \in E_{\beta_j}$.

- Rewrite the terms $i \in E_{(0,...,0)}$ into $i \notin S_1 \cup \dots \cup S_n$ and absolute complements $S^c$ as relative complements $(S_1 \cup \dots \cup S_n) \setminus S$, so that the resulting formula contains no absolute complements.

10. We output the disjunction of the formulas constructed in the previous step.

11. For each array index $i$ and each array variable $a$ used in the constructed formulas, add formulas $a[i] = e_i$ where $e_i$ is a fresh element variable.

**Proposition 15.** Let $\Gamma$ be a conjunction of flat $\Sigma_F$-literals, let $\Delta = \text{witness}_F(\Gamma)$, and let $\bar{v} = \text{vars}(\Delta) \setminus \text{vars}(\Gamma)$. Then $\Gamma$ and $(\exists \bar{v})\Delta$ are $T_F$-equivalent.

*Proof.* Indeed, if $\mathcal{A}$ is a model of $\Gamma$ then it contains at least $n$ elements. Moreover, there will be some distribution of these $s$ elements over the Venn diagram satisfying the disjunction introduced in Step 10 Thus, $\mathcal{A}$ satisfies $(\exists \bar{v})\Delta$. The converse direction is trivial since $\Gamma$ is part of $\Delta$.
**Proposition 16.** Let $\Gamma$ be a conjunction of flat $\Sigma_F$-literals such that $\text{vars}_{\text{elem}}(\Gamma) \neq \emptyset$ and $\text{vars}_{\text{index}}(\Gamma) \neq \emptyset$. If $\Delta$ is $T_F$-satisfiable then there exists a $T_F$-interpretation $\mathcal{A}$ satisfying $\Delta$ such that $A_{\text{index}} = [\text{vars}_{\text{index}}(\Gamma)]^A$ and $A_{\text{elem}} = [\text{vars}_{\text{elem}}(\Gamma)]^A$

*Proof.* If $\Delta$ is $T_F$-satisfiable then it is also satisfied by a structure $\mathcal{A}$ of minimal index-set size $s$. Since $\Delta$ requires the existence of $s$ distinct indices, it follows that the interpretations of the index variables yield the carrier set of the index sort in $\mathcal{A}$. Since all the array elements referenced by the indices are also in the formula, it follows that the interpretations of the element variables in the formula yield the carrier set of the element sort in $\mathcal{A}$.

**Proposition 17 (Additivity).** $T_F$ is additively finitely witnessable w.r.t. $\{\text{elem, index}\}$.

*Proof* The proof is analogous to the one given in Proposition 11.

**Proposition 18 (Finite witnessability).** The theory $T_F$ is additively finitely witnessable with respect to $\{\text{elem, index}\}$.

*Proof.* By Proposition 2, 15, 16 and 17.

By Corollary 3, Proposition 18, we get:

**Theorem 3 (Politeness).**

- $T_F$ is strongly polite with respect to elem.

- $T_F(\varphi_1, \dots, \varphi_n)$ is strongly polite w.r.t. $\{\text{elem, index}\}$.

# 7 Conclusion

We investigated the politeness of several theories of data structures introduced after the original work on the subject [14]. We proved that extending the quantifier-free theory of arrays with component-wise relations preserves politeness with respect to the index and element sorts. We showed the politeness properties for a variant of the theory of sets with cardinalities [22], reusing the idea of computing the minimal size of the universe for the finite witness function. [2] left the politeness of this theory for future work. We finally showed the politeness with respect to the index and element sorts of the simple flat array fragment [5]. When fixing the formulas in the set interpretations. An interesting research direction would be to compare our politeness results with the handling of finite structures in [11].
References

1. Alberti, F., Ghilardi, S., Pagani, E.: Cardinality constraints for arrays (decidability results and applications). Formal Methods Syst. Design **51**(3), 545–574 (2017). https://doi.org/10.1007/s10703-017-0279-6

2. Bansal, K., Barrett, C., Reynolds, A., Tinelli, C.: Reasoning with finite sets and cardinality constraints in SMT. Log. Methods Comput. Sci. **14**(4) (2018). https://doi.org/10.23638/LMCS-14(4:12)2018

3. Bansal, K., Reynolds, A., Barrett, C., Tinelli, C.: A new decision procedure for finite sets and cardinality constraints in SMT. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS (LNAI), vol. 9706, pp. 82–98. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-40229-1_7

4. Feferman, S., Vaught, R.: The first order properties of products of algebraic systems. Fundam. Math. **47**(1), 57–103 (1959)

5. Ghilardi, S., Pagani, E.: Higher-order quantifier elimination, counter simulations and fault-tolerant systems. J. Autom. Reason. **65**(3), 425–460 (2020). https://doi.org/10.1007/s10817-020-09578-5

6. Hodges, W.: Model Theory. Encyclopedia of Mathematics and its Applications. Cambridge University Press, Cambridge (1993)

7. Jovanović, D., Barrett, C.: Polite theories revisited. In: Fermüller, C.G., Voronkov, A. (eds.) LPAR 2010. LNCS, vol. 6397, pp. 402–416. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-16242-8_29

8. Kuncak, V., Rinard, M.: Towards efficient satisfiability checking for Boolean algebra with Presburger arithmetic. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 215–230. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73595-3_15

9. Mostowski, A.: On direct products of theories. J. Symb. Log. **17**(1), 1–31 (1952). https://doi.org/10.2307/2267454

10. de Moura, L., Bjørner, N.: Generalized, efficient array decision procedures. In: 2009 Formal Methods in Computer-Aided Design, pp. 45–52. IEEE, Austin (2009). https://doi.org/10.1109/FMCAD.2009.5351142

11. de Moura, L., Bjørner, N.: Model-based theory combination. Electron. Notes Theor. Comput. Sci. **198**(2), 37–49 (2008). https://doi.org/10.1016/j.entcs.2008.04.079

12. Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Trans. Program. Lang. Syst. **1**(2), 245–257 (1979). https://doi.org/10.1145/357073.357079

13. Piskac, R., Kuncak, V.: Decision procedures for multisets with cardinality constraints. In: Logozzo, F., Peled, D.A., Zuck, L.D. (eds.) VMCAI 2008. LNCS, vol. 4905, pp. 218–232. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78163-9_20

14. Ranise, S., Ringeissen, C., Zarba, C.G.: Combining data structures with nonstably infinite theories using many-sorted logic. In: Gramlich, B. (ed.) FroCoS 2005. LNCS (LNAI), vol. 3717, pp. 48–64. Springer, Heidelberg (2005). https://doi.org/10.1007/11559306_3

15. Ranise, S., Ringeissen, C., Zarba, C.G.: Combining data structures with nonstably infinite theories using many-sorted logic. Rapport de recherche 5678, INRIA (2005)

16. Raya, R., Kunčak, V.: NP satisfiability for arrays as powers. In: Finkbeiner, B., Wies, T. (eds.) VMCAI 2022. LNCS, vol. 13182, pp. 301–318. Springer, Cham (2022). https://doi.org/10.1007/978-3-030-94583-1_15
17. Raya, R., Kunčak, V.: Succinct ordering and aggregation constraints in algebraic array theories. J. Log. Algebraic Methods Program. **140**, 100978 (2024). https://doi.org/10.1016/j.jlamp.2024.100978

18. Sheng, Y., et al.: Reasoning about vectors using an SMT theory of sequences. In: Blanchette, J., Kovács, L., Pattinson, D. (eds.) IJCAR 2022. LNCS, vol. 13385, pp. 125–143. Springer, Cham (2022). https://doi.org/10.1007/978-3-031-10769-6_9

19. Sheng, Y., Zohar, Y., Ringeissen, C., Lange, J., Fontaine, P., Barrett, C.: Polite combination of algebraic datatypes. J. Autom. Reason. **66**(3), 331–355 (2022). https://doi.org/10.1007/s10817-022-09625-3

20. Stump, A., Barrett, C., Dill, D., Levitt, J.: A decision procedure for an extensional theory of arrays. In: Proceedings 16th Annual IEEE Symposium on Logic in Computer Science, pp. 29–37. IEEE Computer Society, Boston (2001). https://doi.org/10.1109/LICS.2001.932480

21. Wies, T., Piskac, R., Kuncak, V.: Combining theories with shared set operations. In: Ghilardi, S., Sebastiani, R. (eds.) FroCoS 2009. LNCS (LNAI), vol. 5749, pp. 366–382. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-04222-5_23

22. Zarba, C.G.: Combining sets with cardinals. J. Autom. Reason. **34**(1), 1–29 (2005). https://doi.org/10.1007/s10817-005-3075-8

**Open Access** This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
# Number Theory Combination: Natural Density and SMT

Guilherme V. Toledo(✉) and Yoni Zohar

Bar-Ilan University, Ramat Gan, Israel

guivtoledo@gmail.com

**Abstract.** The study of theory combination in Satisfiability Modulo Theories (SMT) involves various model theoretic properties (e.g., stable infiniteness, smoothness, etc.). We show that such properties can be partly captured by the natural density of the spectrum of the studied theories, which is the set of sizes of their finite models. This enriches the toolbox of the theory combination researcher, by providing new tools to determine the possibility of combining theories. It also reveals interesting and surprising connections between theory combination and number theory.

## 1 Introduction

Imagine this: you are a researcher in Satisfiability Modulo Theories (SMT) [2], studying a theory $\mathcal{T}$, which is the combination of theories $\mathcal{T}_1$ and $\mathcal{T}_2$ (in the same way that, say, the theory of lists of integers is the combination of the theories of lists and integers). Given algorithms for $\mathcal{T}_1$ and $\mathcal{T}_2$, you can plug them together using theory combination methods, such as Nelson and Oppen's method [12], polite combination [14], shiny combination [20], or gentle combination [8].

But, before you can produce a decision procedure for $\mathcal{T}$, you must test certain properties of $\mathcal{T}_1$ and $\mathcal{T}_2$, or their absence, to determine their applicability to the combination method. For example, using the Nelson-Oppen method requires that both theories are stably infinite, while using the polite combination method requires that one of them is strongly polite. The obvious way of doing so is by directly applying the definitions of these properties, what can be highly non-trivial (for example, to prove a theory is strongly polite, one needs to construct a computable function satisfying an involved set of conditions).

In this paper, we give you alternative tests, based on number theoretic *natural densities* [19], computed over the *spectrum* of the theory [10]. When testing whether a theory admits or lacks a theory combination property, you can now use these tests. We provide examples for cases where this is simpler to do, compared to the direct application of the definitions. Beyond the introduction of such tools, the results of this paper relate number theory and theory combination in surprising and insightful ways. We focus on one-sorted theories, leaving many-sorted ones for future work.
Section 2 surveys relevant notions. Section 3 contains our main results: sufficient and necessary conditions for theory combination properties, in terms of the natural density, our most involved (and perhaps more interesting) results being found in Sect. 3.2.4 and 3.2.5; we also have in Sect. 3.2.1 important results relating gentleness to politeness, shininess and stable infiniteness. In Sect. 4 we provide generalizations to non-empty signatures. Section 5 summarizes, and gives directions for future research.

## Related Work

### 0-1-Laws and Densities.
Studies on spectra and densities go back as far as [4, 7, 9]. While we consider only models of a theory, these results, including the famous 0-1 laws, concern random models, that is, any models. 0-1 laws remain powerful for theories with finite axiomatizations (as we can represent their axiomatizations using a conjunction), but here we consider also infinite axiomatizations. Later studies, such as [3, 5], considered densities with respect to a theory, or even a (sufficiently well-behaved) class of models, but have not considered properties associated with theory combination. We focus on theories, and on the relationship between their combination properties and the behavior of their density.

### Descriptive Complexity.
Note that we use slightly different definitions for the spectrum of a theory than those found in descriptive complexity [10]: although our definition of $Spec(T, \phi)$ is the usual one for the spectrum of a formula relative to a theory, the spectrum of a theory $T$ is more commonly understood as the map from cardinals to cardinals which, given $\kappa$, returns the number of non-isomorphic models of $T$ of cardinality $\kappa$. But for the case of finite cardinalities in the empty signature this map would return either 0 or 1. Then, our definition coincides with taking the pre-image of 1 in the more standard definition.

### Theory Combination Properties.
The current paper deals with, among other topics, Boolean combinations of theory combination properties (especially in Table 1), something comprehensively researched in [23, 25, 26]. While those papers study the combinations of properties per se, here we focus on establishing these properties (or lack of) through the analysis of their density.

## 2 Preliminaries

If $X$ is a set, $|X|$ denotes its cardinality. We denote by $\aleph_0$ the cardinality of $N$, which for us contains 0; the set $N \setminus \{0\}$ is denoted by $\mathbb{Z}^+$.

### 2.1 First-Order Logic

One can find a standard reference in first-order logic in [17]. A first-order signature $\Sigma$ is a pair $(\mathcal{F}_{\Sigma}, \mathcal{P}_{\Sigma})$, where: $\mathcal{F}_{\Sigma}$ is a countable set of function symbols, each with an arity $n \in N$; and $\mathcal{P}_{\Sigma}$ is a countable set of predicate symbols, each
with an arity $n \in \mathbb{N}$, containing at least the equality $=$ of arity 2. We denote by $\Sigma_1$ the signature with no function or predicate symbols other than $=$, which is therefore called *empty*. Assuming countably many variables, we define by structural induction terms, literals, formulas, and sentences (formulas without free variables) in the usual way. The set of all quantifier-free $\Sigma$-formulas is denoted by $QF(\Sigma)$; the set of all variables in $\varphi$ shall be written as $vars(\varphi)$.

A $\Sigma$-interpretation $\mathcal{A}$ consists of: a non-empty set $dom(\mathcal{A})$, called the domain of $\mathcal{A}$; for each function symbol $f$ of arity $n$, a function $f^A : dom(\mathcal{A})^n \to dom(\mathcal{A})$; for each predicate symbol $P$ of arity $n$, a subset $P^A$ of $dom(\mathcal{A})^n$, where $=$^A$ is the identity; and, for every variable $x$, an element $x^A$ of $dom(\mathcal{A})$. The value of a term $\alpha$ in $\mathcal{A}$ is denoted by $\alpha^A$, while for a set of terms $\Gamma$ we make $\Gamma^A = \{\alpha^A : \alpha \in \Gamma\}$; if $\mathcal{A}$ satisfies the formula $\varphi$, we write $\mathcal{A} \models \varphi$. Recurrent formulas include those in Fig. 1, that are satisfied by an interpretation $\mathcal{A}$ iff: $dom(\mathcal{A})$ has at least $n$ elements, in the case of $\psi_{\ge n}$; $dom(\mathcal{A})$ has at most $n$ elements, in the case of $\psi_{\le n}$; and $dom(\mathcal{A})$ has precisely $n$ elements, in the case of $\psi_{=n}$. Notice that $\psi_{\ge n}$ can be defined in terms of $\psi_{\le n}$, however we explicitly define both for greater clarity.

$$ \begin{array}{l@{\qquad}l} \#(x_1, \dots, x_n) = \bigwedge_{i=1}^{n-1} \bigwedge_{j=i+1}^{n} \neg(x_i = x_j) & \psi_{\le n} = \exists x_1, \dots, x_n. \forall y. \bigvee_{i=1}^{n} y = x_i \\ \psi_{\ge n} = \exists x_1 \dots x_n. \#(x_1, \dots, x_n) & \psi_{=n} = \psi_{\ge n} \wedge \psi_{\le n} \end{array} $$

<caption>Fig. 1. Cardinality formulas.</caption>

A *theory* is the class of all interpretations (thus called *T*-interpretations, or the models of *T*) satisfying some set of sentences $Ax(T)$ (which does not need to be computably enumerable), called the *axiomatization of T*. A formula $\varphi$ is then: (*T*)-satisfiable if there is a (*T*)-interpretation that satisfies $\varphi$; (*T*)-equivalent to a formula $\psi$ if every (*T*)-interpretation that satisfies one also satisfies the other; and (*T*)-valid if every (*T*)-interpretation satisfies $\varphi$, denoted $\models\varphi$ ($\models_T\varphi$).

We denote, for $n \le m$, the set $\{n, \dots, m\}$ by $[n, m]$; if $n=0$, we simplify it to $[m]$. Of course, $|[n, m]|=m-n+1$, and $|[m]|=m+1$. Furthermore, $A \cap \{1, n\}$ will be denoted by $A_n$; we denote $\{|dom(\mathcal{A})| : \mathcal{A}$ is a $T$-interpretation\} \cap \mathbb{N}$ by $Spec(T)$, and we define $Spec_n(T)$ as $Spec(T) \cap \{1, n\}$. Analogously, $Spec(T, \phi)$ is the set of finite cardinalities of $T$-interpretations that satisfy $\phi$. We can then also define $Spec_n(T, \phi)$ as $Spec(T, \phi) \cap \{1, n\}$.

## 2.2 Number Theory

The *natural density* [19] of a set $A \subseteq \mathbb{N}$ is the following real number, if the limit indeed exists (and then we say the density of $A$ exists): $\mu(A) = \lim_{n \to \infty} |A \cap \{n\}|/|A|.$
**Example 1.** Consider the set $\mathcal{A}$ of even non-negative integers: we then have that $\mu(\mathcal{A})$ is the limit of the sequence $a_n$ which equals $(n+2)/2(n+1)$ if $n$ is even, and $1/2$ if it is odd, meaning that $\mu(\mathcal{A})$ exists and equals $1/2$.

It is easy to prove that $\mu$ satisfies, for all disjoint sets $A$ and $B$ for which it is defined: $0 \le \mu(A)$; $\mu(\mathbb{N}) = 1$; and $\mu(A \cup B) = \mu(A) + \mu(B)$. The subsets of the non-negative integers we shall calculate the natural density of are sets of finite cardinalities of interpretations in a theory: since they are never zero (as we assume $dom(\mathcal{A})$ is never empty), we can change $\mu(A)$ to be the limit of the ratio of $|A \cap \{1, \dots, n\}|$ to $|\{1, \dots, n\}| = n$.<fnref n="1" /> With this, we can finally define the natural density of a theory (relative to a quantifier-free formula or not) as the natural density of its spectrum: $\mu(\mathcal{T}) = \lim_{n \to \infty} |\text{Spec}_n(\mathcal{T})|/|[1, n]|$, and $\mu(\mathcal{T}, \phi) = \lim_{n \to \infty} |\text{Spec}_n(\mathcal{T}, \phi)|/|[1, n]|$.

**Definition 1.** Let $r \in \mathbb{R}$. $r$ is computable $[2^\gamma]$ if there are computable sequences $\{a_n\}_{n \in \mathbb{N}}$ in $\mathbb{Z}$ and $\{b_n\}_{n \in \mathbb{N}}$ in $\mathbb{Z}^+$ with $\lim_{n \to \infty} a_n/b_n = r$.

**Example 2.** Every rational number $p/q$ is computable: just take $a_n=p$ and $b_n=q$. The number $\sum_{n=1}^{\infty} 2^{-c(n)} = 0.57824...$ is not computable, for $c$ the busy beaver function [13], which maps $n \in \mathbb{N}$ to the maximum number of 1's a Turing machine with at most $n$ states can write when it halts, assuming the tape begins with only 0's. Now, $0.57824...$ is the limit of $5/10, 57/100, 578/1000, ...$. Consider then the theory $\mathcal{T}$ with models of size 1 through 5, 11 through $52 = 57 - 5$, 101 through $521 = 578 - 57$, and so on. Its density is the limit of the fractions $5/10, 57/100, 578/1000$ and so on, i.e. $0.57824...$, although this number is irrational. More generally, any $0 \le r \le 1$ is the density of some theory.

## 2.3 Theory Combination

In what follows, let $\Sigma$ be an arbitrary signature and $\mathcal{T}$ be a $\Sigma$-theory.

$\mathcal{T}$ is **stably infinite** [12] if for every satisfiable quantifier-free formula $\phi$, there is a $\mathcal{T}$-interpretation $\mathcal{A}$ that satisfies $\phi$ with $|dom(\mathcal{A})| \ge \aleph_0$. $\mathcal{T}$ is **smooth** when, for all quantifier-free formulas $\phi$, $\mathcal{T}$-interpretations $\mathcal{A}$ that satisfy $\phi$, and cardinals $\kappa > |dom(\mathcal{A})|$, there exists a $\mathcal{T}$-interpretation $\mathcal{B}$ that satisfies $\phi$ with $|dom(\mathcal{B})| = \kappa$. Notice that being smooth implies being stably infinite.

$\mathcal{T}$ is **finitely witnessable** [14] when there is a computable function $wit$ (called a witness) from the quantifier-free formulas into themselves such that, for every quantifier-free formula $\phi$: (I) $\phi$ and $\exists \vec{x}. wit(\phi)$ are $\mathcal{T}$-equivalent, where $\vec{x} = vars(wit(\phi)) \setminus vars(\phi)$; and (II) if $wit(\phi)$ is $\mathcal{T}$-satisfiable, then there is a $\mathcal{T}$-interpretation $\mathcal{A}$ that satisfies $wit(\phi)$ and, in addition, $dom(\mathcal{A}) = vars(wit(\phi))^{\mathcal{A}}$ (that is, every element of $dom(\mathcal{A})$ is the interpretation of a variable in $wit(\phi)$). Now, given a finite set of variables $V$ on the signature $\Sigma$, and an equivalence $E$ on $V$, the **arrangement** on $V$ induced by $E$, written $\delta_V^E$ or $\delta_V$ if $E$ is clear from context, is the formula $\bigwedge_{x \in V} (x=y) \wedge \bigwedge_{x \in \bar{V}} \neg(x=y)$, where $\bar{V}$ is the complement of $E$. Intuitively, an arrangement codifies the relationships between a finite set

<footnote n="1">¹ Of course, this does not change the value of $\mu(A)$.</footnote>
of variables, that is, if they should be equal or different to one another. $\mathcal{T}$ is
then **strongly finitely witnessable** [11] if it has a witness *wit* (that in this
case will be called a strong witness) satisfying, in addition to $(I)$ and $(II)$, the
stronger $(II^*)$: for every finite set of variables $V$ and arrangement $\delta_V$ on $V$, if
$wit(\phi) \wedge \delta_V$ is $\mathcal{T}$-satisfiable, then there exists a $\mathcal{T}$-interpretation $\mathcal{A}$ that satisfies
that formula and, in addition, $dom(\mathcal{A}) = vars(wit(\phi) \wedge \delta_V)^A$.

*Example 3.* The theory axiomatized by {$\psi_{\le 3}$} has as strong witness $wit(\phi) = \phi \wedge \bigwedge_{i=1}^3 x_i = x_i$, where $x_1, x_2$ and $x_3$ are fresh variables (i.e., not in $\phi$).

$\mathcal{T}$ has the **finite model property (FMP)** if for every $\mathcal{T}$-satisfiable quantifier-free formula $\phi$, there is a $\mathcal{T}$-interpretation $\mathcal{A}$ that satisfies $\phi$ with $|dom(\mathcal{A})| < \aleph_0$.<fnref n="2" /> Consider $N_\omega = \mathbb{N} \cup \{\aleph_0\}$. A **minimal model function** [21] for $\mathcal{T}$ is a function $\minmod_\mathcal{T} : QF(\Sigma) \to N_\omega$ such that, if $\phi$ is quantifier-free and $\mathcal{T}$-satisfiable, then $\minmod_\mathcal{T}(\phi) = n$ if, and only if: there exists a $\mathcal{T}$-interpretation $\mathcal{A}$ that satisfies $\phi$ with $|dom(\mathcal{A})| = n$; and if $\mathcal{B}$ is another $\mathcal{T}$-interpretation that satisfies $\phi$, then $|dom(\mathcal{B})| \ge n$.

*Example 4.* The theory axiomatized by {$\psi_{\ge 3}$} has a computable minimal model function. To calculate it on a quantifier-free formula $\phi$, take the cardinality $n$ of the smallest interpretation in equational logic that satisfies $\phi$, which can easily be found algorithmically. If $n < 3$, $\minmod(\phi) = 3$; otherwise $\minmod(\phi) = n$.

$\mathcal{T}$ is **(strongly) polite** if it is smooth and (strongly) finitely witnessable. It is **shiny** if it is smooth, has the FMP and a computable minimal model function. $\mathcal{T}$ is **gentle** [8] if for every quantifier-free formula $\phi$, $Spec(\mathcal{T}, \phi)$ is fully computable, that is: (i) it is computable; (ii) it is either co-finite,<fnref n="3" /> or a finite set of finite cardinalities, and there is an algorithm with $\phi$ as input that tells which one is the case; (iii) if $Spec(\mathcal{T}, \phi)$ is finite, $\max(Spec(\mathcal{T}, \phi))$ is computable, and if it is infinite $\max(N \setminus Spec(\mathcal{T}, \phi))$ is computable, both with $\phi$ as input.<fnref n="4" />

*Example 5.* Consider the $\Sigma_1$-theory $\mathcal{T}_{even}^\infty$ (see [25]), with axiomatization $\{\neg\psi_{=2n+1} : n \in \mathbb{N}\}$: it is not gentle, as $x=x$ has as spectrum the set of even positive numbers, which is neither finite nor cofinite.

**3 Theory Combination and Natural Density**

In this section we establish various connections between model-theoretic proper-
ties of a theory, and its natural density. We focus our investigation on the empty
signature $\Sigma_1$, that has a single sort and no function and predicate symbols other
than equality. Generalizations to non-empty signatures are given in Sect. 4.

<footnote n="2">² A common definition for the finite model property demands this condition holds for all formulas, but in theory combination quantifier-free formulas are typically used.</footnote>

<footnote n="3">³ I.e., $N \setminus Spec(T, \phi)$ is finite.</footnote>

<footnote n="4">⁴ If $Spec(\mathcal{T}, \phi)$ or $N \setminus Spec(\mathcal{T}, \phi)$ are empty, their respective maxima are 0, as usual, so $\mathcal{T}$ must be decidable as $\max(Spec(\mathcal{T}, \phi)) = 0$ iff $\phi$ is not $\mathcal{T}$-satisfiable.</footnote>
We start with the empty signature, because a theory on such a signature has essentially one natural density, while for the non-empty case we must consider the density with respect to both a formula and the theory (this can also be done on the empty case, but all $\mathcal{T}$-satisfiable formulas will give the same density). Furthermore, some results will not hold on the non-empty case, such as the third item in Theorem 1 below.

Section 3.1 deals with sufficient conditions: if the density satisfies them, then we can deduce some combination properties. Section 3.2 obtains necessary conditions: one would use the contrapositive and conclude that the theory does not have the properties at hand, and then at least one knows that a different combination method has to be used.

## 3.1 Sufficient Conditions

In Theorem 1 we identify sufficient conditions for stable infiniteness, the finite model property and finite witnessability, properties that are needed for Nelson-Oppen combination, shiny combination, and polite combination, respectively.

**Theorem 1.** The positivity of the natural density $\mu(\mathcal{T})$ of a $\Sigma_1$-theory $\mathcal{T}$ is sufficient for $\mathcal{T}$ to: 1. be stably infinite; 2. have the finite model property; and 3. be finitely witnessable.

*Remark 1.*$^5$ The proof of the third item in Theorem 1 is more involved than that of the first two, which are routine. Szemerédi’s theorem [18], which settled a well-known conjecture by Erdös and Turán, showed that each set with positive natural density contains arbitrarily long finite subsequences in arithmetic progression (i.e., the difference between two consecutive elements is constant). Item 3 is a similarly flavored result, although with a much simpler proof than that of Erdös and Turán, that will guarantee that any theory $\mathcal{T}$ which is not finitely witnessable and has a natural density must satisfy $\mu(\mathcal{T}) = 0$.

The following example shows a simple application of Theorem 1.

*Example 6.* Fix some positive natural number $n$, and consider the theory $\mathcal{T}_{\ge n}$, with axiomatization $\{\psi_{\ge n}\}$. It obviously has positive density. By Theorem 1 it is stably infinite, has the finite model property, and is finitely witnessable.

The following example shows that all the reciprocals of Theorem 1 are false, a single counterexample being enough for all three.

*Example 7.* Take the $\Sigma_1$-theory $\mathcal{T}_{=2^i}$ with axiomatization $\{\psi_{\ge 2^n} \lor \bigvee_{i=0}^n \psi_{=2^i} : n \in \mathbb{N}\}$, which has interpretations $\mathcal{A}$ with domains whose cardinality is either infinite or a power of two. It is stably infinite, has the finite model property and is finitely witnessable,$^6$ but $\mu(\mathcal{T}_{=2^i}) = \lim_{n \to \infty} \frac{|\text{Spec}_n(\mathcal{T}_{=2^i})|}{n} = \lim_{n \to \infty} \frac{[\log_2(n)]+1}{n} = 0$.

<footnote>$^5$ Full proofs appear in [24].</footnote>

<footnote>$^6$ A witness being, if $\phi$ has $n$ variables, $wit(\phi) = \phi \wedge \bigwedge_{i=1}^{2^n} x_i = x_i$, for fresh $x_i$s.</footnote>
The following example shows the sharpness of Theorem 1, in the sense that its assumption is really needed to reach its conclusions.

*Example 8.* The conclusion of Theorem 1 cannot hold under the assumption that $\mu(T) = 0$. The theory $T_\infty$, with axiomatization $\{\psi_{\ge n} : n \in \mathbb{Z}^+\}$, has only infinite models. It has density 0 but does not have the finite model property. The theory $T_1$, with axiomatization $\{\psi_1\}$, has a single model up to isomorphism, with a single element. It has density 0 but is not stably infinite. For item 3, a theory that is not finitely witnessable and has natural density 0 is $T_\zeta$, from [26], with axiomatization $\{\psi_{\ge \zeta(n)} \vee \bigvee_{i=2}^n \psi_{=\zeta(i)} : n \in \mathbb{N} \setminus \{0, 1\}\}$ for $\zeta : \mathbb{N} \to \mathbb{N}$ the busy beaver function (see Example 2). The cardinalities of its finite models are precisely the Busy Beaver numbers, that is, the elements of the image of $\zeta$. We can show that $\mu(T) = 0$. In a way, item 3 of Theorem 1 shows that every theory not finitely witnessable must, like $\zeta$, "escape" all computable functions, and thus have natural density 0.

## 3.2 Necessary Conditions

We now move on to the results establishing necessary conditions for gentleness (Sect. 3.2.1), smoothness and finite model property (Sect. 3.2.2), strong finite witnessability (Sect. 3.2.3), the computability of a minimal model function (Sect. 3.2.4), and finite witnessability (Sect. 3.2.5).

We consider, therefore, 7 properties related to theory combination in total. Were we to consider all Boolean combinations of them, we would need to analyze 128 cases; [23, Theorems 5,6,7] has shown, however, that for $\Sigma_1$ there are only 8 of these possibilities, excluding gentleness. It may look like we need to analyze 16 possibilities then, but we can cut them down to 9 by using Lemmas 1 and 2 below. This will allow us to easily write down all possible natural densities for every combination, what will be done in Sect. 3.2.6.

### 3.2.1 Gentleness

**Theorem 2.** If $T$ is a $\Sigma_1$-theory with a density, then $\mu(T)$ being equal to 0 or 1 is a necessary condition for $T$ to be gentle.

*Proof (Sketch).* By taking a tautology $\phi$ for a gentle $\Sigma_1$-theory $T$, we see that $\text{Spec}(T) = \text{Spec}(T, \phi)$ is either finite (and then its density is 0) or co-finite (and then its density is 1).

The following example provides a simple application of Theorem 2.

*Example 9.* Consider the theory $T_{even}^\infty$ from Example 5: it's density is $1/2$, what implies by the theorem it is not gentle.

The reciprocal of Theorem 2 is false, as shown by the next example.
**Example 10.** Example 7 presents a theory $\mathcal{T}_{=2^i}$ that has density 0 but is not gentle (since both $\text{Spec}(\mathcal{T}_{=2^i})$ and $\mathbb{N} \setminus \text{Spec}(\mathcal{T}_{=2^i})$ are infinite). On the other hand, take the $\Sigma_1$-theory $\mathcal{T}_{\neq 2^i}$ with axiomatization $\{\neg\psi_{=2^n} : n \in \mathbb{N}\}$, which has interpretations $\mathcal{A}$ with either $|\text{dom}(\mathcal{A})|$ infinite, or $|\text{dom}(\mathcal{A})|$ finite but not a power of two. It is not gentle, yet $\mu(\mathcal{T}_{\neq 2^i}) = \lim_{n \to \infty} \frac{|\text{Spec}_n(\mathcal{T}_{\neq 2^i})|}{n} = \lim_{n \to \infty} \frac{n - \lfloor \log_2(n) \rfloor - 1}{n} = 1$.

Notice also that both cases of Theorem 2 are possible, namely: there are gentle theories with density 0 and gentle theories with density 1. Before showing them, let us present two useful lemmas, that relate gentleness to other properties: the first shows that the computability involved in gentleness is enough to guarantee the computability of a minimal model function, and that the forms of the possible spectra in a gentle theory lead to it having the finite model property.

**Lemma 1.** If $\mathcal{T}$ is gentle, then $\mathcal{T}$ has a computable minimal model function and the finite model property, and therefore is finitely witnessable as well.

*Proof (Sketch).* Because the spectra of any quantifier-free formula in a gentle theory is either a finite set of finite cardinalities or co-finite, it always contains an element of $\mathbb{N}$, implying the finite model property. To compute $\text{minmod}(\phi) = \min(\text{Spec}(\mathcal{T}, \phi))$ we use the facts that the spectrum is always computable, if it is finite we know $\max(\text{Spec}(\mathcal{T}, \phi))$, and if it is co-finite we know $\max(\mathbb{N} \setminus \text{Spec}(\mathcal{T}, \phi))$.

The second of our useful lemmas reveals two unexpected results involving gentleness: that a theory that is not stably infinite is gentle, and that a strongly finitely witnessable theory is also gentle; This lemma, however, is restricted to $\Sigma_1$, while the previous one is not. This extends to gentleness, in a way, the research found in [23,25,26] of combining combination properties, at least for the one-sorted, empty signature.

**Lemma 2.** Let $\mathcal{T}$ be a $\Sigma_1$-theory: if $\mathcal{T}$ is not stably infinite, or if it is strongly finitely witnessable, then $\mathcal{T}$ is gentle.

*Proof (Sketch).* If $\mathcal{T}$ is not stably infinite, its models must have a maximum cardinality, so all spectra are finite sets of finite cardinalities. If $\mathcal{T}$ is strongly finitely witnessable but not stably infinite we then have nothing to prove; if it is strongly finitely witnessable and stably infinite we have that, by [25], it is smooth and has the finite model property, so the spectra are co-finite.

*Example 11.*

1. The trivial $\Sigma_1$-theory $\mathcal{T}_{\ge 1}$, with axiomatization $\{\psi_{\ge 1}\}$, consists of all $\Sigma_1$-interpretations. It is strongly finitely witnessable (given its axiomatization is given by an universal formula, this is proven in [15]), and of course $\text{Spec}_n(\mathcal{T}_{\ge 1}) = [1, n]$ so $\mu(\mathcal{T}_{\ge 1}) = 1$.

2. The $\Sigma_1$-theory $\mathcal{T}_I$ from Example 8 is also strongly finitely witnessable and thus gentle (Lemma 2), but $\text{Spec}_n(\mathcal{T}_I) = \{1\}$ so $\mu(\mathcal{T}_I) = 0$.

3. An example of a $\Sigma_1$-theory that is gentle and has density 0, but is not strongly finitely witnessable, is denoted by $\mathcal{T}_{\langle m,n \rangle}$, for any fixed $m, n \in \mathbb{Z}^+$. It has axiomatization $\{\psi_{=m} \lor \psi_{=n}\}$, and its models have cardinalities $m$ or $n$.
### 3.2.2 Smoothness and Finite Model Property

The next result involves both smoothness and the finite model property.

**Theorem 3.** If $\mathcal{T}$ is a $\Sigma_1$-theory with a density, $\mu(\mathcal{T})$ being equal to 1 is necessary for $\mathcal{T}$ to simultaneously admit smoothness and the finite model property.

*Proof (Sketch).* The proof is dual to that of Theorem 1: if a theory is smooth and has the finite model property, it has all sufficiently large numbers as cardinalities of its models, and its density is therefore 1.

The following example not only allows one to visualize the use of Theorem 3, but will also help later in providing examples for each and all possible combination of the properties under consideration.

*Example 12.* Consider again $T_{\text{even}}^{\infty}$ from Example 9, with density $1/2$. It was already shown in [16] that $T_{\text{even}}^{\infty}$ has the finite model property without being smooth, but notice that Theorem 3 perfectly encapsulates an intuition for why that is: as the theory has the finite model property, it has a finite model; were it smooth, it would have models of all larger cardinalities, and thus density 1.

*Example 13.* The reciprocal of Theorem 3 is false, as we can see from the theory $T_{\neq 2i}^\infty$ defined in Example 10, which is not smooth.

Now, Example 12 shows an example of a theory that has the finite model property but is not smooth. But all three other Boolean combinations of these two properties are possible, as seen below.

*Example 14.*

1. The theory $T_{\ge 1}$ from Example 11 is smooth and has the finite model property.

2. One example of a smooth theory without the finite model property is the $\Sigma_1$-theory $T_\infty$ from Example 8. It has density 0, as it has no finite models.

3. To see one of a theory that is neither smooth nor has the finite model property, which by Theorem 1 must have density 0, fix an $n \in \mathbb{Z}^+$ and consider the $\Sigma_1$-theory $T_{n,\infty}$, defined in [25] by the axiomatization $\{\psi_n \lor \psi_{\ge m} : m \in \mathbb{Z}^+\}$. Its finite models must have cardinality $n$.

### 3.2.3 Strong Finite Witnessability

The following result, which is a corollary of earlier ones, is specially useful: proving a theory is not strongly finitely witnessable is quite challenging; it involves finding a quantifier-free formula, a set of variables, and an arrangement on that set which fail the conditions to be a strong witness, for every candidate for a strong witness. Checking whether the theory's density is 0 or 1 can be fairly easier.

**Corollary 1.** If $\mathcal{T}$ is a $\Sigma_1$-theory with a density, then $\mu(\mathcal{T})$ being equal to 0 or 1 is a necessary condition for $\mathcal{T}$ to be strongly finitely witnessable.

*Proof.* By Lemma 2 and Theorem 2.
*Example 15.* The theory $\mathcal{T}_{\text{even}}^{\infty}$ from Example 9 is not strongly finitely witnessable, as proven in [16], but the proof found there is quite involved, demanding careful use of arrangements. Here, we only need to point to the fact that $\mathcal{T}_{\text{even}}^{\infty}$ has natural density $1/2$.

*Example 16.* The reciprocal of Corollary 1 is false: the theories $\mathcal{T}_{\le 2i}$ and $\mathcal{T}_{\ge 2i}$ from Examples 7 and 10 have, respectively, densities 0 and 1, but neither is strongly finitely witnessable, which follows from the fact that both are stably infinite without being smooth, together with [25, Theorem 7], which shows stably infinite, one-sorted theories that are strongly finitely witnessable are smooth.

### 3.2.4 Computability of Minimal Model Functions

We move now to the question of computability of a minimal model function, one of the more complex topics in this paper. For this, we first establish in Proposition 1 a connection between this and the computability of the spectra.

**Proposition 1.** *T is a $\Sigma_1$-theory with a computable minimal model function if, and only if, $\text{Spec}(T)$ is computable.*

This proposition plays an important role in the proof of the theorem below:

**Theorem 4.** If $T$ is a $\Sigma_1$-theory with a density, the fact that $\mu(T)$ is a computable number is a necessary condition for $T$ to have a computable minimal model function. Furthermore, for every computable number $0 \le r \le 1$, there exists a $\Sigma_1$-theory $\mathcal{T}$ with $\mu(\mathcal{T}) = r$ that has a computable minimal model function and the finite model property, but is not smooth.

The proof of the first part takes a theory $\mathcal{T}$ with a computable minimal model function, and from Proposition 1 one sees that $\text{Spec}(\mathcal{T})$ is computable; we then prove that this implies $\mu(\mathcal{T})$ is itself a computable real number, ruling out non-computable numbers. Indeed, if $A$ is a computable set, the sequence $\{|A_n|\}_{n \in \mathbb{N}} = \{|\{k \in A : k \le n\}|\}_{n \in \mathbb{N}}$ is computable (and so is $\{n\}_{n \in \mathbb{N}}$, but that is obvious); if $\mu(A) = r$, we have $r = \lim_{n \to \infty} |A_n|/n$, proving $r$ is computable.

We prove the second part by constructing in Definition 2 below, from two sequences $\{a_n\}_{n \in \mathbb{N}}$ and $\{b_n\}_{n \in \mathbb{N}}$, a function $f$ whose image (which will also equal the spectrum of the theory to be constructed) will be a computable set and have a density associated to the medians of the ratios $a_n/b_n$, where the median of the fractions $a/b$ and $c/d$ is the fraction $(a+c)/(b+d)$. Although tedious to prove, it is true that the limit of the medians of the ratios between two sequences equals the limit of the ratios, and this guarantees that the natural density of the image of $f$ will be the limit of $a_n/b_n$.

**Definition 2.** Given sequences $\{a_n\}_{n \in \mathbb{N}}$ and $\{b_n\}_{n \in \mathbb{N}}$ with $0 < a_n < b_n$ and $a_n, b_n \in \mathbb{N}$, for all $n \in \mathbb{N}$, we define an associated function $f: \mathbb{Z}^+ \to \mathbb{Z}^+$ inductively as follows: $f(n)=n$ for $1 \le n \le a_0$, and $f(n)=a_0$ for $a_0+1 \le n \le b_0$; and, assuming $f(n)$ defined for all $1 \le n \le M = \sum_{i=0}^{m} b_i$, for any $m \ge 0$, we make $f(n)=n$ for $M+1 \le n \le M+a_{m+1}$, and $f(n) = M + a_{m+1}$ for $M + a_{m+1} + 1 \le n \le M + b_{m+1}$.
<figure><img src="image_37.png" /><figcaption>**Fig. 2.** (A) Initial values of the function *f* from Definition 2, for *a*₀ = 4, *a*₁ = 3, *a*₂ = 7, *b*₀ = 6, *b*₁ = 4 and *b*₂ = 10. (B) Initial values of the functions *G* (smaller, red bullet points) and *f* (larger, black bullet points) from the case with computable *r* of Theorem 5, for *a*₀ = 1, *a*₁ = 2, *a*₂ = 3, *b*₀ = 2, *b*₁ = 3, *b*₂ = 5, *g*(1) = 1, *g*(2) = 1 and *g*(3) = 0.</figcaption></figure>

The construction defined in Definition 2 is outlined in Fig. 2 (A). Notice the step-shape of the function, that can be computed by induction on *n*.

We next show an application of Theorem 4, by identifying a theory that
according to this theorem does not have a computable minimal model function,
but this fact seems difficult to prove without using this theorem.

Example 17. Take $\Omega=0.57824\dots$ from Example 2. Take the sequence of fractions $5/10, 57/100, \dots$ converging to $\Omega$, and define a function $f$ as in Definition 2: so $f(n) = n$ for $1 \le n \le 4$, and $f(n) = 5$ for $5 \le n \le 10$; $f(n) = n$ for $11 \le n \le 66$, and $f(n)=67$ for $67 \le n \le 110$, and so on. Define then a theory $\mathcal{T}_\Omega$ with axiomatization $\{\psi_{\ge f(n+1)} \lor \bigvee_{i=1}^n \psi_{=f(n)} : n \in \mathbb{Z}^+\}$: it has models of size 1 through 5, 11 through 67, and so on.<fnref n="7" /> We can prove that it has natural density $\Omega$, and thus does not have a computable minimal model function. It is, however unclear how one would prove this without resorting to Theorem 4 and Proposition 1.

The reciprocal of Theorem 4 is false, in the sense that a theory without a
computable minimal model function can still have a computable natural density.

*Example 18.* Consider again the theory $\mathcal{T}_\zeta$ from Example 8, whose natural density we have shown to be the computable number 0, despite the fact it does not have a computable minimal model function (see [6, Lemma 128]), what by Proposition 1 means $\text{Spec}(\mathcal{T}_\zeta)$ is not computable.

<footnote n="7">⁷ Notice $\mathcal{T}_\Omega$ is not the same as the theory from Example 2: indeed, the construction from Definition 2 is more general.</footnote>
Notice that, from [25, Lemma 7] and [23, Theorem 4], the theories in Theorem 4 are also finitely witnessable without being strongly finitely witnessable. They are also not gentle in the case that $0 < \mu(T) < 1$. It is still possible to come up with gentle examples for $\mu(T) = 1$ or $\mu(T) = 0$, as the next example shows.

*Example 19.* To obtain $\Sigma_1$-theories $\mathcal{T}$, with $\mu(\mathcal{T}) = 1$ or $\mu(\mathcal{T}) = 0$, that have a computable minimal model function and are gentle but not strongly finitely witnessable it is enough to consider, for the first case, $\mathcal{T}$ with axiomatization $\{\psi_{=1} \lor \psi_{\ge 3}\}$; for the second, $\mathcal{T}$ with axiomatization $\{\psi_{=1} \lor \psi_{=3}\}$.

### 3.2.5 Finite Witnessability

The theorems so far have provided necessary conditions for a theory to be gentle, smooth, strongly finitely witnessable, or have a computable minimal model function. We now show that this is as far as this goes: namely, we cannot achieve necessary conditions using natural densities for finite witnessability alone.

In fact, any real number $r$ is the natural density of a finitely witnessable theory. If $r$ is computable then Theorem 4 already constructs a finitely witnessable theory $\mathcal{T}$ with $\mu(\mathcal{T}) = r$, as [23, Theorem 4] proved that a theory with a computable minimal model function is finitely witnessable. However, in the next theorem we construct such a theory also for non-computable numbers. In addition, the theorem shows that the generated theory does not need to have a computable minimal model function even if $r$ is computable. These will constitute the most intricate results of this paper.

**Theorem 5.** For every number $0 \le r \le 1$, there exists a $\Sigma_1$-theory $\mathcal{T}$ with $\mu(\mathcal{T})=r$ that is finitely witnessable yet doesn't have a computable minimal model function.

The proof of Theorem 5 is divided in two cases: when $r$ is computable, and when it is not. When it is not, we write it in decimal notation, take the obvious series of decimal fractions converging to it, define the function $f$ as in Definition 2 and take the theory whose spectrum is the image of $f$.

If $r$ is computable, which is the difficult case, we take computable sequences $\{a_n\}_{n \in \mathbb{N}}$ and $\{b_n\}_{n \in \mathbb{N}}$ such that $a_n/b_n$ converges to $r$, and a non-computable function $g: \mathbb{Z}^+ \to \{0, 1\}$. We then define an auxiliary function $G: \mathbb{Z}^+ \to \{0, 1\}$ by making, for $M = 2 \sum_{i=0}^{m} b_i$: $G(M+1) = g(M+2)$; $G(n) = 0$ for $M+2 \le n \le 2(b_{m+1}-a_{m+1})+M$; $G(2(b_{m+1}-a_{m+1})+M+1)=0$ if $g(M+2)=1$, and otherwise $G(2(b_{m+1}-a_{m+1})+M+1)=1$; and $G(n)=1$ for $2(b_{m+1}-a_{m+1})+M+2 \le n \le M+2b_{m+1}$. We make $f(n) = \max\{m \le n : G(m) = 1\}$, and take the theory whose spectrum is the image of $f$, axiomatized by $\{\psi_{\ge f(n+1)} \lor \bigvee_{i=1}^n \psi_{=f(i)} : n \in \mathbb{Z}^+\}$, which will have a density equal to whatever is the limit of $a_n/b_n$, i.e. $r$. An example of this construction appears in Fig. 2(B), where the smaller, red bullet points represent $G$, and the larger, black bullet points represent $f$: for the corresponding theory we will have $\text{Spec}_{20}(\mathcal{T}) = \{1, 4, 5, 8, 9, 10, 15, 16, 17, 18, 19, 20\}$.

### 3.2.6 Summary

We can now, as this section about necessary conditions for the empty signature
comes to an end, summarize its overall arch: we have seen what are all possible values for the density of a theory given some of its theory combination properties, for all such combinations of properties.

In Table 1, **SI** stands for stably infinite; **SM** for smooth; **FW** for finitely witnessable; **SW** for strongly finitely witnessable; **FM** for the finite model property; **CF** for a computable minimal model function; and **G** for gentle. **REC** denotes the set of real computable numbers.

Each line in the table corresponds to a possible combination of properties (that remains possible after Lemmas 1 and 2). For example, the first line corresponds to theories that admit all properties, while the second line corresponds to theories that are stably infinite, smooth, have a computable minimal model function, but do not admit any of the other properties.

For each possible combination of properties, we list in the table the possible natural densities of theories that admit the corresponding properties. For example, theories that admit all properties must have density one.<fnref n="8" />

The column titled “Reference” leads to the result in this paper proving the values are indeed restricted to the mentioned ones; and the column “Construction” refers to examples of theories having the possible natural densities shown.

<table><caption>**Table 1.** Classification of combinations *vis-à-vis* their natural densities.</caption><thead><tr><th>SI</th><th>SM</th><th>FW</th><th>SW</th><th>FM</th><th>CF</th><th>G</th><th>Natural densities</th><th>Reference</th><th>Construction</th></tr></thead><tbody><tr><td rowspan="6">T</td><td rowspan="2">T</td><td>T</td><td>T</td><td>T</td><td>T</td><td>T</td><td>1</td><td>Theorem 3</td><td>Example 11</td></tr><tr><td>F</td><td>F</td><td>F</td><td>T</td><td>F</td><td>0</td><td>Theorem 1</td><td>Example 14</td></tr><tr><td rowspan="4">F</td><td rowspan="2">T</td><td rowspan="2">F</td><td>T</td><td>T</td><td>T</td><td>{0, 1}</td><td>Theorem 2</td><td>Example 19</td></tr><tr><td>F</td><td>F</td><td>REC ∩ [0, 1]</td><td>Theorem 4</td><td>Theorem 4</td></tr><tr><td rowspan="2">F</td><td rowspan="2">F</td><td>T</td><td>F</td><td>F</td><td>[0, 1]</td><td>Theorem 5</td><td>Theorem 5</td></tr><tr><td>F</td><td>F</td><td>0</td><td>Theorem 1</td><td>Example 8</td></tr><tr><td rowspan="2">F</td><td rowspan="2">F</td><td rowspan="2">T</td><td>F</td><td>T</td><td>F</td><td>0</td><td>Theorem 1</td><td>Example 14</td></tr><tr><td>F</td><td>T</td><td>T</td><td>T</td><td>0</td><td>Theorem 1</td><td>Example 11</td></tr></tbody></table>

## 4 Non-empty Signatures

In this section we provide generalizations of the results of Sect. 3 to non-empty signatures. We are able to do so by considering $\mu(T, \phi)$ for all formulas $\phi$, rather than $\mu(T)$: this is due to the fact that in a non-empty signature we can have two quantifier-free satisfiable formulas with distinct densities.

<footnote n="8">⁸ The theory found in this specific row, $T_{\ge 1}$ from Example 11, is strongly finitely witnessable, and Lemma 2 then shows it is also gentle, as implied by the table.</footnote>
**Example 20.** Take the theory $\mathcal{T}$ on the signature with a unary function $s$, axiomatized by $\{\psi_{=2} \lor \forall x.s(x)=x\}$. In its models that do not have exactly two elements, $s$ must be interpreted as the identity. For $\phi_1 = \neg(s(x)=x)$ and $\phi_2 = (s(x)=x)$ we have $\mu(\mathcal{T}, \phi_1) = 0$ and $\mu(\mathcal{T}, \phi_2) = 1$.

We start by generalizing items 1 and 2 in Theorem 1. As for the third item of Theorem 1, we show in Example 22 below that it cannot be generalized similarly.

**Theorem 6.** The positivity of $\mu(\mathcal{T}, \phi)$ for every $\mathcal{T}$-satisfiable quantifier-free formula $\phi$ is sufficient for $\mathcal{T}$ to be stably infinite and have the finite model property.

In the next example we show how to use Theorem 6.

**Example 21.** Consider a signature $\Sigma$ with only function symbols, and the $\Sigma$-theory $\mathcal{T}$ of uninterpreted functions. For every quantifier-free formula $\phi$ and $\mathcal{T}$-interpretation $\mathcal{A}$ that satisfies it, we can add an element $a$ to its domain, from that it follows that $\mu(\mathcal{T}, \phi) = 1$, and that $\mathcal{T}$ is stably infinite. But by using Theorem 6 we can also conclude that the theory of uninterpreted functions has the finite model property.

Next, we generalize the result concerning gentleness to non empty signatures. The proof of the following result is, mutatis mutandis, the same as Theorem 2.

**Theorem 7.** $\mu(\mathcal{T}, \phi)$ being in $\{0,1\}$ for all quantifier-free $\mathcal{T}$-satisfiable formulas $\phi$ is a necessary condition for $\mathcal{T}$ to be gentle.

The following theorem generalizes Theorem 3, and provides a necessary condition for smoothness and the finite model property for non-empty signatures.

**Theorem 8.** Let $\mathcal{T}$ be a theory. $\mu(\mathcal{T}, \phi)$ being equal to 1 for all $\mathcal{T}$-satisfiable quantifier-free formulas $\phi$ is then a necessary condition for $\mathcal{T}$ to simultaneously be smooth and have the finite model property.

Theorem 8 can be used to show that the third item of Theorem 1 is not generalizable to non-empty signatures.

**Example 22.** Consider the function $\zeta^{-1}: \mathbb{N} \to \mathbb{N}$ which is a left inverse of $\zeta$, and the theory $\mathcal{T}_\zeta^s$ on the signature with only a single unary function $s$, both defined in [26]. Both $\zeta^{-1}$ and $\mathcal{T}_\zeta^s$ are given in Fig. 3. It is smooth, has the finite model property, but is not finitely witnessable (see [22, Lemmas 71,72,73]), meaning $\mu(\mathcal{T}_\zeta^s, \phi) = 1$ for all quantifier-free $\mathcal{T}_\zeta^s$-satisfiable formulas $\phi$ by Theorem 8. Thus, the obvious generalization of item 3 of Theorem 1 is not valid.

Theorem 8 is also useful to show, for example, that a variant of the SMT-LIB theory of bit-vectors is not smooth.

**Example 23.** Fix $n \in \mathbb{Z}^+$, and consider the one-sorted fragment of the SMT-LIB theory $\mathbf{BV}[n]$ of bit-vectors [1] of length $n$, with the usual operations (but without concatenation and extraction). The domain of its interpretations has cardinality $2^n$, and so it has the finite model property. By Theorem 8 this theory is not smooth, as for any quantifier-free formula $\phi$ one has $\mu(\mathbf{BV}[n], \phi) = 0$.
# 5 Conclusion

We have studied connections between densities and model-theoretic properties. Table 2 summarizes our main results. For each property, we refer to the theorems that characterize its possible densities, both for empty and non-empty signatures.

<table><caption>**Table 2.** Summary of main results.</caption><thead><tr><th>Property</th><th>Empty case</th><th>Non-empty case</th></tr></thead><tbody><tr><td>Stable Infiniteness</td><td>Theorem 1</td><td>Theorem 6</td></tr><tr><td>Finite Model Property</td><td>Theorem 1</td><td>Theorem 6</td></tr><tr><td>Gentleness</td><td>Theorem 2</td><td>Theorem 7</td></tr><tr><td>Smoothness</td><td>Theorem 3</td><td>Theorem 8</td></tr><tr><td>Strong Finite Witnessability</td><td>Corollary 1</td><td>Theorem 9</td></tr><tr><td>Comp. of Min. Mod. Fun.</td><td>Theorem 4</td><td>Theorem 10</td></tr><tr><td>Finite Witnessability</td><td>Theorem 5</td><td>Theorem 11, Example 22</td></tr></tbody></table>

We conclude by sketching the next steps. In this paper we only considered one-sorted theories, even though many-sorted theories are commonly used in SMT. The main reason for that is that densities for many-sorted theories would be defined on tuples rather than on numbers (i.e. on the cardinalities of the domains rather than on that of the single domain), and it is unclear how this generalization would materialize. We leave this investigation for future work, and briefly describe concrete options for such a generalization.

What makes the natural density so natural is the fact that it calculates the ratio of the number of elements in a set $A$ to the number of elements in $\mathbb{N}$ by doing that for numbers under a bound, and then letting said bound go to infinite. But there is no single way of doing that in $\mathbb{N}^m$, so we are forced to make a choice. Once fixed a bound $n$, do we, for example:

(i) bound all coordinates simultaneously by $n$ (i.e., $\mu(A) = \lim_{n\to\infty} |A_n|/n^m$ for $A_n = A \cap [n]^m$)? (ii) bound the distance of a tuple to the origin by $n$ (i.e., $A_n = A \cap B_d(n)$, where $B_d(n) = \{\mathbf{p} \in \mathbb{N}^m : d(0, \mathbf{p}) \le n\}$, for $0$ the origin)? (iii) If so, what metric do we use to calculate the distance? Do we use the taxicab distance, where $d_1(\mathbf{p}, \mathbf{q}) = \sum_{i=1}^n |p_i - q_i|$, or the generalized euclidean distances $d_m(\mathbf{p}, \mathbf{q}) = (\sum_{i=1}^n (p_i - q_i)^m)^{1/m}$, or something entirely different?

There is a plurality of “natural densities” to explore. Even more, while some generalizations will characterize properties w.r.t. the entire set of sorts $\{\sigma_1, \dots, \sigma_n\}$, others will characterize them with respect to some subset of sorts, while others will offer no characterization whatsoever.

All of this is left to a future work, but we expect that the results from the current paper will still be useful for many-sorted logic, as many of the potential many-sorted densities would rely on the separate projections to each sort.
**Acknowledgments.** This work was partially funded by the NSF-BSF grant 2020704, the ISF grant 619/21, and the Colman-Soreff fellowship.

## References

1. Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB standard: version 2.6. Technical report, Department of Computer Science, The University of Iowa (2017). http://smt-lib.org

2. Barrett, C., Sebastiani, R., Seshia, S., Tinelli, C.: Satisfiability modulo theories. In: Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, Second Edition. Frontiers in Artificial Intelligence and Applications, vol. 336, chap. 33, pp. 825–885. IOS Press (2021). http://www.cs.stanford.edu/~barrett/pubs/BSST21.pdf

3. Bell, J., Burris, S.: Compton's method for proving logical limit laws. Contemp. Math. **558**, 97–128 (2011)

4. Carnap, R.: Logical Foundations of Probability. Chicago University of Chicago Press, Chicago (1950)

5. Compton, K.J., Henson, C.W., Shelah, S.: Nonconvergence, undecidability, and intractability in asymptotic problems. Ann. Pure Appl. Log. **36**, 207–224 (1987). https://doi.org/10.1016/0168-0072(87)90017-0

6. de Toledo, G.V., Zohar, Y.: Combining combination properties: minimal models (2024). http://arxiv.org/abs/2405.01478

7. Fagin, R.: Probabilities on finite models. J. Symb. Log. **41**(1), 50–58 (1976)

8. Fontaine, P.: Combinations of theories for decidable fragments of first-order logic. In: Ghilardi, S., Sebastiani, R. (eds.) FroCoS 2009. LNCS (LNAI), vol. 5749, pp. 263–278. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-04222-5_16

9. Glebskii, Y.V., Kogan, D.I., Liogon'kii, M.I., Talanov, V.A.: Volume and fraction of satisfiability of formulas of the lower predicate calculus. Kibernetica (Kiev) **5**, 17–27 (1969)

10. Immerman, N.: Descriptive Complexity. Texts in Computer Science, 1999th edn. Springer, New York (1998)

11. Jovanović, D., Barrett, C.: Polite theories revisited. In: Fermüller, C.G., Voronkov, A. (eds.) LPAR 2010. LNCS, vol. 6397, pp. 402–416. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-16242-8_29

12. Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Trans. Program. Lang. Syst. **1**(2), 245–257 (1979). https://doi.org/10.1145/357073.357079

13. Radó, T.: On non-computable functions. Bell Syst. Tech. J. **41**(3), 877–884 (1962). https://doi.org/10.1002/j.1538-7305.1962.tb00480.x

14. Ranise, S., Ringeissen, C., Zarba, C.G.: Combining data structures with nonstably infinite theories using many-sorted logic. In: Gramlich, B. (ed.) FroCoS 2005. LNCS, vol. 3717, pp. 48–64. Springer, Heidelberg (2005). https://doi.org/10.1007/11559306_3, https://hal.inria.fr/inria-00000570

15. Sheng, Y., Zohar, Y., Ringeissen, C., Lange, J., Fontaine, P., Barrett, C.: Polite combination of algebraic datatypes. J. Autom. Reason. **66**(3), 331–355 (2022). https://doi.org/10.1007/s10817-022-09625-3
16. Sheng, Y., Zohar, Y., Ringeissen, C., Reynolds, A., Barrett, C., Tinelli, C.: Politeness and stable infiniteness: stronger together. In: Platzer, A., Sutcliffe, G. (eds.) CADE 2021. LNCS (LNAI), vol. 12699, pp. 148–165. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-79876-5_9

17. Smullyan, R.R.: First-Order Logic. Ergebnisse der Mathematik und ihrer Grenzgebiete. 2. Folge. Springer, Heidelberg (2012). https://books.google.com.br/books?id=ZyLyCAAAQBAJ

18. Szemerédi, E.: On sets of integers containing k elements in arithmetic progression. Acta Arithm. **27**, 199–245 (1975). https://doi.org/10.4064/aa-27-1-199-245

19. Tenenbaum, G.: Introduction to Analytic and Probabilistic Number Theory. Cambridge Studies in Advanced Mathematics, vol. 46. Cambridge University Press, Cambridge (1995). Transl. from the 2nd French ed. by C.B. Thomas

20. Tinelli, C., Zarba, C.G.: Combining nonstably infinite theories. J. Autom. Reason. **34**(3), 209–238 (2005)

21. Tinelli, C., Zarba, C.G.: Combining nonstably infinite theories. J. Autom. Reason. **34**(3), 209–238 (2005). https://doi.org/10.1007/s10817-005-5204-9

22. Toledo, G., Zohar, Y., Barrett, C.: Combining finite combination properties: finite models and busy beavers (2023). http://arxiv.org/abs/2307.07885

23. Toledo, G.V., Zohar, Y.: Combining combination properties: minimal models. In: Bjorner, N., Heule, M., Voronkov, A. (eds.) Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning. EPiC Series in Computing, vol. 100, pp. 19–35. EasyChair (2024). https://easychair.org/publications/paper/9KKC, https://doi.org/10.29007/6qkh

24. Toledo, G.V., Zohar, Y.: Number theory combination: natural density and SMT (2025). http://arxiv.org/abs/2505.16840

25. Toledo, G.V., Zohar, Y., Barrett, C.: Combining combination properties: an analysis of stable infiniteness, convexity, and politeness. In: Pientka, B., Tinelli, C. (eds.) CADE 2023. LNCS, vol. 14132, pp. 522–541. Springer, Cham (2023). https://doi.org/10.1007/978-3-031-38499-8_30

26. Toledo, G.V., Zohar, Y., Barrett, C.: Combining finite combination properties: finite models and busy beavers. In: Sattler, U., Suda, M. (eds.) FroCoS 2023. LNCS, vol. 14279, pp. 159–175. Springer, Cham (2023). https://doi.org/10.1007/978-3-031-43369-6_9

27. Turing, A.M.: On computable numbers, with an application to the entscheidungsproblem. Proc. London Math. Soc. **s2-42**(1)2, 30–265 (1937). https://londmathsoc.onlinelibrary.wiley.com/doi/abs/10.1112/plms/s2-42.1.230, http://arxiv.org/abs/https://londmathsoc.onlinelibrary.wiley.com/doi/pdf/10.1112/plms/s2-42.1.230, https://doi.org/https://doi.org/10.1112/plms/s2-42.1.230
**Open Access** This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

<figure><img src="image_38.png" /></figure>
# Term Rewrite Systems
Weighted Rewriting

Martin Avanzini¹ and Akihisa Yamada²(✉)

¹ Centre Inria d'Université Côte d'Azur, Sophia Antipolis, France

martin.avanzini@inria.fr

² AIST, Tokyo Waterfront, Tokyo, Japan

akihisa.yamada@aist.go.jp

**Abstract.** We introduce the notion of weighted abstract reduction systems (weighted ARSs), generalising standard and relative ARSs by allowing non-uniform weights on transition steps. Weighted ARSs give rise to a theory of rewriting where quantitative properties—noteworthy complexity related properties—can be more directly studied. Unlike these standard notions, weighted ARSs permit the study of quantitative properties of reduction systems of non-uniform weight, such as the analysis of expectation-based properties of probabilistic systems. We establish ranking functions as a means to analyse (strong) boundedness of weighted ARSs, i.e., the property that weights of reductions are bounded from above. We showcase their applicability by instantiating them to weighted term rewrite systems and probabilistic reduction systems, the latter generalising Lyapunov ranking functions to reason about expected derivation heights.

# 1 Introduction

Rewriting [7] provides a foundational theory of computing, with significant impact on both the theoretical aspects of computer science and the development of programming languages. Traditionally, rewriting primarily focuses on qualitative properties—such as whether a system is terminating or confluent. However, many applications in program analysis require a more fine-grained, quantitative perspective. Complexity analysis, cost-sensitive transformations, and resource-aware reasoning all demand a deeper understanding of the quantitative aspects of reduction processes. The study of such quantitative features is crucial for various quality assurance tasks, including guaranteed response time, smart contract deployment costs, resilience against side-channel attacks, security of cryptographic routines, and provable safety guarantees.

Abstract reduction systems (ARSs) provide a general model for a wide class of, possibly nondeterministic or probabilistic, systems. A key strength of ARSs is that they permit studying program properties independently of specific programming paradigms. Yet, they often fail to capture quantitative aspects effectively. A prototypical example is the complexity analysis of high-level, declarative languages, where a single reduction step is not an elementary operation. For
instance, in the case of the λ-calculus, it is unrealistic to assume that a single β-reduction step incurs a uniform cost. To endow the λ-calculus with a reasonable cost model—one that relates to Turing machines—Dal Lago and Martini [10] for instance propose to measure the cost of a step in terms of the absolute difference between the size of the reduct and redex. Some approaches to complexity analysis (e.g., [2, 8, 11]) allow the specification of a program’s resource consumption through annotations, the cost of a reduction step thereby becomes dependent on the annotation. A final example, where ARSs fail to model costs effectively, are stochastic, i.e., probabilistic systems.

The key observation of our work is that all these models can be effectively modeled by a *weighted* extension of ARSs, where reduction steps additionally carry *weight* information. Weights are taken from a general (ordered) monoid, whose structure is used to define reflexive and transitive closures, and thereby multi-step reductions. The monoid’s unit serves as the basis for reflexivity, while its binary operation is used for sequential composition.

Weights are otherwise left abstract, and can thereby encompass a range of quantitative aspects.

- Using the ordered monoid $\langle \mathbb{N}, 0, +, \le \rangle$, weighted ARSs encompass rewriting under a *unitary cost measure*, where each reduction step is attributed a unit cost 1. The cost measure of Dal Lago and Martini [10] falls also within this setting, attributing cost $\max(1, |M| - |N|)$ to each $\beta$-step $M \to_{\beta} N$.

- Taking the ordered monoid $\langle \mathbb{N}, 0, \max, \le \rangle$, weighted ARSs endow computations with *"watermark"-like cost models*, such as (maximal) space usage.

- Products of monoids, with all operations extended pointwise, can be used to track simultaneously several cost metrics.

- Modelling stochastic reductions as an ARS over (multi)distributions [4], taking weights $\langle \mathbb{R}_{\ge 0}, 0, +, \le \rangle$ facilitates the study of *expected resource usage*.

- The monoid $\langle \mathbb{N}^{\text{Var} \to \mathbb{N}}, 0, + \rangle$, with all operations extended pointwise, can attribute non-ground rewrite steps with a *variable-size cost measure*.

Weighted ARSs provide a natural framework for studying quantitative aspects of computations directly. This encompasses quantitative variations of properties traditionally studied—such as strategies, confluence, and termination—taking for instance the length, or more generally cost, of reductions into account. In this work, we focus on termination-like properties, specifically *boundedness*, demanding that (cumulative) weights remain finite. We establish *ranking functions*, formalized as embeddings from weighted ARSs into a *canonical* weighted ARS over weights themselves, as a methodology for proving (strong) *boundedness*. Specifically, we show that this methodology is sound if the underlying monoid is *positive*, and is complete if the monoid is bounded-complete and continuous. Notably, all of the aforementioned instances fall within this setting.

A natural question then is how these abstract notions relate to concrete settings. First, we show that N-weighted ARSs provide a conservative extension of classical and relative ARSs, serving as a sanity check of the proposed theory. We then introduce *weighted term rewrite systems (TRSs)* and *barycentric ARSs*. The former generalises first-order term rewrite systems, where each rule carries
a weight. We show how monotone $\mathcal{F}$-algebras, a sound and complete method for proving termination of TRSs, generalize to a sound and complete method for proving (strong) boundedness of weighted TRSs. Barycentric ARSs allow us to model probabilistic reductions in a way that weights correspond to expected runtimes or costs. We establish *affine ranking functions* as a mean to reason about boundedness of barycentric ARSs.

*Related Work.* Attaching weights to rules is a natural idea that appears in various contexts throughout the literature. One of the most well-studied examples is the theory of weighted automata (cf. [12]). In the context of term rewriting, a form of weighted (integer) TRSs was employed in [17] in order to keep track of the original runtime cost during simplifying the systems. The idea has also been applied to endow imperative [6], functional probabilistic [1], and quantum programs [5] with *non-uniform* cost models, non-uniform in the sense that computation costs of different primitives are not necessarily equal. Our weighted ARSs extract the common essence and serve as a foundation of these works.

A closely related, but fundamentally different idea to incorporate quantitative information is to map reduction steps to weights. For instance, in their study of hyper-normalisation, van Oostrom and Toyama [18] introduce *monoid-measured* ARSs, where steps are assigned weights from a monoid, yielding a derivation measure that abstracts over reduction length. Gavazzo and Florio [15] define *quantitative ARSs*, where steps are mapped to elements of a *quantale*—a monoid endowed with a semilattice structure that satisfies certain distributivity laws. Their construction induces a notion of *distance* between terms in the ARS, conforming to the standard axioms of a metric space. In a similar fashion, weighted transition systems [19] generalize weighted automata with additional structures for metrical analysis. Laird et al. [16] endow a non-deterministic version of Plotkin’s PCF with a quantitative semantics, where the denotation of a (non-deterministic) function is turned from a relation between inputs and outputs, to a function assigning weights to input/output pairs.

The fundamental difference of our work lies in the structure of the rewriting relation: rather than augmenting ARSs ($R \subseteq A \times A$) with mappings $A \times A \to W$, we extend ARSs to a ternary relation ($R \subseteq W \times A \times A$). As a result, our framework imposes no intrinsic constraints on the nature of weights—for instance, they need not represent distances or abstract measures of derivation length.

Finally, Faggian [13] introduces another orthogonal formalism, also dubbed *quantitative ARSs* (QARSs), particularly aimed for the study of quantitative behaviors of probabilistically evolving systems. QARSs assign quantities—the *observations*—to states ($A \to W$). This way, fundamental properties of QARSs can be studied through the sequence of observations. QARSs are mainly used to study so called *asymptotic* behaviors of infinite reduction sequences, e.g., uniqueness of “limits” of reductions.

*Outline.* In Sect. 2, we introduce weighted ARSs and their fundamental properties. In Sect. 3 we establish ranking functions as a means to reason about
bound on the weight an initial state can produce. In Sect. 4 we present the aforementioned instances of weighted ARSs: standard ARSs, weighted TRSs, and barycentric ARSs, and conclude in Sect. 5.

## 2 Weighted Abstract Rewriting

In this section we formally introduce weighted ARSs—a generalization of ARSs where transitions between states have (possibly different) weights. To model the concatenation of multiple weighted reduction steps, we will assume that weights have a monoidal structure. This enables us to model reflexivity and transitivity in the weighted setting. We will also demand that weights are (partially) ordered, so that we can argue about bounds on weights.

We quickly recap some basic notions. A partially ordered set (poset) is a set $\mathcal{W}$ equipped with a partial order $\leq$ on $\mathcal{W}$. We say a subset $X \subseteq \mathcal{W}$ of a poset has an (upper) bound $b \in \mathcal{W}$ (written $X \leq b$), if $x \leq b$ for all $x \in X$. We say $\mathcal{W}$ is bounded-complete if every $X \subseteq \mathcal{W}$ that has an upper bound in $\mathcal{W}$ has the least one, sup $X$. A monoid is a set $\mathcal{W}$ equipped with an associative operator $+$ defined on $\mathcal{W}$ and its neutral element $0 \in \mathcal{W}$, i.e., $(x + y) + z = x + (y + z)$ and $0 + x = x + 0 = x$ for all $x, y, z \in \mathcal{W}$. A monoid $\mathcal{W}$ is ordered if it is also a poset where $x \leq y$ implies $x + z \leq y + z$ and $z + x \leq z + y$ for all $x, y, z \in \mathcal{W}$. An ordered monoid $\mathcal{W}$ is positive if $0 \leq w$ for all $w \in \mathcal{W}$. We say $\mathcal{W}$ is continuous if whenever sup $X \in \mathcal{W}$ is defined, sup{$x + w \mid x \in X$} is defined and is sup $X + w$.

**Example 1.** The sets $\mathbb{N}$ and $\mathbb{R}_{\geq 0}$ of natural and non-negative real numbers form bounded-complete positive monoids with $0, +$, and $\leq$ as usual. For any nonempty $X$, the function space $X \to \mathcal{W}$ over a bounded-complete positive monoid $\mathcal{W}$ forms one with respect to the pointwise extensions, i.e., $0(x) := 0$, $(f + g)(x) := f(x) + g(x)$, and $f \leq g \iff \forall x \in X. f(x) \leq g(x)$.

**Definition 1 (weighted ARS).** A $\mathcal{W}$-weighted ARS over state space $A$ and positive monoid $\mathcal{W}$ is a ternary relation<fnref n="1" /> $\rightsquigarrow \subseteq \mathcal{W} \times A \times A$. We write $\rightsquigarrow^{[w]}$ for $\{\langle a, b \rangle \mid \langle w, a, b \rangle \in \rightsquigarrow\}$, and hence $a \rightsquigarrow^{[w]} b$ means $\langle w, a, b \rangle \in \rightsquigarrow$. We say $\rightsquigarrow$ is a weighted order if it is

- reflexive: $a \rightsquigarrow^{[0]} a$ for all $a \in A$; and

- transitive: $a \rightsquigarrow^{[w]} b$ and $b \rightsquigarrow^{[v]} c$ implies $a \rightsquigarrow^{[w+v]} c$ for all $a, b, c \in A$.

We denote by $\rightsquigarrow$ the least weighted order containing $\rightsquigarrow$, and write $\rightsquigarrow^w$ for $\rightsquigarrow^{[w]}$. When we know that $\rightsquigarrow$ is transitive, we may write $\rightsquigarrow^w$ instead of $\rightsquigarrow^{[w]}$. Alternatively, the ARS $\rightsquigarrow^w$ can be defined by the following inference rules:

$$ \begin{array}{ccc} \underline{a \rightsquigarrow^0 a} & \underline{a \rightsquigarrow^{[w]} b} & \underline{a \rightsquigarrow^{w} b} \\ & \underline{a \rightsquigarrow^{w} b} & \underline{a \rightsquigarrow^{w+v} c} \end{array} $$

<footnote n="1">¹ In the literature a weighted relation is often given as $A \times \mathcal{W} \times A$. In our context, $\mathcal{W} \times A \times A$ turns out notationally more convenient.</footnote>
**Definition 2 (closures and normal forms).** Given a weighted ARS $\rightsquigarrow \subseteq W \times A \times A$, we define transitive weighted ARSs $\rightsquigarrow \ge$ and $\rightsquigarrow >$ as follows:

$$ a \rightsquigarrow^{\ge w} b :\iff \exists v \ge w. a \rightsquigarrow^v b \qquad a \rightsquigarrow^{> w} b :\iff \exists v > w. a \rightsquigarrow^v b $$

We call $\rightsquigarrow \ge$ the downward closure as $w \ge v$ implies $\rightsquigarrow \ge w \subseteq \rightsquigarrow \ge v$. By convention, we write $\rightsquigarrow^* \subseteq A \times A$ for $\rightsquigarrow \ge 0$ and $\rightsquigarrow^+ \ge 0$ for $\rightsquigarrow > 0$. We say $a \in A$ is a normal form (or terminal) with respect to $\rightsquigarrow$ if no such $b \in A$ exists that $a \rightsquigarrow^+ b$. The set of normal forms with respect to $\rightsquigarrow$ is denoted by $\text{NF}(\rightsquigarrow)$.

**Definition 3 (weighted reduction sequence).** A reduction sequence w.r.t. a weighted ARS $\rightsquigarrow$ is a (possibly infinite) sequence $a_0 \rightsquigarrow [w_1] a_1 \rightsquigarrow [w_2] a_2 \rightsquigarrow [w_3] \dots$. The sequence is called

- terminating, if there exists $n \in \mathbb{N}$ such that $w_n = w_{n+1} = \dots = 0$;

- bounded (by $b \in W$), if $w_1 + \dots + w_n \le b$ for any $n = 1, 2, \dots$;

- Zeno, if it is bounded but not terminating.

*Example 2.* Consider the $\mathbb{R}_{\ge 0}$-weighted ARS $\rightsquigarrow := \{\langle \frac{1}{2^n}, n, n+1 \rangle \mid n \in \mathbb{N}\} \cup \{\langle 0, n, n \rangle \mid n \in \mathbb{N}\}$ over states $\mathbb{N}$. Reduction sequences such as $0 \rightsquigarrow [1] 1 \rightsquigarrow [1/2]$ $2 \rightsquigarrow [0] 2 \rightsquigarrow [0] \dots$ are terminating, as after the third step only weight-0 steps occur. The sequence $0 \rightsquigarrow [1] 1 \rightsquigarrow [1/2] 2 \rightsquigarrow [1/4] 3 \rightsquigarrow [1/8] \dots$ is not terminating as $\frac{1}{2^n} \ne 0$ for any $n \in \mathbb{N}$, but is bounded by $1 + \frac{1}{2} + \frac{1}{4} + \frac{1}{8} + \dots = 2$; i.e., Zeno.

We now define the properties of weighted ARSs that are of interest in this work. The first two properties generalize the corresponding notions of standard ARSs, and the next two generalize the positive and strong almost-sure termination of probabilistic ARSs [4,9], respectively; the latter was (independently) called “bounded termination” by [14], which inspired the naming below.

<figure><img src="image_39.png" /><figcaption>**Fig. 1.** Hasse diagrams illustrating the impact of non-Zeno and finite branching restrictions on the relationships among the properties from Definition 4. Here TRSs are supposed to be finite.</figcaption></figure>