Higher-order rigid E-unification

  • Jean Goubault
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 822)


Higher-order E-unification, i.e. the problem of finding substitutions that make two simply typed λ-terms equal modulo Β or Βη-equivalence and a given equational theory, is undecidable. We propose to rigidifyit, to get a resource-bounded decidable unification problem (with arbitrary high bounds), providing a complete higher-order E-unification procedure. The techniques are inspired from Gallier's rigid E-unification and from Dougherty and Johann's use of combinatory logic to solve higher-order E-unification problems. We improve their results by using general equational theories, and by defining optimizations such as higher-order rigid E-preunification, where flexible terms are used, gaining much efficiency, as in the non-equational case due to Huet.


Type Variable Free Variable Function Symbol Equational Theory Combinatory Logic 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    P. B. Andrews. Theorem proving via general matings. J.ACM, 28(2):193–214, 1981.Google Scholar
  2. 2.
    P. B. Andrews, D. Miller, E. Cohen, and F. Pfenning. Automating higher-order logic. Contemporary Mathematics, 29:169–192, 1984.Google Scholar
  3. 3.
    H. Barendregt. The Lambda Calculus, Its Syntax and Semantics, volume 103. North-Holland, 1984.Google Scholar
  4. 4.
    W. Bibel. Automated Theorem Proving. Vieweg, 2nd edition, 1987.Google Scholar
  5. 5.
    M. W. Bunder. Predicate calculus and naive set theory in pure combinatory logic. Archiv für Mathematische Logik und Grundlagenforschung, 21:169–177, 1981.Google Scholar
  6. 6.
    F. W. Burton. A linear space translation of functional programs to Turner combinators. Information Processing Letters, 14(5):201–204, 1982.Google Scholar
  7. 7.
    V. Dahl. Translating Spanish into logic through logic. American Journal of Computational Linguistics, 7:149–164, 1981.Google Scholar
  8. 8.
    J. Darlington. A partial mechanization of second-order logic. Machine Intelligence, 6:91–100, 1971.Google Scholar
  9. 9.
    A. Diller. Compiling Functional Languages. John Wiley and Sons, 1988.Google Scholar
  10. 10.
    D. J. Dougherty and P. Johann. A combinatory logic approach to higher-order E-unification. In 11th CADE, LNAI 607, pages 79–93. Springer, 1992.Google Scholar
  11. 11.
    P. K. Downey, R. Sethi, and R. E. Tarjan. Variations on the common subexpression problem. J.ACM, 27(4):758–771, 1980.Google Scholar
  12. 12.
    J. Gallier, P. Narendran, S. Raatz, and W. Snyder. Theorem proving using equational matings and rigid E-unification. J.ACM, 39(2):377–429, 1992.Google Scholar
  13. 13.
    J. Gallier, S. Raatz, and W. Snyder. Theorem proving using rigid E-unification equational matings. In 2nd LICS, pages 338–346, 1987.Google Scholar
  14. 14.
    J. Gallier and W. Snyder. Designing unification procedures using transformations: A survey. In I. Moschovakis, editor, Workshop on Logic From Computer Science, MSRI, Berkeley, CA, USA, 1989.Google Scholar
  15. 15.
    J. Gallier and W. Snyder. Higher-order unification revisited: Complete sets of transformations. J.Symb.Comp., 8:101–140, 1989.Google Scholar
  16. 16.
    J. Gallier, W. Snyder, P. Narendran, and D. Plaisted. Rigid E-unification is NP-complete. In 3rd LICS, pages 218–227, 1988.Google Scholar
  17. 17.
    M. J. C. Gordon, R. Milner, and C. Wadsworth. Edinburgh LCF, A Mechanical Logic of Computation. LNCS 78. Springer, 1979.Google Scholar
  18. 18.
    J. Goubault. Démonstration automatique en logique classique: complexité et méthodes. PhD thesis, école Polytechnique, Palaiseau, France, 1993.Google Scholar
  19. 19.
    J. Goubault. A rule-based algorithm for rigid E-unification. In A. Leitsch, editor, Third Kurt Gödel Colloquium, LNCS 713. Springer Verlag, 1993.Google Scholar
  20. 20.
    J. Goubault. A rule-based algorithm for rigid E-unification. Technical Report 93024, Bull S.A., 1993.Google Scholar
  21. 21.
    J. R. Hindley. The principal type scheme of an object in combinatory logic. Trans. AMS, 146:29–60, 1969.Google Scholar
  22. 22.
    J. R. Hindley and J. P. Seldin. Introduction to Combinators and λ-Calculus, volume 1. Cambridge University Press, 1988.Google Scholar
  23. 23.
    R. Holmes. Systems of combinatory logic related to Quine's ‘New Foundations'. Annals of Pure and Applied Logics, 53, 1991.Google Scholar
  24. 24.
    G. P. Huet. A mechanization of type theory. In 3rd IJCAI, pages 139–146, 1973.Google Scholar
  25. 25.
    G. P. Huet. A unification algorithm for typed λ-calculus. TCS, 1:27–57, 1975.Google Scholar
  26. 26.
    J.-J. Lévy. Réductions correctes et optimales dans le lambda-calcul. PhD thesis, Université Paris VII, France, 1978. Thèse d'état.Google Scholar
  27. 27.
    D. Miller and G. Nadathur. Higher-order logic programming. In 3rd ICLP, 1986.Google Scholar
  28. 28.
    R. Milner. A theory of type polymorphism in programming. J.Comp.Sys.Sci., 17:348–375, 1978.Google Scholar
  29. 29.
    G. Nelson and D. C. Oppen. Fast decision procedures based on congruence closure. J.ACM, 27(2):356–364, 1980.Google Scholar
  30. 30.
    T. Nipkow and Z. Qian. Modular higher-order E-unification. In 4th RTA, pages 200–214, 1991.Google Scholar
  31. 31.
    T. Pietrzykowski. A complete mechanization of second order logic. J.ACM, 20(2), 1973.Google Scholar
  32. 32.
    T. Pietrzykowski and D. Jensen. A complete mechanization of Ω-order type theory. ACM Nat.Conf., 1:82–92, 1972.Google Scholar
  33. 33.
    D. Prawitz. An improved proof procedure. Theoria, 26:102–139, 1960.Google Scholar
  34. 34.
    W. Snyder. Higher-order E-unification. In 10th CADE, LNAI 449, pages 573–587. Springer, 1990.Google Scholar
  35. 35.
    R. Statman. The typed λ-calculus is not elementary recursive. TCS, 9:73–81, 1979.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1994

Authors and Affiliations

  • Jean Goubault
    • 1
  1. 1.Bull Corporate Research CenterLes Clayes sous BoisFrance

Personalised recommendations