More Like this

1. Combining Combination Properties: An Analysis of Stable Infiniteness, Convexity, and Politeness

   https://doi.org/10.1007/978-3-031-38499-8_30  

   Toledo, Guilherme V.; Zohar, Yoni; Barrett, Clark (September 2023, Lecture notes in computer science)

   Pientka, B.; Tinelli, C. (Ed.)

   We make two contributions to the study of theory combination in satisfiability modulo theories. The first is a table of examples for the combinations of the most common model-theoretic properties in theory combination, namely stable infiniteness, smoothness, convexity, finite witnessability, and strong finite witnessability (and therefore politeness and strong politeness as well). All of our examples are sharp, in the sense that we also offer proofs that no theories are available within simpler signatures. This table significantly progresses the current understanding of the various properties and their interactions. The most remarkable example in this table is of a theory over a single sort that is polite but not strongly polite (the existence of such a theory was only known until now for two-sorted signatures). The second contribution is a new combination theorem showing that in order to apply polite theory combination, it is sufficient for one theory to be stably infinite and strongly finitely witnessable, thus showing that smoothness is not a critical property in this combination method. This result has the potential to greatly simplify the process of showing which theories can be used in polite combination, as showing stable infiniteness is considerably simpler than showing smoothness. 

   more » « less
2. Combining Stable Infiniteness and (Strong) Politeness

   https://doi.org/10.1007/s10817-023-09684-0  

   Sheng, Ying; Zohar, Yoni; Ringeissen, Christophe; Reynolds, Andrew; Barrett, Clark; Tinelli, Cesare (December 2023, Journal of Automated Reasoning)

   Polite theory combination is a method for obtaining a solver for a combination of two (or more) theories using the solvers of each individual theory as black boxes. Unlike the earlier Nelson–Oppen method, which is usable only when both theories are stably infinite, only one of the theories needs to be strongly polite in order to use the polite combination method. In its original presentation, politeness was required from one of the theories rather than strong politeness, which was later proven to be insufficient. The first contribution of this paper is a proof that indeed these two notions are different, obtained by presenting a polite theory that is not strongly polite. We also study several variants of this question. The cost of the generality afforded by the polite combination method, compared to the Nelson–Oppen method, is a larger space of arrangements to consider, involving variables that are not necessarily shared between the purified parts of the input formula. The second contribution of this paper is a hybrid method (building on both polite and Nelson–Oppen combination), which aims to reduce the number of considered variables when a theory is stably infinite with respect to some of its sorts but not all of them. The time required to reason about arrangements is exponential in the worst case, so reducing the number of variables considered has the potential to improve performance significantly. We show preliminary evidence for this by demonstrating significant speed-up on a smart contract verification benchmark. 

   more » « less
3. Shafarevich’s Conjecture for Families of Hypersurfaces over Function Fields

   https://doi.org/10.1093/imrn/rnaf225  

   Engel, Philip; Lin, Alice; Tayou, Salim (August 2025, International Mathematics Research Notices)

   Given a smooth quasi-projective complex algebraic variety $$\mathcal{S}$$, we prove that there are only finitely many Hodge-generic non-isotrivial families of smooth projective hypersurfaces over $$\mathcal{S}$$ of degree $$d$$ in $$\mathbb{P}_{\mathbb C}^{n+1}$$. We prove that the finiteness is uniform in $$\mathcal{S}$$ and give examples where the result is sharp. We also prove similar results for certain complete intersections in $$\mathbb{P}_{\mathbb C}^{n+1}$$ of higher codimension and more generally for algebraic varieties whose moduli space admits a period map that satisfies the infinitesimal Torelli theorem. 

   more » « less
4. On smooth plane models for modular curves of Shimura type

   https://doi.org/10.1007/s40993-022-00409-7  

   Anni, Samuele; Assaf, Eran; Lorenzo García, Elisa (June 2023, Research in Number Theory)

   Abstract In this paper we prove that there are finitely many modular curves that admit a smooth plane model. Moreover, if the degree of the model is greater than or equal to 19, no such curve exists. For modular curves of Shimura type we show that none can admit a smooth plane model of degree 5, 6 or 7. Further, if a modular curve of Shimura type admits a smooth plane model of degree 8 we show that it must be a twist of one of four curves. 

   more » « less
5. Rényi mutual information in quantum field theory, tensor networks, and gravity

   https://doi.org/10.1007/JHEP06(2024)195  

   Kudler-Flam, Jonah; Nie, Laimei; Vijay, Akash (June 2024, Journal of High Energy Physics)

   A<sc>bstract</sc> We explore a large class of correlation measures called theα−zRényi mutual informations (RMIs). Unlike the commonly used notion of RMI involving linear combinations of Rényi entropies, theα−zRMIs are positive semi-definite and monotonically decreasing under local quantum operations, making them sensible measures of total (quantum and classical) correlations. This follows from their descendance from Rényi relative entropies. In addition to upper bounding connected correlation functions between subsystems, we prove the much stronger statement that for certain values ofαandz, theα−zRMIs also lower bound certain connected correlation functions. We develop an easily implementable replica trick which enables us to compute theα−zRMIs in a variety of many-body systems including conformal field theories, free fermions, random tensor networks, and holography. 

   more » « less