On the Complexity of the Standard Translation of Lambda Calculus into Combinatory Logic

Łukasz Lachowski

Abstrakt

We investigate the complexity of the standard translation of lambda calculus into combinatory logic. The main result shows that the asymptotic growth rate of the size of a translated term is Ø(n3) in worst-case, where n denotes the size of the lambda term.

 

Received 8 June 2017

This work was partially supported by the grant 2013/11/B/ST6/00975 funded by the Polish National Science Center.

AMS subject classification: 03B40, 68Q25, 68N18.

Słowa kluczowe: combinatory logic, lambda calculus, complexity analysis, functional programming
References

[1] H.P. Barendregt, The Lambda Calculus: Its Syntax and Semantics, College Publications, London, 2012.

[2] D.A. Turner, Another Algorithm for Bracket Abstraction, The Journal of Symbolic Logic 44:2 (1979), 729–740.

[3] S. Broda and L. Damas, Compact bracket abstraction in combinatory logic, The Journal of Symbolic Logic 62:3 (1997), 729–740.

[4] A. Church, An Unsolvable Problem of Elementary Number Theory, American Journal of Mathematics 58:2 (1936), 345–363.

[5] H.B. Curry, Grundlagen der Kombinatorischen Logik, American Journal of Mathematics 3 (1930), 509–536.

[6] M.S. Joy, On the efficient implementation of combinators as an object code for functional programs, PhD Thesis University of East Anglia (1985).

[7] R. Kennaway and M.R. Sleep, Variable Abstraction in O(n log n) Space, Information Processing Letters 24:5 (1987), 343–349.

[8] žL. Lachowski, l2cl, A computer program which searches for worst-case instances of the standard translation. Available at: https://bitbucket.org/zbyszko/l2cl, 2017.

[9] K. Noshita, Translation of Turner Combinators in O(n log n) Space, Information Processing Letters 20:2 (1985), 71–74.

[10] M. Sch¨onfinkel, Uber die Bausteine der mathematischen Logik, ¨ Mathematische Annalen 92:3 (1924), 305–316.

[11] D.A. Turner, Another Algorithm for Bracket Abstraction, The Journal of Symbolic Logic 44:2 (1979), 267–270.

Czasopismo ukazuje się w sposób ciągły on-line.
Pierwotną formą czasopisma jest wersja elektroniczna.