On complexity of the anti-unification problem

E. V. Kostylev ; V. A. Zakharov

Diskretnaya Matematika, Tome 20 (2008) no. 1, pp. 131-144.

Résumé

In this paper we suggest a new algorithm of anti-unification of logic terms represented by acyclic directed graphs and estimate its complexity. The anti-unification problem consists of the following: for two given terms find the most specific term that has the given terms as instances. We suggest an anti-unification algorithm whose complexity linearly depends on the size of the most specific term it computes. It is thus established that the anti-unification problem is of almost the same complexity as the unification problem. It is also shown that there exist terms whose most specific term is of size $O(n^2)$, where $n$ is the size of the graphs representing these terms.

Bibliographie

[1] Apt K. R., Olderog E.-R., Verification of sequential and concurrent Programs, Springer, Berlin, 1997 | MR | Zbl

[2] Baxter L. D., An efficient unification algorithm, Techn. Rep. CS-73-23, Dept. Anal. Comp. Sci, Univ. Waterloo, Ontario, Canada, 1973

[3] Godlevskii A. B., Krivoi S. L., “O proektirovanii effektivnykh algoritmov privedeniya avtomatov dlya nekotorykh otnoshenii ekvivalentnosti”, Kibernetika, 1989, no. 6, 54–61

[4] Delcher A. L., Kasif S., “Efficient parallel term matching and anti-unification”, J. Autom. Reasoning, 9:3 (1992), 391–406 | DOI | MR | Zbl

[5] Degtyarev A. I., Ob ispolzovanii aksiom funktsionalnoi refleksivnosti v $(P\ R)$ protsedure oproverzheniya, Preprint In-ta Kibernetiki AN USSR, No 75-28, 1975

[6] Eder E., “Properties of substitutions and unifications”, J. Symb. Comput., 1 (1985), 31–46 | DOI | MR | Zbl

[7] Kostylev E. V., Zakharov V. A., “Bystrye algoritmy antiunifikatsii i ikh primenenie pri analize programm”, Materialy 13-i Mezhdunarodnoi shkoly-seminara “Sintez i slozhnost upravlyayuschikh sistem”, T. 1, Penza, 2002, 76–81

[8] Kuper G. M., McAloon K. W., Palem K. V., Perry K. J., “A note on the parallel complexity of anti-unification”, J. Autom. Reasoning, 9:3 (1992), 381–389 | DOI | MR | Zbl

[9] Lassez J. I., Maher M. J., Marriot K., “Unification revisited”, Lect. Notes Comput. Sci., 306, 1988, 67–113 | Zbl

[10] Martelli A., Montanari U., “An efficient unification algorithm”, ACM Trans. Program. Lang. Syst., 4:2 (1982), 258–282 | DOI | Zbl

[11] Nielson F., Nielson H., Hankin C., Principles of program analysis, Springer, Berlin, 1999 | MR | Zbl

[12] Oancea C. E., So C., Watt S. M., “Generalization in Maple”, Maple Conf., 2005, 277–382

[13] Palamidessi C., “Algebraic properties of idempotent substitutions”, Lect. Notes Comput. Sci., 443, 1990, 386–399 | DOI | MR | Zbl

[14] Paterson M. S., Wegman M. N., “Linear unification”, J. Comput. Syst. Sci., 16:2 (1978), 158–167 | DOI | MR | Zbl

[15] Plotkin G. D., “A note on inductive generalization”, Machine Intelligence, 5, no. 1, 1970, 153–163 | MR

[16] Reynolds J. C., “Transformational systems and the algebraic structure of atomic formulas”, Machine Intelligence, 5, no. 1, 1970, 135–151 | MR

[17] Robinson J. A., “A machine-oriented logic based on the resolution principle”, J. ACM, 12:1 (1965), 23–41 | DOI | MR | Zbl

[18] Sabelfeld V. K., “Polinomialnaya otsenka slozhnosti raspoznavaniya logiko-termalnoi ekvivalentnosti”, Dokl. AN SSSR, 249:4 (1979), 793–796 | MR

[19] Sorensen M. H., Gluck R., “An algorithm of generalization in positive supercompilation”, Proc. 1995 Intern. Symp. Logic Programming, MIT Press, 1995, 465–479

[20] Watt S. M., “Algebraic generalization”, ACM SIGSAM Bull., 39:3 (2005), 93–94 | DOI

[21] Zakharov V. A., “On the refinement of logic programs by means of anti-unification”, Proc. 2nd Panhellenic Logic Symp, Delphi, Greece, 1999, 219–224