1
$\begingroup$

Nelson-Oppen requires theories to be stably infinite. Meaning, that each theory allows extending models to have an infinite domain. A commonly mentioned counter example is that the theory of bit vectors is not stably infinite. Intuitively, this makes sense, as there are only finitely many n-bit numbers. What I don't understand is how this interferes with infinite models. E.g. given a model that includes the 5-bit bit vectors in its domain. If I add the natural numbers to the domain, surely the model is still true? I have a hard time making this formal because there are so many definitions around. But my intuition is that, if you have a model for some formula about the natural numbers, the model is still true if you add rational numbers to the domain. In a way, I am expecting the sorts in smt to allow safe extension of models with finite sorts.

I must be missing something. Because all smt solvers support the bool type, which is clearly finite. Yet I have not seen papers about Z3/cvc4/5/etc. discussing the tricks they needed to safely integrated finite sorts. This leads me to believe that having finite sorts does not imply non-stably-infinite models, which in turn would mean you can just have bit vectors while also still having stably infinite theories... Can someone help me spot the error in my reasoning?

$\endgroup$

2 Answers 2

0
$\begingroup$

"Stably infinite" is a mathematical concept with a precise definition. You are trying to reason about a precise mathematical concept with imprecise vague English language / analogies (e.g., "allows extending models to have an infinite domain"). Instead, I suggest that you learn the precise mathematical definition of "stably infinite", then try applying that definition to your example, and check whether it satisfies the definition or not.

$\endgroup$
0
$\begingroup$

Yes. In "Combining Data Structures with Nonstably Infinite Theories Using Many-Sorted Logic" by Ranise et al (1), they state on page 1:

One way to reason about data structures over elements of a given nature is to use the Nelson-Oppen method in order to modularly combine a decision procedure for a theory S modeling the data structure with a decision procedure for a theory T modeling the elements. However, this solution requires that both S and T be stably infinite. Unfortunately, this requirement is not satisfied by many practically relevant theories such as, for instance, the theory of booleans, the theory of integers modulo n, and the theory of fixed-width bit-vectors.

Later, on page 5, they also define stable infinity for many-sorted first order logic:

Definition 6 (Stable infiniteness). Let Σ be a signature, let S ⊆ Σ$^S$ be a set of sorts, and let T be a Σ-theory. We say that T is stably infinite with respect to S if for every T-satisfiable quantifier-free Σ-formula φ there exists a T-interpretation A satisfying φ such that A$_σ$ is infinite, for each sort σ ∈ S.

So essentially, for a many-sorted first order logic theory to be infinite, the interpretations for the theory needs to only have infinite sorts. Luckily, the paper also describes how to combine non-stably infinite theories using politeness and a modified Nelson-Oppen method.

For those interested in how Z3 supports the boolean sort without having to modify Nelson-Oppen, I refer to my answer here.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.