Towards Quantifier-Free Interpolation in Array Languages with Unbounded Data Specifications
arXiv:2607.05126
Abstract
We investigate quantifier-free interpolation properties for several fragments generalising the extensional theory of arrays. Our results include the (general) quantifier-free interpolation properties of combinatory array logic with iterated diffs and the uniform interpolation property of the simple flat array fragment. To our knowledge, these are the first positive quantifier-free interpolation results obtained for theories of arrays featuring expressive specifications over unbounded domains.