论文标题
与MaxDiff（扩展版）的阵列插值和合并
Interpolation and Amalgamation for Arrays with MaxDiff (Extended Version)
论文作者
论文摘要
在本文中，提出了麦卡锡的延伸阵列的理论，并带有麦克斯迪夫操作（此操作返回两个给定阵列不同的最大索引）。从文献中知道，阵列理论需要进行差异操作，以便在无量词级别享受craig插值属性。但是，文献中引入的DIFF操作仅对此目的有用，并且只有纯正式含义（它是从扩展性公理的Skolemistion获得的）。我们的Maxdiff操作大大提高了表达水平。但是，获得最终理论的插值结果成为一项令人惊讶的艰巨任务。我们通过对理论模型及其融合特性的模型进行彻底的语义分析获得此类结果。结果相对于索引理论是模块化的，它显示了如何通过分层方法将它们转换为具体的插值算法。
In this paper, the theory of McCarthy's extensional arrays enriched with a maxdiff operation (this operation returns the biggest index where two given arrays differ) is proposed. 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; however, obtaining interpolation results for the resulting theory becomes a surprisingly hard task. We obtain such results 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 it is shown how to convert them into concrete interpolation algorithms via a hierarchical approach.
