Optimal Matching for Sharing and Linearity Analysis
Gianluca Amato, Francesca Scozzari · Theory and Practice of Logic Programming · 2024
Abstract 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}$ .