On the undecidability of second-order unification. (English) Zbl 1005.03007
Summary: There is a close relationship between word unification and second-order unification. This similarity has been exploited, for instance, in order to prove decidability of monadic second-order unification and decidability of linear second-order unification when no second-order variable occurs more than twice. The attempt to prove the second result for (nonlinear) second-order unification failed and led instead to a natural reduction from simultaneous rigid \(E\)-unification to this second-order unification. This reduction is the first main result of this paper, and it is the starting point for proving some novel results about the undecidability of second-order unification presented in the rest of the paper. We prove that second-order unification is undecidable in the following three cases: (1) each second-order variable occurs at most twice and there are only two second-order variables; (2) there is only one second-order variable and it is unary; (3) the following conditions (i)–(iv) hold for some fixed integer \(n\): (i) the arguments of all second-order variables are ground terms of size \(<n\), (ii) the arity of all second-order variables is \(<n\), (iii) the number of occurrences of second-order variables is \(\leq 5\), (iv) there is either a single second-order variable or there are two second-order variables and no first-order variables.
MSC:
| 03B35 | Mechanization of proofs and logical operations |
| 03D35 | Undecidability and degrees of sets of sentences |
| 68Q42 | Grammars and rewriting systems |
| 68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |
| 68W30 | Symbolic computation and algebraic computation |
References:
| [1] | Baader, F.; Nipkow, T., Term Rewriting and All That (1998), Cambridge University Press: Cambridge University Press Cambridge |
| [2] | Brainerd, W., Tree generating regular systems, Inform. and Control, 14, 217-231 (1969) · Zbl 0169.31601 |
| [3] | Comon, H. 1993, Completion of rewrite systems with membership constraints, to appear in, J. Symbolic Comput.; Comon, H. 1993, Completion of rewrite systems with membership constraints, to appear in, J. Symbolic Comput. |
| [4] | Comon, H.; Jurski, Y., Higher-order matching and tree automata, (Nielsen, M.; Thomas, W., Proc. Conf. on Computer Science Logic. Proc. Conf. on Computer Science Logic, Lecture Notes in Computer Science, 1414 (1997), Springer-Verlag: Springer-Verlag Berlin), 157-176 · Zbl 0911.03006 |
| [5] | Cortier, V.; Ganzinger, H.; Jacquemard, F.; Veanes, M., Decidable fragments of simultaneous rigid reachability, 26th International Colloquium on Automata, Languages, and Programming, ICALP’99. 26th International Colloquium on Automata, Languages, and Programming, ICALP’99, Lecture Notes in Computer Science (1999), Springer-Verlag: Springer-Verlag Berlin · Zbl 0943.68096 |
| [6] | Dauchet, M., Rewriting and tree automata, (Comon, H.; Jouannaud, J. P., Term Rewriting (French Spring School of Theoretical Computer Science, Font Romeux, France. Term Rewriting (French Spring School of Theoretical Computer Science, Font Romeux, France, Lecture Notes in Computer Science, 909 (1993), Springer-Verlag: Springer-Verlag Berlin), 95-113 |
| [7] | Degtyarev, A.; Voronkov, A., Technical Report (1995) |
| [8] | Degtyarev, A.; Voronkov, A., The undecidability of simultaneous rigid \(E\)-unification, Theoret. Comput. Sci., 166, 291-300 (1996) · Zbl 0872.68173 |
| [9] | Degtyarev, A.; Gurevich, Y.; Voronkov, A., Herbrand’s theorem and equational reasoning: Problems and solutions, Bulletin of the European Association for Theoretical Computer Science (1996) · Zbl 0866.68102 |
| [10] | Degtyarev, A.; Matiyasevich, Y.; Voronkov, A., Simultaneous rigid \(E\)-unification and related algorithmic problems, Eleventh Annual IEEE Symposium on Logic in Computer Science (LICS’96), New Brunswick, NJ (1996), IEEE Computer Society Press: IEEE Computer Society Press Los Alamitos, p. 494-502 |
| [11] | Dowek, G., A second-order pattern matching algorithm for the cube of typed \(λ\)-calculi, (Tarlecki, A., Proceedings of Mathematical Foundations of Computer Science (MFCS ’91), Kazimierz Dolny, Poland. Proceedings of Mathematical Foundations of Computer Science (MFCS ’91), Kazimierz Dolny, Poland, Lecture Notes in Computer Science, 520 (1991), Springer-Verlag: Springer-Verlag Berlin), 151-160 · Zbl 0764.68045 |
| [12] | Dowek, G., Third order matching is decidable, Ann. Pure Appl. Logic, 69, 135-155 (1994) · Zbl 0822.03010 |
| [13] | Farmer, W. M., A unification algorithm for second-order monadic terms, Ann. Pure Appl. Logic, 39, 131-174 (1988) · Zbl 0655.03004 |
| [14] | Farmer, W. M., Simple second-order languages for which unification is undecidable, Theoret. Comput. Sci., 87, 173-214 (1991) · Zbl 0731.03005 |
| [15] | Gallier, J. H.; Narendran, P.; Plaisted, D.; Snyder, W., Rigid \(E\)-unification is NP-complete, Proc. IEEE Conf. on Logic in Computer Science, LICS’88 (1988), p. 338-346 |
| [16] | Gallier, J. H.; Raatz, S.; Snyder, W., Theorem proving using rigid \(E\)-unification: Equational matings, Proc. IEEE Conf. on Logic in Computer Science, LICS’87 (1987), p. 338-346 |
| [17] | Ganzinger, H.; Jacquemard, F.; Veanes, M., Rigid reachability, (Hsiang, J.; Ohori, A., Advances in Computing Science—ASIAN’98, 4th Asian Computing Science Conference, Manila, The Philippines, December 1998, Proceedings. Advances in Computing Science—ASIAN’98, 4th Asian Computing Science Conference, Manila, The Philippines, December 1998, Proceedings, Lecture Notes in Computer Science, 1538 (1998), Springer-Verlag: Springer-Verlag Berlin), 4-21 · Zbl 0928.03002 |
| [18] | Goldfarb, W. D., The undecidability of the second-order unification problem, Theoret. Comput. Sci., 13, 225-230 (1981) · Zbl 0457.03006 |
| [19] | Gurevich, Y.; Veanes, M., Logic with equality: Partisan corroboration, and shifted pairing, Inform. and Comput., 152, 205-235 (1999) · Zbl 1004.03036 |
| [20] | Gurevich, Y.; Voronkov, A., Monadic simultaneous rigid \(E\)-unification and related problems, (Degano, P.; Corrieri, R.; Marchetti-Spaccamella, A., Automata, Languages and Programming, 24th International Colloquium, ICALP’97. Automata, Languages and Programming, 24th International Colloquium, ICALP’97, Lecture Notes in Computer Science, 1256 (1997), Springer-Verlag: Springer-Verlag Berlin), 154-165 · Zbl 1401.03037 |
| [21] | Hindley, J.; Seldin, J., Introduction to Combinatorics and \(λ\)-Calculus (1986), Cambridge University Press: Cambridge University Press Cambridge · Zbl 0614.03014 |
| [22] | Hopcroft, J. E.; Ullman, J. D., Introduction to Automata Theory, Languages and Computation (1979), Addison-Wesley: Addison-Wesley Reading · Zbl 0196.01701 |
| [23] | Huet, G., The undecidability of unification in third-order logic, Inform. and Control, 22, 257-267 (1973) · Zbl 0257.02038 |
| [24] | Huet, G.; Lang, B., Proving and applying program transformations expressed with second-order patterns, Acta Inform., 11, 21-55 (1978) · Zbl 0389.68008 |
| [25] | Levy, J., Linear second-order unification, 7th Int. Conf. on Rewriting Techniques and Applications, RTA’96, New Jersey. 7th Int. Conf. on Rewriting Techniques and Applications, RTA’96, New Jersey, Lecture Notes in Computer Science, 1103 (1996), Springer-Verlag: Springer-Verlag Berlin, p. 332-346 · Zbl 1503.68130 |
| [26] | Levy, J., Decidable and undecidable second-order unification problems, (Nipkow, T., Rewriting Techniques and Applications. Rewriting Techniques and Applications, Lecture Notes in Computer Science, 1379 (1998), Springer-Verlag: Springer-Verlag Berlin), 47-60 · Zbl 0901.03013 |
| [27] | Levy, J.; Veanes, M., On unification problems in restricted second-order languages, Annual Conference of the European Association for Computer Science Logic, CSL’98, Brno, Czech Republic (1998) |
| [28] | Lucchesi, C. L., The undecidability of the unification problem for third-order languages, Technical Report (1972) |
| [29] | Makanin, G. S., The problem of solvability of equations in a free semigroup, Math. USSR Sbornik, 32, 129-198 (1977) · Zbl 0396.20037 |
| [30] | Matiyasevich, Y., The diophantiness of recursively enumerable sets (in Russian), Soviet Math. Dokl., 279-282 (1970) |
| [31] | Niehren, J.; Pinkal, M.; Ruhrberg, P., On equality up-to constraints over finite trees, context unification, and one-step rewriting, (McCune, W., Proceedings of the 14th International Conference on Automated Deduction, Townsville, North Queensland, Australia. Proceedings of the 14th International Conference on Automated Deduction, Townsville, North Queensland, Australia, Lecture Notes in Artificial Intelligence, 1249 (1997), Springer-Verlag: Springer-Verlag Berlin), 34-48 · Zbl 1430.68137 |
| [32] | Padovani, V., Filtrage d’ordre supérieur (1996), Université Paris VII |
| [33] | Pietrzykowski, T., A complete mechanization of second-order logic, J. Assoc. Comput. Mach., 20, 333-364 (1973) · Zbl 0253.68021 |
| [34] | Plaisted, D. A., Technical Report (1995) |
| [35] | Prehofer, C., Decidable higher-order unification problems, (Bundy, A., 12th International Conference on Automated Deduction, Nancy, France. 12th International Conference on Automated Deduction, Nancy, France, Lecture Notes in Artificial Intelligence, 814 (1994), Springer-Verlag: Springer-Verlag Berlin), 635-649 · Zbl 1433.68562 |
| [36] | Schmidt-Schauß, M., Technical Report (1995) |
| [37] | Schmidt-Schauß, M., Frank-report-11 (1999) |
| [38] | Schmidt-Schauß, M.; Schulz, K., Decidability of context unification with two variables, Research Report, 71-74 (1998) |
| [39] | Schubert, A., Second-order unification and type inference for church-style polymorphism, Technical Report (1997) |
| [40] | Schubert, A., Second-order unification and type inference for Church-style polymorphism, Conference Record of POPL’98: The 25TH ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Diego (1998), ACM Press: ACM Press New York, p. 279-288 |
| [41] | Schulz, K. U., Technical Report (1991) |
| [42] | Veanes, M., UPMAIL Technical Report (1996) |
| [43] | Veanes, M., The relation between second-order unification and simultaneous rigid \(E\)-unification, Proc. Thirteenth Annual IEEE Symposium on Logic in Computer Science, June 21-24, 1998, Indianapolis, Indiana (LICS’98) (1998), IEEE Computer Society Press: IEEE Computer Society Press Los Alamitos, p. 264-275 · Zbl 0945.03528 |
| [44] | Voronkov, A., Simultaneous rigid \(E\)-unification and other decision problems related to the Herbrand theorem, Theoret. Comput. Sci. (1998) |
| [45] | Zhezherun, A. P., Decidability of the unification problem for second-order languages with unary functional symbols, Kibernetika (Kiev), 5, 120-125 (1979) · Zbl 0443.03009 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
