Static analysis of logic programs by abstract interpretation requires designing abstract operators which mimic the concrete ones, such as unification, renaming and projection. In the case of goal-driven analysis, where goal-dependent semantics are used, we also need a backward-unification operator, typically implemented through matching. In this paper we study the problem of deriving optimal abstract matching operators for sharing and linearity properties. We provide an optimal operator for matching in the domain ${\mathtt{ShLin}^{\omega}}$, which can be easily instantiated to derive optimal operators for the domains ${\mathtt{ShLin}^{2}}$ by Andy King and the reduced product $\mathtt{Sharing} \times \mathtt{Lin}$.

翻译：基于抽象解释的逻辑程序静态分析需要设计模拟具体操作（如合一、重命名和投影）的抽象操作符。在使用目标依赖语义的目标驱动分析中，我们还需要一个反向合一操作符，通常通过匹配实现。本文研究了为共享与线性性质推导最优抽象匹配操作符的问题。我们为域${\mathtt{ShLin}^{\omega}}$中的匹配提供了最优操作符，该操作符可轻松实例化，从而推导出Andy King提出的域${\mathtt{ShLin}^{2}}$及积域$\mathtt{Sharing} \times \mathtt{Lin}$的最优操作符。