main-content

Published in:

05-05-2022

# Polite Combination of Algebraic Datatypes

Authors: Ying Sheng, Yoni Zohar, Christophe Ringeissen, Jane Lange, Pascal Fontaine, Clark Barrett

Published in: Journal of Automated Reasoning | Issue 3/2022

## Abstract

Algebraic datatypes, and among them lists and trees, have attracted a lot of interest in automated reasoning and Satisfiability Modulo Theories (SMT). Since its latest stable version, the SMT-LIB standard defines a theory of algebraic datatypes, which is currently supported by several mainstream SMT solvers. In this paper, we study this particular theory of datatypes and prove that it is strongly polite, showing how it can be combined with other arbitrary disjoint theories using polite combination. The combination method uses a new, simple, and natural notion of additivity that enables deducing strong politeness from (weak) politeness.
Footnotes
1
A preliminary version of this work was published in the proceedings of IJCAR 2020 [26]. The current article extends the original versions with complete proofs, as well as a discussion and results regarding existential theories (see Proposition 2). Additionally, Sect. 5 is extended to provide a more comprehensive treatment of axiomatizations for trees.

2
We note that in practice, the new variables in $$wtn (\phi )$$ are assumed to be fresh not only with respect to $$\phi$$, but also with respect to the formula from the second theory being combined.

