# Beta-reduction as unification

Banach Center Publications (1999)

- Volume: 46, Issue: 1, page 137-158
- ISSN: 0137-6934

## Access Full Article

top## Abstract

top## How to cite

topKfoury, A.. "Beta-reduction as unification." Banach Center Publications 46.1 (1999): 137-158. <http://eudml.org/doc/208918>.

@article{Kfoury1999,

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.},

author = {Kfoury, A.},

journal = {Banach Center Publications},

keywords = {-unification; -strong normalization of terms; -calculus; undecidability; intersection types},

language = {eng},

number = {1},

pages = {137-158},

title = {Beta-reduction as unification},

url = {http://eudml.org/doc/208918},

volume = {46},

year = {1999},

}

TY - JOUR

AU - Kfoury, A.

TI - Beta-reduction as unification

JO - Banach Center Publications

PY - 1999

VL - 46

IS - 1

SP - 137

EP - 158

AB - 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.

LA - eng

KW - -unification; -strong normalization of terms; -calculus; undecidability; intersection types

UR - http://eudml.org/doc/208918

ER -

## References

top- [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. Zbl0551.03007
- [3] Farmer, W. M., 'Simple second-order languages for which unification is undecidable', Theoretical Computer Science, Vol 87, pp 25-41, 1991. Zbl0731.03005
- [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. Zbl0423.03010
- [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. Zbl0834.68063
- [8] Goldfarb, W. D., 'The undecidability of the second-order unification problem'. Theoretical Computer Science, Vol 13, pp 225-230, 1981. Zbl0457.03006
- [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. Zbl0769.68059
- [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. Zbl0644.03032
- [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. Zbl0762.03006
- [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.

## NotesEmbed ?

topTo embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.