Hostname: page-component-586b7cd67f-t8hqh Total loading time: 0 Render date: 2024-11-22T15:41:17.714Z Has data issue: false hasContentIssue false
  • English
  • Français

Compact bracket abstraction in combinatory logic

Published online by Cambridge University Press:  12 March 2014

Sabine Broda  and
Luís Damas
Sabine Broda
Affiliation:
LIACC, Universidade do Porto, R. do Campo Alegre 823, 4150 Porto, PortugalPhone: 351 2 6001672, Fax: 351 2 6003654, E-mail: [email protected]
Luís Damas
Affiliation:
LIACC, Universidade do Porto, R. do Campo Alegre 823, 4150 Porto, Portugal Phone: 351 2 6001672 Fax: 351 2 6003654, E-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

Translations from Lambda calculi into combinatory logics can be used to avoid some implementational problems of the former systems. However, this scheme can only be efficient if the translation produces short output with a small number of combinators, in order to reduce the time and transient storage space spent during reduction of combinatory terms. In this paper we present a combinatory system and an abstraction algorithm, based on the original bracket abstraction operator of Schönfinkel [9]. The algorithm introduces at most one combinator for each abstraction in the initial Lambda term. This avoids explosive term growth during successive abstractions and makes the system suitable for practical applications. We prove the correctness of the algorithm and establish some relations between the combinatory system and the Lambda calculus.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 62 , Issue 3 , September 1997 , pp. 729 - 740
Copyright
Copyright © Association for Symbolic Logic 1997

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

[1]Abdali, S. K., An abstraction algorithm for combinatory logic, this Journal, vol. 41 (1976), pp. 222–224.Google Scholar
[2]Barendregt, H., The Lambda calculus, its syntax and semantics, North-Holland, Amsterdam, 1981.Google Scholar
[3]Barendregt, H., Functional programming and Lambda calculus, Handbook of Theoretical Computer Science (1990), pp. 322–63.Google Scholar
[4]Curry, H. B. and Feys, R., Combinatory logic, vol. 1, North-Holland, Amsterdam, 1958.Google Scholar
[5]Hindley, J. R., BCK-combinators and linear X-terms have types, Theoretical Computer Science, vol. 64 (1989), pp. 97–105.CrossRefGoogle Scholar
[6]Kennaway, J. R. and Sleep, M. R., Counting director strings, University of East Anglia, Norwich, 1984.Google Scholar
[7]Mulder, J. C., Complexity of combinatory code, Preprint 389, University Utrecht, Department of Mathematics, 08 1985.Google Scholar
[8]Jones, S. L. Peyton, The implementation offunctional programming languages, Prentice-Hall, 1987.Google Scholar
[9]Schönfinkel, M., Über die Bausteine der mathematischen Logik, Mathematische Annalen, vol. 92 (1924), pp. 305–316.CrossRefGoogle Scholar
[10]Statman, R., On translating Lambda terms into combinators; the basis problem, Proceedings of the LICS '86, IEEE, 1986, pp. 378–382.Google Scholar
[11]Turner, D. A., Another algorithm for bracket abstraction, this Journal, vol. 44 (1979), pp. 267–270.Google Scholar
[12]Turner, D. A., A new implementation technique for applicative languages, Software-Practice and Experience, vol. 9 (1979), pp. 31–49.CrossRefGoogle Scholar