×

Definable isomorphism problem. (English) Zbl 1509.03103

Summary: We investigate the isomorphism problem in the setting of definable sets (equivalent to sets with atoms): given two definable relational structures, are they related by a definable isomorphism? Under mild assumptions on the underlying structure of atoms, we prove decidability of the problem. The core result is parameter-elimination: existence of an isomorphism definable with parameters implies existence of an isomorphism definable without parameters.

MSC:

03C40 Interpolation, preservation, definability
03C15 Model theory of denumerable and separable structures
03C35 Categoricity and completeness of theories
03B25 Decidability of theories and sets of sentences

Software:

LOIS; NLambda
PDFBibTeX XMLCite
Full Text: arXiv

References:

[1] [Bab16]L´aszl´o Babai. Graph isomorphism in quasipolynomial time [extended abstract]. In Procs. STOC 2016, pages 684-697, 2016. · Zbl 1376.68058
[2] [BBKL12] Miko laj Boja´nczyk, Laurent Braud, Bartek Klin, and S lawomir Lasota. Towards nominal computation. In Procs. POPL 2012, pages 401-412, 2012. · Zbl 1321.68139
[3] [BKL14]Miko laj Boja´nczyk, Bartek Klin, and S lawomir Lasota. Automata theory in nominal sets. Log. Meth. Comp. Sci., 10, 2014. · Zbl 1338.68140
[4] [BKLT13] Miko laj Boja´nczyk, Bartek Klin, S lawomir Lasota, and Szymon Toru´nczyk. Turing machines with atoms. In Procs. LICS 2014, pages 183-192, 2013. · Zbl 1367.68098
[5] [Boj]Miko laj Boja´nczyk. Slightly infinite sets. A draft of a book available at https://www.mimuw.edu. pl/ bojan/paper/atom-book.
[6] [BT12]M. Boja´nczyk and S. Toru´nczyk. Imperative programming in sets with atoms. In Procs. FSTTCS 2012, volume 18 of LIPIcs, 2012.
[7] [Eng59]Erwin Engeler. ¨Aquivalenzklassen von n-tupeln. Z. Math. Logic Grundl. Math., 5:340-345, 1959. · Zbl 0092.24903
[8] [Fra53]R. Fra¨ıss´e. Theory of relations. North-Holland, 1953.
[9] [Hod93]Wilfrid Hodges. Model Theory. Number 42 in Encyclopedia of Mathematics and its Applications. Cambridge University Press, 1993.
[10] [KKOT15] Bartek Klin, Eryk Kopczy´nski, Joanna Ochremiak, and Szymon Toru´nczyk. Locally finite constraint satisfaction problems. In Procs. LICS’15, pages 475-486, 2015. · Zbl 1394.68186
[11] [KLOT14] Bartek Klin, S lawomir Lasota, Joanna Ochremiak, and Szymon Toru´nczyk. Turing machines with atoms, constraint satisfaction problems, and descriptive complexity. In Procs. CSL-LICS’14, pages 58:1-58:10, 2014. · Zbl 1401.68079
[12] [KLOT16] Bartek Klin, Slawomir Lasota, Joanna Ochremiak, and Szymon Toru´nczyk. Homomorphism problems for first-order definable structures. In Procs. FSTTCS 2016, pages 14:1-14:15, 2016. · Zbl 1434.03093
[13] [KS16]Bartek Klin and Michal Szynwelski. SMT solving for functional programming over infinite structures. In Procs.of MSFP 2016, pages 57-75, 2016. · Zbl 1477.68072
[14] [KT16]Eryk Kopczy´nski and Szymon Toru´nczyk. LOIS: an application of SMT solvers. In Procs. SMT Workshop, volume 1716 of CEUR Proceedings, pages 51-60, 2016.
[15] [KT17]Eryk Kopczynski and Szymon Toru´nczyk. LOIS: syntax and semantics. In Procs. POPL, pages · Zbl 1380.68125
[16] [Luk82]Eugene M. Luks. Isomorphism of graphs of bounded valence can be tested in polynomial time. J. Comput. Syst. Sci., 25(1):4265, 1982. · Zbl 0493.68064
[17] [Pit13]A. M. Pitts. Nominal Sets: Names and Symmetry in Computer Science. Cambridge University Press, 2013. · Zbl 1297.68008
[18] [RN59]Czes law Ryll-Nardzewski. On category in power ≤ ℵ0. Bull. Acad. Pol. Sci. Ser. Math. Astr. Phys., 7:545-548, 1959. · Zbl 0117.01101
[19] [Sve59]Lars Svenonius. ℵ0-categoricity in first
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.