In the analysis of logic programs, abstract domains for detecting sharing properties are widely used. Recently the new domain \Linp has been introduced to generalize both sharing and linearity information. This domain is endowed with an optimal abstract operator for single-binding unification. The authors claim that the repeated application of this operator is also optimal for multi-binding unification. This is the proof of such a claim.
Cite
@article{arxiv.1306.2291,
title = {Optimal multi-binding unification for sharing and linearity analysis},
author = {Gianluca Amato and Francesca Scozzari},
journal= {arXiv preprint arXiv:1306.2291},
year = {2016}
}
Comments
To appear in Theory and Practice of Logic Programming (TPLP)