Literature
1.
Armando, A., Bonacina, M.P., Ranise, S., Schulz, S.: New results on rewrite-based satisfiability procedures. ACM Trans. Comput. Log. 10(1), 4:1-4:51 (2009)
2.
Baader, F., Snyder, W., Narendran, P., Schmidt-Schauß, M., Schulz, K.U.: Unification theory. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning (in 2 Volumes), pp. 445–532. Elsevier/MIT Press, New York (2001) CrossRef
3.
Barrett, C.W., Dill, D.L., Stump, A.: A generalization of shostak’s method for combining decision procedures. In: A. Armando (ed.) Frontiers of Combining Systems, 4th International Workshop, FroCoS 2002, Santa Margherita Ligure, Italy, April 8–10, 2002, Proceedings, Lecture Notes in Computer Science, vol. 2309, pp. 132–146. Springer (2002)
4.
Barrett, C.W., Shikanian, I., Tinelli, C.: An abstract decision procedure for a theory of inductive data types. J. Satisfiab. Boolean Model. Comput. 3(1–2), 21–46 (2007)
5.
Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanović, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Proceedings of the 23rd International Conference on Computer Aided Verification, CAV’11, pp. 171–177. Springer (2011). http://​dl.​acm.​org/​citation.​cfm?​id=​2032305.​2032319
6.
Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB Standard: Version 2.6. Tech. rep., Department of Computer Science, The University of Iowa (2017). Available at www.​SMT-LIB.​org
7.
Berthon, R., Ringeissen, C.: Satisfiability modulo free data structures combined with bridging functions. In: T. King, R. Piskac (eds.) Proceedings of SMT@IJCAR 2016, CEUR Workshop Proceedings, vol. 1617, pp. 71–80. CEUR-WS.org (2016)
8.
Bonacina, M.P., Echenim, M.: Rewrite-based satisfiability procedures for recursive data structures. Electron. Notes Theor. Comput. Sci. 174(8), 55–70 (2007) CrossRef
9.
Bonacina, M.P., Fontaine, P., Ringeissen, C., Tinelli, C.: Theory combination: Beyond equality sharing. In: C. Lutz, U. Sattler, C. Tinelli, A. Turhan, F. Wolter (eds.) Description Logic, Theory Combination, and All That - Essays Dedicated to Franz Baader on the Occasion of His 60th Birthday, Lecture Notes in Computer Science, vol. 11560, pp. 57–89. Springer (2019)
10.
Casal, F., Rasga, J.: Many-sorted equivalence of shiny and strongly polite theories. J. Autom. Reason. 60(2), 221–236 (2018)
11.
Chocron, P., Fontaine, P., Ringeissen, C.: Politeness and combination methods for theories with bridging functions. J. Autom. Reason. 64(1), 97–134 (2020)
12.
Enderton, H.B.: A Mathematical Introduction to Logic. Academic Press, New York (2001) MATH
13.
Fontaine, P.: Combinations of theories for decidable fragments of first-order logic. In: S. Ghilardi, R. Sebastiani (eds.) Frontiers of Combining Systems, 7th International Symposium, FroCoS 2009, Trento, Italy, September 16–18, 2009. Proceedings, Lecture Notes in Computer Science, vol. 5749, pp. 263–278. Springer (2009)
14.
Gutiérrez, R., Meseguer, J.: Variant-based decidable satisfiability in initial algebras with predicates. In: F. Fioravanti, J.P. Gallagher (eds.) Logic-Based Program Synthesis and Transformation—27th International Symposium, LOPSTR 2017, Namur, Belgium, October 10–12, 2017, Revised Selected Papers, Lecture Notes in Computer Science, vol. 10855, pp. 306–322. Springer (2017)
15.
Hojjat, H., Rümmer, P.: Deciding and interpolating algebraic data types by reduction. In: T. Jebelean, V. Negru, D. Petcu, D. Zaharie, T. Ida, S.M. Watt (eds.) 19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2017, Timisoara, Romania, September 21–24, 2017, pp. 145–152. IEEE Computer Society (2017)
16.
Jovanovic, D., Barrett, C.W.: Polite theories revisited. In: C.G. Fermüller, A. Voronkov (eds.) Logic for Programming, Artificial Intelligence, and Reasoning—17th International Conference, LPAR-17, Yogyakarta, Indonesia, October 10–15, 2010. Proceedings, Lecture Notes in Computer Science, vol. 6397, pp. 402–416. Springer (2010). Extended technical report is available at http://​theory.​stanford.​edu/​~barrett/​pubs/​JB10-TR.​pdf
17.
Kovács, L., Robillard, S., Voronkov, A.: Coming to terms with quantified reasoning. In: G. Castagna, A.D. Gordon (eds.) Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18–20, 2017, pp. 260–270. ACM (2017)
18.
Krstic, S., Conchon, S.: Canonization for disjoint unions of theories. Inf. Comput. 199(1–2), 87–106 (2005)
19.
Krstic, S., Goel, A., Grundy, J., Tinelli, C.: Combined satisfiability modulo parametric theories. In: O. Grumberg, M. Huth (eds.) Tools and Algorithms for the Construction and Analysis of Systems, 13th International Conference, TACAS 2007, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007 Braga, Portugal, March 24–April 1, 2007, Proceedings, Lecture Notes in Computer Science, vol. 4424, pp. 602–617. Springer (2007)
20.
Manna, Z., Zarba, C.G.: Combining decision procedures. In: B.K. Aichernig, T.S.E. Maibaum (eds.) Formal Methods at the Crossroads. From Panacea to Foundational Support, 10th Anniversary Colloquium of UNU/IIST, the International Institute for Software Technology of The United Nations University, Lisbon, Portugal, March 18–20, 2002, Revised Papers, Lecture Notes in Computer Science, vol. 2757, pp. 381–422. Springer (2002)
21.
Meseguer, J.: Variant-based satisfiability in initial algebras. Sci. Comput. Program. 154, 3–41 (2018) CrossRef
22.
Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Trans. Program. Lang. Syst. 1(2), 245–257 (1979) CrossRef
23.
Ranise, S., Ringeissen, C., Zarba, C.G.: Combining data structures with nonstably infinite theories using many-sorted logic. In: B. Gramlich (ed.) Frontiers of Combining Systems, 5th International Workshop, FroCoS 2005, Vienna, Austria, September 19–21, 2005, Proceedings, Lecture Notes in Computer Science, vol. 3717, pp. 48–64. Springer (2005). Extended technical report is available at https://​hal.​inria.​fr/​inria-00070335/​
24.
Reynolds, A., Blanchette, J.C.: A decision procedure for (co)datatypes in SMT solvers. J. Autom. Reason. 58(3), 341–362 (2017)
25.
Reynolds, A., Viswanathan, A., Barbosa, H., Tinelli, C., Barrett, C.W.: Datatypes with shared selectors. In: D. Galmiche, S. Schulz, R. Sebastiani (eds.) Automated Reasoning - 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14–17, 2018, Proceedings, Lecture Notes in Computer Science, vol. 10900, pp. 591–608. Springer (2018)
26.
Sheng, Y., Zohar, Y., Ringeissen, C., Lange, J., Fontaine, P., Barrett, C.W.: Politeness for the theory of algebraic datatypes. In: IJCAR (1), Lecture Notes in Computer Science, vol. 12166, pp. 238–255. Springer (2020)
27.
Sheng, Y., Zohar, Y., Ringeissen, C., Reynolds, A., Barrett, C.W., Tinelli, C.: Politeness and stable infiniteness: Stronger together. In: CADE, Lecture Notes in Computer Science, vol. 12699, pp. 148–165. Springer (2021)
28.
Shostak, R.E.: A practical decision procedure for arithmetic with function symbols. J. ACM 26(2), 351–360 (1979)
29.
Sofronie-Stokkermans, V.: Locality results for certain extensions of theories with bridging functions. In: R.A. Schmidt (ed.) Automated Deduction - CADE-22, 22nd International Conference on Automated Deduction, Montreal, Canada, August 2–7, 2009. Proceedings, Lecture Notes in Computer Science, vol. 5663, pp. 67–83. Springer (2009)
30.
Tinelli, C.: Cooperation of background reasoners in theory reasoning by residue sharing. J. Autom. Reason. 30(1), 1–31 (2003)
31.
Tinelli, C., Zarba, C.G.: Combining decision procedures for sorted theories. In: J.J. Alferes, J.A. Leite (eds.) Logics in Artificial Intelligence, 9th European Conference, JELIA 2004, Lisbon, Portugal, September 27–30, 2004, Proceedings, Lecture Notes in Computer Science, vol. 3229, pp. 641–653. Springer (2004)
32.
Tinelli, C., Zarba, C.G.: Combining nonstably infinite theories. J. Autom. Reason. 34(3), 209–238 (2005)
33.
Tran, D., Ringeissen, C., Ranise, S., Kirchner, H.: Combination of convex theories: modularity, deduction completeness, and explanation. J. Symb. Comput. 45(2), 261–286 (2010)
Title
Polite Combination of Algebraic Datatypes
Authors
Ying Sheng
Yoni Zohar
Christophe Ringeissen
Jane Lange
Pascal Fontaine
Clark Barrett
Publication date
05-05-2022
Publisher
Springer Netherlands
Published in
Journal of Automated Reasoning / Issue 3/2022
Print ISSN: 0168-7433
Electronic ISSN: 1573-0670
DOI
https://doi.org/10.1007/s10817-022-09625-3

Go to the issue