Download PDF - Beta-reduction as unificationAll rights reserved. Copyright exceptions and limitations apply

ArticleOriginal scientific text

Title

Beta-reduction as unification

Authors 1

Affiliations

  1. Department of Computer Science, Boston University, Boston, MA 02215, U.S.A.

Abstract

We define a new unification problem, which we call β-unification and which can be used to characterize the β-strong normalization of terms in the λ-calculus. We prove the undecidability of β-unification, its connection with the system of intersection types, and several of its basic properties.

Bibliography

  1. Bass, S. R., 'The undecidability of k-provability', Annals of Pure and Applied Logic, Vol 53, pp 75-102, 1991.
  2. Barendregt, H. P., The Lambda Calculus, Its Syntax and Semantics, revised edition, North-Holland, Amsterdam, 1984.
  3. Farmer, W. M., 'Simple second-order languages for which unification is undecidable', Theoretical Computer Science, Vol 87, pp 25-41, 1991.
  4. Cardone, F., and Coppo, M., 'Two extensions of Curry's type inference system', in Logic and Computer Science, ed. P. Odifreddi, APIC series no. 31, pp 19-75, Academic Press, 1990.
  5. Coppo, M., and Dezani-Ciancaglini, M., 'An extension of basic functionality theory for λ-calculus', Notre Dame Journal of Formal Logic, Vol 21, no. 4, pp 685-693, 1980.
  6. Coppo, M., and Giannini, P., 'A complete type inference algorithm for simple intersection types', in Proceedings of CAAP '92, 17th Colloquium on Trees in Algebras and Programming, ed. J.-C. Raoult, Rennes, France. LNCS Vol 581, pp 102-123, Springer-Verlag, 1992.
  7. Coppo, M., and Giannini, P., 'Principal Types and Unification For a Simple Intersection Type System', Information and Computation, Vol 122, pp 70-96, 1995.
  8. Goldfarb, W. D., 'The undecidability of the second-order unification problem'. Theoretical Computer Science, Vol 13, pp 225-230, 1981.
  9. Hindley, J. R., Basic Simple Type Theory, Cambridge Tracts in Theoretical Computer Science 42, Cambridge University Press, 1997.
  10. Kfoury, A. J., 'A linearization of the λ-calculus and an application'. Submitted for publication.
  11. Kfoury, A. J., 'Beta-reduction as unification'. Technical report, Boston University, 96-019, June 1997. Also available at URL: http://www.cs.bu.edu/faculty/kfoury/research.html
  12. Kfoury, A. J., Tiuryn, J., and Urzyczyn, P., 'The undecidability of the semi-unification problem'. Information and Computation, Vol 102, no. 1, pp 83-101, 1993.
  13. Kfoury, A. J., and Wells, J. B., 'New Notions of Reduction and Non-Semantic Proofs of Beta Strong Normalization in Typed Lambda Calculi', Proceedings of Logic in Computer Science, June 1995.
  14. Krajíček, J., and Pudlák, P., 'The number of proof lines and the size of proofs in first order logic'. Archive for Mathematical Logic, Vol 27, pp 69-84, 1988.
  15. Leivant, D., 'Polymorphic Type Inference', Proceedings of Tenth Annual ACM Symposium on Principles of Programming Languages, pp 88-98, 1983.
  16. Levy, J., 'Linear second-order unification'. In Proceedings of RTA, July 1996. Also available at URL: http://www-lsi.upc.es/~jlevy
  17. Mitchell, J. C., Foundations for Programming Languages, MIT Press, 1996.
  18. Pottinger, G., 'A Type Assignment for the Strongly Normalizable λ-terms', in To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism, J.P. Seldin and J.R. Hindley, eds., pp 561-577, Academic Press, 1980.
  19. Schmidt-Schauß, M., 'Unification of stratified second-order terms'. Technical Report, Fachbereich Informatik, Johann Wolfgang-Goethe-Universität Frankfurt, 1996. Author's e-mail: schauss@informatik.uni-frankfurt.de
  20. Schubert, A., 'Second-order unification and type inference for Church-style polymorphism'. Technical Report, Institute of Informatics, Warsaw University, January 1997. Available from FTP site: zls.mimuw.edu.pl in files: pub/alx/simple.dvi.tar.gz and pub/alx/simple.ps.gz. Shorter version in Proceedings of 26th Annual ACM Symposium on Principles of Programming Languages, 1998.
  21. Retoré, C., 'A Note on Intersection Types', INRIA report RR-2431, %January 1995, postscript available at: ftp://ftp.inria.fr/INRIA/publication/publi-ps-gz/RR/RR-2431.ps.gz
  22. van Bakel, S., 'Complete restrictions of the intersection type discipline'. Theo. Comp. Sc., Vol 102, pp 135-163, 1992.
  23. van Bakel, S., Intersection Type Disciplines in Lambda Calculus and Applicative Term Rewriting Systems. Doctoral dissertation, Catholic University of Nijmegen, also issued by the Mathematisch Centrum, Amsterdam, 1993.
Banach Center Publications
1999/46/1
Export to PBN, Opens in new tab
Pages:
137-158
Main language of publication
English
Published
1999
Exact and natural sciences