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.
@article{bwmeta1.element.bwnjournal-article-bcpv46i1p137bwm,
author = {Kfoury, A.},
title = {Beta-reduction as unification},
journal = {Banach Center Publications},
volume = {50},
year = {1999},
pages = {137-158},
zbl = {0929.03022},
language = {en},
url = {http://dml.mathdoc.fr/item/bwmeta1.element.bwnjournal-article-bcpv46i1p137bwm}
}
Kfoury, A. Beta-reduction as unification. Banach Center Publications, Tome 50 (1999) pp. 137-158. http://gdmltest.u-ga.fr/item/bwmeta1.element.bwnjournal-article-bcpv46i1p137bwm/
[000] [1] Bass, S. R., 'The undecidability of k-provability', Annals of Pure and Applied Logic, Vol 53, pp 75-102, 1991.
[001] [2] Barendregt, H. P., The Lambda Calculus, Its Syntax and Semantics, revised edition, North-Holland, Amsterdam, 1984. | Zbl 0551.03007
[002] [3] Farmer, W. M., 'Simple second-order languages for which unification is undecidable', Theoretical Computer Science, Vol 87, pp 25-41, 1991. | Zbl 0731.03005
[003] [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.
[004] [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. | Zbl 0423.03010
[005] [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.
[006] [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. | Zbl 0834.68063
[007] [8] Goldfarb, W. D., 'The undecidability of the second-order unification problem'. Theoretical Computer Science, Vol 13, pp 225-230, 1981. | Zbl 0457.03006
[008] [9] Hindley, J. R., Basic Simple Type Theory, Cambridge Tracts in Theoretical Computer Science 42, Cambridge University Press, 1997.
[009] [10] Kfoury, A. J., 'A linearization of the λ-calculus and an application'. Submitted for publication.
[010] [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
[011] [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. | Zbl 0769.68059
[012] [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.
[013] [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. | Zbl 0644.03032
[014] [15] Leivant, D., 'Polymorphic Type Inference', Proceedings of Tenth Annual ACM Symposium on Principles of Programming Languages, pp 88-98, 1983.
[015] [16] Levy, J., 'Linear second-order unification'. In Proceedings of RTA, July 1996. Also available at URL: http://www-lsi.upc.es/~jlevy
[016] [17] Mitchell, J. C., Foundations for Programming Languages, MIT Press, 1996.
[017] [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.
[018] [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
[019] [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.
[020] [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
[021] [22] van Bakel, S., 'Complete restrictions of the intersection type discipline'. Theo. Comp. Sc., Vol 102, pp 135-163, 1992. | Zbl 0762.03006
[022] [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.