Hostname: page-component-78c5997874-g7gxr Total loading time: 0 Render date: 2024-11-05T21:18:51.234Z Has data issue: false hasContentIssue false
  • English
  • Français

Some improvements to Turner's algorithm for bracket abstraction

Published online by Cambridge University Press:  12 March 2014

M. W. Bunder
M. W. Bunder*
Affiliation:
Faculty of Mathematical Sciences, University of Wollongong, Wollongong, New South Wales 2500, Australia
Get access Rights & Permissions [Opens in a new window]

Extract

A computer handles λ-terms more easily if these are translated into combinatory terms. This translation process is called bracket abstraction. The simplest abstraction algorithm—the (fab) algorithm of Curry (see Curry and Feys [6])—is lengthy to implement and produces combinatory terms that increase rapidly in length as the number of variables to be abstracted increases.

There are several ways in which these problems can be alleviated:

(1) A change in order of the clauses in the algorithm so that (f) is performed as a last resort.

(2) The use of an extra clause (c), appropriate to βη reduction.

(3) The introduction of a finite number of extra combinators.

The original 1924 form of bracket abstraction of Schönfinkel [17], which in fact predates λ-calculus, uses all three of these techniques; all are also mentioned in Curry and Feys [6].

A technique employed by many computing scientists (Turner [20], Peyton Jones [16], Oberhauser [15]) is to use the (fab) algorithm followed by certain “optimizations” or simplifications involving extra combinators and sometimes special cases of (c).

Another is either to allow a fixed infinite set of (super-) combinators (Abdali [1], Kennaway and Sleep [10], Krishnamurthy [12], Tonino [19]) or to allow new combinators to be defined one by one during the abstraction process (Hughes [7] and [8]).

A final method encodes the variables to be abstracted as an n-tuple—this requires only a finite number of combinators (Curien [5], Statman [18]).

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 55 , Issue 2 , June 1990 , pp. 656 - 669
Copyright
Copyright © Association for Symbolic Logic 1990

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] Bunder, M. W., On adding further forms of (ξ) to weak equality in combinatory logic, Preprint No. 8/87, Department of Mathematics, University of Wollongong, Wollongong, 1987.Google Scholar
[3] Bunder, M. W., Hindley, J. R. and Seldin, J. P., On adding (ξ) to weak equality, this Journal, vol. 54(1989), pp. 590–607.Google Scholar
[4] Burton, F. W., A linear space translation of functional programs to Turner combinators, Information Processing Letters, vol. 14 (1982), pp. 201–204.CrossRefGoogle Scholar
[5] Curien, P. L., Categorical combinators, sequential algorithms and functional programming, Research Notes in Theoretical Computer Science, Pitman, London, and Wiley, New York, 1986.Google Scholar
[6] Curry, H. B. and Feys, R., Combinatory logic, Vol. 1, North-Holland, Amsterdam, 1958.Google Scholar
[7] Hughes, R. J. M., The design and implementation of programming languages, Technical Monograph PR6-40, Oxford University Computing Laboratory, Oxford, 1983.Google Scholar
[8] Hughes, R. J. M., Super-combinators, Conference record of the 1982 ACM symposium on LISP and functional programming, pp. 1–10.Google Scholar
[9] Kennaway, J. R., The complexity of a translation of λ-calculus to combinators, Internal Report CSA/13/1984, Declarative Systems Architecture Group, University of East Anglia, Norwich, 1984.Google Scholar
[10] Kennaway, J. R. and Sleep, M. R., Counting director strings, Preprint, University of East Anglia, Norwich, 1984.Google Scholar
[11] Kennaway, J. R. and Sleep, M. R., Variable abstraction in O(n log n) space, Information Processing Letters, vol. 24 (1987), pp. 343–349.CrossRefGoogle Scholar
[12] Krishnamurthy, V., Parallelism in functional languages using combinators and delayed evaluation, Ph.D. thesis, University of Waikato, Hamilton, New Zealand, 1986.Google Scholar
[13] Lins, R. D., Categorical multi-combinators, Functional programming languages and computer architecture (Kahn, G., editor), Lecture Notes in Computer Science, vol. 274, Springer-Verlag, Berlin, 1987, pp. 60–79.CrossRefGoogle Scholar
[14] Mulder, J. C., Complexity of combinatorial code, Preprint No. 389, Department of Mathematics, University of Utrecht, Utrecht, 1985.Google Scholar
[15] Oberhauser, H. G., On the correspondence of lambda style reduction and combinator style reduction, Graph reduction (proceedings, Santa Fe, New Mexico, 1986), Lecture Notes in Computer Science, vol. 279, Springer-Verlag, Berlin, 1987, pp. 1–25.Google Scholar
[16] Jones, S. L. PeytonThe implementation of functional programming languages, Prentice-Hall, Englewood Cliffs, New Jersey, 1986.Google Scholar
[17] Schönfinkel, M., Über die Bausteine der mathematischen Logik, Mathematische Annalen, vol. 92 (1924), pp. 305–316; English translation, From Frege to Gödel: a source-book in mathematical logic (J. van Heijenoort, editor), Harvard University Press, Cambridge, Massachusetts, 1967, pp. 355–366.CrossRefGoogle Scholar
[18] Statman, R., An optimal translation of λ terms into combinators, preprint, Carnegie-Mellon University, Pittsburgh, Pennsylvania, 1983.Google Scholar
[19] Tonino, M. M. E., private communication, 1984 (see Mulder [14]).Google Scholar
[20] Turner, D. A., Another algorithm for bracket abstraction, this Journal, vol. 44 (1979), pp. 267–270.Google Scholar