×

Decidability of bounded higher-order unification. (English) Zbl 1126.03017

Summary: It is shown that unifiability of terms in the simply typed lambda calculus with \(\beta \) and \(\eta \) rules becomes decidable if there is a bound on the number of bound variables and lambdas in a unifier in \(\eta \)-expanded \(\beta \)-normal form.

MSC:

03B25 Decidability of theories and sets of sentences
03B40 Combinatory logic and lambda calculus
68W30 Symbolic computation and algebraic computation

Software:

Haskell; Miranda; ETPS; Curry; ML
PDFBibTeX XMLCite
Full Text: DOI Link

References:

[1] Andrews, P., An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof (1986), Academic Press · Zbl 0617.03001
[2] Andrews, P., Classical type theory, (Robinson, A.; Voronkov, A., Handbook of Automated Reasoning, vol. 2 (2001), North-Holland), 965-1007, (Chapter 15) · Zbl 0992.03011
[3] Barendregt, H. P., The Lambda Calculus. Its Syntax and Semantics (1984), North-Holland: North-Holland Amsterdam, New York · Zbl 0551.03007
[4] Barendregt, H. P., Functional programming and lambda calculus, (van Leeuwen, J., Handbook of Theoretical Computer Science: Formal Models and Semantics, vol. B (1990), Elsevier), 321-363, (Chapter 7) · Zbl 0900.68110
[5] Beckmann, A., Exact bounds for lengths of reductions in typed \(\lambda \)-calculus, J. Symbolic Logic, 66, 1277-1285 (2001) · Zbl 1159.03305
[6] Bird, R., Introduction to Functional Programming using Haskell (1998), Prentice Hall
[7] Burstall, R., MacQueen, D., Sanella, D.T., 1980. Hope: an experimental applicative language. In: Proc. LISP Conference. pp. 136-143; Burstall, R., MacQueen, D., Sanella, D.T., 1980. Hope: an experimental applicative language. In: Proc. LISP Conference. pp. 136-143
[8] Baader, F.; Siekmann, J., Unification theory, (Gabbay, D. M.; Hogger, C. J.; Robinson, J. A., Handbook of Logic in Artificial Intelligence and Logic Programming (1994), Oxford University Press), 41-125
[9] Comon, H.; Jurski, Y., Higher-order matching and tree automata, (Proc. of CSL 97. Proc. of CSL 97, LNCS, vol. 1414 (1997)), 157-176 · Zbl 0911.03006
[10] Comon, H., Completion of rewrite systems with membership constraints. Part I: Deduction rules, J. Symbolic Comput., 25, 4, 397-419 (1998) · Zbl 0983.68091
[11] Cervesato, I.; Pfenning, F., Linear higher-order pre-unification, (Proc. 12th LICS (1997)), 422-433
[12] Dershowitz, N.; Jouannaud, J.-P., Rewrite systems, (van Leeuwen, J., Handbook of Theoretical Computer Science: Formal Models and Semantics, vol. B (1990), Elsevier), 243-320, (Chapter 6) · Zbl 0900.68283
[13] Dowek, G., Third order matching is decidable, (Proceedings of the 7th Annual IEEE Symposium on Logic in Computer Science (1992)), 2-10
[14] Dowek, G., Third order matching is decidable, Ann. Pure Appl. Logic, 69, 2-3, 135-155 (1994) · Zbl 0822.03010
[15] Dowek, G., Higher-order unification and matching, (Robinson, A.; Voronkov, A., Handbook of Automated Reasoning, vol. 2 (2001), North-Holland), 1009-1062, (Chapter 16) · Zbl 1011.03005
[16] Dougherty, D.; Wierzbicki, T., A decidable variant of higher order matching, (Proc. RTA’02. Proc. RTA’02, LNCS, vol. 2378 (2002), Springer), 340-351 · Zbl 1045.68068
[17] Farmer, W. A., A unification algorithm for second order monadic terms, Ann. Pure Appl. Logic, 39, 131-174 (1988) · Zbl 0655.03004
[18] Farmer, W. A., Simple second-order languages for which unification is undecidable, J. Theoret. Comput. Sci., 87, 173-214 (1991)
[19] Gandy, R. O., Proofs of strong normalization, (Seldin, J. P.; Hindley, J. R., H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism (1980), Academic Press), 457-477
[20] Goubault-Larrecq, J.; Mackie, I., Proof Theory and Automated Deduction, (Applied Logic Series, vol. 6 (1997), Kluwer) · Zbl 0896.03014
[21] Goldfarb, W. D., The undecidability of the second-order unification problem, Theoret. Comput. Sci., 13, 225-230 (1981) · Zbl 0457.03006
[22] Gutierrez, C., Satisfiability of word equations with constants is in exponential space, (Proceedings FOCS’98 (1998), IEEE Computer Society Press: IEEE Computer Society Press Palo Alto, CA), 112-119
[23] Hindley, J. R., Basic Simple Type Theory, (Cambridge tracts in theoretical computer science (1997), Cambridge University Press) · Zbl 0514.03009
[24] Hanus, M.; Kuchen, H.; Moreno-Navarro, J. J., Curry: A truly functional logic language, (Proc. ILPS’95 Workshop on Visions for the Future of Logic Programming (1995)), 95-107
[25] Hindley, J. R.; Seldin, J. P., Introduction to Combinators and \(\lambda \)-calculus (1986), Cambridge University Press · Zbl 0614.03014
[26] Huet, G., A unification algorithm for typed \(\lambda \)-calculus, Theoret. Comput. Sci., 1, 27-57 (1975) · Zbl 0337.68027
[27] Huet, G., 1976. Résolution d’équations dans des langages d’ordre 1,2,…\( \omega \); Huet, G., 1976. Résolution d’équations dans des langages d’ordre 1,2,…\( \omega \)
[28] Jensen, D.; Pietrzykowski, T., Mechanizing \(\omega \)-order type theory through unification, Theoret. Comput. Sci., 3, 2, 123-171 (1976) · Zbl 0361.02020
[29] Klop, J. W., Term rewriting systems, (Abramsky, S.; Gabbay, D. M.; Maibaum, T. S.E., Handbook of Logic in Computer Science, vol. 2 (1992), Oxford University Press), 2-116
[30] Kościelski, A.; Pacholski, L., Complexity of Makanin’s algorithms, J. Assoc. Comput. Machinery, 43, 670-684 (1996) · Zbl 0882.68073
[31] Levy, J., Linear second order unification, (Proceedings of the 7th International Conference on Rewriting Techniques and Applications. Proceedings of the 7th International Conference on Rewriting Techniques and Applications, Lecture Notes in Computer Science, vol. 1103 (1996)), 332-346 · Zbl 1503.68130
[32] Loader, R., Higher order beta matching is undecidable, Logic J. IGPL, 11, 1, 51-68 (2003) · Zbl 1014.03017
[33] Levy, J.; Veanes, M., On the undecidability of second-order unification, Inform. and Comput., 159, 125-150 (2000) · Zbl 1005.03007
[34] Levy, J.; Villaret, M., Linear second-order unification and context unification with tree-regular constraints, (Proceedings of the 11th Int. Conf. on Rewriting Techniques and Applications. Proceedings of the 11th Int. Conf. on Rewriting Techniques and Applications, Lecture Notes in Computer Science, vol. 1833 (2000)), 156-171 · Zbl 0964.68074
[35] Makanin, G. S., The problem of solvability of equations in a free semigroup, Math. USSR Sbornik, 32, 2, 129-198 (1977) · Zbl 0396.20037
[36] Miller, D., A logic programming language with lambda-abstraction, function variables and simple unification, J. Logic Comput., 1, 4, 497-536 (1991) · Zbl 0738.68016
[37] Narendran, P., 1990. Some remarks on second order unification. Technical Report, Inst. of Programming and Logics, Department of Computer Science, Univ. of NY at Albany; Narendran, P., 1990. Some remarks on second order unification. Technical Report, Inst. of Programming and Logics, Department of Computer Science, Univ. of NY at Albany
[38] Nipkow, T., 1991. Higher-order critical pairs, Proc. 6th IEEE Symp. LICS, pp. 342-349; Nipkow, T., 1991. Higher-order critical pairs, Proc. 6th IEEE Symp. LICS, pp. 342-349
[39] Niehren, J.; Pinkal, M.; Ruhrberg, P., On equality up-to constraints over finite trees, context unification, and one-step rewriting, (Proceedings of the International Conference on Automated Deduction. Proceedings of the International Conference on Automated Deduction, Lecture Notes in Computer Science, vol. 1249 (1997)), 34-48 · Zbl 1430.68137
[40] Niehren, J.; Tison, S.; Treinen, R., On rewrite constraints and context unification, Inform. Process. Lett., 74, 35-40 (2000) · Zbl 1014.68076
[41] Padovani, V., Decidability of fourth-order matching, Math. Structures Comput. Sci., 10, 3, 361-372 (2000) · Zbl 0954.03017
[42] Paulson, L. C., ML for the Working Programmer (1991), Cambridge University Press · Zbl 0863.68032
[43] Paulson, L. C., Isabelle, Lecture Notes in Computer Science, vol. 828 (1994), Springer-Verlag · Zbl 0825.68059
[44] Pfenning, F., Logical frameworks, (Robinson, A.; Voronkov, A., Handbook of Automated Reasoning, vol. 2 (2001), North-Holland), 1063-1147, (Chapter 17) · Zbl 0992.03038
[45] Plandowski, W., Satisfiability of word equations with constants is in PSPACE, (FOCS 99 (1999)), 495-500
[46] Schwichtenberg, H., Complexity of normalization in the pure typed \(\lambda \)-calculus, (Troelstra, A. S.; van Dalen, D., The L.E.J. Brouwer Centenary Symposium. Proceedings of the Conference hold in Noordwijkerhout. The L.E.J. Brouwer Centenary Symposium. Proceedings of the Conference hold in Noordwijkerhout, 8-13 June, 1981. The L.E.J. Brouwer Centenary Symposium. Proceedings of the Conference hold in Noordwijkerhout. The L.E.J. Brouwer Centenary Symposium. Proceedings of the Conference hold in Noordwijkerhout, 8-13 June, 1981, Studies in Logic and the Foundations of Mathematics, vol. 110 (1982), North Holland), 453-458
[47] Schulz, K. U., Makanin’s algorithm — two improvements and a generalization, (Proc. of IWWERT 1990. Proc. of IWWERT 1990, Lecture Notes in Computer Science, vol. 572 (1990), Springer-Verlag), 85-150
[48] Schwichtenberg, H., An upper bound for reduction sequences in the typed \(\lambda \)-calculus, Arch. Math. Logic, 30, 405-408 (1991), Dedicated to Kurt Schütte on the occasion of his 80th birthday · Zbl 0719.03007
[49] Schulz, K. U., Word unification and transformation of generalized equations, J. Automat. Reason., 149-184 (1993) · Zbl 0802.68136
[50] Schmidt-Schauß, M., 1994. Unification of stratified second-order terms. Internal Report 12/94, Fachbereich Informatik, J.W. Goethe-Universität Frankfurt, Frankfurt, Germany; Schmidt-Schauß, M., 1994. Unification of stratified second-order terms. Internal Report 12/94, Fachbereich Informatik, J.W. Goethe-Universität Frankfurt, Frankfurt, Germany
[51] Schmidt-Schauß, M., Decidability of bounded second order unification. Frank Report 11, FB Informatik, J.W. Goethe-Universität Frankfurt am Main (1999)
[52] Schmidt-Schauß, M., A decision algorithm for stratified context unification. Frank-Report 12, Fachbereich Informatik, J.W. Goethe-Universität Frankfurt, Frankfurt, Germany (1999), Available at
[53] Schmidt-Schauß, M., Stratified context unification is in PSPACE, (Proceedings of CSL’01. Proceedings of CSL’01, LNCS, vol. 2142 (2001)), 498-512 · Zbl 0999.03008
[54] Schmidt-Schauß, M., A decision algorithm for stratified context unification, J. Logic Comput., 12, 6, 929-953 (2002) · Zbl 1019.03002
[55] Schmidt-Schauß, M., Decidability of arity-bounded higher-order matching, (CADE-19. CADE-19, LNCS, 2741 (2003), Springer), 488-502 · Zbl 1278.68281
[56] Schmidt-Schauß, M., Decidability of bounded second order unification, Inform. and Comput., 188, 2, 143-178 (2004) · Zbl 1078.68139
[57] Schmidt-Schauß, M.; Schulz, K. U., On the exponent of periodicity of minimal solutions of context equations, (Proceedings of the 9th Int. Conf. on Rewriting Techniques and Applications. Proceedings of the 9th Int. Conf. on Rewriting Techniques and Applications, Lecture Notes in Computer Science, vol. 1379 (1998)), 61-75 · Zbl 0901.03034
[58] Schmidt-Schauß, M.; Schulz, K. U., Decidability of bounded higher-order unification, (CSL 2002. CSL 2002, LNCS, vol. 2471 (2002), Springer-Verlag), 522-536 · Zbl 1021.03004
[59] Schmidt-Schauß, M.; Schulz, K. U., Solvability of context equations with two context variables is decidable, J. Symbolic Comput., 33, 1, 77-122 (2002) · Zbl 1017.68165
[60] Statman, R., The typed \(\lambda \)-calculus is not elementary recursive, Theoret. Comput. Sci., 9, 73-81 (1979) · Zbl 0411.03050
[61] Turner, D. A., Miranda: A non-strict functional language with polymorphic types, (Functional Programming Languages and Computer Architecture. Functional Programming Languages and Computer Architecture, Lecture Notes in Computer Science, vol. 201 (1985), Springer), 1-16 · Zbl 0592.68014
[62] Vorobyov, S., \( \forall \exists^\ast \)-equational theory of context unification is \(\Pi_1^0\)-hard, (MFCS 1998. MFCS 1998, Lecture Notes in Computer Science, vol. 1450 (1998), Springer-Verlag), 597-606 · Zbl 0912.03006
[63] Wierzbicki, T., Complexity of the higher-order matching, (Proc. 16th CADE. Proc. 16th CADE, LNCS, vol. 1632 (1999), Springer-Verlag), 82-96 · Zbl 0937.03023
[64] Wolfram, D. A., The Clausal Theory of Types, Cambridge Tracts in Theoretical Computer Science, vol. 21 (1993), Cambridge University Press · Zbl 0782.68007
[65] Zhezherun, A. P., Decidability of the unification problem for second order languages with unary function symbols, Kibernetika (Kiev). Kibernetika (Kiev), Cybernetics, 15, 5, 735-741 (1980), Translated as · 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.