Higher-order unification via combinators.(English)Zbl 0772.68061

Summary: We present an algorithm for unification in the simply typed lambda calculus which enumerates complete sets of unifiers using a finitely branching search space. In fact, the types of terms may contain type variables, so that a solution may involve type-substitution as well as term substitution. The problem is first translated into the problem of unification with respect to extensional equality in combinatory logic, and the algorithm is defined in terms of transformations on systems of combinatory terms. These transformations are based on a new method (itself based on systems) for deciding extensional equality between typed combinatory logic terms.

MSC:

 68W30 Symbolic computation and algebraic computation 03B45 Modal logic (including the logic of norms)
Full Text:

References:

 [1] Barbanera, F., Adding algebraic rewriting to the calculus of constructions: strong normalization preserved, (), 149-156 [2] Breazu-Tannen, V., Combining algebra and higher-order types, (), 82-90 [3] Breazu-Tannen, V.; Gallier, J., Polymorphic rewriting conserves algebraic strong normalization and confluence, Theoret. comput. sci., 83, 3-28, (1991) · Zbl 0745.68065 [4] Curry, H.B.; Feys, R., Combinatory logic, Vol. I, (1958), North-Holland Amsterdam · Zbl 0175.27601 [5] Curry, H.B.; Hindley, J.R.; Seldin, J.P., Combinatory logic, Vol. II, (1972), North-Holland Amsterdam · Zbl 0269.02005 [6] Inform. and Comput. to appear. [7] J. Symbolic Comput., to appear. [8] Elliott, C., Higher-order unification with dependent function types, (), 121-136 [9] Fay, M., First-order unification in an equational theory, Austin, TX, Proc. 4th workshop on automated deduction, 161-167, (1979) [10] Gallier, J.H.; Snyder, W., Complete sets of transformations for general E-unification, Theoret. comput. sci., 67, 2, 3, 203-260, (1989) · Zbl 0686.68024 [11] Gallier, J.H.; Snyder, W., Higher-order unification revisited: complete sets of transformations, J. symbolic comput., 8, 1 & 2, 101-140, (1989) · Zbl 0682.03034 [12] Goldfarb, D., The undecidability of the second-order unification problem, Theoret. comput. sci., 13, 225-230, (1981) · Zbl 0457.03006 [13] Hindley, R., The principal type-scheme of an object in combinatory logic, Trans. amer. math. soc., 146, 29-60, (1969) · Zbl 0196.01501 [14] Hindley, R.; Lercher, B., A short proof of Curry’s normal form theorem, Proc. amer. math. soc., 24, 808-810, (1970) · Zbl 0195.02101 [15] Hindley, J.R.; Seldin, J.P., Introduction to combinators and λ-calculus, (1986), Cambridge University Press Cambridge · Zbl 0614.03014 [16] Huet, G., The undecidability of unification in third-order logic, Inform. and control, 22, 257-267, (1973) · Zbl 0257.02038 [17] Huet, G., A unification algorithm for typed λ-calculus, Theoret. comput. sci., 1, 27-57, (1975) · Zbl 0337.68027 [18] Huet, G., Résolution d’equations dans LES langages d’ordre 1, 2, …, ω, () [19] Hughes, R.J.M., Super-combinators, Proc. ACM conf. on LISP and functional programming, 1-10, (1982) [20] Hughes, R.J.M., The design and implementation of programming languages, () [21] Jensen, D.; Pietrzykowski, T., Mechanizing ω-order type theory through unification, () · Zbl 0361.02020 [22] Johann, P., Complete sets of transformations for unification problems, () [23] Lecher, B., Strong reduction and normal form in combinatory logic, Symbolic logic, 2, 213-223, (1967) · Zbl 0153.00602 [24] Martelli, A.; Montanari, U., An efficient unification algorithm, ACM trans. prog. languages systems, 4, 2, 258-282, (1982) · Zbl 0478.68093 [25] Nadathur, G., A higher-order logic as the basis for logic programming, () · Zbl 0900.68129 [26] Nipkow, T., Higher-order unification, polymorphism, and subsorts, (), 229-237 [27] Paulson, L.C., Isabelle: the next 700 theorem provers, () [28] Peyton-Jones, S.L., The implementation of functional programming languages, (1987), Prentice-Hall Englewood Cliffs, NJ · Zbl 0712.68017 [29] Pietzykowski, T., A complete mechanization of second-order logic, ACM j., 20, 2, 333-364, (1971) [30] Réty, P., Improving basic narrowing techniques, Proc. 2nd internat. conf. on rewriting techniques and applications, 228-241, (1987) · Zbl 0638.68101 [31] Scheevel, M., Norma: a graph reduction processor, Proc. ACM conf. on LISP and functional programming, 212-219, (1986) [32] Snyder, W., Higher-order E-unification, (), 573-587 [33] Statman, R., On translating lambda terms into combinators: the basis problem, Proc. symp. on logic in computer science, 378-382, (1986) [34] Stoye, W.R., The implementation of functional languages using custom hardware, () [35] Turner, D.A., A new implementation technique for applicative languages, Software practice and experience, 9, 31-49, (1979) · Zbl 0386.68009
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.