We enrich the McCarthy theory of arrays with a maxdiff operation (this operation returns the biggest index where two given arrays differ). It is known from the literature that a diff operation is required for the theory of arrays in order to enjoy the Craig interpolation property at the quantifier-free level. However, the diff operation introduced in the literature is merely instrumental to this purpose and has only a purely formal meaning (it is obtained from the Skolemization of the extensionality axiom). Our maxdiff operation significantly increases the level of expressivity (for instance, it allows the definition of a length function); however, obtaining interpolation results for the resulting theory becomes a surprisingly hard task. We obtain such results in this paper, via a thorough semantic analysis of the models of the theory and of their amalgamation properties. The results are modular with respect to the index theory and we show how to convert them into concrete interpolation algorithms via a hierarchical approach.
翻译：我们用最大值操作来丰富麦卡锡阵列理论( 本次操作将返回两个给定阵列不同的最大指数 ) 。 从文献中可以知道, 数组理论需要一个 diff 操作来享受 克雷格 内插属性 。 然而, 文献中引入的 diff 操作只是对此目的有帮助, 并且只有纯粹形式上的意义( 它来自扩展性Axiom 的Skolem化 ) 。 我们的 最大值操作极大地提高了表达性( 例如, 它允许给一个长度函数下定义 ) ; 但是, 获取由此得出的理论的内插结果将是一项令人惊讶的艰巨任务 。 我们通过对理论模型及其合并属性的模型进行彻底的语义分析, 在本文中获得这样的结果。 其结果与指数理论有关是模块化的, 我们展示如何通过等级方法将其转换为具体的内插算法 。
相关内容
微信扫码咨询专知VIP会员