Polymorphic recursion and semi-unification

  • Hans Leiß
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 440)


Semi-unification is a common generalization of unification and matching which arose independently in the areas of proof theory, term rewriting, and type theory of programming languages. We introduce semi-unification via the typability problem for polymorphic recursive definitions, present a reduction calculus for semi-unification problems, and discuss partial results on termination of reductions. We prove decidability of semi-unification in two variables.


Proof Theory Basic Reduction Type Inference Functional Language Recursive Definition 
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]
    L. Damas and R. Milner. Principle type-schemes for functional programs. In In Proceedings of the 9th ACM Symposium on Principles of Programming Languages, pages 207–212, 1982.Google Scholar
  2. [2]
    R. Harper. Introduction to Standard ML. LFCS Report Series ECS-LFCS-86-14, Laboratory for Foundations of Computer Science, Dept. of Computer Science, University of Edinburgh, November 1986.Google Scholar
  3. [3]
    F. Henglein. Type inference and semi-unification. In Proceedings of the 1988 ACM Conference on LISP and Functional Programming. Snowbird, Utah, July 25–27, pages 184–197, 1988.Google Scholar
  4. [4]
    D. Kapur, D. Musser, P. Narendran, and J. Stillman. Semi-unification. In Proceedings of the 8th Conference on Foundations of Software Technology and Theoretical Computer Science. Pune, India, December 21–23, 1988, pages 435–454. Springer LNCS 338.Google Scholar
  5. [5]
    A. J. Kfoury, J. Tiuryn, and P. Urzyczyn. Computational consequences and partial solutions of a generalized unification problem. In Fourth IEEE Symposium on Logic in Computer Science. Asilomar, California, June 5–8, 1989.Google Scholar
  6. [6]
    A. J. Kfoury, J. Tiuryn, and P. Urzyczyn. Undecidability of the semi-unification problem. types electronic mailing list, Sept. 25, 1989.Google Scholar
  7. [7]
    H. Leiß. On type inference for object-oriented programming languages. In E. Börger, H. Kleine-Büning, and M. M. Richter, editors, CSL '87. 1st Workshop on Computer Science Logic. Karlsruhe, FRG, October 12–16, 1987, pages 151–172. Springer LNCS 329, 1988.Google Scholar
  8. [8]
    H. Leiß. Semi-unification and type inference for polymorphic recursion. Bericht INF2-ASE-5-89, Siemens AG, München, May 1989.Google Scholar
  9. [9]
    R. Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17:348–375, 1978.CrossRefGoogle Scholar
  10. [10]
    A. Mycroft. Polymorphic type schemes and recursive definitions. In International Symposium on Programming. 6th Colloquium. Toulouse, April 17–19, 1984, pages 217–228. Springer LNCS 167, 1984.Google Scholar
  11. [11]
    P. Pudlák. On a unification problem related to Kreisel's conjecture. Commentationes Mathematicae Universitatis Carolinae, 29(3):551–556, 1988.Google Scholar
  12. [12]
    D. A. Turner. Miranda: a non-strict functional language with polymorphic types. In Proceedings of the IFIP International Conference on Fuctional Programming Languages and Computer Architecture. Springer LNCS 201, 1985.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1990

Authors and Affiliations

  • Hans Leiß
    • 1
  1. 1.Siemens AG, ZFE F2 INF 2München 83

Personalised recommendations