Polymorphic recursion and semi-unification
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.
KeywordsProof Theory Basic Reduction Type Inference Functional Language Recursive Definition
Unable to display preview. Download preview PDF.
- 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
- 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
- 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
- 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
- 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
- A. J. Kfoury, J. Tiuryn, and P. Urzyczyn. Undecidability of the semi-unification problem. types electronic mailing list, Sept. 25, 1989.Google Scholar
- 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
- H. Leiß. Semi-unification and type inference for polymorphic recursion. Bericht INF2-ASE-5-89, Siemens AG, München, May 1989.Google Scholar
- 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
- P. Pudlák. On a unification problem related to Kreisel's conjecture. Commentationes Mathematicae Universitatis Carolinae, 29(3):551–556, 1988.Google Scholar
- 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